Commit 4c6500b7 authored by Maxime Perrotin's avatar Maxime Perrotin
Browse files

Update simulation/model checking templates

parent de9a7dd3
......@@ -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;
......
......@@ -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;
......
......@@ -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);
......
......@@ -17,6 +17,8 @@ package Simulator is
Empty_Queue : exception;
-- Global state (accessible from API users for read/write)
State : aliased asn1SccSystem_State;
-- State : aliased asn1SccSystem_State;
-- Event list (call of PI/RI)
Events : asn1SccEvents_Ty := asn1SccEvents_Ty_Init;
end Simulator;
......@@ -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",
......
Supports Markdown
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