User Manual for Rodin v.2.3: Events

2.7.3 Events

We saw in Section 2.4 what an event basically looks like 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 might occur, i.e. under which combinations of the values of the machine’s variables and the parameters. The actions describe what changes apply 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 the reference section 3.2.3.4.3.

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

Now our aim is to prove that the invariants always hold. To do this, we must prove two things:

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

Rodin generates proof obligations for every invariant that can be changed by an event, i.e. the invariant contains variables 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 initialization, we cannot use the invariants because we do not make any assumptions about uninitialized machines.

Rodin Handbook

2.7.3 Events