MTC (Models and Theory of Computation): Mocha Demo
Ecole Polytechnique Fédérale de Lausanne
Mocha Demo
english only

Tasting Mocha: Ready Made Mocha:

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

Specification: A list of invariants or ATL formulae

Model Checking: Module formulae pairs or check_refine commands