WIP: Statistical model-checker communication module
A first version of a communication module with a statistical model-checker, tracking several global variables. The final goal is to allow simulation control from outside the simulator, for example from a statistical model-checker such as Cosmos (see http://cosmos.lacl.fr/).
This module communicates over two named pipes, the first version of the protocol is summarized below.
From simulator to outside
-
T timestamp var1=val1 var2=val2
is sent after a simulation step where one of the monitored variable (var1
,var2
) is changed (or whenever the time is greater than the timeout value given) or when the simulation stops naturally; -
RST seed1 seed2 seed3 seed4 seed5 seed6
is sent at the end of a simulation, and give the six diferent integers forming the seed of RngStream.
From outside to simulator
-
TIMEOUT timestamp
is used to set the timeout value totimestamp
-
START
is used to start the simulation (the main use is to avoid any commands from previous simulation being wrongly used) -
CONT
is used to continue the simulation after a step where the variables have been written -
STOP
is used to forcefully stop a simulation