Commit 61048977 authored by yoogx's avatar yoogx
Browse files

* Change output of Petri Nets to files instead of standard

          output.

          Update reference output accordingly.
parent 4e12737a
This diff is collapsed.
...@@ -31,6 +31,8 @@ ...@@ -31,6 +31,8 @@
-- -- -- --
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
with GNAT.OS_Lib; use GNAT.OS_Lib;
with Namet; with Namet;
with Ocarina.Backends.Expander; with Ocarina.Backends.Expander;
...@@ -69,18 +71,9 @@ package body Ocarina.Backends.PN is ...@@ -69,18 +71,9 @@ package body Ocarina.Backends.PN is
------------------- -------------------
procedure Generate_TINA (AADL_Root : Types.Node_Id) is procedure Generate_TINA (AADL_Root : Types.Node_Id) is
Pn_Generated, Instance_Root : Node_Id; PN_Generated, Instance_Root : Node_Id;
pragma Warnings (Off, Pn_Generated);
begin begin
Write_Line ("------------------------------------------");
Write_Line ("------ Ocarina Petri Nets Generator ------");
Write_Line ("------------------------------------------");
Write_Line (" ");
-----------
-- work for TPN generation
-- Instantiate the AADL tree -- Instantiate the AADL tree
Instance_Root := Instantiate_Model (AADL_Root); Instance_Root := Instantiate_Model (AADL_Root);
...@@ -89,20 +82,19 @@ package body Ocarina.Backends.PN is ...@@ -89,20 +82,19 @@ package body Ocarina.Backends.PN is
Expand (Instance_Root); Expand (Instance_Root);
if Instance_Root /= No_Node then if Present (Instance_Root) then
Pn_Generated := Process_Architecture_Instance (Instance_Root, 1); -- Generate Petri Net
else
Pn_Generated := No_Node;
end if;
if Pn_Generated /= No_Node then PN_Generated := Process_Architecture_Instance (Instance_Root, 1);
-- Set TINA printers
Set_Printers (OPFT.Print_Place'Access, Set_Printers (OPFT.Print_Place'Access,
OPFT.Print_Trans'Access, OPFT.Print_Trans'Access,
OPFT.Print_Formalism_Information'Access); OPFT.Print_Formalism_Information'Access);
Write_Line ("~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~");
Write_Line ("~~~~~~~~~~~ Timed Petri Nets ~~~~~~~~~~~"); Set_Output (Create_File ("model.nd", Binary));
Write_Line ("~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~"); Print_PN_Generated (PN_Generated);
Print_Pn_Generated (Pn_Generated); Set_Standard_Error;
end if; end if;
end Generate_TINA; end Generate_TINA;
...@@ -111,13 +103,9 @@ package body Ocarina.Backends.PN is ...@@ -111,13 +103,9 @@ package body Ocarina.Backends.PN is
------------------- -------------------
procedure Generate_CAMI (AADL_Root : Types.Node_Id) is procedure Generate_CAMI (AADL_Root : Types.Node_Id) is
Pn_Generated, Instance_Root : Node_Id; PN_Generated, Instance_Root : Node_Id;
pragma Warnings (Off, Pn_Generated);
begin begin
-----------
-- work for CPN generation
-- Instantiate the AADL tree -- Instantiate the AADL tree
Instance_Root := Instantiate_Model (AADL_Root); Instance_Root := Instantiate_Model (AADL_Root);
...@@ -127,19 +115,13 @@ package body Ocarina.Backends.PN is ...@@ -127,19 +115,13 @@ package body Ocarina.Backends.PN is
Expand (Instance_Root); Expand (Instance_Root);
if Instance_Root /= No_Node then if Instance_Root /= No_Node then
Pn_Generated := Process_Architecture_Instance (Instance_Root, 0); PN_Generated := Process_Architecture_Instance (Instance_Root, 0);
else
Pn_Generated := No_Node;
end if;
if Pn_Generated /= No_Node then
Set_Printers (OPFC.Print_Place'Access, Set_Printers (OPFC.Print_Place'Access,
OPFC.Print_Trans'Access, OPFC.Print_Trans'Access,
OPFC.Print_Formalism_Information'Access); OPFC.Print_Formalism_Information'Access);
Write_Line ("~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~"); Set_Output (Create_File ("model.cami", Binary));
Write_Line ("~~~~~~~~~~~ Colored Petri Nets ~~~~~~~~~~~"); Print_PN_Generated (PN_Generated);
Write_Line ("~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~"); Set_Standard_Error;
Print_Pn_Generated (Pn_Generated);
end if; end if;
end Generate_CAMI; end Generate_CAMI;
......
------------------------------------------
------ Ocarina Petri Nets Generator ------
------------------------------------------
test.aadl:12:03: warning: CPU references a component type test.aadl:12:03: warning: CPU references a component type
ocarina: Total: 0 error and 1 warning ocarina: Total: 0 error and 1 warning
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
~~~~~~~~~~~ Timed Petri Nets ~~~~~~~~~~~
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
net AADL_TO_TPN_GENERATED
tr pr_A_Producer_Init_Dispatch [0,w[ pr_A_Producer_Halted pr_A_Result_Consumer_Halted pr_B_Consumer_Halted pr_B_Result_Producer_Halted -> pr_A_Producer_Wait_For_Dispatch pr_A_Result_Consumer_Wait_For_Dispatch pr_B_Consumer_Wait_For_Dispatch pr_B_Result_Producer_Wait_For_Dispatch
tr pr_A_Producer_Period_Event [20,20] pr_A_Producer_Hyperperiod -> pr_A_Producer_Clock
pl pr_A_Producer_Halted (1)
pl pr_A_Producer_Wait_For_Dispatch (0)
pl pr_A_Producer_Hyperperiod (1)
pl pr_A_Producer_Clock (0)
tr pr_A_Producer_Begin [0,w[ CPU_Processor pr_A_Producer_Clock pr_A_Producer_Wait_For_Dispatch -> pr_A_Producer_Work1
tr pr_A_Producer_End [0,w[ pr_A_Producer_Work2 -> CPU_Processor pr_A_Producer_Data_Sourcepr_A_Producer__Store_Port pr_A_Producer_Wait_For_Dispatch
tr pr_A_Producer_Preemp1 [0,w[ pr_A_Producer_Work1 -> pr_A_Producer_ContextSwitch CPU_Processor
tr pr_A_Producer_Preemp2 [0,w[ pr_A_Producer_ContextSwitch CPU_Processor -> pr_A_Producer_Work2
pl pr_A_Producer_Work1 (0)
pl pr_A_Producer_Work2 (0)
pl pr_A_Producer_ContextSwitch (0)
tr pr_A_Producer_Data_Sourcepr_A_Producer__Pop_Port [0,w[ pr_A_Producer_Data_Sourcepr_A_Producer__Store_Port -> pr_A_Producer_Data_Source_Bus
pl pr_A_Producer_Data_Sourcepr_A_Producer__Store_Port (0)
tr pr_A_Result_Consumer_Period_Event [20,20] pr_A_Result_Consumer_Hyperperiod -> pr_A_Result_Consumer_Clock
pl pr_A_Result_Consumer_Halted (1)
pl pr_A_Result_Consumer_Wait_For_Dispatch (0)
pl pr_A_Result_Consumer_Hyperperiod (1)
pl pr_A_Result_Consumer_Clock (0)
tr pr_A_Result_Consumer_Begin [0,w[ CPU_Processor pr_A_Result_Consumer_Data_Sinkpr_A_Result_Consumer__Store_Port pr_A_Result_Consumer_Clock pr_A_Result_Consumer_Wait_For_Dispatch -> pr_A_Result_Consumer_Work1 pr_A_Result_Consumer_Data_Sinkpr_A_Result_Consumer__Store_Port
tr pr_A_Result_Consumer_End [0,w[ pr_A_Result_Consumer_Work2 -> CPU_Processor pr_A_Result_Consumer_Wait_For_Dispatch
tr pr_A_Result_Consumer_Preemp1 [0,w[ pr_A_Result_Consumer_Work1 -> pr_A_Result_Consumer_ContextSwitch CPU_Processor
tr pr_A_Result_Consumer_Preemp2 [0,w[ pr_A_Result_Consumer_ContextSwitch CPU_Processor -> pr_A_Result_Consumer_Work2
pl pr_A_Result_Consumer_Work1 (0)
pl pr_A_Result_Consumer_Work2 (0)
pl pr_A_Result_Consumer_ContextSwitch (0)
tr pr_A_Result_Consumer_Data_Sinkpr_A_Result_Consumer__Push_Port [0,w[ pr_A_Result_Consumer_Data_Sinkpr_A_Result_Consumer__Store_Port pr_B_Result_Producer_Data_Source_Bus -> pr_A_Result_Consumer_Data_Sinkpr_A_Result_Consumer__Store_Port
pl pr_A_Result_Consumer_Data_Sinkpr_A_Result_Consumer__Store_Port (1)
tr pr_B_Consumer_Period_Event [20,20] pr_B_Consumer_Hyperperiod -> pr_B_Consumer_Clock
pl pr_B_Consumer_Halted (1)
pl pr_B_Consumer_Wait_For_Dispatch (0)
pl pr_B_Consumer_Hyperperiod (1)
pl pr_B_Consumer_Clock (0)
tr pr_B_Consumer_Begin [0,w[ CPU_Processor pr_B_Consumer_Data_Sinkpr_B_Consumer__Store_Port pr_B_Consumer_Clock pr_B_Consumer_Wait_For_Dispatch -> pr_B_Consumer_Work1 pr_B_Consumer_Data_Sinkpr_B_Consumer__Store_Port
tr pr_B_Consumer_End [0,w[ pr_B_Consumer_Work2 -> CPU_Processor pr_B_Consumer_Wait_For_Dispatch
tr pr_B_Consumer_Preemp1 [0,w[ pr_B_Consumer_Work1 -> pr_B_Consumer_ContextSwitch CPU_Processor
tr pr_B_Consumer_Preemp2 [0,w[ pr_B_Consumer_ContextSwitch CPU_Processor -> pr_B_Consumer_Work2
pl pr_B_Consumer_Work1 (0)
pl pr_B_Consumer_Work2 (0)
pl pr_B_Consumer_ContextSwitch (0)
tr pr_B_Consumer_Data_Sinkpr_B_Consumer__Push_Port [0,w[ pr_B_Consumer_Data_Sinkpr_B_Consumer__Store_Port pr_A_Producer_Data_Source_Bus -> pr_B_Consumer_Data_Sinkpr_B_Consumer__Store_Port
pl pr_B_Consumer_Data_Sinkpr_B_Consumer__Store_Port (1)
tr pr_B_Result_Producer_Period_Event [20,20] pr_B_Result_Producer_Hyperperiod -> pr_B_Result_Producer_Clock
pl pr_B_Result_Producer_Halted (1)
pl pr_B_Result_Producer_Wait_For_Dispatch (0)
pl pr_B_Result_Producer_Hyperperiod (1)
pl pr_B_Result_Producer_Clock (0)
tr pr_B_Result_Producer_Begin [0,w[ CPU_Processor pr_B_Result_Producer_Clock pr_B_Result_Producer_Wait_For_Dispatch -> pr_B_Result_Producer_Work1
tr pr_B_Result_Producer_End [0,w[ pr_B_Result_Producer_Work2 -> CPU_Processor pr_B_Result_Producer_Data_Sourcepr_B_Result_Producer__Store_Port pr_B_Result_Producer_Wait_For_Dispatch
tr pr_B_Result_Producer_Preemp1 [0,w[ pr_B_Result_Producer_Work1 -> pr_B_Result_Producer_ContextSwitch CPU_Processor
tr pr_B_Result_Producer_Preemp2 [0,w[ pr_B_Result_Producer_ContextSwitch CPU_Processor -> pr_B_Result_Producer_Work2
pl pr_B_Result_Producer_Work1 (0)
pl pr_B_Result_Producer_Work2 (0)
pl pr_B_Result_Producer_ContextSwitch (0)
tr pr_B_Result_Producer_Data_Sourcepr_B_Result_Producer__Pop_Port [0,w[ pr_B_Result_Producer_Data_Sourcepr_B_Result_Producer__Store_Port -> pr_B_Result_Producer_Data_Source_Bus
pl pr_B_Result_Producer_Data_Sourcepr_B_Result_Producer__Store_Port (0)
pl CPU_Processor (1)
pl pr_A_Producer_Data_Source_Bus (0)
pl pr_B_Result_Producer_Data_Source_Bus (0)
test.aadl:12:03: warning: CPU references a component type test.aadl:12:03: warning: CPU references a component type
ocarina: Total: 0 error and 1 warning ocarina: Total: 0 error and 1 warning
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
~~~~~~~~~~~ Colored Petri Nets ~~~~~~~~~~~
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
CN(3:net,1)
CM(11:declaration,1,1,1,5:Class)
CM(11:declaration,1,2,1,20:Threads_Ids is 0..4;)
CM(11:declaration,1,3,1,19:Msg_Types is [msg];)
CM(11:declaration,1,4,1,6:Domain)
CM(11:declaration,1,5,1,32:mess is <Threads_Ids,Msg_Types>;)
CM(11:declaration,1,6,1,3:Var)
CM(11:declaration,1,7,1,45: x, y, x361, x405, x488, x532 in Threads_Ids;)
CM(11:declaration,1,8,1,16: m in Msg_Types;)
CN(10:transition,739)
CT(4:name,739,27:pr_A_Producer_Init_Dispatch)
CA(3:arc,744,731,739)
CT(9:valuation,744,6:<x361>)
CA(3:arc,1587,910,739)
CT(9:valuation,1587,6:<x405>)
CA(3:arc,1607,1129,739)
CT(9:valuation,1607,6:<x488>)
CA(3:arc,1627,1348,739)
CT(9:valuation,1627,6:<x532>)
CA(3:arc,749,739,735)
CT(9:valuation,749,6:<x361>)
CA(3:arc,1592,739,914)
CT(9:valuation,1592,6:<x405>)
CA(3:arc,1612,739,1133)
CT(9:valuation,1612,6:<x488>)
CA(3:arc,1632,739,1352)
CT(9:valuation,1632,6:<x532>)
CN(5:place,731)
CT(4:name,731,20:pr_A_Producer_Halted)
CT(6:domain,731,11:Threads_Ids)
CT(7:marking,731,3:<1>)
CN(5:place,735)
CT(4:name,735,31:pr_A_Producer_Wait_For_Dispatch)
CT(6:domain,735,11:Threads_Ids)
CN(10:transition,819)
CT(4:name,819,19:pr_A_Producer_Begin)
CA(3:arc,1519,735,819)
CT(9:valuation,1519,3:<x>)
CA(3:arc,851,819,839)
CT(9:valuation,851,3:<x>)
CN(10:transition,829)
CT(4:name,829,21:pr_A_Producer_Preemp1)
CA(3:arc,856,839,829)
CT(9:valuation,856,3:<x>)
CA(3:arc,861,829,847)
CT(9:valuation,861,3:<x>)
CN(10:transition,834)
CT(4:name,834,21:pr_A_Producer_Preemp2)
CA(3:arc,866,847,834)
CT(9:valuation,866,3:<x>)
CA(3:arc,871,834,843)
CT(9:valuation,871,3:<x>)
CN(5:place,839)
CT(4:name,839,19:pr_A_Producer_Work1)
CT(6:domain,839,11:Threads_Ids)
CN(5:place,843)
CT(4:name,843,19:pr_A_Producer_Work2)
CT(6:domain,843,11:Threads_Ids)
CN(5:place,847)
CT(4:name,847,27:pr_A_Producer_ContextSwitch)
CT(6:domain,847,11:Threads_Ids)
CN(5:place,910)
CT(4:name,910,27:pr_A_Result_Consumer_Halted)
CT(6:domain,910,11:Threads_Ids)
CT(7:marking,910,3:<2>)
CN(5:place,914)
CT(4:name,914,38:pr_A_Result_Consumer_Wait_For_Dispatch)
CT(6:domain,914,11:Threads_Ids)
CN(10:transition,1002)
CT(4:name,1002,26:pr_A_Result_Consumer_Begin)
CA(3:arc,1533,1085,1002)
CT(9:valuation,1533,5:<y,m>)
CA(3:arc,1543,914,1002)
CT(9:valuation,1543,3:<x>)
CA(3:arc,1034,1002,1022)
CT(9:valuation,1034,3:<x>)
CA(3:arc,1538,1002,1085)
CT(9:valuation,1538,5:<y,m>)
CN(10:transition,1007)
CT(4:name,1007,24:pr_A_Result_Consumer_End)
CA(3:arc,1059,1026,1007)
CT(9:valuation,1059,3:<x>)
CA(3:arc,1548,1007,914)
CT(9:valuation,1548,3:<x>)
CN(10:transition,1012)
CT(4:name,1012,28:pr_A_Result_Consumer_Preemp1)
CA(3:arc,1039,1022,1012)
CT(9:valuation,1039,3:<x>)
CA(3:arc,1044,1012,1030)
CT(9:valuation,1044,3:<x>)
CN(10:transition,1017)
CT(4:name,1017,28:pr_A_Result_Consumer_Preemp2)
CA(3:arc,1049,1030,1017)
CT(9:valuation,1049,3:<x>)
CA(3:arc,1054,1017,1026)
CT(9:valuation,1054,3:<x>)
CN(5:place,1022)
CT(4:name,1022,26:pr_A_Result_Consumer_Work1)
CT(6:domain,1022,11:Threads_Ids)
CN(5:place,1026)
CT(4:name,1026,26:pr_A_Result_Consumer_Work2)
CT(6:domain,1026,11:Threads_Ids)
CN(5:place,1030)
CT(4:name,1030,34:pr_A_Result_Consumer_ContextSwitch)
CT(6:domain,1030,11:Threads_Ids)
CN(10:transition,1075)
CT(4:name,1075,60:pr_A_Result_Consumer_Data_Sinkpr_A_Result_Consumer_Push_Port)
CA(3:arc,1107,1085,1075)
CT(9:valuation,1107,5:<y,m>)
CA(3:arc,1597,1460,1075)
CT(9:valuation,1597,3:<x>)
CA(3:arc,1093,1075,1085)
CT(9:valuation,1093,7:<x,msg>)
CA(3:arc,1602,1075,1352)
CT(9:valuation,1602,3:<x>)
CN(5:place,1085)
CT(4:name,1085,62:pr_A_Result_Consumer_Data_Sinkpr_A_Result_Consumer__Store_Port)
CT(6:domain,1085,4:mess)
CT(7:marking,1085,8:<data,0>)
CN(5:place,1129)
CT(4:name,1129,20:pr_B_Consumer_Halted)
CT(6:domain,1129,11:Threads_Ids)
CT(7:marking,1129,3:<3>)
CN(5:place,1133)
CT(4:name,1133,31:pr_B_Consumer_Wait_For_Dispatch)
CT(6:domain,1133,11:Threads_Ids)
CN(10:transition,1221)
CT(4:name,1221,19:pr_B_Consumer_Begin)
CA(3:arc,1553,1304,1221)
CT(9:valuation,1553,5:<y,m>)
CA(3:arc,1563,1133,1221)
CT(9:valuation,1563,3:<x>)
CA(3:arc,1253,1221,1241)
CT(9:valuation,1253,3:<x>)
CA(3:arc,1558,1221,1304)
CT(9:valuation,1558,5:<y,m>)
CN(10:transition,1226)
CT(4:name,1226,17:pr_B_Consumer_End)
CA(3:arc,1278,1245,1226)
CT(9:valuation,1278,3:<x>)
CA(3:arc,1568,1226,1133)
CT(9:valuation,1568,3:<x>)
CN(10:transition,1231)
CT(4:name,1231,21:pr_B_Consumer_Preemp1)
CA(3:arc,1258,1241,1231)
CT(9:valuation,1258,3:<x>)
CA(3:arc,1263,1231,1249)
CT(9:valuation,1263,3:<x>)
CN(10:transition,1236)
CT(4:name,1236,21:pr_B_Consumer_Preemp2)
CA(3:arc,1268,1249,1236)
CT(9:valuation,1268,3:<x>)
CA(3:arc,1273,1236,1245)
CT(9:valuation,1273,3:<x>)
CN(5:place,1241)
CT(4:name,1241,19:pr_B_Consumer_Work1)
CT(6:domain,1241,11:Threads_Ids)
CN(5:place,1245)
CT(4:name,1245,19:pr_B_Consumer_Work2)
CT(6:domain,1245,11:Threads_Ids)
CN(5:place,1249)
CT(4:name,1249,27:pr_B_Consumer_ContextSwitch)
CT(6:domain,1249,11:Threads_Ids)
CN(10:transition,1294)
CT(4:name,1294,46:pr_B_Consumer_Data_Sinkpr_B_Consumer_Push_Port)
CA(3:arc,1326,1304,1294)
CT(9:valuation,1326,5:<y,m>)
CA(3:arc,1617,843,1294)
CT(9:valuation,1617,3:<x>)
CA(3:arc,1312,1294,1304)
CT(9:valuation,1312,7:<x,msg>)
CA(3:arc,1622,1294,735)
CT(9:valuation,1622,3:<x>)
CN(5:place,1304)
CT(4:name,1304,48:pr_B_Consumer_Data_Sinkpr_B_Consumer__Store_Port)
CT(6:domain,1304,4:mess)
CT(7:marking,1304,8:<data,0>)
CN(5:place,1348)
CT(4:name,1348,27:pr_B_Result_Producer_Halted)
CT(6:domain,1348,11:Threads_Ids)
CT(7:marking,1348,3:<4>)
CN(5:place,1352)
CT(4:name,1352,38:pr_B_Result_Producer_Wait_For_Dispatch)
CT(6:domain,1352,11:Threads_Ids)
CN(10:transition,1436)
CT(4:name,1436,26:pr_B_Result_Producer_Begin)
CA(3:arc,1573,1352,1436)
CT(9:valuation,1573,3:<x>)
CA(3:arc,1468,1436,1456)
CT(9:valuation,1468,3:<x>)
CN(10:transition,1446)
CT(4:name,1446,28:pr_B_Result_Producer_Preemp1)
CA(3:arc,1473,1456,1446)
CT(9:valuation,1473,3:<x>)
CA(3:arc,1478,1446,1464)
CT(9:valuation,1478,3:<x>)
CN(10:transition,1451)
CT(4:name,1451,28:pr_B_Result_Producer_Preemp2)
CA(3:arc,1483,1464,1451)
CT(9:valuation,1483,3:<x>)
CA(3:arc,1488,1451,1460)
CT(9:valuation,1488,3:<x>)
CN(5:place,1456)
CT(4:name,1456,26:pr_B_Result_Producer_Work1)
CT(6:domain,1456,11:Threads_Ids)
CN(5:place,1460)
CT(4:name,1460,26:pr_B_Result_Producer_Work2)
CT(6:domain,1460,11:Threads_Ids)
CN(5:place,1464)
CT(4:name,1464,34:pr_B_Result_Producer_ContextSwitch)
CT(6:domain,1464,11:Threads_Ids)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment