Rodin User’s Handbook v.2.8: Events

2.7.3 Events

We saw in Section 2.4 what an event basically looks like by using the example of a traffic light:

Event

set_cars $\mathrel {\widehat=}$

any

$\it new\_ value$

where

$\tt grd1 :$: $\it new\_ value \in BOOL$

then

$\tt act1 :$: $\it cars\_ go := new\_ value$

end

We have the event’s name $set\_ cars$ , a parameter with the name $new\_ value$ , a guard with label grd1 and an action with label act1. An event can have an arbitrary number of parameters, guards and events.

The guards specify when an event is allowed to occur, i.e. the event can only be executed if the values of the machine’s variables and parameters match the values listed in the guard. If this is the case, we say that the event is enabled. The actions describe what changes will then be applied to the variables.

Only the variables that are explicitly mentioned in the actions are affected. All the other variables keep their old values. Beside the simple assignment ( $\mathrel {:\mkern 1mu=}$ ), there are other forms of actions ( $\mathrel {:\mkern 1mu\in }$ or $\mathrel {:\mkern 1mu\mid }$ ) which are explained in Section 3.2.4.4.3.

The initialisation of the machine is a special form of event. It has neither parameters nor guards.

Invariants must always be valid. To verify this, we must prove two things:

The initialisation leads to a state where the invariant is valid.
Assuming that the machine is in a state where the invariant is valid, every enabled event leads to a state where the invariant is valid.

Rodin generates proof obligations for every invariant that can be affected by an event, i.e. the invariant contains variables that can be changed by an event. The name of the proof obligation is then
event_name/invariant_label/INV. The goal of such a proof is to assert that when all affected variables are replaced by new values from the actions, the invariant still holds. The hypotheses for such a proof obligation consist of:

All invariants, because we assume that all invariants hold before the event is triggered,
All guards, because events can only be triggered when the guards are valid.

In the special case of an initialisation event, we cannot use the invariants because we do not make any assumptions about uninitialized machines.

Rodin Handbook

2.7.3 Events