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

Model checking: create a library for python interfacing

parent 0d657839
...@@ -4,6 +4,8 @@ all: mc ...@@ -4,6 +4,8 @@ all: mc
mc: observer/my_observer.adb mcsrc/mc.adb mcsrc/properties.adb mc: observer/my_observer.adb mcsrc/mc.adb mcsrc/properties.adb
ADA_PROJECT_PATH=~/.local/share/gpr:${ADA_PROJECT_PATH} gprbuild -p -P mc ADA_PROJECT_PATH=~/.local/share/gpr:${ADA_PROJECT_PATH} gprbuild -p -P mc
# also make a library version for python interfacing
ADA_PROJECT_PATH=~/.local/share/gpr:${ADA_PROJECT_PATH} gprbuild -p -P mc_lib.gpr
observer/my_observer.adb: observer/observer.pr observer/observer.asn observer/my_observer.adb: observer/observer.pr observer/observer.asn
cd observer && opengeode --toAda observer.pr && \ cd observer && opengeode --toAda observer.pr && \
......
...@@ -8,7 +8,7 @@ project mc is ...@@ -8,7 +8,7 @@ project mc is
"observer" "observer"
--"../build/node1/simulation" --"../build/node1/simulation"
); );
for Main use ("mc.adb"); for Main use ("modelcheck.adb");
package Compiler is package Compiler is
for Default_Switches ("Ada") use ("-g", "-O2"); for Default_Switches ("Ada") use ("-g", "-O2");
end Compiler; end Compiler;
......
with "share/gpr/demo_simulator.gpr";
with "asn1_iterators";
library project mc_lib is
for Library_Name use "simulator";
for Library_Dir use ".";
for Library_Kind use "dynamic";
for Library_Standalone use "encapsulated";
for Library_Options use ("-lrt", "-lm");
for Interfaces use (
"properties.ads",
"gser.ads",
"my_observer.ads",
"my_observer_datamodel.ads",
"my_observer_ri.ads",
"mc.ads"
);
for Source_Dirs use (
"mcsrc",
"../dataview/iterators",
"observer"
);
for Object_Dir use "../build/node1/demo_simu_obj";
package Compiler is
for Default_Switches ("Ada") use (
"-Wall",
"-Wextra",
"-Wcast-align"
);
end Compiler;
end mc_lib;
with Text_IO; use Text_IO; package body MC is
procedure Startup is
begin
Put_Line ("[Model Checker] Initialization done");
Init_Done := True;
end Startup;
with Simulator_Interface; procedure Model_Check is
begin
with Properties; -- user-defined properties if not Init_Done then
Startup;
procedure MC is end if;
use Properties; Simulator_Pkg.Run_Exhaustive_Simulation;
end Model_Check;
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,
State_As_String => State_To_String,
Run_Observers => Properties.My_Properties'Access);
use Simulator_Pkg;
-- 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 begin
Simulator_Pkg.Simulation_Startup; Startup;
Put_Line ("Now exhausting all interfaces...");
Simulator_Pkg.Run_Exhaustive_Simulation;
end MC; end MC;
with Text_IO; use Text_IO;
with Simulator_Interface;
with Properties; -- user-defined properties
-- External interface to the model checker.
-- Symbols are exported in C so that they can be called from Python via ctypes
package MC is
use Properties;
procedure Model_Check with Export, Convention => C, Link_Name => "mc_run_exhaustive";
private
init_done : boolean := False;
procedure Startup;
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,
State_As_String => State_To_String,
Run_Observers => Properties.My_Properties'Access);
use Simulator_Pkg;
-- 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;
end MC;
with MC;
procedure modelcheck is
begin
MC.Model_Check;
end modelcheck;
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