To open the Rodin archive, install the Rodin tool and then
the UML-B plug-in.  Open the project using Import/existing project.

See http://www.event-b.org/ for tool installation.

The status of some proof obligations for ATM_R4 and ATM_R5 
is shown as manually proved.  In fact these were all proved 
automatically by simply calling NewPP in the interactive
prover and thus are counted as automatic in the paper.

The reason they do not get proved by the high level auto 
tactic used by the project builder is because the timeout
threshold used within that tactic is too low.
When NewPP is called from the interactive prover, the timeout
threshold is higher and these POs get proved automatically.