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