The project file contains a manually generated semantics of the simulation for the
Square example, as well as its correctness verification.
The simulation was verified against the RoboChart model with
assumptions TA1
, TA2
and TA3
.
The file with the CSP models and verification assertions is:
src-gen/timed/square_assertions-noabstracteventsinthesemantics.csp
The interested reader can load this file in the FDR4 tool and check the assertions. The relevant assertions are:
assert PConstrainedSpecA3; TSTOP :[deadlock free]
assert PConstrainedSpecA3 \ ExternalEvents_MSquare [FD= PSimSpec
assert PSimSpec [FD= PConstrainedSpecA3 \ ExternalEvents_MSquare
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500 | Fax: 01904 325599