SimB: Difference between revisions

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.

Now, you can open a SimB file (JSON format) controlling the underlying formal 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.

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"}
 ]
}

Probabilistic and Timing Elements in SimB

The SimB file always contains an activations field storing all elements controlling the simulation in a list. There are two types of activations: direct activation and probabilistic choice. All activations are identified by their id.

Direct Activation

A direct activation requires the fields id, and execute to be defined. All other fields can be defined optionally.

• execute identifies the activated event by its name.
• after defines the scheduled time (in ms) when activating an event. By default, it is set to 0 ms, e.g., when this field is not defined explicitly.
• activating stores events that will be activated when executing the event defined by execute. Missing definition leads to the behavior that no other events are activated. The modeler can either write a String (to activate a single event) or a list of Strings (to activate multiple events)
• activationKind stores the kind of activation for execute. Possible options are multi, single, single:min, and single:max. The default value is multi
  • multi means that the activation will be queued for execution.
  • single means that the activation will only be queued if there are no queued activations with the same id
  • single:min means that the activation will only be queued if (1) there are no queued activations for the same id or (2) there is a queued activation with the same id whose value for the scheduled time is greater. In the case of (2), the already queued activation will be discarded.
  • single:max means that the activation will only be queued if (1) there are no queued activations for the same id or (2) there is a queued activation with the same id whose value for the scheduled time is lower. In the case of (2), the already queued activation will be discarded.

{
   "id":  ...
   "execute": ...
   "after": ...
   "activating": ...
   "activationKind": ...
   "additionalGuards": ...
   "fixedVariables": ....
   "probabilisticVariables": ....
   "priority": ...
}

Probabilistic Choice

{
   "id":  ...
   "chooseActivation": ...
}

Real-Time Simulation

Timed Trace Replay

Monte Carlo Simulation

Hypothesis Testing

Estimation