Skip to content

WIP: Statistical model-checker communication module

Yann Duplouy requested to merge pikachuyann/simgrid:StatMC into master

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 to timestamp
  • 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

Merge request reports