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

Update model checker

parent 991344f4
......@@ -94,6 +94,7 @@ package body @_CAPITALIZE:Name_@_Events is
end case;
end Print_Event;
@@IF@@ @_Language_@ = GUI
procedure Exhaust_Interfaces
(Global_State : in out asn1SccSystem_State;
Callback : access procedure (Event : asn1SccObservable_Event;
......@@ -101,12 +102,62 @@ package body @_CAPITALIZE:Name_@_Events is
begin
-- Put_Line ("Exhaust interfaces of @_Name_@");
@@TABLE@@
Exhaust_@_CAPITALIZE:List_Of_ASync_PIs_@ (Global_State, Callback);
Exhaust_@_CAPITALIZE:List_Of_ASync_RIs_@ (Global_State, Callback);
@@END_TABLE@@
end Exhaust_Interfaces;
@@TABLE@@
procedure Exhaust_@_CAPITALIZE:List_Of_ASync_RIs_@
(Global_State : in out asn1SccSystem_State;
Callback : access procedure (Event : asn1SccObservable_Event;
Limit_Reached : out Boolean)) is
@@IF@@ @_ASync_RI_Param_Name'Length_@ > 0
Iterator : @_CAPITALIZE:REPLACE_ALL(-/_):ASync_RI_Param_Type_@_Pkg.Instance;
Param : asn1Scc@_CAPITALIZE:REPLACE_ALL(-/_):ASync_RI_Param_Type_@;
@@END_IF@@
Original_State : constant asn1SccSystem_State := Global_State;
Event : asn1SccObservable_Event
(Kind => Output_Event_PRESENT);
Limit_Reached : Boolean;
begin
-- Put_Line ("Exhausing interface @_Name_@");
-- Create an event to store as an edge of the state graph
Event.Output_Event.Source := asn1Scc@_CAPITALIZE:Name_@;
Event.Output_Event.Dest := asn1Scc@_CAPITALIZE:Async_RIs_Parent_@;
Event.Output_Event.Event :=
(Kind => @_CAPITALIZE:Name_@_PRESENT,
@_CAPITALIZE:Name_@ =>
(Kind => Msg_OUT_PRESENT,
Msg_Out => (Kind => @_CAPITALIZE:List_Of_ASync_RIs_@_PRESENT, others => <>)));
@@IF@@ @_ASync_RI_Param_Name'Length_@ > 0
for Each of Iterator loop
-- Iterate exhaustively over the interface parameter
Param := @_CAPITALIZE:REPLACE_ALL(-/_):ASync_RI_Param_Type_@_Pkg.To_ASN1 (Each);
Event.Output_Event.Event.@_CAPITALIZE:Name_@.Msg_Out.@_CAPITALIZE:List_Of_ASync_RIs_@.@_ASync_RI_Param_Name_@ := Param;
-- 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@@
Callback (Event, Limit_Reached);
-- Restore previous state
Global_State := Original_State;
@@END_IF@@
end Exhaust_@_CAPITALIZE:List_Of_ASync_RIs_@;
@@END_TABLE@@
@@END_IF@@
@@-- pi.tmplt generate code to exhaust RI parameters
@_Protected_PIs'Indent_@
@_Unprotected_PIs'Indent_@
@@-- @_Protected_PIs'Indent_@
@@-- @_Unprotected_PIs'Indent_@
end @_CAPITALIZE:Name_@_Events;
......@@ -13,7 +13,7 @@ with Simulator;
with @_CAPITALIZE:Block_Names_@_Events;
@@END_TABLE@@
with ASN1_GSER;
-- with ASN1_GSER;
-- use ASN1_GSER;
package body Simulator_Interface is
......@@ -80,7 +80,7 @@ package body Simulator_Interface is
procedure Process_Event (Event : asn1SccObservable_Event) is
begin
Put(" *** AFTER OBSERVER : Event: ");
Put(" *** Process_Event : ");
Print_Event (Event);
User_State := Application_State (Full_state);
case Event.Kind is
......@@ -108,34 +108,52 @@ package body Simulator_Interface is
procedure ES_Callback (Event : asn1SccObservable_Event;
Limit_Reached : out Boolean)
is
-- 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
-- This function is called by the <Function>_Events.Exhaust_<RI> code
-- of each GUI of the system.
-- These functions generate an Output event for each parameter iteration
-- This callback is resonsible for processing this event: calling
-- observers, creating a correponding Input event, execute the PI, etc.
Unused_Hash : Hash_Type;
Current_Event : aliased asn1sccObservable_Event := Event;
Id : Natural;
Stop_Condition : Boolean := False;
Empty_Event : asn1sccObservable_Event := (Kind => No_Event_PRESENT,
No_Event => (null record));
procedure Next_Event (E : in out asn1sccObservable_Event) is
begin
case E.Kind is
when Input_Event_Present =>
Put ("[-] Next Event : Input Event");
Process_Event (E);
Run_Observers (Full_State,
E,
Id,
Stop_Condition);
when others =>
Put ("[-] Next Event : Non-Input Event");
Run_Observers (Full_State,
E,
Id,
Stop_Condition);
if not Stop_Condition then
Process_Event (E);
end if;
end case;
end Next_Event;
begin
-- Flow:
-- (1) call the observers with the input event
-- (1) call the observers with the output event
-- (2) process the event (it may have been altered, even removed)
-- (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:
-- (3) if there was an event it may have created (pushed) new events
-- or put events in the message queues of functions
-- 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
-- (4) 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
-- (5) Store the possible new state with the input event
--
-- "process the event" means:
-- (a) if event == output: create a corresponding input event,
......@@ -144,48 +162,40 @@ 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);
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;
Put_Line ("[-] Callback with state: " & State_As_String (Full_State));
Next_Event (Current_Event);
-- for (4):
-- for (3):
loop
exit when Simulator.Events.Length = 0 or Stop_Condition;
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);
-- Make sure all message queues are drained
@@INLINE( exit when Stop_Condition or \(Simulator.Events.Length = 0 and )( and )(\);\n)@@
@@TABLE@@
@@IF@@ @_Block_Languages_@ /= GUI
User_State.@_CAPITALIZE:Block_Names_@_Queue.Length = 0
@@END_IF@@
@@END_TABLE@@
@@END_INLINE@@
loop
exit when Simulator.Events.Length = 0 or Stop_Condition;
declare
E : asn1SccObservable_Event := Simulator.Pop_Event;
begin
Next_Event (E);
end;
end loop;
-- for (4):
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;
Next_Event (New_In_Event);
end;
end loop;
User_State.@_CAPITALIZE:Block_Names_@_Queue.Length := 0;
......@@ -200,7 +210,7 @@ package body Simulator_Interface is
Put_Line ("Number of states before Add_To_Graph: " & ES.Grafset.Length'Img);
-- for (6):
-- for (5):
Unused_Hash := ES.Add_To_Graph (Event, Id, Stop_Condition);
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);
......@@ -216,13 +226,16 @@ package body Simulator_Interface is
Limit_Reached := ES.Properties.Length >= 10;
end ES_Callback;
-- Exhaust Required Interfaces of GUIs (create Output Events)
procedure Exhaust_All_Interfaces is
begin
User_State := Application_State (Full_State);
ES.Backup_Ctxt := Full_State;
ES.Backup_Hash := ES.State_Hash (Full_State);
@@TABLE@@
@@IF@@ @_Block_Languages_@ = GUI
@_CAPITALIZE:Block_Names_@_Events.Exhaust_Interfaces (User_State, Callback => ES_Callback'Access);
@@END_IF@@
@@END_TABLE@@
end Exhaust_All_Interfaces;
......
......@@ -19,7 +19,7 @@ procedure Exhaust_@_CAPITALIZE:Name_@
@@END_IF@@
Original_State : constant asn1SccSystem_State := Global_State;
Event : asn1SccObservable_Event
(Kind => Input_Event_PRESENT); @@--@_CAPITALIZE:Parent_Function_@_PRESENT);
(Kind => Input_Event_PRESENT);
Limit_Reached : Boolean;
begin
-- Put_Line ("Exhausing interface @_Name_@");
......
......@@ -6,9 +6,10 @@
with Simulation_DataView; use Simulation_Dataview;
@@-- pi.tmplt contains the relevant "with" clauses for ASN.1 modules:
@@-- pi/ri.tmplt contains the relevant "with" clauses for ASN.1 modules:
@_Protected_PIs_@
@_Unprotected_PIs_@
@_Required_@
with @_CAPITALIZE:Name_@_PI;
......@@ -24,6 +25,7 @@ package @_CAPITALIZE:Name_@_Events is
procedure Print_Event (Event : asn1scc@_CAPITALIZE:Name_@_Event);
@@IF@@ @_Language_@ = GUI
-- For exhaustive simulation:
procedure Exhaust_Interfaces
(Global_State : in out asn1SccSystem_State;
......@@ -32,10 +34,10 @@ package @_CAPITALIZE:Name_@_Events is
private
@@TABLE@@
procedure Exhaust_@_CAPITALIZE:List_Of_ASync_PIs_@
procedure Exhaust_@_CAPITALIZE:List_Of_ASync_RIs_@
(Global_State : in out asn1SccSystem_State;
Callback : access procedure (Event : asn1SccObservable_Event;
Limit_Reached : out Boolean));
@@END_TABLE@@
@@END_IF@@
end @_CAPITALIZE:Name_@_Events;
......@@ -3,3 +3,6 @@
@@-- 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
@@TABLE@@
with @_CAPITALIZE:REPLACE(-/_):Param_ASN1_Modules_@; use @_CAPITALIZE:REPLACE(-/_):Param_ASN1_Modules_@;
@@END_TABLE@@
......@@ -26,6 +26,14 @@ BEGIN
env, @_LOWER:REPLACE_ALL(_/-):Block_Names_@
}
-- Current observer state flag (used by model checkers)
Observer-State-Kind ::= ENUMERATED {
regular-state,
error-state,
ignore-state,
success-state
}
-- Event related to the execution of a PI or call of a RI in the functional code
Function-Event ::= CHOICE {
@@INLINE( )(,\n )()@@
......
Markdown is supported
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