## Rodin HandbookThis work is sponsored by the Deploy Project This work is sponsored by the ADVANCE Project This work is licensed under a Creative Commons Attribution 3.0 Unported License |
## 2.7.3 EventsWe saw in Section 2.4 what an event basically looks like by using the example of a traffic light: - Event
*set_cars*- any
- where
- then
- end
We have the event’s name , a The guards specify Only the variables that are explicitly mentioned in the actions are affected. All the other variables keep their old values. Beside the simple assignment (), there are other forms of actions ( or ) which are explained in Section 3.2.4.4.3. The 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 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. |