Skip to content

GitLab

Commit 9350c78e authored by hana's avatar hana
Browse files

Start of AADL Behavior Annex mapping.

parent 23c99ceb
Hide whitespace changes
Inline Side-by-side
Showing with 274 additions and 72 deletions
src/backends/lnt/ocarina-backends-lnt-printer.adb
View file @ 9350c78e
......@@ -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;
......
src/backends/lnt/ocarina-backends-lnt-tree_generator_main.adb
View file @ 9350c78e
......@@ -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 (
......
src/backends/lnt/ocarina-backends-lnt-tree_generator_port.adb
View file @ 9350c78e
......@@ -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,
......
src/backends/lnt/ocarina-backends-lnt-tree_generator_processor.adb
View file @ 9350c78e
......@@ -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 (
......
src/backends/lnt/ocarina-backends-lnt-tree_generator_thread.adb
View file @ 9350c78e
......@@ -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")));
......
src/backends/lnt/ocarina-backends-lnt-tree_generator_types.adb
View file @ 9350c78e
......@@ -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);
......
src/backends/lnt/ocarina-backends-lnt.ads
View file @ 9350c78e
......@@ -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;
......
src/backends/ocarina-backends-lnt-nodes.idl
View file @ 9350c78e
......@@ -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 {};
......
src/core/model/ocarina-analyzer-aadl_ba.adb
View file @ 9350c78e
......@@ -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)
......
src/core/model/ocarina-analyzer-aadl_ba.ads
View file @ 9350c78e
......@@ -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)