Skip to content

GitLab

Commits (5)
Hide whitespace changes
Inline Side-by-side
templates/concurrency_view/aadl_4_makefile/node.tmplt
View file @ 23565c8c
......@@ -27,6 +27,13 @@
TASTE_IV_Properties.aadl TASTE_DV_Properties.aadl \
taste_properties.aadl base_types.aadl \
../dataview/dataview_aadlv2.aadl ../../InterfaceView.aadl ../../DeploymentView.aadl \
@@INLINE@@
@@TABLE@@
@@IF@@ @_VP_Platforms_@ = PLATFORM_AIR_IOP
/home/taste/tool-inst/share/SharedTypes/air_device/air_device-iv-air_device.aadl \
@@END_IF@@
@@END_TABLE@@
@@END_INLINE@@
../../../common/ocarina_components.aadl && \
cd deploymentview_final && rm -f Makefile && (configure --keep-files-silent)
@echo "XML generated, AIR configuration done, building..."
......
templates/concurrency_view/c_pohi_gpr/node.tmplt
View file @ 23565c8c
......@@ -57,7 +57,7 @@ release:
@@TABLE@@
gprbuild -c -p --config=@_LOWER:Partition_Names_@_air.cgpr -P @_LOWER:Partition_Names_@_air.gpr -XCFG="Release" -cargs:C -DSTATIC=""
cp ../deploymentview_final/@_LOWER:Partition_Names_@/linkcmds.inc @_LOWER:Partition_Names_@_obj/
gprbuild -l -p --config=air.cgpr -P @_LOWER:Partition_Names_@_air.gpr -XCFG="Release" -cargs:C -DSTATIC=""
gprbuild -l -p --config=@_LOWER:Partition_Names_@_air.cgpr -P @_LOWER:Partition_Names_@_air.gpr -XCFG="Release" -cargs:C -DSTATIC=""
@@END_TABLE@@
@@ELSIF@@ @_CPU_Platform_@ = PLATFORM_ZYNQZC706
......
templates/concurrency_view/simulation-adb/node.tmplt
View file @ 23565c8c
......@@ -7,15 +7,17 @@ with Text_IO; use Text_IO;
with Ada.Calendar; use Ada.Calendar; -- Time / Clock
with Ada.Containers; use Ada.Containers; -- Hash_Type
with Simulator;
@@TABLE@@
with @_CAPITALIZE:Block_Names_@_Events;
@@END_TABLE@@
with ASN1_GSER;
use ASN1_GSER;
-- with ASN1_GSER;
-- use ASN1_GSER;
package body Simulator_Interface is
use Simulation_Dataview;
-- use Simulation_Dataview;
procedure Simulation_Startup
(Check_Properties : Check_Properties_Access)
......@@ -28,12 +30,14 @@ package body Simulator_Interface is
begin
User_Check_Properties := Check_Properties;
Text_IO.Put_Line ("Simulation startup");
Simulator.State := asn1SccSystem_State_Init;
ES.Backup_Ctxt := Simulator.State;
ES.Backup_Hash := ES.State_Hash (Simulator.State);
Full_State := Full_State_Init;
ES.Backup_Ctxt := Full_State;
ES.Backup_Hash := ES.State_Hash (Full_State);
User_State := Application_State (Full_State);
@@TABLE'ALIGN_ON(" ")@@
@_CAPITALIZE:Block_Names_@_Events.Startup (Simulator.State);
@_CAPITALIZE:Block_Names_@_Events.Startup (User_State);
@@END_TABLE@@
Update_State (Full_State, User_State);
-- Initialize the state graph with the startup event
ES.Start_Hash := ES.Add_To_Graph (Startup_Event, User_Check_Properties);
ES.Queue.Append (ES.Start_Hash);
......@@ -50,7 +54,8 @@ package body Simulator_Interface is
return;
end if;
while ES.Queue.Length > 0 and ES.Properties.Length < 10 loop
Simulator.State :=
-- Simulator.State :=
Full_State :=
ES.Grafset.Element (Key => ES.Queue.Last_Element).Context;
-- Put_Line ("Restored: " & System_State_Pkg.Image (Simulator.State));
ES.Queue.Delete_Last;
......@@ -68,10 +73,11 @@ package body Simulator_Interface is
procedure Execute_Next_Event is
Event : asn1SccEvent := Simulator.Pop_Event;
begin
User_State := Application_State (Full_state);
case Event.Kind is
when System_Startup_PRESENT => null;
@@TABLE'ALIGN_ON("=>", "(", "Global")@@
when @_CAPITALIZE:Block_Names_@_PRESENT => @_CAPITALIZE:Block_Names_@_Events.Process_Event (Event => Event.@_CAPITALIZE:Block_Names_@, Global_State => Simulator.State);
when @_CAPITALIZE:Block_Names_@_PRESENT => @_CAPITALIZE:Block_Names_@_Events.Process_Event (Event => Event.@_CAPITALIZE:Block_Names_@, Global_State => User_State);
@@END_TABLE@@
end case;
end Execute_Next_Event;
......@@ -81,11 +87,15 @@ package body Simulator_Interface is
-- Called at each PI invocation to add to the state graph and verify properties
S_Hash : Hash_Type;
begin
--
-- First empty the stack of events that were generated during the call
while Simulator.State.Events.Length > 0 loop
while Simulator.Events.Length > 0 loop
Execute_Next_Event;
end loop;
-- User code modified the application state -> place it in the full state
Update_State (Full_State, User_State);
-- Put_Line ("Number of states before Add_To_Graph: " & ES.Grafset.Length'Img);
S_Hash := ES.Add_To_Graph (Event, User_Check_Properties);
-- Put_Line ("ES_Callback: " & System_State_Pkg.Image (Simulator.State));
......@@ -95,10 +105,11 @@ package body Simulator_Interface is
procedure Exhaust_All_Interfaces is
begin
ES.Backup_Ctxt := Simulator.State;
ES.Backup_Hash := ES.State_Hash (Simulator.State);
User_State := Application_State (Full_State);
ES.Backup_Ctxt := Full_State; -- Simulator.State;
ES.Backup_Hash := ES.State_Hash (Full_State); -- Simulator.State);
@@TABLE@@
@_CAPITALIZE:Block_Names_@_Events.Exhaust_Interfaces (Simulator.State, Callback => ES_Callback'Access);
@_CAPITALIZE:Block_Names_@_Events.Exhaust_Interfaces (User_State, Callback => ES_Callback'Access);
@@END_TABLE@@
end Exhaust_All_Interfaces;
......
templates/concurrency_view/simulation-adb/partition.tmplt
View file @ 23565c8c
......@@ -7,14 +7,14 @@ with Text_IO; use Text_IO;
package body Simulator is
procedure Push_Event (Event : asn1SccEvent) is
Next_Pos : constant Integer := State.Events.Length + 1;
Next_Pos : constant Integer := Events.Length + 1;
begin
if State.Events.Length < Integer (Max_Events)
if Events.Length < Integer (Max_Events)
then
State.Events.Length := State.Events.Length + 1;
Events.Length := Events.Length + 1;
-- Put_Line ("Storing event at position " & Next_Pos'Img
-- & " - nb of elements: " & State.Events.Length'Img);
State.Events.Data (Integer (Next_Pos)) := Event;
-- & " - nb of elements: " & Events.Length'Img);
Events.Data (Integer (Next_Pos)) := Event;
else
Put_Line ("Event dropped: queue full");
end if;
......@@ -23,17 +23,17 @@ package body Simulator is
function Pop_Event return asn1SccEvent is
Result : asn1SccEvent;
begin
if State.Events.Length = 0 then
if Events.Length = 0 then
raise Empty_Queue;
end if;
Result := State.Events.Data (1);
State.Events.Length := State.Events.Length - 1;
Result := Events.Data (1);
Events.Length := Events.Length - 1;
for I in 1 .. State.Events.Length loop
State.Events.Data (I) := State.Events.Data (I + 1);
for I in 1 .. Events.Length loop
Events.Data (I) := Events.Data (I + 1);
end loop;
-- Reset the slots that were moved, to clean up the global state
State.Events.Data (State.Events.Length + 1 .. Integer (Max_Events)) :=
Events.Data (Events.Length + 1 .. Integer (Max_Events)) :=
(others => asn1SccEvent_Init);
return Result;
......
templates/concurrency_view/simulation-ads/node.tmplt
View file @ 23565c8c
......@@ -4,12 +4,28 @@
@@-- If you have no internet access you can also use (with vim) Ctrl-W-f or gf in vim to open the text doc:
@@-- $HOME/tool-inst/share/kazoo/doc/templates_concurrency_view_sub_node.ascii
with Simulation_Dataview; use Simulation_Dataview;
with Simulator;
with ASN1_Iterators.Exhaustive_Simulation; use ASN1_Iterators;
generic
type State_With_Observers is tagged private;
with function Application_State (Full_State : State_With_Observers) return asn1SccSystem_State is <>;
with procedure Update_State (Full_State : in out State_With_Observers; Application_State : asn1SccSystem_State) is <>;
with function Full_State_Init return State_With_Observers is <>;
package Simulator_Interface is
type Check_Properties_Access is access procedure (Id : out Natural; Success : out Boolean);
-- The full state depends on the number of observers, which is
-- not visible here. This is an opaque type, but it is tagged,
-- and user provides function to read/write the application state
Full_State : State_With_Observers;
User_State : asn1SccSystem_State; -- State without observers
-- Procedure type for the property checking entry point
-- (provided by the user)
type Check_Properties_Access is access procedure
(Full_State : in out State_With_Observers;
Id : out Natural;
Success : out Boolean);
-- To start simulation, user must provide a pointer to the property
-- checking function
procedure Simulation_Startup (Check_Properties : Check_Properties_Access);
......@@ -29,8 +45,8 @@ private
-- Instantiate the exhaustive simulator
package ES is new Exhaustive_Simulation
(Context_Ty => asn1SccSystem_State,
Process_Ctxt => Simulator.State'Access,
(Context_Ty => State_With_Observers,
Process_Ctxt => Full_State'Access,
Event_Ty => asn1SccEvent,
Print_Event => Print_Event,
Check_Ty => Check_Properties_Access);
......
templates/concurrency_view/simulation-ads/partition.tmplt
View file @ 23565c8c
......@@ -16,7 +16,9 @@ package Simulator is
-- Exception raised by Pop_Event if the FIFO is empty
Empty_Queue : exception;
-- Global state (accessible from API users for read/right)
State : aliased asn1SccSystem_State;
-- Global state (accessible from API users for read/write)
-- State : aliased asn1SccSystem_State;
-- Event list (call of PI/RI)
Events : asn1SccEvents_Ty := asn1SccEvents_Ty_Init;
end Simulator;
templates/concurrency_view/simulation_gpr/thread.tmplt
View file @ 23565c8c
......@@ -9,6 +9,12 @@
@@IF@@ @_Language_@ = SDL or @_Language_@ = Ada
"@_LOWER:Pro_Block_Name_@.ads",
"@_LOWER:Pro_Block_Name_@_ri.ads",
"@_LOWER:Pro_Block_Name_@_pi.ads",
"@_LOWER:Pro_Block_Name_@_events.ads",
@@END_IF@@
@@IF@@ @_Language_@ = GUI
"@_LOWER:Pro_Block_Name_@_pi.ads",
"@_LOWER:Pro_Block_Name_@_events.ads",
@@END_IF@@
@@IF@@ @_Language_@ = SDL
"@_LOWER:Pro_Block_Name_@_datamodel.ads",
......
test/iterators/work/simulation/Makefile
View file @ 23565c8c
......@@ -7,7 +7,7 @@ mc: observer/my_observer.adb mcsrc/mc.adb mcsrc/properties.adb
observer/my_observer.adb: observer/observer.pr observer/observer.asn
cd observer && opengeode --toAda observer.pr && \
asn1.exe -Ada -typePrefix asn1scc -equal --target allboards observer.asn my_observer_datamodel.asn && \
asn1.exe -Ada -typePrefix asn1scc -equal --target allboards observer.asn my_observer_datamodel.asn && \
mv src/my_observer_datamodel.ad? .
......
test/iterators/work/simulation/mc.gpr
View file @ 23565c8c
......@@ -2,8 +2,13 @@ with "share/gpr/demo_simulator.gpr";
with "asn1_iterators";
project mc is
for source_dirs use ("mcsrc", "../dataview/iterators", "observer");
for main use ("mc.adb");
for Source_Dirs use (
"mcsrc",
"../dataview/iterators",
"observer"
--"../build/node1/simulation"
);
for Main use ("mc.adb");
package Compiler is
for Default_Switches ("Ada") use ("-g", "-O2");
end Compiler;
......
test/iterators/work/simulation/mcsrc/mc.adb
View file @ 23565c8c
with Text_IO; use Text_IO;
with simulator;
-- with simulator;
with simulator_interface;
with simulation_dataview; use simulation_dataview;
-- with simulation_dataview; use simulation_dataview;
with orchestrator_datamodel; use orchestrator_datamodel;
with properties; -- user-defined properties
-- with orchestrator_datamodel; use orchestrator_datamodel;
with Properties; -- user-defined properties
-- To Encode and MD5 the state:
with Gnat.MD5,
......@@ -17,30 +17,39 @@ with Gnat.MD5,
use Ada.Streams;
procedure mc is
use Properties;
Pulse_Event : asn1SccEvent :=
(Kind => Orchestrator_PRESENT,
Orchestrator =>
(Kind => Msg_In_PRESENT,
Msg_In =>
(Kind => Pulse_PRESENT,
Pulse => (P1 => 2))));
My_Properties_Access : Simulator_Interface.Check_Properties_Access := Properties.My_Properties'access;
procedure Encode_And_md5 (State: asn1SccSystem_State) is
uPER_Encoded : asn1SccSystem_State_uPER_Stream;
uPER_Result : adaasn1rtl.ASN1_RESULT;
begin
uPER_Result := asn1SccSystem_State_IsConstraintValid (State);
Put_Line ("IsConstraintValid: " & uPER_Result.Success'Img & uPER_Result.ErrorCode'Img);
asn1SccSystem_State_Encode (State, uPER_Encoded, uPER_Result);
Put_Line (uPER_Result.Success'Img & uPER_Result.ErrorCode'Img);
Put_Line (adaasn1rtl.encoding.BitStream_Current_Length_In_Bytes(uPER_Encoded)'img);
end Encode_And_md5;
-- Pulse_Event : asn1SccEvent :=
-- (Kind => Orchestrator_PRESENT,
-- Orchestrator =>
-- (Kind => Msg_In_PRESENT,
-- Msg_In =>
-- (Kind => Pulse_PRESENT,
-- Pulse => (P1 => 2))));
package Simulator_Pkg is new Simulator_Interface
(State_With_Observers => State_With_Observers,
Application_State => Application_State,
Update_State => Update_State,
Full_State_Init => Full_State_Init);
use Simulator_Pkg;
My_Properties_Access : Check_Properties_Access :=
Properties.My_Properties'Access;
-- procedure Encode_And_md5 (State: asn1SccSystem_State) is
-- uPER_Encoded : asn1SccSystem_State_uPER_Stream;
-- uPER_Result : adaasn1rtl.ASN1_RESULT;
-- begin
-- uPER_Result := asn1SccSystem_State_IsConstraintValid (State);
-- Put_Line ("IsConstraintValid: " & uPER_Result.Success'Img & uPER_Result.ErrorCode'Img);
-- asn1SccSystem_State_Encode (State, uPER_Encoded, uPER_Result);
-- Put_Line (uPER_Result.Success'Img & uPER_Result.ErrorCode'Img);
-- Put_Line (adaasn1rtl.encoding.BitStream_Current_Length_In_Bytes(uPER_Encoded)'img);
-- end Encode_And_md5;
begin
Simulator_Interface.Simulation_Startup (My_Properties_Access);
Simulator_Pkg.Simulation_Startup (My_Properties_Access);
-- Modify the system state:
-- Simulator.State.Orchestrator.SomeData := 3;
......@@ -50,11 +59,11 @@ begin
-- Simulator.Push_Event (Pulse_Event);
-- Simulator.Push_Event (Pulse_Event);
Encode_And_md5 (Simulator.State);
-- Encode_And_md5 (Simulator.State);
-- while Simulator.State.Events.Length > 0 loop
-- Simulator_Interface.Execute_Next_Event;
-- end loop;
Put_Line ("Now exhausting all interfaces...");
Simulator_Interface.Run_Exhaustive_Simulation;
Simulator_Pkg.Run_Exhaustive_Simulation;
end mc;
test/iterators/work/simulation/mcsrc/properties.adb
View file @ 23565c8c
with iterators_types;
use iterators_types;
with my_observer; use my_observer;
with my_observer;
with My_Observer_Datamodel;
use My_Observer_Datamodel;
-- For the test of the stop condition...
package body Properties is
......@@ -10,11 +14,24 @@ package body Properties is
Res := False;
end Check_Queue;
procedure My_Properties (Id : out Natural; Success : out Boolean) is
procedure Update_State (Full_State : in out State_With_Observers;
Application_State : asn1SccSystem_State) is
begin
Full_State.User_State := Application_State;
end Update_State;
procedure My_Properties (Full_State : in out State_With_Observers;
Id : out Natural;
Success : out Boolean) is
begin
Id := 0;
Observe (Global_State => Simulator.State);
Success := (Simulator.State.Orchestrator.State = asn1SccWait
and Simulator.State.Orchestrator.SeqOf = (Length => 4, Data => (4, 4, 4, 4)));
-- Observer modelled in SDL:
-- Restore the state of the observer, and execute it
My_Observer.Ctxt := Full_State.My_Observer_State;
My_Observer.Observe (Global_State => Full_State.User_State);
-- Simple stop condition:
Success := (My_Observer.Ctxt.State = My_Observer_Datamodel.asn1SccEnd_Success);
end;
end Properties;
test/iterators/work/simulation/mcsrc/properties.ads
View file @ 23565c8c
with simulator;
-- Add the data model of all observers to form the full state
with My_Observer_Datamodel;
with simulation_dataview; use simulation_dataview;
with orchestrator_datamodel; use orchestrator_datamodel;
with adaasn1rtl; use adaasn1rtl;
package Properties is
type State_With_Observers is tagged
record
User_State : asn1sccSystem_State;
My_Observer_State : My_Observer_Datamodel.asn1SccMy_Observer_Context;
end record;
-- Define the functions of the tagged type
-- Later the User state part can be a PER-encoded string to save space
-- When this happens, the following functions need to be update to do
-- The encoding/decoding on the fly
function Application_State (Full_State : State_With_Observers)
return asn1SccSystem_State is (Full_State.User_State);
procedure Update_State (Full_State : in out State_With_Observers;
Application_State : asn1SccSystem_State);
function Full_State_Init return State_With_Observers is
(User_State => asn1sccSystem_State_Init,
My_Observer_State => My_Observer_Datamodel.asn1SccMy_Observer_Context_Init);
-- there are continuous signals in the observers, we need check_queue
procedure Check_Queue (Res : out asn1Boolean);
pragma Export (C, Check_Queue, "my_observer_check_queue");
procedure My_Properties (Id : out Natural; Success : out Boolean);
procedure My_Properties (Full_State : in out State_With_Observers;
Id : out Natural;
Success : out Boolean);
end Properties;
test/iterators/work/simulation/observer/observer.asn
View file @ 23565c8c
......@@ -111,7 +111,7 @@ IMPORTS
T-Null, T-Int, T-SeqOf FROM Iterators-Types
T-Int32, T-UInt32, T-Int8, T-UInt8, T-Boolean, T-Null-Record FROM TASTE-BasicTypes;
Orchestrator-States ::= ENUMERATED {wait, running}
Orchestrator-States ::= ENUMERATED {running, wait}
Orchestrator-Context ::= SEQUENCE {
state Orchestrator-States,
......