Assignment 2

Assignment 2

Assignment 2

The pdf file of the assignment specification is available here.

A fair copy of the solution is available at A2-Context-Sol.pdf and A2-Machine-Sol.pdf.

These are fair copies of the solutions to assignment 2. They are not presented as refinements, because I ran into some Rodin problems that I got around by removing the refinements! (There is a bug when a context appears visible through both the abstract machine and the refining context)

Nor have I given a complete generalization, showing instead through comments at the appropriate place how the declarations in the 3-station model generalize. Note also that this solution has only 3 events (besides Init), and that all the real work is done inside the guards of each event.There are also a minimum number of variables (and could have been fewer, except that the assignment required the separation into up- and down- starters).

Document History

This page maintained by John Hurst. Copyright Monash University Copyright Policy	66 accesses since 16 Jun 2009
Generated at 20090705:0016 from an XML file modified on 20090616:1446 Maintainer use only; not generally accessible: Local ServerWork ServerCSSE Server

285 accesses since 16 Jun 2009, HTML cache rendered at 20120210:2245