Commit a21ef357 authored by Maxime Perrotin's avatar Maxime Perrotin
Browse files

Update simulation templates

parent eabf1981
......@@ -9,17 +9,34 @@ with ASN1_Ada_Iterators.Iterators; use ASN1_Ada_Iterators.Iterators;
package body @_CAPITALIZE:Name_@_Events is
procedure Process_Event (Event : asn1scc@_CAPITALIZE:Name_@_Event; Global_State: in out asn1SccSystem_State) is
procedure Process_Event
(Event : asn1sccObservable_Event;
Global_State : in out asn1SccSystem_State)
is
Evt : constant asn1scc@_CAPITALIZE:Name_@_Event :=
(case Event.Kind is
when Input_Event_Present =>
Event.Input_Event.Event.@_CAPITALIZE:Name_@,
when Output_Event_Present =>
Event.Output_Event.Event.@_CAPITALIZE:Name_@,
when others => asn1scc@_CAPITALIZE:Name_@_Event_Init);
-- To transform outputs into a corresponding input message to place
-- in the recipient queue (with a possibly different name):
Input_Event : asn1SccObservable_Event (Kind => Input_Event_PRESENT);
begin
case Event.Kind is
-- This function executes provided interface events only
if Event.Kind in No_Event_Present .. System_Startup_Present then
return;
end if;
case Evt.Kind is
@@IF@@ @_List_Of_ASync_PIs'Length_@ > 0
when Msg_IN_Present =>
case Event.Msg_In.Kind is
case Evt.Msg_In.Kind is
@@TABLE@@
when @_CAPITALIZE:List_Of_ASync_PIs_@_PRESENT =>
@@IF@@ @_ASync_PI_Param_Name_@ /= ""
declare
Param : asn1Scc@_CAPITALIZE:REPLACE_ALL(-/_):ASync_PI_Param_Type_@ := Event.Msg_In.@_CAPITALIZE:List_Of_ASync_PIs_@.@_CAPITALIZE:ASync_PI_Param_Name_@;
Param : asn1Scc@_CAPITALIZE:REPLACE_ALL(-/_):ASync_PI_Param_Type_@ := Evt.Msg_In.@_CAPITALIZE:List_Of_ASync_PIs_@.@_CAPITALIZE:ASync_PI_Param_Name_@;
begin
@_CAPITALIZE:Name_@_PI.@_CAPITALIZE:List_Of_ASync_PIs_@ (@_CAPITALIZE:ASync_PI_Param_Name_@ => Param, Global_State => Global_State);
end;
......@@ -31,16 +48,9 @@ package body @_CAPITALIZE:Name_@_Events is
@@END_IF@@
@@IF@@ @_List_Of_ASync_RIs'Length_@ > 0
when Msg_OUT_Present =>
case Event.Msg_Out is
@@TABLE@@
when asn1Scc@_CAPITALIZE:List_Of_ASync_RIs_@ =>
null; -- output events don't do anything
-- Put_Line ("[@_Name_@] SEND @_List_Of_ASync_RIs_@");
@@END_TABLE@@
@@TABLE@@
when asn1Scc@_CAPITALIZE:List_Of_Sync_RIs_@ =>
Put_Line ("[@_Name_@] CALL @_List_Of_Sync_RIs_@");
@@END_TABLE@@
-- Create a input message and place it in the recipient msg queue
case Evt.Msg_Out.Kind is
@_Required'Indent_@
end case;
@@END_IF@@
end case;
......@@ -65,13 +75,18 @@ package body @_CAPITALIZE:Name_@_Events is
@@END_IF@@
@@IF@@ @_List_Of_ASync_RIs'Length_@ > 0
when Msg_OUT_Present =>
case Event.Msg_Out is
case Event.Msg_Out.Kind is
@@TABLE@@
when asn1Scc@_CAPITALIZE:List_Of_ASync_RIs_@ =>
when @_CAPITALIZE:List_Of_ASync_RIs_@_PRESENT =>
Put ("@_Name_@: OUTPUT @_CAPITALIZE:List_Of_ASync_RIs_@");
@@IF@@ @_ASync_RI_Param_Name_@ /= ""
Put_Line (" (" & @_CAPITALIZE:REPLACE_ALL(-/_):ASync_RI_Param_Type_@_Pkg.Image (Event.Msg_Out.@_CAPITALIZE:List_Of_ASync_RIs_@.@_CAPITALIZE:ASync_RI_Param_Name_@) & ")");
@@ELSE@@
Put_Line ("()");
@@END_IF@@
@@END_TABLE@@
@@TABLE@@
when asn1Scc@_CAPITALIZE:List_Of_Sync_RIs_@ =>
when @_CAPITALIZE:List_Of_Sync_RIs_@_PRESENT =>
Put_Line ("@_Name_@ : CALL @_List_Of_Sync_RIs_@");
@@END_TABLE@@
end case;
......@@ -79,7 +94,10 @@ package body @_CAPITALIZE:Name_@_Events is
end case;
end Print_Event;
procedure Exhaust_Interfaces (Global_State : in out asn1SccSystem_State; Callback : access procedure (Event : asn1SccEvent; Limit_Reached : out Boolean)) is
procedure Exhaust_Interfaces
(Global_State : in out asn1SccSystem_State;
Callback : access procedure (Event : asn1SccObservable_Event;
Limit_Reached : out Boolean)) is
begin
-- Put_Line ("Exhaust interfaces of @_Name_@");
@@TABLE@@
......
simulation/@_Block_Name_@_events.adb
simulation/@_LOWER:Block_Name_@_events.adb
......@@ -17,31 +17,33 @@ with @_CAPITALIZE:Block_Names_@_Events;
-- use ASN1_GSER;
package body Simulator_Interface is
-- use Simulation_Dataview;
procedure Simulation_Startup
(Check_Properties : Check_Properties_Access)
is
-- Initialize global state from functions after they have
-- executed their startup transition (from elaboration)
Startup_Event : constant asn1SccEvent :=
Startup_Event : constant asn1SccObservable_Event :=
(Kind => System_Startup_PRESENT,
System_Startup => (null record));
begin
User_Check_Properties := Check_Properties;
Text_IO.Put_Line ("Simulation startup");
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 (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);
ES.Visited.Include (ES.Start_Hash);
ES.Start_Hash := ES.Add_To_Graph (Startup_Event);
ES.Queue.Append (ES.Start_Hash);
ES.Visited.Include (ES.Start_Hash);
Init := True;
end Simulation_Startup;
......@@ -53,51 +55,137 @@ package body Simulator_Interface is
Put_Line ("Error: you must call Startup function first");
return;
end if;
while ES.Queue.Length > 0 and ES.Properties.Length < 10 loop
-- 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;
Exhaust_All_Interfaces;
end loop;
if ES.Properties.Length > 0 then
Put_Line ("Generating MSC");
ES.Generate_MSC;
end if;
Put_Line ("Called" & ES.Count'Img & " interfaces");
Put_Line ("Visited" & ES.Grafset.Length'Img & " states");
Put_Line ("Execution time:" & Duration'Image (Clock - Start_Time) & "s.");
end Run_Exhaustive_Simulation;
procedure Execute_Next_Event is
Event : asn1SccEvent := Simulator.Pop_Event;
procedure Process_Event (Event : asn1SccObservable_Event) is
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 => User_State);
@@END_TABLE@@
when System_Startup_PRESENT | No_Event_PRESENT => null;
when Input_Event_PRESENT =>
case Event.Input_Event.Event.Kind is
@@TABLE'ALIGN_ON("=>", "(", "Global")@@
when @_CAPITALIZE:Block_Names_@_PRESENT =>
@_CAPITALIZE:Block_Names_@_Events.Process_Event (Event, User_State);
@@END_TABLE@@
end case;
when Output_Event_PRESENT =>
case Event.Output_Event.Event.Kind is
@@TABLE'ALIGN_ON("=>", "(", "Global")@@
when @_CAPITALIZE:Block_Names_@_PRESENT =>
@_CAPITALIZE:Block_Names_@_Events.Process_Event (Event, User_State);
@@END_TABLE@@
end case;
end case;
end Execute_Next_Event;
-- User code modified the application state -> place it in the full state
Update_State (Full_State, User_State);
end Process_Event;
procedure ES_Callback (Event : asn1SccEvent; Limit_Reached : out Boolean)
procedure ES_Callback (Event : asn1SccObservable_Event;
Limit_Reached : out Boolean)
is
-- Called at each PI invocation to add to the state graph and verify properties
S_Hash : Hash_Type;
-- This function is called by the <Function>_Events.Exhaust_<PI> code
-- that generates an Input event for each iteration of the input vector
-- This callback is resonsible for making the actual call to the PI
-- and invoking the Observers
Unused_Hash : Hash_Type;
Current_Event : aliased asn1sccObservable_Event := Event;
Id : Natural;
Stop_Condition : Boolean;
begin
--
-- First empty the stack of events that were generated during the call
while Simulator.Events.Length > 0 loop
Execute_Next_Event;
-- Flow:
-- (1) call the observers with the input event
-- (2) process the event (it may have been altered, even removed)
-- (3) if there was an event it may have created (pushed) new events
-- .. but if not (list empty) create a No_Event event to the list
-- (to make sure observers are called after execution of PI)
-- (4) while the list of pending events is not empty:
-- get the oldest event
-- call observers with it (they may alter it)
-- process the event
-- (5) read the message queues of all functions
-- (they may have been filled by output event)
-- place the messages in the main event queue
-- (that could be using the priorities to decide ordering)
-- and go back to (4)
-- (6) Store the possible new state with the input event
--
-- "process the event" means:
-- (a) if event == output: create a corresponding input event,
-- place it in the queue of the recipient,
-- (b) if event == input, execute the pi
-- (c) if event == no_event, do nothing
-- for (1) and (2):
Run_Observers (Full_State, Current_Event'Access, Id, Stop_Condition);
Process_Event (Current_Event);
-- for (3):
if Simulator.Events.Length = 0 then
declare
Empty_Event : constant asn1sccObservable_Event :=
(Kind => No_Event_PRESENT,
No_Event => (null record));
begin
Simulator.Push_Event (Empty_Event);
end;
end if;
-- for (4):
loop
exit when Simulator.Events.Length = 0 or Stop_Condition;
declare
Next_Event : aliased asn1sccObservable_Event := Simulator.Pop_Event;
begin
Run_Observers (Full_State, Next_Event'Access, Id, Stop_Condition);
Process_Event (Next_Event);
end;
end loop;
-- User code modified the application state -> place it in the full state
Update_State (Full_State, User_State);
-- for (5):
if not Stop_Condition then
@@TABLE@@
@@IF@@ @_Block_Languages_@ /= GUI
for I in 1 .. User_State.@_CAPITALIZE:Block_Names_@_Queue.Length loop
exit when Stop_Condition;
declare
New_In_Event : aliased asn1sccObservable_Event :=
User_State.@_CAPITALIZE:Block_Names_@_Queue.Data (I);
begin
Run_Observers (Full_State, New_In_Event'Access, Id, Stop_Condition);
Process_Event (New_In_Event);
end;
end loop;
@@END_IF@@
@@END_TABLE@@
end if;
-- Clear the queue of event in case stop conditions interrupted them
Simulator.Events.Length := 0;
-- Put_Line ("Number of states before Add_To_Graph: " & ES.Grafset.Length'Img);
S_Hash := ES.Add_To_Graph (Event, User_Check_Properties);
-- for (6):
Unused_Hash := ES.Add_To_Graph (Event, Id, Stop_Condition);
-- Put_Line ("ES_Callback: " & System_State_Pkg.Image (Simulator.State));
-- Put_Line ("Number of states after Add_To_Graph: " & ES.Grafset.Length'Img);
Limit_Reached := ES.Properties.Length >= 10;
......@@ -106,21 +194,35 @@ package body Simulator_Interface is
procedure Exhaust_All_Interfaces is
begin
User_State := Application_State (Full_State);
ES.Backup_Ctxt := Full_State; -- Simulator.State;
ES.Backup_Hash := ES.State_Hash (Full_State); -- Simulator.State);
ES.Backup_Ctxt := Full_State;
ES.Backup_Hash := ES.State_Hash (Full_State);
@@TABLE@@
@_CAPITALIZE:Block_Names_@_Events.Exhaust_Interfaces (User_State, Callback => ES_Callback'Access);
@@END_TABLE@@
end Exhaust_All_Interfaces;
procedure Print_Event (Event : asn1SccEvent) is
procedure Print_Event (Event : asn1SccObservable_Event) is
begin
case Event.Kind is
when System_Startup_PRESENT => null;
@@TABLE'ALIGN_ON("=>", "(", "Global")@@
when @_CAPITALIZE:Block_Names_@_PRESENT => @_CAPITALIZE:Block_Names_@_Events.Print_Event (Event => Event.@_CAPITALIZE:Block_Names_@);
@@END_TABLE@@
when System_Startup_PRESENT | No_Event_PRESENT => null;
when Input_Event_PRESENT =>
case Event.Input_Event.Event.Kind is
@@TABLE'ALIGN_ON("=>", "(", "Global")@@
when @_CAPITALIZE:Block_Names_@_PRESENT =>
@_CAPITALIZE:Block_Names_@_Events.Print_Event (Event => Event.Input_Event.Event.@_CAPITALIZE:Block_Names_@);
@@END_TABLE@@
end case;
when Output_Event_PRESENT =>
case Event.Output_Event.Event.Kind is
@@TABLE'ALIGN_ON("=>", "(", "Global")@@
when @_CAPITALIZE:Block_Names_@_PRESENT =>
@_CAPITALIZE:Block_Names_@_Events.Print_Event (Event => Event.Output_Event.Event.@_CAPITALIZE:Block_Names_@);
@@END_TABLE@@
end case;
end case;
end Print_Event;
begin
Simulation_Startup;
end Simulator_Interface;
......@@ -6,7 +6,7 @@
with Text_IO; use Text_IO;
package body Simulator is
procedure Push_Event (Event : asn1SccEvent) is
procedure Push_Event (Event : asn1SccObservable_Event) is
Next_Pos : constant Integer := Events.Length + 1;
begin
if Events.Length < Integer (Max_Events)
......@@ -14,19 +14,19 @@ package body Simulator is
Events.Length := Events.Length + 1;
-- Put_Line ("Storing event at position " & Next_Pos'Img
-- & " - nb of elements: " & Events.Length'Img);
Events.Data (Integer (Next_Pos)) := Event;
Events.Data (Next_Pos) := Event;
else
Put_Line ("Event dropped: queue full");
end if;
end Push_Event;
function Pop_Event return asn1SccEvent is
Result : asn1SccEvent;
function Pop_Event return asn1SccObservable_Event is
Result : asn1SccObservable_Event;
begin
if Events.Length = 0 then
raise Empty_Queue;
end if;
Result := Events.Data (1);
Result := Events.Data (1);
Events.Length := Events.Length - 1;
for I in 1 .. Events.Length loop
......@@ -34,7 +34,7 @@ package body Simulator is
end loop;
-- Reset the slots that were moved, to clean up the global state
Events.Data (Events.Length + 1 .. Integer (Max_Events)) :=
(others => asn1SccEvent_Init);
(others => asn1SccObservable_Event_Init);
return Result;
end Pop_Event;
......
......@@ -9,39 +9,61 @@
@@END_IF@@
@@END_TABLE@@
@@IF@@ @_Remote_GUI_@ = TRUE
@@-- Function to exhaust RI parameters. If Remote is GUI, RCM is asynnc and there is only one parameter
procedure Exhaust_@_CAPITALIZE:Name_@ (Global_State : in out asn1SccSystem_State; Callback : access procedure (Event : asn1SccEvent; Limit_Reached : out Boolean)) is
@@IF@@ @_Param_Types'Length_@ > 0
procedure Exhaust_@_CAPITALIZE:Name_@
(Global_State : in out asn1SccSystem_State;
Callback : access procedure (Event : asn1SccObservable_Event;
Limit_Reached : out Boolean)) is
@@IF@@ @_Param_Types'Length_@ > 0
Iterator : @_CAPITALIZE:REPLACE_ALL(-/_):Param_Types_@_Pkg.Instance;
Param : asn1Scc@_CAPITALIZE:REPLACE_ALL(-/_):Param_Types_@;
@@END_IF@@
@@END_IF@@
Original_State : constant asn1SccSystem_State := Global_State;
Event : asn1SccEvent (Kind => @_CAPITALIZE:Parent_Function_@_PRESENT);
Event : asn1SccObservable_Event
(Kind => Input_Event_PRESENT); @@--@_CAPITALIZE:Parent_Function_@_PRESENT);
Limit_Reached : Boolean;
begin
-- Put_Line ("Exhausing interface @_Name_@");
-- Create an event to store as an edge of the state graph
Event.@_Parent_Function_@ := (Kind => Msg_IN_PRESENT,
Msg_In => (Kind => @_CAPITALIZE:Name_@_PRESENT, others => <>));
Event.Input_Event.Source := asn1SccEnv;
Event.Input_Event.Dest := asn1Scc@_CAPITALIZE:Parent_Function_@;
Event.Input_Event.Event :=
(Kind => @_CAPITALIZE:Parent_Function_@_PRESENT,
@_CAPITALIZE:Parent_Function_@ =>
(Kind => Msg_IN_PRESENT,
Msg_In => (Kind => @_CAPITALIZE:Name_@_PRESENT, others => <>)));
@@IF@@ @_Param_Types'Length_@ > 0
for Each of Iterator loop
-- Iterate exhaustively over the interface parameter
Param := @_CAPITALIZE:REPLACE_ALL(-/_):Param_Types_@_Pkg.To_ASN1 (Each);
Event.@_Parent_Function_@.Msg_In.@_Name_@.@_Param_Names_@ := Param;
-- Put_Line ("Param Value: " & @_REPLACE_ALL(-/_):Param_Types_@_Pkg.Image (Param));
@_CAPITALIZE:Parent_Function_@_PI.@_CAPITALIZE:Name_@ (@_CAPITALIZE:Param_Names_@ => Param, Global_State => Global_State);
-- the Callback will add to the state graph and exhaust the events generated by the PI
Event.Input_Event.Event.@_CAPITALIZE:Parent_Function_@.Msg_In.@_Name_@.@_Param_Names_@ := Param;
-- Execute the provided interface
-- @_CAPITALIZE:Parent_Function_@_PI.@_CAPITALIZE:Name_@ (@_CAPITALIZE:Param_Names_@ => Param, Global_State => Global_State);
-- the Callback will call the observers, then execute the event
-- (which may have been altered by the observers), and then
-- process all the new events possibly generated during this execution
-- If a new state is generated at the end, it will be added to the graph
Callback (Event, Limit_Reached);
-- Restore previous state
Global_State := Original_State;
exit when Limit_Reached;
end loop;
@@ELSE@@
-- Execute the provided interface
@_CAPITALIZE:Parent_Function_@_PI.@_CAPITALIZE:Name_@ (Global_State);
Callback (Event, Limit_Reached);
-- Restore previous state
Global_State := Original_State;
@@END_IF@@
end Exhaust_@_CAPITALIZE:Name_@;
@@ELSE@@
procedure Exhaust_@_CAPITALIZE:Name_@ (Global_State : in out asn1SccSystem_State; Callback : access procedure (Event : asn1SccEvent; Limit_Reached : out Boolean)) is null;
procedure Exhaust_@_CAPITALIZE:Name_@
(Global_State : in out asn1SccSystem_State;
Callback : access procedure (Event : asn1SccObservable_Event;
Limit_Reached : out Boolean))
is null;
@@END_IF@@
......@@ -3,3 +3,32 @@
@@-- If you are using vim, go over the URL and pres gx in to follow the link
@@-- If you have no internet access you can also use (with vim) Ctrl-W-f then Ctrl-W-L (or gf)
@@-- in vim to open the doc: $HOME/tool-inst/share/kazoo/doc/templates_concurrency_view_sub_ri.ascii
@@IF@@ @_Kind_@ = SPORADIC_OPERATION
when @_CAPITALIZE:Name_@_PRESENT =>
@@IF@@ @_Remote_Languages_@ = GUI
null; -- message is sent to the environment, which has no input queue
@@ELSE@@
Input_Event.Input_Event.Source := Event.Output_Event.Source;
Input_Event.Input_Event.Dest := Event.Output_Event.Dest;
Input_Event.Input_Event.Event :=
(Kind => @_CAPITALIZE:Remote_Function_Names_@_PRESENT,
@_CAPITALIZE:Remote_Function_Names_@ =>
(Kind => Msg_In_PRESENT,
Msg_In => (Kind => @_CAPITALIZE:Remote_Interface_Names_@_PRESENT,
@_CAPITALIZE:Remote_Interface_Names_@ =>
@@IF@@ @_EXIST:Param_Names_@
(@_Param_Names_@ => Event.Output_Event.Event.@_CAPITALIZE:Parent_Function_@.Msg_Out.@_CAPITALIZE:Name_@.@_Param_Names_@))));
@@ELSE@@
(null record))));
@@END_IF@@
-- Add to the message queue of the receiving function
-- This will raise an exception if the queue size is exceeded
Global_State.@_CAPITALIZE:Remote_Function_Names_@_Queue.Length :=
Global_State.@_CAPITALIZE:Remote_Function_Names_@_Queue.Length + 1;
Global_State.@_CAPITALIZE:Remote_Function_Names_@_Queue.Data
(Global_State.@_CAPITALIZE:Remote_Function_Names_@_Queue.Length) := Input_Event;
@@END_IF@@
@@ELSE@@
when @_CAPITALIZE:Name_@_PRESENT =>
Put_Line ("[@_Name_@] PROCEDURE CALL OF @_Name_@");
@@END_IF@@
......@@ -19,15 +19,23 @@ package @_CAPITALIZE:Name_@_Events is
-- Process event: execute the provided interface for Input events
-- Only report output events
procedure Process_Event (Event : asn1scc@_CAPITALIZE:Name_@_Event; Global_State : in out asn1SccSystem_State);
procedure Process_Event (Event : asn1sccObservable_Event;
Global_State : in out asn1SccSystem_State);
procedure Print_Event (Event : asn1scc@_CAPITALIZE:Name_@_Event);
-- For exhaustive simulation:
procedure Exhaust_Interfaces (Global_State : in out asn1SccSystem_State; Callback : access procedure (Event : asn1SccEvent; Limit_Reached : out Boolean));
procedure Exhaust_Interfaces
(Global_State : in out asn1SccSystem_State;
Callback : access procedure (Event : asn1SccObservable_Event;
Limit_Reached : out Boolean));
private
@@TABLE@@
procedure Exhaust_@_CAPITALIZE:List_Of_ASync_PIs_@ (Global_State : in out asn1SccSystem_State; Callback : access procedure (Event : asn1SccEvent; Limit_Reached : out Boolean));
procedure Exhaust_@_CAPITALIZE:List_Of_ASync_PIs_@
(Global_State : in out asn1SccSystem_State;
Callback : access procedure (Event : asn1SccObservable_Event;
Limit_Reached : out Boolean));
@@END_TABLE@@
end @_CAPITALIZE:Name_@_Events;
simulation/@_Block_Name_@_events.ads
simulation/@_LOWER:Block_Name_@_events.ads
......@@ -11,44 +11,43 @@ generic
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 <>;
Run_Observers : access procedure (Full_State : in out State_With_Observers;
Event : access asn1sccObservable_Event;
Id : out Natural;
Success : out Boolean);
package Simulator_Interface is
-- 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
User_State : aliased 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);
-- (provided by the user) NOW PROVIDED BY THE GENERIC
-- 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);
procedure Simulation_Startup;
procedure Execute_Next_Event;
procedure Process_Event (Event : asn1SccObservable_Event);
procedure Run_Exhaustive_Simulation;
private
Init : Boolean := False;
procedure Exhaust_All_Interfaces;
procedure Print_Event (Event : asn1SccEvent);
procedure ES_Callback (Event : asn1SccEvent; Limit_Reached: out Boolean);
procedure Print_Event (Event : asn1SccObservable_Event);
procedure ES_Callback (Event : asn1SccObservable_Event;
Limit_Reached : out Boolean);
-- Callback for checking properties depend on actual user-provided properties
User_Check_Properties : Check_Properties_Access;
-- Instantiate the exhaustive simulator
package ES is new Exhaustive_Simulation
(Context_Ty => State_With_Observers,
Process_Ctxt => Full_State'Access,
Event_Ty => asn1SccEvent,
Print_Event => Print_Event,
Check_Ty => Check_Properties_Access);
Event_Ty => asn1SccObservable_Event,
Print_Event => Print_Event);
end Simulator_Interface;
......@@ -8,17 +8,15 @@ with Simulation_Dataview; use Simulation_Dataview;
package Simulator is
-- To add an event to the system FIFO (e.g. when functions call a RI)
procedure Push_Event (Event : asn1SccEvent);
procedure Push_Event (Event : asn1SccObservable_Event);
-- Get the first stored event from the FIFO
function Pop_Event return asn1SccEvent;
function Pop_Event return asn1SccObservable_Event;
-- Exception raised by Pop_Event if the FIFO is empty
Empty_Queue : exception;
--