Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
TASTE
Ocarina
Commits
818f742d
Commit
818f742d
authored
May 19, 2017
by
Jerome Hugues
Committed by
GitHub
May 19, 2017
Browse files
Merge pull request #90 from HannaMk/master
Update of AADL-LNT generation
parents
f4386e25
15aede27
Changes
22
Expand all
Hide whitespace changes
Inline
Side-by-side
configure.ac
View file @
818f742d
...
...
@@ -421,6 +421,7 @@ AC_OUTPUT([
resources/runtime/aadl_xml/Makefile
resources/runtime/alloy/Makefile
resources/runtime/cheddar/Makefile
resources/runtime/lnt/Makefile
resources/runtime/python/Makefile
projects/ocarina.gpr
src/main/Makefile
...
...
resources/runtime/Makefile.am
View file @
818f742d
SUBDIRS
=
cheddar aadl_xml python alloy
SUBDIRS
=
cheddar aadl_xml python alloy
lnt
@DEBUG_FALSE@
DEBUG_FLAG
=
--disable-debug
@DEBUG_TRUE@
DEBUG_FLAG
=
--enable-debug
...
...
resources/runtime/lnt/LNT_Generic_Process_For_Port_Connections.lnt
0 → 100644
View file @
818f742d
module LNT_Generic_Process_For_Port_Connections (Types) is
-- No Behavior Annex
-- data port --
process Data_Port [
Input: LNT_Channel_Port,
Output: LNT_Channel_Port]
is
var Data : LNT_Type_Data in
Data := EMPTY;
loop
select
Input (?Data)
[]
Output (Data)
end select
end loop
end var
end process
-- event port --
-- for no periodic threads --
process Event_Port [
Input: LNT_Channel_Port,
Output: LNT_Channel_Port,
Notify: LNT_Channel_Event](
Queue_Size: Nat)
is
var
Data : LNT_Type_Data,
FIFO : LNT_Type_Data_FIFO,
Is_New : bool
in
FIFO := {};
Data := EMPTY;
Is_New := false;
loop
select
Input (?Data);
Is_New := true;
if length (FIFO) >= Queue_Size then
FIFO := tail (FIFO)
end if;
FIFO := append (Data, FIFO)
[]
if (FIFO != {}) then
Output (Head (FIFO));
FIFO := tail (FIFO)
else
Output (EMPTY)
end if
[]
if (Is_New) then
Notify (Incoming_Event);
Is_New := false
else
Notify (No_Event)
end if
end select
end loop
end var
end process
-- for periodic threads
process Event_Port_For_Periodic [
Input: LNT_Channel_Port,
Output: LNT_Channel_Port](
Queue_Size: Nat)
is
var
Data : LNT_Type_Data,
FIFO : LNT_Type_Data_FIFO,
Is_New : bool
in
FIFO := {};
Data := EMPTY;
Is_New := false;
loop
select
Input (?Data);
Is_New := true;
if length (FIFO) >= Queue_Size then
FIFO := tail (FIFO)
end if;
FIFO := append (Data, FIFO)
[]
if (FIFO != {}) then
Output (Head (FIFO));
FIFO := tail (FIFO)
else
Output (EMPTY)
end if
end select
end loop
end var
end process
end module
resources/runtime/lnt/LNT_Generic_Process_For_Port_Connections_BA.lnt
0 → 100644
View file @
818f742d
module LNT_Generic_Process_For_Port_Connections_BA (BA_Types) is -- With Behavior Annex
-- data port --
process Data_Port [
Input: LNT_Channel_Data_Port,
Output: LNT_Channel_Data_Port]
is
var Data : LNT_Type_Data in
Data := DATA_INIT;
loop
select
Input (?Data)
[]
Output (Data)
end select
end loop
end var
end process
-- event port --
-- for no periodic threads --
process Event_Port [
Input: LNT_Channel_Event_Port,
Output: LNT_Channel_Event_Port,
Notify: LNT_Channel_Event](
Queue_Size: Nat)
is
var
Nb_Events : Nat,
Is_New : bool
in
Nb_Events := 0;
Is_New := false;
loop
select
Input (true);
Is_New := true;
if (Nb_Events < Queue_Size) then
Nb_Events := Nb_Events + 1
end if
[]
if (Nb_Events > 0) then
Output (true);
Nb_Events := Nb_Events - 1
else
Output (false)
end if
[]
if (Is_New) then
Notify (Incoming_Event);
Is_New := false
else
Notify (No_Event)
end if
end select
end loop
end var
end process
-- for periodic threads --
process Event_Port_For_Periodic [
Input: LNT_Channel_Event_Port,
Output: LNT_Channel_Event_Port](
Queue_Size: Nat)
is
var
Nb_Events : Nat
in
Nb_Events := 0;
loop
select
Input (true);
if (Nb_Events < Queue_Size) then
Nb_Events := Nb_Events + 1
end if
[]
if (Nb_Events > 0) then
Output (true);
Nb_Events := Nb_Events - 1
else
Output (false)
end if
end select
end loop
end var
end process
-- event data port
-- for no periodic threads --
process Event_Data_Port_Sporadic [
Input: LNT_Channel_Event_Data_Port,
Output: LNT_Channel_Event_Data_Port,
Notify: LNT_Channel_Event](
Queue_Size: Nat)
is
var
FIFO : LNT_Type_Data_FIFO,
Is_New : bool,
D : LNT_Type_Data
in
FIFO := {};
D := DATA_INIT;
Is_New := false;
loop
select
Input (?D, true);
Is_New := true;
if length (FIFO) >= Queue_Size then
FIFO := tail (FIFO)
end if;
FIFO := append (D, FIFO)
[]
if (Is_New) then
Notify (Incoming_Event);
Is_New := false
else
Notify (No_Event)
end if
[]
if (FIFO != {}) then
Output (Head (FIFO), true);
FIFO := tail (FIFO)
else
Output (D,false)
end if
end select
end loop
end var
end process
-- for periodic threads --
process Event_Data_Port_For_Periodic [
Input: LNT_Channel_Event_Data_Port,
Output: LNT_Channel_Event_Data_Port](
Queue_Size: Nat)
is
var
FIFO : LNT_Type_Data_FIFO,
D : LNT_Type_Data
in
FIFO := {};
D := DATA_INIT;
loop
select
Input (?D, true);
if length (FIFO) >= Queue_Size then
FIFO := tail (FIFO)
end if;
FIFO := append (D, FIFO)
[]
if (FIFO != {}) then
Output (Head (FIFO), true);
FIFO := tail (FIFO)
else
Output (D,false)
end if
end select
end loop
end var
end process
end module
resources/runtime/lnt/Makefile.am
0 → 100644
View file @
818f742d
AUTOMAKE_OPTIONS
=
no-dependencies
LNT_FILES
=
$(srcdir)
/LNT_Generic_Process_For_Port_Connections.lnt
\
$(srcdir)
/LNT_Generic_Process_For_Port_Connections_BA.lnt
EXTRA_DIST
=
$(LNT_FILES)
lnt_generic
=
${
shell
$(CYGPATH_U)
'
$(includedir)
/ocarina/runtime/lnt'
}
install-data-local
:
$(INSTALL)
-d
$(DESTDIR)$(lnt_generic)
for
f
in
$(LNT_FILES)
;
do
$(INSTALL)
-m
444
$$
f
$(DESTDIR)$(lnt_generic)
;
done
src/backends/lnt/ocarina-backends-lnt-components.adb
View file @
818f742d
...
...
@@ -756,7 +756,7 @@ package body Ocarina.Backends.Lnt.Components is
(
Defining_Identifier
:
Node_Id
;
Actual_Gates
:
List_Id
:=
No_List
;
Actual_Parameters
:
List_Id
:=
No_List
;
Is_
Spora
dic
:
b
oolean
:=
false
)
Is_
Not_Perio
dic
:
B
oolean
:=
false
)
return
Node_Id
is
pragma
Assert
(
Defining_Identifier
/=
No_Node
);
...
...
@@ -766,7 +766,7 @@ package body Ocarina.Backends.Lnt.Components is
Set_Identifier
(
N
,
Defining_Identifier
);
Set_Actual_Gates
(
N
,
Actual_Gates
);
Set_Actual_Parameters
(
N
,
Actual_Parameters
);
Set_Is_
Spora
dic
(
N
,
Is_
Spora
dic
);
Set_Is_
Not_Perio
dic
(
N
,
Is_
Not_Perio
dic
);
return
N
;
end
Make_Process_Instantiation_Statement
;
...
...
@@ -899,17 +899,21 @@ package body Ocarina.Backends.Lnt.Components is
---------------------------
function
Make_Var_Loop_Select
(
Var_Dec
:
List_Id
;
Out_Loop
:
List_Id
;
In_Select
:
List_Id
)
In_Select
:
List_Id
;
With_Select
:
Boolean
:=
true
)
return
Node_Id
is
N
:
Node_Id
;
N_Loop
:
Node_Id
;
L_Var
:
List_Id
;
begin
L_Var
:=
Out_Loop
;
N_Loop
:=
Make_Loop_Statement
(
New_List
(
Make_Select_Statement
(
In_Select
)));
if
With_Select
then
N_Loop
:=
Make_Loop_Statement
(
New_List
(
Make_Select_Statement
(
In_Select
)));
else
N_Loop
:=
Make_Loop_Statement
(
In_Select
);
end
if
;
Append_Node_To_List
(
N_Loop
,
L_Var
);
N
:=
Make_Var_Statement
(
Var_Dec
,
L_Var
);
return
N
;
end
Make_Var_Loop_Select
;
...
...
src/backends/lnt/ocarina-backends-lnt-components.ads
View file @
818f742d
...
...
@@ -244,7 +244,7 @@ package Ocarina.Backends.Lnt.Components is
(
Defining_Identifier
:
Node_Id
;
Actual_Gates
:
List_Id
:=
No_List
;
Actual_Parameters
:
List_Id
:=
No_List
;
Is_
Spora
dic
:
b
oolean
:=
false
)
Is_
Not_Perio
dic
:
B
oolean
:=
false
)
return
Node_Id
;
function
Make_Communication_Statement
...
...
@@ -290,6 +290,7 @@ package Ocarina.Backends.Lnt.Components is
function
Make_Var_Loop_Select
(
Var_Dec
:
List_Id
;
Out_Loop
:
List_Id
;
In_Select
:
List_Id
)
In_Select
:
List_Id
;
With_Select
:
Boolean
:=
true
)
return
Node_Id
;
end
Ocarina
.
Backends
.
Lnt
.
Components
;
src/backends/lnt/ocarina-backends-lnt-printer.adb
View file @
818f742d
...
...
@@ -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.adb
View file @
818f742d
...
...
@@ -50,7 +50,7 @@ package body Ocarina.Backends.LNT.Tree_Generator is
procedure
Get_N_Thread
(
Sys
:
Node_Id
;
Thread_Number
:
in
out
Natural
;
Spora
dic_Thread_Number
:
in
out
Natural
)
is
Not_Perio
dic_Thread_Number
:
in
out
Natural
)
is
Sys_N
:
Node_Id
;
Proc
:
Node_Id
;
Proc_N
:
Node_Id
;
...
...
@@ -64,7 +64,7 @@ package body Ocarina.Backends.LNT.Tree_Generator is
if
Get_Category_Of_Component
(
Proc
)
=
CC_System
then
Get_N_Thread
(
Proc
,
Thread_Number
,
Spora
dic_Thread_Number
);
Not_Perio
dic_Thread_Number
);
end
if
;
if
Get_Category_Of_Component
(
Proc
)
=
CC_Process
then
if
not
AINU
.
Is_Empty
(
Subcomponents
(
Proc
))
then
...
...
@@ -73,11 +73,11 @@ package body Ocarina.Backends.LNT.Tree_Generator is
Thr
:=
Corresponding_Instance
(
Proc_N
);
if
Get_Category_Of_Component
(
Thr
)
=
CC_Thread
then
Thread_Number
:=
Thread_Number
+
1
;
if
(
Get_Thread_Dispatch_Protocol
(
Thr
)
=
Thread_
Spora
dic
)
if
(
Get_Thread_Dispatch_Protocol
(
Thr
)
/=
Thread_
Perio
dic
)
then
Spora
dic_Thread_Number
:=
Spora
dic_Thread_Number
+
1
;
Not_Perio
dic_Thread_Number
:=
Not_Perio
dic_Thread_Number
+
1
;
end
if
;
end
if
;
Proc_N
:=
AIN
.
Next_Node
(
Proc_N
);
...
...
src/backends/lnt/ocarina-backends-lnt-tree_generator.ads
View file @
818f742d
...
...
@@ -33,6 +33,6 @@ package Ocarina.Backends.LNT.Tree_Generator is
procedure
Get_N_Thread
(
Sys
:
Node_Id
;
Thread_Number
:
in
out
Natural
;
Spora
dic_Thread_Number
:
in
out
Natural
);
Not_Perio
dic_Thread_Number
:
in
out
Natural
);
end
Ocarina
.
Backends
.
LNT
.
Tree_Generator
;
src/backends/lnt/ocarina-backends-lnt-tree_generator_main.adb
View file @
818f742d
...
...
@@ -74,36 +74,13 @@ package body Ocarina.Backends.LNT.Tree_Generator_Main is
procedure
Visit_Thread_Instance
(
E
:
Node_Id
);
procedure
Visit_Device_Instance
(
E
:
Node_Id
);
function
Build_Name_From_Path
(
Path
:
List_Id
)
return
Name_Id
;
procedure
Find_Instance_By_Name
(
Key
:
Name_Id
;
Target
:
List_Id
;
Instance
:
out
Node_Id
;
Index
:
out
Natural
;
Is_Sporadic
:
out
boolean
);
function
Is_Sporadic
(
Index
:
Natural
;
Target
:
List_Id
)
return
boolean
;
Is_Not_Periodic
:
out
boolean
);
procedure
Make_Process_Main
;
function
Make_Gate_Identifier
(
S
:
Node_Id
)
return
Name_Id
;
function
Build_Name_From_Path
(
Path
:
List_Id
)
return
Name_Id
is
N
:
Node_Id
:=
AIN
.
First_Node
(
Path
);
First
:
Boolean
:=
True
;
begin
Set_Str_To_Name_Buffer
(
""
);
while
Present
(
N
)
loop
if
First
then
First
:=
False
;
else
Add_Str_To_Name_Buffer
(
"_"
);
end
if
;
Get_Name_String_And_Append
(
AIN
.
Name
(
AIN
.
Identifier
(
AIN
.
Item
(
N
))));
N
:=
AIN
.
Next_Node
(
N
);
end
loop
;
return
Name_Find
;
end
Build_Name_From_Path
;
function
Make_Gate_Identifier
(
S
:
Node_Id
)
return
Name_Id
is
N_Connection
:
Node_Id
;
L
:
List_Id
;
...
...
@@ -113,47 +90,40 @@ package body Ocarina.Backends.LNT.Tree_Generator_Main is
-- port_in thread
L
:=
Sources
(
S
);
-- port_out thread, first connection 1-1
N_Connection
:=
AIN
.
Item
(
AIN
.
First_Node
(
L
));
while
(
AIN
.
Is_In
(
N_Connection
))
loop
L
:=
Sources
(
N_Connection
);
if
Present
(
AIN
.
First_Node
(
L
))
then
N_Connection
:=
AIN
.
Item
(
AIN
.
First_Node
(
L
));
end
loop
;
N_Connection
:=
AIN
.
Extra_Item
(
AIN
.
First_Node
(
L
));
-- connection Path system
Connection
:=
Add_Prefix_To_Name
(
"RECEIVE_"
,
Build_Name_From_Path
(
Path
(
Source
(
N_Connection
))));
Connection
:=
Add_Suffix_To_Name
(
"__"
,
Connection
);
Connection
:=
Add_Suffix_To_Name
(
Get_Name_String
(
Build_Name_From_Path
(
Path
(
Destination
(
N_Connection
)))),
Connection
);
while
(
AIN
.
Is_In
(
N_Connection
))
loop
L
:=
Sources
(
N_Connection
);
if
Present
(
AIN
.
First_Node
(
L
))
then
N_Connection
:=
AIN
.
Item
(
AIN
.
First_Node
(
L
));
end
if
;
end
loop
;
N_Connection
:=
AIN
.
Extra_Item
(
AIN
.
First_Node
(
L
));
-- connection identifier at system level
Connection
:=
Add_Prefix_To_Name
(
"RECEIVE_"
,
AIN
.
Display_Name
(
AIN
.
Identifier
(
N_Connection
)));
end
if
;
elsif
(
AIN
.
Is_Out
(
S
))
then
-- port_in thread
L
:=
Destinations
(
S
);
-- port_out thread, first connection 1-1
N_Connection
:=
AIN
.
Item
(
AIN
.
First_Node
(
L
));
while
(
AIN
.
Is_Out
(
N_Connection
))
loop
-- port_out process
L
:=
Destinations
(
N_Connection
);
if
Present
(
AIN
.
First_Node
(
L
))
then
N_Connection
:=
AIN
.
Item
(
AIN
.
First_Node
(
L
));
end
loop
;
-- connection instance system/process
N_Connection
:=
AIN
.
Extra_Item
(
AIN
.
First_Node
(
L
));
Connection
:=
Add_Prefix_To_Name
(
"SEND_"
,
Build_Name_From_Path
(
Path
(
Source
(
N_Connection
))));
Connection
:=
Add_Suffix_To_Name
(
"__"
,
Connection
);
Connection
:=
Add_Suffix_To_Name
(
Get_Name_String
(
Build_Name_From_Path
(
Path
(
Destination
(
N_Connection
)))),
Connection
);
while
(
AIN
.
Is_Out
(
N_Connection
))
loop
-- port_out process
L
:=
Destinations
(
N_Connection
);
if
Present
(
AIN
.
First_Node
(
L
))
then
N_Connection
:=
AIN
.
Item
(
AIN
.
First_Node
(
L
));
end
if
;
end
loop
;
-- connection instance system/process
N_Connection
:=
AIN
.
Extra_Item
(
AIN
.
First_Node
(
L
));
Connection
:=
Add_Prefix_To_Name
(
"SEND_"
,
AIN
.
Display_Name
(
AIN
.
Identifier
(
N_Connection
)));
end
if
;
end
if
;
return
Connection
;
end
Make_Gate_Identifier
;
...
...
@@ -167,6 +137,8 @@ package body Ocarina.Backends.LNT.Tree_Generator_Main is
-- Main_Hide_Declaration_List : List_Id := No_List;
Main_Gate_Declaration_List
:
List_Id
:=
No_List
;
Processor_Gates_List
:
List_Id
:=
No_List
;
Processor_Event_Gates_List
:
List_Id
:=
No_List
;
Processor_Event_Gate_Declaration_List
:
List_Id
:=
No_List
;
Main_Interface_Synchronisation_List
:
List_Id
:=
No_List
;
function
Generate_LNT_Main
(
AADL_Tree
:
Node_Id
)
...
...
@@ -176,6 +148,9 @@ package body Ocarina.Backends.LNT.Tree_Generator_Main is
Processor_Gates_List
:=
New_List
;
Main_Gate_Declaration_List
:=
New_List
;
Main_Interface_Synchronisation_List
:=
New_List
;
Processor_Event_Gate_Declaration_List
:=
New_List
;
Processor_Event_Gates_List
:=
New_List
;
LNT_Processor_Gate_Declaration_List
:=
New_List
;
Visit
(
AADL_Tree
);
return
Module_Node
;
end
Generate_LNT_Main
;
...
...
@@ -214,18 +189,24 @@ package body Ocarina.Backends.LNT.Tree_Generator_Main is
end
if
;
Definitions_List
:=
New_List
;
Modules_List
:=
New_List
(
New_Identifier
(
Get_String_Name
(
"_Types"
),
Get_Name_String
(
System_Name
)),
Make_Identifier
(
"Types"
),
New_Identifier
(
Get_String_Name
(
"_Processor"
),
Get_Name_String
(
System_Name
)),
New_Identifier
(
Get_String_Name
(
"_Threads"
),
Get_Name_String
(
System_Name
)),
New_Identifier
(
Get_String_Name
(
"_Ports"
),
Get_Name_String
(
System_Name
)));
if
BLNu
.
Is_Empty
(
LNT_States_List
)
then
BLNu
.
Append_Node_To_List
(
Make_Identifier
(
"LNT_Generic_Process_For_Port_Connections"
),
Modules_List
);
else
BLNu
.
Append_Node_To_List
(
Make_Identifier
(
"LNT_Generic_Process_For_Port_Connections_BA"
),
Modules_List
);
end
if
;
Predefined_Functions_List
:=
New_List
;
Visit
(
N
);
...
...
@@ -272,7 +253,6 @@ package body Ocarina.Backends.LNT.Tree_Generator_Main is
S
:=
AIN
.
Next_Node
(
S
);
end
loop
;
end
if
;
end
Visit_System_Instance
;
----------------------------
...
...
@@ -340,7 +320,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
);
...
...
@@ -353,8 +333,8 @@ package body Ocarina.Backends.LNT.Tree_Generator_Main is
-- port
Port_Gates_List
:=
New_List
(
Aux_N_Port_2
,
-- RECEIVE
_
Make_Identifier
(
N_SEND
)
);
--
SEND
_
Make_Identifier
(
N_SEND
),
-- SEND
_
Aux_N_Port_2
);
--
RECEIVE
_
N_Port
:=
Make_Process_Instantiation_Statement
(
Make_Identifier
(
"Data_Port"
),
...
...
@@ -440,16 +420,20 @@ package body Ocarina.Backends.LNT.Tree_Generator_Main is
S
:
Node_Id
;
Ni
:
Node_Id
;
P
:
Node_Id
;
Event_Number
:
Natural
:=
0
;