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

Update templates for model checking

parent bda33792
...@@ -13,7 +13,7 @@ with Simulator; ...@@ -13,7 +13,7 @@ with Simulator;
with @_CAPITALIZE:Block_Names_@_Events; with @_CAPITALIZE:Block_Names_@_Events;
@@END_TABLE@@ @@END_TABLE@@
-- with ASN1_GSER; with ASN1_GSER;
-- use ASN1_GSER; -- use ASN1_GSER;
package body Simulator_Interface is package body Simulator_Interface is
...@@ -39,6 +39,9 @@ package body Simulator_Interface is ...@@ -39,6 +39,9 @@ package body Simulator_Interface is
Update_State (Full_State, User_State); Update_State (Full_State, User_State);
-- Initialize the state graph with the startup event -- Initialize the state graph with the startup event
ES.Backup_Ctxt := Full_State;
ES.Backup_Hash := ES.State_Hash (Full_State);
ES.Start_Hash := ES.Add_To_Graph (Startup_Event); ES.Start_Hash := ES.Add_To_Graph (Startup_Event);
ES.Queue.Append (ES.Start_Hash); ES.Queue.Append (ES.Start_Hash);
...@@ -50,6 +53,7 @@ package body Simulator_Interface is ...@@ -50,6 +53,7 @@ package body Simulator_Interface is
procedure Run_Exhaustive_Simulation procedure Run_Exhaustive_Simulation
is is
Start_Time : constant Time := Clock; Start_Time : constant Time := Clock;
Iterations : integer := 0;
begin begin
if not Init then if not Init then
Put_Line ("Error: you must call Startup function first"); Put_Line ("Error: you must call Startup function first");
...@@ -57,9 +61,12 @@ package body Simulator_Interface is ...@@ -57,9 +61,12 @@ package body Simulator_Interface is
end if; end if;
while ES.Queue.Length > 0 and ES.Properties.Length < 10 loop while ES.Queue.Length > 0 and ES.Properties.Length < 10 loop
exit when iterations = 4;
Iterations := Iterations + 1; -- debug
Full_State := Full_State :=
ES.Grafset.Element (Key => ES.Queue.Last_Element).Context; ES.Grafset.Element (Key => ES.Queue.Last_Element).Context;
-- Put_Line ("Restored: " & System_State_Pkg.Image (Simulator.State)); User_State := Application_State (Full_State);
Put_Line (State_As_String (Full_State));
ES.Queue.Delete_Last; ES.Queue.Delete_Last;
Exhaust_All_Interfaces; Exhaust_All_Interfaces;
end loop; end loop;
...@@ -187,6 +194,15 @@ package body Simulator_Interface is ...@@ -187,6 +194,15 @@ package body Simulator_Interface is
-- for (6): -- for (6):
Unused_Hash := ES.Add_To_Graph (Event, Id, Stop_Condition); 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("Stop Condition = " & Stop_Condition'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 ("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);
......
...@@ -11,6 +11,7 @@ generic ...@@ -11,6 +11,7 @@ generic
with function Application_State (Full_State : State_With_Observers) return asn1SccSystem_State is <>; 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 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 <>; with function Full_State_Init return State_With_Observers is <>;
with function State_As_String (Full_State : State_With_Observers) return String is <>;
Run_Observers : access procedure (Full_State : in out State_With_Observers; Run_Observers : access procedure (Full_State : in out State_With_Observers;
Event : access asn1sccObservable_Event; Event : access asn1sccObservable_Event;
Id : out Natural; Id : out Natural;
...@@ -48,6 +49,7 @@ private ...@@ -48,6 +49,7 @@ private
(Context_Ty => State_With_Observers, (Context_Ty => State_With_Observers,
Process_Ctxt => Full_State'Access, Process_Ctxt => Full_State'Access,
Event_Ty => asn1SccObservable_Event, Event_Ty => asn1SccObservable_Event,
State_As_String => State_As_String,
Print_Event => Print_Event); Print_Event => Print_Event);
end Simulator_Interface; end Simulator_Interface;
...@@ -20,6 +20,7 @@ library project @_CAPITALIZE:Name_@_Simulator is ...@@ -20,6 +20,7 @@ library project @_CAPITALIZE:Name_@_Simulator is
"simulator_interface.ads", "simulator_interface.ads",
"taste_basictypes.ads", "taste_basictypes.ads",
"adaasn1rtl-encoding.ads", "adaasn1rtl-encoding.ads",
"asn1_gser.ads",
@_Threads'Indent_@ @_Threads'Indent_@
"adaasn1rtl.ads"); "adaasn1rtl.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