About the MOVIDA Model Checker
Loading a TNCES
Configuring the model
Configuring state space creation
Computing the state space
Saving and loading state spaces
Checking CTL formulas
Using the Formula list GUI