Skip to content
GitLab
Unverified Commit 65b8ff13 authored by Jerome Hugues's avatar Jerome Hugues Committed by GitHub
Browse files

Merge pull request #167 from HannaMk/master 

Update of FCS and Robot case studies ...
parents 3d023950 0aac8d23
Hide whitespace changes
Inline Side-by-side
tests/LNT/FCS/FCS.aadl.out
View file @ 65b8ff13
......@@ -2,246 +2,345 @@
---------- Ocarina LNT Generator ---------
------------------------------------------
FCS.aadl:110:03FCS.aadl:111:03FCS.aadl:112:03FCS.aadl:113:03FCS.aadl:114:03FCS.aadl:115:03FCS.aadl:116:03Begin Thread
Begin Thread
Begin Processor
Begin Types
Begin Port
Begin Main
FCS.aadl:73:03 FCS.aadl:9:03 FCS.aadl:10:03 FCS.aadl:22:03 FCS.aadl:34:03 FCS.aadl:35:03 FCS.aadl:47:03 FCS.aadl:59:03 FCS.aadl:60:03 FCS.aadl:84:03 FCS.aadl:85:03 "Main.bcg"= divbranching reduction of "FLIGHTCONTROLSYSTEM_Main.lnt";
% DEFAULT_MCL_LIBRARIES="standard.mcl"
"Main.bcg"= divbranching reduction of "FLIGHTCONTROLSYSTEM_Main.lnt";
property PROPERTY_Deadlock is
deadlock of "Main.bcg";
expected FALSE;
end property;
property Scheduling_Test (ID) is
"Main_$ID.bcg"="Main.bcg"|=
[ true* . "ACTIVATION_$ID !T_Error" ] false;
property Scheduling_Test (ID)
"Scheduling Test "is
"Main.bcg"|= with evaluator3
NEVER ("ACTIVATION_$ID !T_Error");
expected TRUE;
end property;
check Scheduling_Test ( 1);
check Scheduling_Test ( 2);
check Scheduling_Test ( 3);
check Scheduling_Test ( 4);
check Scheduling_Test ( 5);
check Scheduling_Test ( 6);
check Scheduling_Test ( 7);
property Connection (ID)
"Connection Test "is
"Main.bcg"|= with evaluator3
AFTER_1_INEVITABLE_2 ('SEND_$ID !*' , 'RECEIVE_$ID !*');
expected TRUE;
end property;
property Is_Preempted (ID)
"Is_Preempted Test "is
"Main.bcg"|= with evaluator3
SOME (true* ."ACTIVATION_$ID !T_DISPATCH_PREEMPTION". true* . ("ACTIVATION_$ID !T_PREEMPTION")* . true* . "ACTIVATION_$ID !T_PREEMPTION_COMPLETION");
expected TRUE;
end property;
check Is_Preempted ( 1);
check Is_Preempted ( 2);
check Is_Preempted ( 3);
check Is_Preempted ( 4);
check Is_Preempted ( 5);
check Is_Preempted ( 6);
check Is_Preempted ( 7);
property Data_Loss (ID)
"Between two consecutive SEND_$ID actions, there is a RECEIVE_$ID" is
"Main.bcg"|= with evaluator3
NEVER (true* ."SEND_$ID !AADLDATA". (not"RECEIVE_$ID !AADLDATA")* ."SEND_$ID !AADLDATA");
expected TRUE;
end property;
property Transition (TH_NAME, Si, Sj)
"Thread $TH_NAME, being in state $Si, the corresponding $Sj state is eventually reachable" is
"Main.bcg"|= with evaluator3
AFTER_1_INEVITABLE_2 ("DISPLAY_STATE !$TH_NAME !$Si","DISPLAY_STATE !$TH_NAME !$Sj");
expected TRUE;
end property;
module FLIGHTCONTROLSYSTEM_Threads (FLIGHTCONTROLSYSTEM_Types) is
Begin Port
module FLIGHTCONTROLSYSTEM_Threads (Types) is
process Thread_FF [
ACTIVATION: LNT_Channel_Dispatch,
AADL_PORT_ANGLE_O: LNT_Channel_Data,
AADL_PORT_ANGLE: LNT_Channel_Data]
PORT_ANGLE_O: LNT_Channel_Port,
PORT_ANGLE: LNT_Channel_Port]
is
loop
select
var
ANGLE_O : LNT_Type_Data,
ANGLE : LNT_Type_Data
in
ANGLE_O := AADLDATA;
ANGLE := EMPTY;
loop
select
ACTIVATION (T_Begin);
AADL_PORT_ANGLE (AADLDATA)
[]
ACTIVATION (T_End);
AADL_PORT_ANGLE_O (AADLDATA)
select
ACTIVATION (T_Dispatch_Preemption);
PORT_ANGLE (?ANGLE)
[]
ACTIVATION (T_Preemption_Completion);
PORT_ANGLE_O (ANGLE_O)
[]
ACTIVATION (T_Dispatch_Completion);
PORT_ANGLE (?ANGLE);
PORT_ANGLE_O (ANGLE_O)
[]
ACTIVATION (T_Preemption)
end select ;
ACTIVATION (T_Complete)
[]
ACTIVATION (T_All);
AADL_PORT_ANGLE (AADLDATA);
AADL_PORT_ANGLE_O (AADLDATA)
ACTIVATION (T_Error)
[]
ACTIVATION (T_Preempt)
end select ;
ACTIVATION (T_Ok)
[]
ACTIVATION (T_Error)
[]
ACTIVATION (T_Stop)
end select
end loop
ACTIVATION (T_Stop)
end select
end loop
end var
end process
process Thread_NL [
ACTIVATION: LNT_Channel_Dispatch,
AADL_PORT_POS_C: LNT_Channel_Data,
AADL_PORT_POS_O: LNT_Channel_Data,
AADL_PORT_ACC_C: LNT_Channel_Data]
PORT_POS_C: LNT_Channel_Port,
PORT_POS_O: LNT_Channel_Port,
PORT_ACC_C: LNT_Channel_Port]
is
loop
select
var
POS_C : LNT_Type_Data,
POS_O : LNT_Type_Data,
ACC_C : LNT_Type_Data
in
POS_C := EMPTY;
POS_O := EMPTY;
ACC_C := AADLDATA;
loop
select
ACTIVATION (T_Begin);
AADL_PORT_POS_C (AADLDATA);
AADL_PORT_POS_O (AADLDATA)
[]
ACTIVATION (T_End);
AADL_PORT_ACC_C (AADLDATA)
select
ACTIVATION (T_Dispatch_Preemption);
PORT_POS_C (?POS_C);
PORT_POS_O (?POS_O)
[]
ACTIVATION (T_Preemption_Completion);
PORT_ACC_C (ACC_C)
[]
ACTIVATION (T_Dispatch_Completion);
PORT_POS_C (?POS_C);
PORT_POS_O (?POS_O);
PORT_ACC_C (ACC_C)
[]
ACTIVATION (T_Preemption)
end select ;
ACTIVATION (T_Complete)
[]
ACTIVATION (T_All);
AADL_PORT_POS_C (AADLDATA);
AADL_PORT_POS_O (AADLDATA);
AADL_PORT_ACC_C (AADLDATA)
ACTIVATION (T_Error)
[]
ACTIVATION (T_Preempt)
end select ;
ACTIVATION (T_Ok)
[]
ACTIVATION (T_Error)
[]
ACTIVATION (T_Stop)
end select
end loop
ACTIVATION (T_Stop)
end select
end loop
end var
end process
process Thread_NF [
ACTIVATION: LNT_Channel_Dispatch,
AADL_PORT_POS_I: LNT_Channel_Data,
AADL_PORT_POS_O: LNT_Channel_Data]
PORT_POS_I: LNT_Channel_Port,
PORT_POS_O: LNT_Channel_Port]
is
loop
select
var
POS_I : LNT_Type_Data,
POS_O : LNT_Type_Data
in
POS_I := EMPTY;
POS_O := AADLDATA;
loop
select
ACTIVATION (T_Begin);
AADL_PORT_POS_I (AADLDATA)
select
ACTIVATION (T_Dispatch_Preemption);
PORT_POS_I (?POS_I)
[]
ACTIVATION (T_Preemption_Completion);
PORT_POS_O (POS_O)
[]
ACTIVATION (T_Dispatch_Completion);
PORT_POS_I (?POS_I);
PORT_POS_O (POS_O)
[]
ACTIVATION (T_Preemption)
end select ;
ACTIVATION (T_Complete)
[]
ACTIVATION (T_End);
AADL_PORT_POS_O (AADLDATA)
ACTIVATION (T_Error)
[]
ACTIVATION (T_All);
AADL_PORT_POS_I (AADLDATA);
AADL_PORT_POS_O (AADLDATA)
[]
ACTIVATION (T_Preempt)
end select ;
ACTIVATION (T_Ok)
[]
ACTIVATION (T_Error)
[]
ACTIVATION (T_Stop)
end select
end loop
ACTIVATION (T_Stop)
end select
end loop
end var
end process
process Thread_PL [
ACTIVATION: LNT_Channel_Dispatch,
AADL_PORT_ACC_C: LNT_Channel_Data,
AADL_PORT_ACC_O: LNT_Channel_Data,
AADL_PORT_ANGLE_C: LNT_Channel_Data]
PORT_ACC_C: LNT_Channel_Port,
PORT_ACC_O: LNT_Channel_Port,
PORT_ANGLE_C: LNT_Channel_Port]
is
loop
select
var
ACC_C : LNT_Type_Data,
ACC_O : LNT_Type_Data,
ANGLE_C : LNT_Type_Data
in
ACC_C := EMPTY;
ACC_O := EMPTY;
ANGLE_C := AADLDATA;
loop
select
ACTIVATION (T_Begin);
AADL_PORT_ACC_C (AADLDATA);
AADL_PORT_ACC_O (AADLDATA)
select
ACTIVATION (T_Dispatch_Preemption);
PORT_ACC_C (?ACC_C);
PORT_ACC_O (?ACC_O)
[]
ACTIVATION (T_Preemption_Completion);
PORT_ANGLE_C (ANGLE_C)
[]
ACTIVATION (T_Dispatch_Completion);
PORT_ACC_C (?ACC_C);
PORT_ACC_O (?ACC_O);
PORT_ANGLE_C (ANGLE_C)
[]
ACTIVATION (T_Preemption)
end select ;
ACTIVATION (T_Complete)
[]
ACTIVATION (T_End);
AADL_PORT_ANGLE_C (AADLDATA)
ACTIVATION (T_Error)
[]
ACTIVATION (T_All);
AADL_PORT_ACC_C (AADLDATA);
AADL_PORT_ACC_O (AADLDATA);
AADL_PORT_ANGLE_C (AADLDATA)
[]
ACTIVATION (T_Preempt)
end select ;
ACTIVATION (T_Ok)
[]
ACTIVATION (T_Error)
[]
ACTIVATION (T_Stop)
end select
end loop
ACTIVATION (T_Stop)
end select
end loop
end var
end process
process Thread_PF [
ACTIVATION: LNT_Channel_Dispatch,
AADL_PORT_ACC_I: LNT_Channel_Data,
AADL_PORT_ACC_O: LNT_Channel_Data]
PORT_ACC_I: LNT_Channel_Port,
PORT_ACC_O: LNT_Channel_Port]
is
loop
select
var
ACC_I : LNT_Type_Data,
ACC_O : LNT_Type_Data
in
ACC_I := EMPTY;
ACC_O := AADLDATA;
loop
select
ACTIVATION (T_Begin);
AADL_PORT_ACC_I (AADLDATA)
[]
ACTIVATION (T_End);
AADL_PORT_ACC_O (AADLDATA)
select
ACTIVATION (T_Dispatch_Preemption);
PORT_ACC_I (?ACC_I)
[]
ACTIVATION (T_Preemption_Completion);
PORT_ACC_O (ACC_O)
[]
ACTIVATION (T_Dispatch_Completion);
PORT_ACC_I (?ACC_I);
PORT_ACC_O (ACC_O)
[]
ACTIVATION (T_Preemption)
end select ;
ACTIVATION (T_Complete)
[]
ACTIVATION (T_All);
AADL_PORT_ACC_I (AADLDATA);
AADL_PORT_ACC_O (AADLDATA)
ACTIVATION (T_Error)
[]
ACTIVATION (T_Preempt)
end select ;
ACTIVATION (T_Ok)
[]
ACTIVATION (T_Error)
[]
ACTIVATION (T_Stop)
end select
end loop
ACTIVATION (T_Stop)
end select
end loop
end var
end process
process Thread_FL [
ACTIVATION: LNT_Channel_Dispatch,
AADL_PORT_ANGLE_C: LNT_Channel_Data,
AADL_PORT_ANGLE_O: LNT_Channel_Data,
AADL_PORT_ORDER: LNT_Channel_Data]
PORT_ANGLE_C: LNT_Channel_Port,
PORT_ANGLE_O: LNT_Channel_Port,
PORT_ORDER: LNT_Channel_Port]
is
loop
select
var
ANGLE_C : LNT_Type_Data,
ANGLE_O : LNT_Type_Data,
ORDER : LNT_Type_Data
in
ANGLE_C := EMPTY;
ANGLE_O := EMPTY;
ORDER := AADLDATA;
loop
select
ACTIVATION (T_Begin);
AADL_PORT_ANGLE_C (AADLDATA);
AADL_PORT_ANGLE_O (AADLDATA)
[]
ACTIVATION (T_End);
AADL_PORT_ORDER (AADLDATA)
select
ACTIVATION (T_Dispatch_Preemption);
PORT_ANGLE_C (?ANGLE_C);
PORT_ANGLE_O (?ANGLE_O)
[]
ACTIVATION (T_Preemption_Completion);
PORT_ORDER (ORDER)
[]
ACTIVATION (T_Dispatch_Completion);
PORT_ANGLE_C (?ANGLE_C);
PORT_ANGLE_O (?ANGLE_O);
PORT_ORDER (ORDER)
[]
ACTIVATION (T_Preemption)
end select ;
ACTIVATION (T_Complete)
[]
ACTIVATION (T_All);
AADL_PORT_ANGLE_C (AADLDATA);
AADL_PORT_ANGLE_O (AADLDATA);
AADL_PORT_ORDER (AADLDATA)
ACTIVATION (T_Error)
[]
ACTIVATION (T_Preempt)
end select ;
ACTIVATION (T_Ok)
[]
ACTIVATION (T_Error)
[]
ACTIVATION (T_Stop)
end select
end loop
ACTIVATION (T_Stop)
end select
end loop
end var
end process
process Thread_AP [
ACTIVATION: LNT_Channel_Dispatch,
AADL_PORT_POSITION: LNT_Channel_Data,
AADL_PORT_ACC: LNT_Channel_Data,
AADL_PORT_ACC_I: LNT_Channel_Data,
AADL_PORT_POS_I: LNT_Channel_Data]
PORT_POSITION: LNT_Channel_Port,
PORT_ACC: LNT_Channel_Port,
PORT_ACC_I: LNT_Channel_Port,
PORT_POS_I: LNT_Channel_Port]
is
loop
select
var
POSITION : LNT_Type_Data,
ACC : LNT_Type_Data,
ACC_I : LNT_Type_Data,
POS_I : LNT_Type_Data
in
POSITION := EMPTY;
ACC := EMPTY;
ACC_I := AADLDATA;
POS_I := AADLDATA;
loop
select
ACTIVATION (T_Begin);
AADL_PORT_POSITION (AADLDATA);
AADL_PORT_ACC (AADLDATA)
select
ACTIVATION (T_Dispatch_Preemption);
PORT_POSITION (?POSITION);
PORT_ACC (?ACC)
[]
ACTIVATION (T_Preemption_Completion);
PORT_ACC_I (ACC_I);
PORT_POS_I (POS_I)
[]
ACTIVATION (T_Dispatch_Completion);
PORT_POSITION (?POSITION);
PORT_ACC (?ACC);
PORT_ACC_I (ACC_I);
PORT_POS_I (POS_I)
[]
ACTIVATION (T_Preemption)
end select ;
ACTIVATION (T_Complete)
[]
ACTIVATION (T_End);
AADL_PORT_ACC_I (AADLDATA);
AADL_PORT_POS_I (AADLDATA)
ACTIVATION (T_Error)
[]
ACTIVATION (T_All);
AADL_PORT_POSITION (AADLDATA);
AADL_PORT_ACC (AADLDATA);
AADL_PORT_ACC_I (AADLDATA);
AADL_PORT_POS_I (AADLDATA)
[]
ACTIVATION (T_Preempt)
end select ;
ACTIVATION (T_Ok)
[]
ACTIVATION (T_Error)
[]
ACTIVATION (T_Stop)
end select
end loop
ACTIVATION (T_Stop)
end select
end loop
end var
end process
process Device_Operator [
AADL_PORT_POS_C: LNT_Channel_Data]
PORT_POS_C: LNT_Channel_Port]
is
loop
select
AADL_PORT_POS_C (AADLDATA)
PORT_POS_C (AADLDATA)
[]
null
end select
......@@ -249,11 +348,11 @@ module FLIGHTCONTROLSYSTEM_Threads (FLIGHTCONTROLSYSTEM_Types) is
end process
process Device_GPS [
AADL_PORT_POSITION: LNT_Channel_Data]
PORT_POSITION: LNT_Channel_Port]
is
loop
select
AADL_PORT_POSITION (AADLDATA)
PORT_POSITION (AADLDATA)
[]
null
end select
......@@ -261,24 +360,24 @@ module FLIGHTCONTROLSYSTEM_Threads (FLIGHTCONTROLSYSTEM_Types) is
end process
process Device_IMU [
AADL_PORT_ANGLE: LNT_Channel_Data,
AADL_PORT_ACC: LNT_Channel_Data]
PORT_ANGLE: LNT_Channel_Port,
PORT_ACC: LNT_Channel_Port]
is
loop
select
AADL_PORT_ANGLE (AADLDATA)
PORT_ANGLE (AADLDATA)
[]
AADL_PORT_ACC (AADLDATA)
PORT_ACC (AADLDATA)
end select
end loop
end process
process Device_Platform [
AADL_PORT_ORDER: LNT_Channel_Data]
PORT_ORDER: LNT_Channel_Port]
is
loop
select
AADL_PORT_ORDER (AADLDATA)
PORT_ORDER (AADLDATA)
[]
null
end select
......@@ -286,55 +385,18 @@ module FLIGHTCONTROLSYSTEM_Threads (FLIGHTCONTROLSYSTEM_Types) is
end process
end module
module FLIGHTCONTROLSYSTEM_Ports (FLIGHTCONTROLSYSTEM_Types) is
process Data_Port [
Input: LNT_Channel_Data,
Output: LNT_Channel_Data]
is
loop
select
Input (AADLDATA)
[]
Output (AADLDATA)
end select
end loop
end process
process Event_Port_Periodic [
Input: LNT_Channel_Data,
Output: LNT_Channel_Data](
Queue_Size: Nat)
is
var
Nb_Input : Nat
in
Nb_Input := 0;
loop
select
Input (AADLDATA);
if (Nb_Input < Queue_Size)
then
Nb_Input := Nb_Input + 1
end if
[]
if (Nb_Input > 0)
then
Output (AADLDATA);
Nb_Input := Nb_Input - 1
end if
end select
end loop
end var
end process
end module
module FLIGHTCONTROLSYSTEM_Types
module Types
with "==", "eq" , "<", "lt" , "<=", "le" , ">", "gt" , ">=", "ge" is
type LNT_Type_Data is
AADLDATA
AADLDATA, EMPTY
end type
channel LNT_Channel_Data is
type LNT_Type_Data_FIFO is
list of LNT_Type_Data
with "==", "eq" , "length" , "append" , "tail" , "head" , "<>", "ne", "!="
end type
channel LNT_Channel_Port is
(LNT_Type_Data)
end channel
type LNT_Type_Time_Constraint is
......@@ -350,7 +412,7 @@ with "==", "eq" , "<", "lt" , "<=", "le" , ">", "gt" , ">=", "ge" is
end type
type LNT_Type_Dispatch is
T_Begin, T_End, T_All, T_Preempt, T_Stop, T_Error, T_Ok
T_Dispatch_Preemption, T_Preemption_Completion, T_Dispatch_Completion, T_Preemption, T_Stop, T_Error, T_Complete
end type
type LNT_Type_Event is
......@@ -400,7 +462,141 @@ with "==", "eq" , "<", "lt" , "<=", "le" , ">", "gt" , ">=", "ge" is
end function
end module
module FLIGHTCONTROLSYSTEM_Processor (FLIGHTCONTROLSYSTEM_Types) is
module FLIGHTCONTROLSYSTEM_Main (Types, FLIGHTCONTROLSYSTEM_Processor, FLIGHTCONTROLSYSTEM_Threads, LNT_Generic_Process_For_Port_Connections) is
process Main [
ACTIVATION_3: LNT_Channel_Dispatch,
SEND_V5: LNT_Channel_Port,
RECEIVE_V16: LNT_Channel_Port,
ACTIVATION_6: LNT_Channel_Dispatch,
RECEIVE_V13: LNT_Channel_Port,
RECEIVE_V3: LNT_Channel_Port,
SEND_V1: LNT_Channel_Port,
ACTIVATION_7: LNT_Channel_Dispatch,
RECEIVE_V7: LNT_Channel_Port,
SEND_V3: LNT_Channel_Port,
ACTIVATION_5: LNT_Channel_Dispatch,
RECEIVE_V1: LNT_Channel_Port,
RECEIVE_V4: LNT_Channel_Port,
SEND_V2: LNT_Channel_Port,
ACTIVATION_4: LNT_Channel_Dispatch,
RECEIVE_V6: LNT_Channel_Port,
SEND_V4: LNT_Channel_Port,