From 9350c78e07b433341461eb27796eaa68d901ed10 Mon Sep 17 00:00:00 2001 From: hana Date: Wed, 10 May 2017 21:10:01 +0100 Subject: [PATCH] Start of AADL Behavior Annex mapping. --- .../lnt/ocarina-backends-lnt-printer.adb | 10 + ...arina-backends-lnt-tree_generator_main.adb | 11 +- ...arina-backends-lnt-tree_generator_port.adb | 4 +- ...-backends-lnt-tree_generator_processor.adb | 10 +- ...ina-backends-lnt-tree_generator_thread.adb | 185 +++++++++++++++--- ...rina-backends-lnt-tree_generator_types.adb | 87 ++++++-- src/backends/lnt/ocarina-backends-lnt.ads | 2 +- src/backends/ocarina-backends-lnt-nodes.idl | 7 + src/core/model/ocarina-analyzer-aadl_ba.adb | 15 -- src/core/model/ocarina-analyzer-aadl_ba.ads | 15 ++ 10 files changed, 274 insertions(+), 72 deletions(-) diff --git a/src/backends/lnt/ocarina-backends-lnt-printer.adb b/src/backends/lnt/ocarina-backends-lnt-printer.adb index 3590a157..a02d1126 100644 --- a/src/backends/lnt/ocarina-backends-lnt-printer.adb +++ b/src/backends/lnt/ocarina-backends-lnt-printer.adb @@ -573,6 +573,16 @@ package body Ocarina.Backends.LNT.Printer is L_Write ("and"); when K_Or => L_Write ("or"); + when K_Head => + L_Write ("head"); + when K_Tail => + L_Write ("tail"); + when K_Append => + L_Write ("append"); + when K_Length => + L_Write ("length"); + when K_Reverse => + L_Write ("reverse"); when others => null; end case; diff --git a/src/backends/lnt/ocarina-backends-lnt-tree_generator_main.adb b/src/backends/lnt/ocarina-backends-lnt-tree_generator_main.adb index 036811b8..8655991e 100644 --- a/src/backends/lnt/ocarina-backends-lnt-tree_generator_main.adb +++ b/src/backends/lnt/ocarina-backends-lnt-tree_generator_main.adb @@ -275,7 +275,7 @@ package body Ocarina.Backends.LNT.Tree_Generator_Main is if not AINU.Is_Empty (Connections (E)) then S := AIN.First_Node (Connections (E)); while Present (S) loop - Put_Line (Image (AIN.Display_Name (AIN.Identifier (S)))); + -- Put_Line (Image (AIN.Display_Name (AIN.Identifier (S)))); S := AIN.Next_Node (S); end loop; end if; @@ -346,7 +346,7 @@ package body Ocarina.Backends.LNT.Tree_Generator_Main is Aux_N_Port_3 := BLNu.Make_Node_Container (N_Port); BLNu.Append_Node_To_List (Make_Gate_Declaration - (Make_Identifier ("LNT_Channel_Data"), + (Make_Identifier ("LNT_Channel_Port"), N_Port), L_Gates_Declaration); BLNu.Append_Node_To_List (Aux_N_Port_1, Device_Gates_List); @@ -456,6 +456,7 @@ package body Ocarina.Backends.LNT.Tree_Generator_Main is N_Event : Node_Id; Aux_N_Event : Node_Id; + Aux_N_Event_1 : Node_Id; N_Port : Node_Id; Aux_N_Port_1 : Node_Id; Aux_N_Port_2 : Node_Id; @@ -513,7 +514,7 @@ package body Ocarina.Backends.LNT.Tree_Generator_Main is Aux_N_Port_4 := BLNu.Make_Node_Container (N_Port); BLNu.Append_Node_To_List (Make_Gate_Declaration - (Make_Identifier ("LNT_Channel_Data"), + (Make_Identifier ("LNT_Channel_Port"), N_Port), L_Gates_Declaration); BLNu.Append_Node_To_List (Aux_N_Port_1, Thread_Gates_List); @@ -558,7 +559,9 @@ package body Ocarina.Backends.LNT.Tree_Generator_Main is elsif AIN.Is_Event (S) then -- event port if Is_Not_Periodic then + Aux_N_Event := BLNu.Make_Node_Container (N_Event); + Aux_N_Event_1 := BLNu.Make_Node_Container (N_Event); Port_Gates_List := New_List ( Make_Identifier (N_SEND), -- SEND_ Aux_N_Port_3, -- RECEIVE_ @@ -569,7 +572,7 @@ package body Ocarina.Backends.LNT.Tree_Generator_Main is New_List (Make_Identifier (Integer'Image (Queue_Size)))); - BLNu.Append_Node_To_List (N_Event, + BLNu.Append_Node_To_List (Aux_N_Event_1, Interface_Connection_Gates_List); else Port_Gates_List := New_List ( diff --git a/src/backends/lnt/ocarina-backends-lnt-tree_generator_port.adb b/src/backends/lnt/ocarina-backends-lnt-tree_generator_port.adb index 7c06e3e0..5a680827 100644 --- a/src/backends/lnt/ocarina-backends-lnt-tree_generator_port.adb +++ b/src/backends/lnt/ocarina-backends-lnt-tree_generator_port.adb @@ -91,10 +91,10 @@ package body Ocarina.Backends.LNT.Tree_Generator_Port is No_List, New_List ( Make_Gate_Declaration - (Make_Identifier ("LNT_Channel_Data"), + (Make_Identifier ("LNT_Channel_Port"), Make_Identifier ("Input")), Make_Gate_Declaration - (Make_Identifier ("LNT_Channel_Data"), + (Make_Identifier ("LNT_Channel_Port"), Make_Identifier ("Output"))), No_List, No_List, diff --git a/src/backends/lnt/ocarina-backends-lnt-tree_generator_processor.adb b/src/backends/lnt/ocarina-backends-lnt-tree_generator_processor.adb index 15a863c5..aa98113f 100644 --- a/src/backends/lnt/ocarina-backends-lnt-tree_generator_processor.adb +++ b/src/backends/lnt/ocarina-backends-lnt-tree_generator_processor.adb @@ -1454,7 +1454,7 @@ package body Ocarina.Backends.LNT.Tree_Generator_Processor is New_List ( Make_Communication_Statement (Make_Identifier ("ACTIVATION"), - New_List (Make_Identifier ("T_All")), + New_List (Make_Identifier ("T_Dispatch_Completion")), false, No_Node), Make_Assignment_Statement ( Make_Identifier ("Threads"), @@ -1485,7 +1485,7 @@ package body Ocarina.Backends.LNT.Tree_Generator_Processor is New_List ( Make_Communication_Statement (Make_Identifier ("ACTIVATION"), - New_List (Make_Identifier ("T_End")), + New_List (Make_Identifier ("T_Preemption_Completion")), false, No_Node), Make_Assignment_Statement ( Make_Identifier ("Threads"), @@ -1507,7 +1507,7 @@ package body Ocarina.Backends.LNT.Tree_Generator_Processor is New_List ( Make_Communication_Statement (Make_Identifier ("ACTIVATION"), - New_List (Make_Identifier ("T_Begin")), + New_List (Make_Identifier ("T_Dispatch_Preemption")), false, No_Node), Make_Assignment_Statement ( Make_Identifier ("Threads"), @@ -1520,7 +1520,7 @@ package body Ocarina.Backends.LNT.Tree_Generator_Processor is New_List (Make_Communication_Statement (Make_Identifier ("ACTIVATION"), - New_List (Make_Identifier ("T_Preempt")), + New_List (Make_Identifier ("T_Preemption")), false, No_Node))), Make_Assignment_Statement ( Make_Identifier ("Threads"), @@ -1532,7 +1532,7 @@ package body Ocarina.Backends.LNT.Tree_Generator_Processor is Make_Time_Const (0)))), Make_Communication_Statement (Make_Identifier ("ACTIVATION"), - New_List (Make_Identifier ("T_Ok")))), + New_List (Make_Identifier ("T_Complete")))), New_List ( Make_Elsif_Statement (Make_Infix_Function_Call_Expression ( diff --git a/src/backends/lnt/ocarina-backends-lnt-tree_generator_thread.adb b/src/backends/lnt/ocarina-backends-lnt-tree_generator_thread.adb index 42ff8e0f..2520ab5b 100644 --- a/src/backends/lnt/ocarina-backends-lnt-tree_generator_thread.adb +++ b/src/backends/lnt/ocarina-backends-lnt-tree_generator_thread.adb @@ -40,6 +40,11 @@ with Ocarina.ME_AADL; with Ocarina.ME_AADL.AADL_Instances.Nodes; with Ocarina.ME_AADL.AADL_Instances.Nutils; with Ocarina.ME_AADL.AADL_Instances.Entities; +with Ocarina.ME_AADL_BA.BA_Tree.Nodes; +-- with Ocarina.ME_AADL_BA.BA_Tree.Debug; +with Ocarina.Analyzer.AADL_BA; +with Ocarina.ME_AADL_BA.BA_Tree.Nutils; + with Utils; use Utils; use Ocarina.Backends.LNT.Components; @@ -63,6 +68,13 @@ package body Ocarina.Backends.LNT.Tree_Generator_Thread is use BLN; use BLNu; + package BATN renames Ocarina.ME_AADL_BA.BA_Tree.Nodes; + package BANu renames Ocarina.ME_AADL_BA.BA_Tree.Nutils; + -- package ATN renames Ocarina.ME_AADL.AADL_Tree.Nodes; + -- use ATN; + use BATN; + use BANu; + procedure Visit (E : Node_Id); procedure Visit_Architecture_Instance (E : Node_Id); procedure Visit_Component_Instance (E : Node_Id); @@ -190,9 +202,12 @@ package body Ocarina.Backends.LNT.Tree_Generator_Thread is ---------------------------- procedure Visit_Thread_Instance (E : Node_Id) is S : Node_Id; + BA : Node_Id; N : Node_Id; N_Activation : Node_Id; N_Port : Node_Id; + N_Variable_Port : Node_Id; + Aux_N_Variable_Port : Node_Id; Gate : Node_Id; Communication : Node_Id; Aux_Communication : Node_Id; @@ -203,19 +218,38 @@ package body Ocarina.Backends.LNT.Tree_Generator_Thread is L_All : List_Id; L_Gates : List_Id; L_Statements : List_Id; - N_Loop : Node_Id; + -- When BA + Has_BA : Boolean := false; + Si : Node_Id; + N_Si : Node_Id; + Vi : Node_Id; + N_Vi : Node_Id; + Var_Dec : List_Id; + Out_Loop : List_Id; + In_Select : List_Id; + Variable : Node_Id; + Thread_Identifier : constant Name_Id := AIN.Display_Name (AIN.Identifier (E)); begin N_Activation := Make_Identifier ("ACTIVATION"); + LNT_States_List := New_List; + Var_Dec := New_List; + Out_Loop := New_List; L_Out_Port := New_List; L_In_Port := New_List; L_Begin := New_List (Make_Communication_Statement - (N_Activation, New_List (Make_Identifier ("T_Begin")))); + (N_Activation, New_List (Make_Identifier + ("T_Dispatch_Preemption")))); L_All := New_List (Make_Communication_Statement - (N_Activation, New_List (Make_Identifier ("T_All")))); + (N_Activation, New_List (Make_Identifier + ("T_Dispatch_Completion")))); L_End := New_List (Make_Communication_Statement - (N_Activation, New_List (Make_Identifier ("T_End")))); + (N_Activation, New_List (Make_Identifier + ("T_Preemption_Completion")))); + L_Gates := New_List (Make_Gate_Declaration + (Make_Identifier ("LNT_Channel_Dispatch"), N_Activation)); + -- Visit all the subcomponents of the thread if not AINU.Is_Empty (Subcomponents (E)) then S := AIN.First_Node (Subcomponents (E)); @@ -224,37 +258,125 @@ package body Ocarina.Backends.LNT.Tree_Generator_Thread is S := AIN.Next_Node (S); end loop; end if; - L_Gates := New_List ( - Make_Gate_Declaration - (Make_Identifier ("LNT_Channel_Dispatch"), - N_Activation)); + -- BA mapping + if not AINU.Is_Empty (AIN.Annexes (E)) then + S := AIN.First_Node (AIN.Annexes (E)); + loop + if (To_Upper (AIN.Display_Name (AIN.Identifier (S))) = + To_Upper (Get_String_Name ("behavior_specification"))) + and then Present (AIN.Corresponding_Annex (S)) + then + Has_BA := true; + BA := AIN.Corresponding_Annex (S); + if not BANu.Is_Empty (BATN.States (BA)) then + Si := BATN.First_Node (BATN.States (BA)); + loop + N_Si := BATN.First_Node (BATN.Identifiers (Si)); + loop + if Analyzer.AADL_BA.Is_Initial (BA, N_Si) then + Variable := Make_Var_Declaration ( + Make_Identifier ("STATE"), + Make_Identifier ("LNT_Type_States")); + BLNu.Append_Node_To_List (Variable, Var_Dec); + BLNu.Append_Node_To_List (Make_Assignment_Statement + (Make_Identifier ("STATE"), Make_Identifier ( + To_Upper (BATN.Display_Name (N_Si)))), + Out_Loop); + end if; + BLNu.Append_Node_To_List (Make_Identifier ( + To_Upper (BATN.Display_Name (N_Si))), + LNT_States_List); + N_Si := BATN.Next_Node (N_Si); + exit when No (N_Si); + end loop; + Si := BATN.Next_Node (Si); + exit when No (Si); + end loop; + end if; + if not BANu.Is_Empty (BATN.Variables (BA)) then + Vi := BATN.First_Node (BATN.Variables (BA)); + loop + N_Vi := BATN.First_Node (BATN.Identifiers (Vi)); + loop + BLNu.Append_Node_To_List (Make_Identifier ( + To_Upper (BATN.Display_Name (N_Vi))), + LNT_States_List); + N_Vi := BATN.Next_Node (N_Vi); + exit when No (N_Vi); + end loop; + Vi := BATN.Next_Node (Vi); + exit when No (Vi); + end loop; + end if; + end if; + S := AIN.Next_Node (S); + exit when No (S); + end loop; + end if; + -- end BA mapping if not AINU.Is_Empty (Features (E)) then S := AIN.First_Node (Features (E)); loop if (AIN.Kind (S) = K_Port_Spec_Instance) then + -- gate identifier N_Port := New_Identifier (To_Upper (AIN.Name - (AIN.Identifier (S))), "AADL_PORT_"); - + (AIN.Identifier (S))), "PORT_"); + -- variable identifier + N_Variable_Port := Make_Identifier (To_Upper (AIN.Name + (AIN.Identifier (S)))); + Aux_N_Variable_Port := BLNu.Make_Node_Container + (N_Variable_Port); + -- port variable + Variable := Make_Var_Declaration (N_Variable_Port, + Make_Identifier ("LNT_Type_Data")); + BLNu.Append_Node_To_List (Variable, Var_Dec); + + -- gate declaration Gate := Make_Gate_Declaration ( - Make_Identifier ("LNT_Channel_Data"), N_Port); + Make_Identifier ("LNT_Channel_Port"), N_Port); BLNu.Append_Node_To_List (Gate, L_Gates); - - Communication := Make_Communication_Statement - (N_Port, New_List (Make_Identifier ("AADLDATA"))); - Aux_Communication := BLNu.Make_Node_Container (Communication); + -- gate communication if AIN.Is_Out (S) then + -- port variable initialization + if Has_BA then + BLNu.Append_Node_To_List (Make_Assignment_Statement + (Aux_N_Variable_Port, Make_Identifier ("NONE")), + Out_Loop); + else + BLNu.Append_Node_To_List (Make_Assignment_Statement + (Aux_N_Variable_Port, Make_Identifier ("AADLDATA")), + Out_Loop); + end if; + Communication := Make_Communication_Statement + (N_Port, New_List (Make_Offer_Statement + (No_Node, N_Variable_Port, false))); + Aux_Communication := BLNu.Make_Node_Container + (Communication); + BLNu.Append_Node_To_List (Communication, L_Out_Port); - BLNu.Append_Node_To_List - (Aux_Communication, L_End); + BLNu.Append_Node_To_List (Aux_Communication, L_End); elsif AIN.Is_In (S) then + -- port variable initialization + if Has_BA then + BLNu.Append_Node_To_List (Make_Assignment_Statement + (Aux_N_Variable_Port, Make_Identifier ("NONE")), + Out_Loop); + else + BLNu.Append_Node_To_List (Make_Assignment_Statement + (Aux_N_Variable_Port, Make_Identifier ("EMPTY")), + Out_Loop); + end if; + Communication := Make_Communication_Statement + (N_Port, New_List (Make_Offer_Statement + (No_Node, N_Variable_Port, true))); + Aux_Communication := BLNu.Make_Node_Container + (Communication); + BLNu.Append_Node_To_List (Communication, L_In_Port); - BLNu.Append_Node_To_List - (Aux_Communication, L_Begin); + BLNu.Append_Node_To_List (Aux_Communication, L_Begin); end if; - end if; - -- Visit (Corresponding_Instance (S)); S := AIN.Next_Node (S); exit when No (S); end loop; @@ -268,10 +390,7 @@ package body Ocarina.Backends.LNT.Tree_Generator_Thread is not BLNu.Is_Empty (L_End) or else not BLNu.Is_Empty (L_All)) then - N_Loop := Make_Loop_Statement ( - New_List ( - Make_Select_Statement ( - New_List ( + In_Select := New_List ( Make_Select_Statement_Alternative (New_List ( Make_Select_Statement ( New_List ( @@ -280,17 +399,21 @@ package body Ocarina.Backends.LNT.Tree_Generator_Thread is Make_Select_Statement_Alternative (L_All), Make_Select_Statement_Alternative (New_List ( Make_Communication_Statement - (N_Activation, New_List (Make_Identifier ("T_Preempt"))))))), + (N_Activation, New_List (Make_Identifier ("T_Preemption"))))))), Make_Communication_Statement - (N_Activation, New_List (Make_Identifier ("T_Ok"))))), + (N_Activation, New_List (Make_Identifier ("T_Complete"))))), Make_Select_Statement_Alternative (New_List ( Make_Communication_Statement (N_Activation, New_List (Make_Identifier ("T_Error"))))), Make_Select_Statement_Alternative (New_List ( Make_Communication_Statement - (N_Activation, New_List (Make_Identifier ("T_Stop"))))))))); - L_Statements := BLNu.New_List (N_Loop); + (N_Activation, New_List (Make_Identifier ("T_Stop")))))); + L_Statements := BLNu.New_List ( + Make_Var_Loop_Select ( + Var_Dec, + Out_Loop, + In_Select)); else L_Statements := BLNu.New_List (Make_Null_Statement); end if; @@ -338,10 +461,10 @@ package body Ocarina.Backends.LNT.Tree_Generator_Thread is loop if (AIN.Kind (S) = K_Port_Spec_Instance) then N_Port := New_Identifier (To_Upper (AIN.Name - (AIN.Identifier (S))), "AADL_PORT_"); + (AIN.Identifier (S))), "PORT_"); Gate := Make_Gate_Declaration ( - Make_Identifier ("LNT_Channel_Data"), N_Port); + Make_Identifier ("LNT_Channel_Port"), N_Port); Communication := Make_Communication_Statement (N_Port, New_List (Make_Identifier ("AADLDATA"))); diff --git a/src/backends/lnt/ocarina-backends-lnt-tree_generator_types.adb b/src/backends/lnt/ocarina-backends-lnt-tree_generator_types.adb index 00f0e83b..5c491433 100644 --- a/src/backends/lnt/ocarina-backends-lnt-tree_generator_types.adb +++ b/src/backends/lnt/ocarina-backends-lnt-tree_generator_types.adb @@ -108,19 +108,19 @@ package body Ocarina.Backends.LNT.Tree_Generator_Types is Make_Type_Exp ( No_Node, New_List ( - Make_Type_Constructor (Make_Identifier ("T_Begin"), - No_List, No_List), - Make_Type_Constructor (Make_Identifier ("T_End"), - No_List, No_List), - Make_Type_Constructor (Make_Identifier ("T_All"), - No_List, No_List), - Make_Type_Constructor (Make_Identifier ("T_Preempt"), - No_List, No_List), + Make_Type_Constructor (Make_Identifier + ("T_Dispatch_Preemption"), No_List, No_List), + Make_Type_Constructor (Make_Identifier + ("T_Preemption_Completion"), No_List, No_List), + Make_Type_Constructor (Make_Identifier + ("T_Dispatch_Completion"), No_List, No_List), + Make_Type_Constructor (Make_Identifier + ("T_Preemption"), No_List, No_List), Make_Type_Constructor (Make_Identifier ("T_Stop"), No_List, No_List), Make_Type_Constructor (Make_Identifier ("T_Error"), No_List, No_List), - Make_Type_Constructor (Make_Identifier ("T_Ok"), + Make_Type_Constructor (Make_Identifier ("T_Complete"), No_List, No_List)), false, false, false, false, false, false), No_List, @@ -140,7 +140,18 @@ package body Ocarina.Backends.LNT.Tree_Generator_Types is No_List, No_List); BLNu.Append_Node_To_List (N, L_Types); - + -- When BA + if not Is_Empty (LNT_States_List) then + N := Make_Type_Def + (Make_Identifier ("LNT_Type_States"), + Make_Type_Exp ( + No_Node, + LNT_States_List, + false, false, false, false, false, false), + No_List, + No_List); + BLNu.Append_Node_To_List (N, L_Types); + end if; end Add_LNT_Types; procedure Add_LNT_Channels (L_Channels : List_Id) is @@ -161,6 +172,31 @@ package body Ocarina.Backends.LNT.Tree_Generator_Types is Make_Gate_Profile (New_List (Make_Identifier ("LNT_Type_Event"))))); BLNu.Append_Node_To_List (N, L_Channels); + -- When BA + if not Is_Empty (LNT_States_List) then + N := Make_Channel ( + Make_Identifier ("LNT_Channel_Event_Port"), + New_List ( + Make_Gate_Profile (New_List (Make_Identifier + ("Bool"))))); + BLNu.Append_Node_To_List (N, L_Channels); + + N := Make_Channel ( + Make_Identifier ("LNT_Channel_Event_Data_Port"), + New_List ( + Make_Gate_Profile (New_List ( + Make_Identifier ("LNT_Type_Data"), + Make_Identifier ("Bool") + )))); + BLNu.Append_Node_To_List (N, L_Channels); + + N := Make_Channel ( + Make_Identifier ("LNT_Channel_Data_Port"), + New_List ( + Make_Gate_Profile (New_List (Make_Identifier + ("LNT_Type_Data"))))); + BLNu.Append_Node_To_List (N, L_Channels); + end if; end Add_LNT_Channels; procedure Add_LNT_Functions (L_Functions : List_Id; @@ -329,19 +365,42 @@ package body Ocarina.Backends.LNT.Tree_Generator_Types is (New_Identifier (Get_String_Name ("_Types"), Get_Name_String (System_Name))); Definitions_List := New_List; + -- Data generic type N := Make_Type_Def (Make_Identifier ("LNT_Type_Data"), - Make_Identifier ("AADLDATA"), + Make_Type_Exp ( + No_Node, + New_List ( + Make_Type_Constructor (Make_Identifier ("AADLDATA"), + No_List, No_List), + Make_Type_Constructor (Make_Identifier ("EMPTY"), + No_List, No_List)), + false, false, false, false, false, false), No_List, No_List); BLNu.Append_Node_To_List (N, Definitions_List); - + -- generic list of Data + N := Make_Type_Def + (Make_Identifier ("LNT_Type_Data_FIFO"), + Make_Type_Exp ( + Make_Identifier ("LNT_Type_Data"), + No_List, + false, false, true, false, false, false), + No_List, + New_List (Make_Predefined_Function (K_Equality, true), + Make_Predefined_Function (K_Length, true), + Make_Predefined_Function (K_Append, true), + Make_Predefined_Function (K_Tail, true), + Make_Predefined_Function (K_Head, true), + Make_Predefined_Function (K_Inequality, true) + )); + BLNu.Append_Node_To_List (N, Definitions_List); + -- generic channel N := Make_Channel - (Make_Identifier ("LNT_Channel_Data"), + (Make_Identifier ("LNT_Channel_Port"), New_List ( Make_Gate_Profile (New_List ( Make_Identifier ("LNT_Type_Data"))))); - BLNu.Append_Node_To_List (N, Definitions_List); Add_LNT_Types (Definitions_List, Thread_Number, Hyperperiod); diff --git a/src/backends/lnt/ocarina-backends-lnt.ads b/src/backends/lnt/ocarina-backends-lnt.ads index 3d6b25f6..32276c33 100644 --- a/src/backends/lnt/ocarina-backends-lnt.ads +++ b/src/backends/lnt/ocarina-backends-lnt.ads @@ -59,7 +59,7 @@ package Ocarina.Backends.LNT is Not_Periodic_Thread_Number : Natural := 0; Hyperperiod : Integer := 0; LNT_Thread_Instance_List : List_Id := No_List; - + LNT_States_List : List_Id := No_List; private Separator : Types.Name_Id; LNT_Threads : Node_Id; diff --git a/src/backends/ocarina-backends-lnt-nodes.idl b/src/backends/ocarina-backends-lnt-nodes.idl index 050379f4..b3708573 100644 --- a/src/backends/ocarina-backends-lnt-nodes.idl +++ b/src/backends/ocarina-backends-lnt-nodes.idl @@ -112,6 +112,13 @@ module Ocarina::Backends::LNT::Nodes { interface First_Element : Predefined_Function {}; // "first" interface Last_Element : Predefined_Function {}; // "last" + // predefined functions for LNT lists + interface Length : Predefined_Function {}; // "length" + interface Append : Predefined_Function {}; // "append" + interface Head : Predefined_Function {}; // "head" + interface Tail : Predefined_Function {}; // "tail" + interface Reverse : Predefined_Function {}; // "reverse" + // Functions on Booleans and, and then, or, or else, xor, implies interface _And : Predefined_Function {}; interface _Or : Predefined_Function {}; diff --git a/src/core/model/ocarina-analyzer-aadl_ba.adb b/src/core/model/ocarina-analyzer-aadl_ba.adb index 70a12c29..6aa20b0e 100644 --- a/src/core/model/ocarina-analyzer-aadl_ba.adb +++ b/src/core/model/ocarina-analyzer-aadl_ba.adb @@ -120,21 +120,6 @@ package body Ocarina.Analyzer.AADL_BA is List_First_Node : in out Node_Id; List_Last_Node : in out Node_Id); - function Is_Complete - (BA_Root : Node_Id; - State : Node_Id) - return boolean; - - function Is_Initial - (BA_Root : Node_Id; - State : Node_Id) - return boolean; - - function Is_Final - (BA_Root : Node_Id; - State : Node_Id) - return boolean; - function Exist_In_Modes (Component : Node_Id; State : Node_Id) diff --git a/src/core/model/ocarina-analyzer-aadl_ba.ads b/src/core/model/ocarina-analyzer-aadl_ba.ads index 94a1b181..cf86ff7f 100644 --- a/src/core/model/ocarina-analyzer-aadl_ba.ads +++ b/src/core/model/ocarina-analyzer-aadl_ba.ads @@ -38,4 +38,19 @@ package Ocarina.Analyzer.AADL_BA is function Analyze_Model (Root : Node_Id) return Boolean; -- Proceed to BA analysis + function Is_Complete + (BA_Root : Node_Id; + State : Node_Id) + return boolean; + + function Is_Initial + (BA_Root : Node_Id; + State : Node_Id) + return boolean; + + function Is_Final + (BA_Root : Node_Id; + State : Node_Id) + return boolean; + end Ocarina.Analyzer.AADL_BA; -- GitLab