Purpose of this assignment

This assignment is concerned with:

• use of context machines machine and SEES;
• consolidation of the understanding of invariant;
• consolidation of the understanding of guards;
• expansion of general knowledge of and experience with Event-B;
• specifying events;
• experience with refinement, including data refinement.
• using proof obligations to find problems in developments.
• using the animator to check the understanding and capture of requirements;

This assignment is concerned with the modelling of a simple ticket dispensing machine.

The modelling is to be done in three stages:

Atomic the first stage in which the purchase of tickets is an indivisible event.

Algorithmic refinement the second stage in which the purchase of tickets is distributed across a number of events with actions that are typical of what is commonly seen on a real ticket machine.

In this refinement, payment is made using coins, but the refinement is algorithmic refinement.

Aata refinement: refinement of the second stage is expressed totally in terms of coins.

Additions to Requirements

1. Animation should be used to provide a check on requirements. Animation can be used to discover weak or contradictory requirements. In AnimB, an important check is to critically examine the possible animation options at each step in the animation. This can be more valuable than simply following your animation scenario.

2. List_ctxis intended to model a first-in, first-out data-structure. It should not be modified to suit this assignment if that modification breaks the first-in, first-out discipline. List_ctxhas already been sent to all in the class, but will be sent again.

3. List_ctxcan be installed as follows:
o open Rodin
o select File/Import
o select General/Archive File
o select Next
o locate List_ctx.zip; Rodin will do a search to find the file
o follow remaining instructions
Overview of assignment
This assignment extends a simple library. The stages are:
1. LibraryR0: a simple library with:
o registed members
o books: each book is unique - there are no copies
o no borrowing limit
o no borrowing expirty date
2. LibraryR1
o addition of a borrowing limit;

Don't create the refinement from scratch by hand

You want to refine and then choose Refine from the options. Fill in the name of the refinement machine and Rodin will create a base for your refinement with all events being extended.

In some cases you will not want an extension, for example when you want to modify the guards of an event, not simply add more guards. In such cases you will want to turn off extension for such events.