MTC (Models and Theory of Computation): Mocha Demo
Logo EPFL
I&C
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