Execution mode

The CIF simulator’s execution mode can be used to simulate a CIF specification in a way that adheres to the execution scheme defined by the CIF controller properties checker. This way the simulation will be more similar to the execution of generated code.

The simulator’s execution mode can be used to reduce the validation effort, by simulating only traces that are similar to what will occur in executions of implementations of the specification. That is, traces that can’t occur due to the execution scheme in executions, then also don’t need to be simulated. However, while the simulator’s execution mode tries to mimic the execution behavior as best it can, it may not be exactly the same. Enabling the execution mode thus runs the risk of missing behavior that can occur during executions.

The execution mode is disabled by default. It can be enabled using the Execution mode option (Simulator category).

Preconditions

To be able to enable the execution mode, several preconditions must be satisfied. Some preconditions are related to the specification being simulated:

  • The specification being simulated must not have any 'tau' edges. This means both edges with explicitly a tau event on them, as well as edges without an event that are implicitly 'tau' edges, are not supported for execution mode. Such edges are explicitly forbidden by the execution scheme.

  • The specification being simulated must not have an events that are neither controllable nor uncontrollable. Such events are explicitly forbidden by the execution scheme.

  • The specification being simulated must not have any SVG input mappings that map to an event. Such SVG input mappings are not strictly compatible with the execution scheme. Instead, use SVG input mappings with updates.

Other preconditions are related to simulation options:

  • A finite maximum delay for time transitions must be set. The execution scheme requires that the code to execute events is regularly executed. This means that the simulator must stop letting time pass regularly, allowing it to again consider event transitions. Therefore, a finite maximum duration of time transitions must be set.

    Typically, it is best to set this to a value that fits the execution frequency used for the execution of the implementation of the specification. If in the implementation the code is executed a certain number of times per second, so with a certain frequency, then the maximum delay should be set to match. For instance, for a frequency of 100 times per second, set the maximum delay to 1 / 100 = 0.01.

    If a maximum delay is chosen that is too large, then events may be executed much later than that they become enabled. For instance, if a transition for a controllable event leads to a state where an uncontrollable event becomes enabled, a transition for the uncontrollable event can only occur after a time transition. Thus, it typically won’t occur until 'maximum delay' time units have passed.

    If real-time simulation is enabled, it is recommended to set the maximum delay to match the frame rate.

  • The complete mode option must be disabled. The way the execution scheme is defined, calculating multiple different possible transitions from a single state is not applicable.

    Note that this also implies restrictions on which input mode can be used: only the automatic input mode and SVG input mode may be used. Furthermore, it implies that the automatic mode choice algorithm must be configured to always choose the first possible transition.

    By default, if these additional restrictions are satisfied, complete mode is automatically disabled, and therefore does not need to be disabled explicitly.

  • The non-urgent events option must not be used to make any events non-urgent. That is, all events must be simulated as urgent. The way the execution scheme is defined, events are executed as part of their event loop as long as they are enabled. Time may only pass after the execution of both the uncontrollable and controllable event loops.

Working

The way the execution mode work, is as follows, starting from the first item for the initial state:

  1. The simulator will try to perform transitions for SVG input mapping with updates, if any are queued due to having clicked a corresponding interactive SVG element. Once no more clicks need to be processed, it proceeds to the second item.

  2. The simulator will try to perform transitions for uncontrollable events, in the order specified by the execution scheme. Once no more uncontrollable events are enabled, it proceeds to the third item.

  3. The simulator will try to perform transitions for controllable events, in the order specified by the execution scheme. Once no more controllable events are enabled, it proceeds to the fourth item.

  4. The simulator will try to perform a time transition. If no time transition is possible, it proceeds to the first item. If a time transition is possible, it proceeds to the first item after the time transition ends.

If from a state no transitions are possible for any of these items, the simulation deadlocks.