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

Update test case for model checker

parent 102bdd41
......@@ -7,7 +7,7 @@ mc: observer/my_observer.adb mcsrc/mc.adb mcsrc/properties.adb
observer/my_observer.adb: observer/observer.pr observer/observer.asn
cd observer && opengeode --toAda observer.pr && \
asn1.exe -Ada -typePrefix asn1scc -equal --target allboards observer.asn my_observer_datamodel.asn && \
asn1.exe -Ada -typePrefix asn1scc -equal --target allboards observer.asn my_observer_datamodel.asn && \
mv src/my_observer_datamodel.ad? .
......
......@@ -2,8 +2,13 @@ with "share/gpr/demo_simulator.gpr";
with "asn1_iterators";
project mc is
for source_dirs use ("mcsrc", "../dataview/iterators", "observer");
for main use ("mc.adb");
for Source_Dirs use (
"mcsrc",
"../dataview/iterators",
"observer"
--"../build/node1/simulation"
);
for Main use ("mc.adb");
package Compiler is
for Default_Switches ("Ada") use ("-g", "-O2");
end Compiler;
......
with Text_IO; use Text_IO;
with simulator;
-- with simulator;
with simulator_interface;
with simulation_dataview; use simulation_dataview;
-- with simulation_dataview; use simulation_dataview;
with orchestrator_datamodel; use orchestrator_datamodel;
with properties; -- user-defined properties
-- with orchestrator_datamodel; use orchestrator_datamodel;
with Properties; -- user-defined properties
-- To Encode and MD5 the state:
with Gnat.MD5,
......@@ -17,30 +17,39 @@ with Gnat.MD5,
use Ada.Streams;
procedure mc is
use Properties;
Pulse_Event : asn1SccEvent :=
(Kind => Orchestrator_PRESENT,
Orchestrator =>
(Kind => Msg_In_PRESENT,
Msg_In =>
(Kind => Pulse_PRESENT,
Pulse => (P1 => 2))));
My_Properties_Access : Simulator_Interface.Check_Properties_Access := Properties.My_Properties'access;
procedure Encode_And_md5 (State: asn1SccSystem_State) is
uPER_Encoded : asn1SccSystem_State_uPER_Stream;
uPER_Result : adaasn1rtl.ASN1_RESULT;
begin
uPER_Result := asn1SccSystem_State_IsConstraintValid (State);
Put_Line ("IsConstraintValid: " & uPER_Result.Success'Img & uPER_Result.ErrorCode'Img);
asn1SccSystem_State_Encode (State, uPER_Encoded, uPER_Result);
Put_Line (uPER_Result.Success'Img & uPER_Result.ErrorCode'Img);
Put_Line (adaasn1rtl.encoding.BitStream_Current_Length_In_Bytes(uPER_Encoded)'img);
end Encode_And_md5;
-- Pulse_Event : asn1SccEvent :=
-- (Kind => Orchestrator_PRESENT,
-- Orchestrator =>
-- (Kind => Msg_In_PRESENT,
-- Msg_In =>
-- (Kind => Pulse_PRESENT,
-- Pulse => (P1 => 2))));
package Simulator_Pkg is new Simulator_Interface
(State_With_Observers => State_With_Observers,
Application_State => Application_State,
Update_State => Update_State,
Full_State_Init => Full_State_Init);
use Simulator_Pkg;
My_Properties_Access : Check_Properties_Access :=
Properties.My_Properties'Access;
-- procedure Encode_And_md5 (State: asn1SccSystem_State) is
-- uPER_Encoded : asn1SccSystem_State_uPER_Stream;
-- uPER_Result : adaasn1rtl.ASN1_RESULT;
-- begin
-- uPER_Result := asn1SccSystem_State_IsConstraintValid (State);
-- Put_Line ("IsConstraintValid: " & uPER_Result.Success'Img & uPER_Result.ErrorCode'Img);
-- asn1SccSystem_State_Encode (State, uPER_Encoded, uPER_Result);
-- Put_Line (uPER_Result.Success'Img & uPER_Result.ErrorCode'Img);
-- Put_Line (adaasn1rtl.encoding.BitStream_Current_Length_In_Bytes(uPER_Encoded)'img);
-- end Encode_And_md5;
begin
Simulator_Interface.Simulation_Startup (My_Properties_Access);
Simulator_Pkg.Simulation_Startup (My_Properties_Access);
-- Modify the system state:
-- Simulator.State.Orchestrator.SomeData := 3;
......@@ -50,11 +59,11 @@ begin
-- Simulator.Push_Event (Pulse_Event);
-- Simulator.Push_Event (Pulse_Event);
Encode_And_md5 (Simulator.State);
-- Encode_And_md5 (Simulator.State);
-- while Simulator.State.Events.Length > 0 loop
-- Simulator_Interface.Execute_Next_Event;
-- end loop;
Put_Line ("Now exhausting all interfaces...");
Simulator_Interface.Run_Exhaustive_Simulation;
Simulator_Pkg.Run_Exhaustive_Simulation;
end mc;
with iterators_types;
use iterators_types;
with my_observer; use my_observer;
with my_observer;
with My_Observer_Datamodel;
use My_Observer_Datamodel;
-- For the test of the stop condition...
package body Properties is
......@@ -10,11 +14,24 @@ package body Properties is
Res := False;
end Check_Queue;
procedure My_Properties (Id : out Natural; Success : out Boolean) is
procedure Update_State (Full_State : in out State_With_Observers;
Application_State : asn1SccSystem_State) is
begin
Full_State.User_State := Application_State;
end Update_State;
procedure My_Properties (Full_State : in out State_With_Observers;
Id : out Natural;
Success : out Boolean) is
begin
Id := 0;
Observe (Global_State => Simulator.State);
Success := (Simulator.State.Orchestrator.State = asn1SccWait
and Simulator.State.Orchestrator.SeqOf = (Length => 4, Data => (4, 4, 4, 4)));
-- Observer modelled in SDL:
-- Restore the state of the observer, and execute it
My_Observer.Ctxt := Full_State.My_Observer_State;
My_Observer.Observe (Global_State => Full_State.User_State);
-- Simple stop condition:
Success := (My_Observer.Ctxt.State = My_Observer_Datamodel.asn1SccEnd_Success);
end;
end Properties;
with simulator;
-- Add the data model of all observers to form the full state
with My_Observer_Datamodel;
with simulation_dataview; use simulation_dataview;
with orchestrator_datamodel; use orchestrator_datamodel;
with adaasn1rtl; use adaasn1rtl;
package Properties is
type State_With_Observers is tagged
record
User_State : asn1sccSystem_State;
My_Observer_State : My_Observer_Datamodel.asn1SccMy_Observer_Context;
end record;
-- Define the functions of the tagged type
-- Later the User state part can be a PER-encoded string to save space
-- When this happens, the following functions need to be update to do
-- The encoding/decoding on the fly
function Application_State (Full_State : State_With_Observers)
return asn1SccSystem_State is (Full_State.User_State);
procedure Update_State (Full_State : in out State_With_Observers;
Application_State : asn1SccSystem_State);
function Full_State_Init return State_With_Observers is
(User_State => asn1sccSystem_State_Init,
My_Observer_State => My_Observer_Datamodel.asn1SccMy_Observer_Context_Init);
-- there are continuous signals in the observers, we need check_queue
procedure Check_Queue (Res : out asn1Boolean);
pragma Export (C, Check_Queue, "my_observer_check_queue");
procedure My_Properties (Id : out Natural; Success : out Boolean);
procedure My_Properties (Full_State : in out State_With_Observers;
Id : out Natural;
Success : out Boolean);
end Properties;
......@@ -111,7 +111,7 @@ IMPORTS
T-Null, T-Int, T-SeqOf FROM Iterators-Types
T-Int32, T-UInt32, T-Int8, T-UInt8, T-Boolean, T-Null-Record FROM TASTE-BasicTypes;
Orchestrator-States ::= ENUMERATED {wait, running}
Orchestrator-States ::= ENUMERATED {running, wait}
Orchestrator-Context ::= SEQUENCE {
state Orchestrator-States,
......
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