University of California at Berkeley Department of Electrical Engineering and Computer Sciences University of Pennsylvania Department of Computer and Information Science State University of New York at Stony Brook Department of Computer Science

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

Please send questions or comments about MOCHA here. This site is maintained by the mocha-webmaster. Mirror sites are maintained at the University of Pennsylvania and the SUNY at Stony Brook.