SimB: Difference between revisions

No edit summary
Line 14: Line 14:


A SimB file consists of probabilistic and timing elements to simulate the model.
A SimB file consists of probabilistic and timing elements to simulate the model.
Within these elements, the modeler can user B expressions which are evaluated on the current state
Within these elements, the modeler can user B expressions which are evaluated on the current state.
 
In the following, an example for a SimB file controlling a Traffic Lights for cars and pedestrians is shown:
 
<pre>
{
"activations": [
  {"id":"$initialise_machine", "execute":"$initialise_machine",
  "activating":"choose"},
  {"id":"choose", "chooseActivation":{"cars_ry": "0.8", "peds_g": "0.2"}},
  {"id":"cars_ry", "execute":"cars_ry", "after":5000, "activating":"cars_g"},
  {"id":"cars_g", "execute":"cars_g", "after":500, "activating":"cars_y"},
  {"id":"cars_y", "execute":"cars_y", "after":5000, "activating":"cars_r"},
  {"id":"cars_r", "execute":"cars_r", "after":500, "activating":"choose"},
  {"id":"peds_g", "execute":"peds_g", "after":5000, "activating":"peds_r"},
  {"id":"peds_r", "execute":"peds_r", "after":5000, "activating":"choose"}
]
}
</pre>

Revision as of 09:16, 3 March 2021

SimB

SimB is a simulator built on top of ProB. It is available in the latest SNAPSHOT version in the new JavaFX based user interface ProB2-UI, The modeler can write SimB annotations for a formal model to simulate it. Furthermore, it is then possible to validate probabilistic and timing properties with statistical validation techniques such as hypothesis testing and estimation.

Using SimB

Start SimB via "Open Simulator" in the "Advanced" Menu after opening a machine.

Open SimB.png

Now, you can open a SimB file (JSON format) controlling the underlying formal model.

SimB Window.png

A SimB file consists of probabilistic and timing elements to simulate the model. Within these elements, the modeler can user B expressions which are evaluated on the current state.

In the following, an example for a SimB file controlling a Traffic Lights for cars and pedestrians is shown:

{
 "activations": [
  {"id":"$initialise_machine", "execute":"$initialise_machine",
   "activating":"choose"},
  {"id":"choose", "chooseActivation":{"cars_ry": "0.8", "peds_g": "0.2"}},
  {"id":"cars_ry", "execute":"cars_ry", "after":5000, "activating":"cars_g"},
  {"id":"cars_g", "execute":"cars_g", "after":500, "activating":"cars_y"},
  {"id":"cars_y", "execute":"cars_y", "after":5000, "activating":"cars_r"},
  {"id":"cars_r", "execute":"cars_r", "after":500, "activating":"choose"},
  {"id":"peds_g", "execute":"peds_g", "after":5000, "activating":"peds_r"},
  {"id":"peds_r", "execute":"peds_r", "after":5000, "activating":"choose"}
 ]
}