MTC (Models and Theory of Computation): Mocha Demo
Mocha Demo
english only
EPFL
>
I&C
>
IIF
>
MTC
Tasting Mocha:
Ready Made Mocha:
Empty Page
Simple counter
Peterson's protocol
For editing use the mouse to cut and paste. Use the mouse to select a position and type in your changes.
System definition
: A set of reactive modules
-- reactive modules definitions
Specification
: A list of invariants or ATL formulae
-- specifications: invariants and ATL formulae
Model Checking
: Module formulae pairs or check_refine commands