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

Update templates for native model checker

parent 419075b1
......@@ -53,7 +53,6 @@ package body Simulator_Interface is
procedure Run_Exhaustive_Simulation
is
Start_Time : constant Time := Clock;
Iterations : integer := 0;
begin
if not Init then
Put_Line ("Error: you must call Startup function first");
......@@ -61,12 +60,10 @@ package body Simulator_Interface is
end if;
while ES.Queue.Length > 0 and ES.Properties.Length < 10 loop
exit when iterations = 4;
Iterations := Iterations + 1; -- debug
Full_State :=
ES.Grafset.Element (Key => ES.Queue.Last_Element).Context;
User_State := Application_State (Full_State);
Put_Line (State_As_String (Full_State));
-- Put_Line (State_As_String (Full_State));
ES.Queue.Delete_Last;
Exhaust_All_Interfaces;
end loop;
......@@ -83,6 +80,8 @@ package body Simulator_Interface is
procedure Process_Event (Event : asn1SccObservable_Event) is
begin
Put(" *** AFTER OBSERVER : Event: ");
Print_Event (Event);
User_State := Application_State (Full_state);
case Event.Kind is
when System_Startup_PRESENT | No_Event_PRESENT => null;
......@@ -117,14 +116,17 @@ package body Simulator_Interface is
Current_Event : aliased asn1sccObservable_Event := Event;
Id : Natural;
Stop_Condition : Boolean := False;
Empty_Event : asn1sccObservable_Event := (Kind => No_Event_PRESENT,
No_Event => (null record));
begin
-- 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:
-- (3) if event is an input event, call observers with an empty event
-- to check the state right after execution of the input event
-- Observers cannot transform a No_Event into a new event
-- (4) if there was an event it may have created (pushed) new events:
-- while the list of pending events is not empty:
-- get the oldest event
-- call observers with it (they may alter it)
-- process the event
......@@ -142,70 +144,75 @@ package body Simulator_Interface is
-- (c) if event == no_event, do nothing
-- for (1) and (2):
Put_Line ("CALLBACK WITH STATE: " & State_As_String (Full_State));
Run_Observers (Full_State, Current_Event, 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;
if not Stop_Condition then
Process_Event (Current_Event);
-- for (3) - Post-INPUT call of the observers
if Current_Event.Kind = Input_Event_PRESENT then
Run_Observers (Full_State, Empty_Event, Id, Stop_Condition);
end if;
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, Id, Stop_Condition);
Process_Event (Next_Event);
end;
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, Id, Stop_Condition);
Process_Event (Next_Event);
if Current_Event.Kind = Input_Event_PRESENT then
Run_Observers (Full_State, Empty_Event, Id, Stop_Condition);
end if;
end;
end loop;
-- 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, Id, Stop_Condition);
Process_Event (New_In_Event);
if Current_Event.Kind = Input_Event_PRESENT then
Run_Observers (Full_State, Empty_Event, Id, Stop_Condition);
end if;
end;
end loop;
User_State.@_CAPITALIZE:Block_Names_@_Queue.Length := 0;
Update_State (Full_State, User_State);
@@END_IF@@
@@END_TABLE@@
end if;
end loop;
-- 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, Id, Stop_Condition);
Process_Event (New_In_Event);
end;
end loop;
User_State.@_CAPITALIZE:Block_Names_@_Queue.Length := 0;
Update_State (Full_State, User_State);
@@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);
Put_Line ("Number of states before Add_To_Graph: " & ES.Grafset.Length'Img);
-- for (6):
Unused_Hash := ES.Add_To_Graph (Event, Id, Stop_Condition);
Put_Line ("State:");
Put_Line (State_As_String (Full_State));
Put_Line ("hash: " & Unused_Hash'Img & " In Grafset: " & ES.Grafset.Contains (Key=>Unused_Hash)'Img);
Put_Line ("ES Queue Length : " & ES.Queue.Length'Img);
Put_Line ("STATE AT THE END OF CALLBACK: " & State_As_String (Full_State));
-- Put_Line ("hash: " & Unused_Hash'Img & " In Grafset: " & ES.Grafset.Contains (Key=>Unused_Hash)'Img);
-- Put_Line ("ES Queue Length : " & ES.Queue.Length'Img);
Put_Line("Stop Condition = " & Stop_Condition'img);
Put_Line ("ES.Visited.Contains(Hash)? " & ES.Visited.Contains(Unused_Hash)'Img);
-- Put_Line ("ES.Visited.Contains(Hash)? " & ES.Visited.Contains(Unused_Hash)'Img);
-- Restore the full state (to get the observer in original state for the next iteration
Full_State := ES.Backup_Ctxt;
-- Put_Line ("ES_Callback: " & System_State_Pkg.Image (Simulator.State));
-- Put_Line ("Number of states after Add_To_Graph: " & ES.Grafset.Length'Img);
Put_Line ("Number of states after Add_To_Graph: " & ES.Grafset.Length'Img);
Limit_Reached := ES.Properties.Length >= 10;
end ES_Callback;
......
......@@ -24,13 +24,6 @@ package Simulator_Interface is
Full_State : State_With_Observers;
User_State : aliased asn1SccSystem_State; -- State without observers
-- Procedure type for the property checking entry point
-- (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);
procedure Simulation_Startup;
procedure Process_Event (Event : asn1SccObservable_Event);
......
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