## 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.6 Introducing Contexts
In this tutorial, we will create a model of the well known Agatha puzzle. We use this instead of the already introduced traffic light example because it provides us with more possibilities to apply Event-B’s logic and to use operations on relations. Here is a brief description of the puzzle:
Contexts are used to model static properties of a model, things that do not change over time. Whereas with machines we model the dynamic properties like the traffic light above. The objective of this section is to get familiar with contexts by modelling the Agatha puzzle. |