Workspaces
----
apbd
asves
asvpapers
bear
blast
buildmaster
caltrop
cases
compaan
concurrency
cosi
dif
diva
dopcenter
dopsysadmin
elab
embedded
embeddedadmin
giotto
healtheu
hyinfo
m2t2
mescal
metropolis
mica
mobies
mocpaper
msgadmin
mvsis
nephest
platform
ransom
robosysadmin
savg
sec
seminar
sensorprivacy
smartnets
systems
truck
video
webmaster
wow
Note:
JavaScript is disabled
, see the
Site Map
for navigation links
Tasting Mocha
Write your own input files. For editing use the mouse to cut and paste. Use the mouse to select a position and type.
System definition
: A set of reactive modules
-- reactive modules definitions
Specification
: A list of invariants or ATL formulae
-- specficiations: invariants and ATL formulae
Model Checking
: Module formulae pairs or check_refine commands
Last modified: , Hits
