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

Interact with the system with python

parent 8e0f3769
# this file was written manually.. for now
all: mc
all: modelcheck
mc: observer/my_observer.adb mcsrc/mc.adb mcsrc/properties.adb
modelcheck: observer/my_observer.adb mcsrc/modelcheck.adb mcsrc/properties.adb mcsrc/mc.adb mcsrc/mc.ads
ADA_PROJECT_PATH=~/.local/share/gpr:${ADA_PROJECT_PATH} gprbuild -p -P mc
# also make a library version for python interfacing
libsimulator.so: observer/my_observer.adb mcsrc/modelcheck.adb mcsrc/properties.adb mcsrc/mc.adb mcsrc/mc.ads mc.py
# make a library version for python interfacing
ADA_PROJECT_PATH=~/.local/share/gpr:${ADA_PROJECT_PATH} gprbuild -p -P mc_lib.gpr
$(MAKE) python/observer_asn.py
simu: libsimulator.so
cp mc.py libsimulator.so lib/demo_simulator/demo_simulator/libdemo.so python
cd python && LD_LIBRARY_PATH=~/.local/lib:${LD_LIBRARY_PATH}:. ./mc.py
observer/my_observer.adb: observer/observer.pr observer/observer.asn
cd observer && opengeode --toAda observer.pr && \
......@@ -19,6 +27,16 @@ observer/my_observer.adb: observer/observer.pr observer/observer.asn
observer/observer.asn: ../dataview/dataview-uniq.asn ../build/simulation.asn ../orchestrator/SDL/code/orchestrator_datamodel.asn ../another_function/SDL/code/another_function_datamodel.asn
cat $^ > $@
# create the python interface to the dataview to allow python instantiate ASN.1 types
python/observer_asn.py: observer/observer.asn
mkdir -p python
asn2dataModel -o python -toPython $^
$(MAKE) -C python -f Makefile.python
clean:
ADA_PROJECT_PATH=~/.local/share/gpr:${ADA_PROJECT_PATH} gprclean -P mc
rm observer/my_observer.ad?
ADA_PROJECT_PATH=~/.local/share/gpr:${ADA_PROJECT_PATH} gprclean -P mc_lib || :
ADA_PROJECT_PATH=~/.local/share/gpr:${ADA_PROJECT_PATH} gprclean -P mc || :
rm -f observer/my_observer.ad?
rm -f *.ali *.[cho] *.so *.ad[bs]
.PHONY: simu clean all
#!/usr/bin/env python3
import ctypes
import observer_asn
dll = ctypes.CDLL ("libsimulator.so")
dll.mc_run_exhaustive()
evt = observer_asn.Observable_Event()
testEvent = "output-event: {source simulator-gui, dest orchestrator, event simulator-gui: msg-out: pulse: {p1 42}}"
#queue = dll.global_event_queue (type Events_Ty)
# this would possibly work
queue_ptr = ctypes.c_int.in_dll(dll, "global_event_queue")
asn1_queue = observer_asn.Events_Ty (queue_ptr)
# this sequence works:
from opengeode import Asn1scc
ASN1_AST=Asn1scc.parse_asn1(["observer.asn"], rename_policy=Asn1scc.ASN1.RenameOnlyConflicting, ast_version=Asn1scc.ASN1.UniqueEnumeratedNames, flags=[Asn1scc.ASN1.AstOnly]).types
from asn1_value_editor import vn
import observer_asn
vn.valueNotationToCTypes(testEvent, evt, ASN1_AST["Observable-Event"].type, observer_asn, ASN1_AST)
evt.Reset()
dll.send_event(evt._ptr)
print(asn1_queue.GSER())
......@@ -12,6 +12,11 @@ package body MC is
end if;
Simulator_Pkg.Run_Exhaustive_Simulation;
end Model_Check;
procedure Send_Event (Event : asn1SccObservable_Event) is
begin
Simulator_Pkg.Process_Event (Event);
end Send_Event;
begin
Startup;
......
......@@ -2,6 +2,8 @@ with Text_IO; use Text_IO;
with Simulator_Interface;
with Simulation_Dataview; use Simulation_Dataview;
with Properties; -- user-defined properties
-- External interface to the model checker.
......@@ -10,6 +12,8 @@ package MC is
use Properties;
procedure Model_Check with Export, Convention => C, Link_Name => "mc_run_exhaustive";
procedure Send_Event (Event : asn1SccObservable_Event)
with Export, Convention => C, Link_Name => "send_event";
private
......
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