Command Documentation


_atlp_convertToDag
Command that converts a list of formula into a DAG.
_mocha_end
Frees all mocha data structures.
atl_check
Model check ATL formula
atl_print
Prints an ATL formula.
atl_read
Reads in a formula containing the ATL formulas
check_refine
Performs symbolic (mdd based) refinement check. Assumes that all history dependent variables of specModule are present in implModule
check_refine_atom
Do one step in the compositional refinement proof of "implementation refines specification"
check_simulation
Performs symbolic (mdd based) simulation check
compose
parallel composition of two modules.
enum_init
Computes the set of initial states of a module.
enum_post
Computes the set of post (successor) states of a state.
enum_search
Performs enumerative state space search on a module.
exit
Ends the current MOCHA session
help
Give help for the commands
hide
hides the interface variables of the module
inv_check
Checks invariants on a module.
inv_print
Prints all the invariants.
inv_read
Reads in a file containing the invariants.
isEventVariable
Test if a variable is an event variable
isExternalVariable
Test if a variable is a external variable
isHistoryFreeVariable
Test if a variable is a history-free variable
isInterfaceVariable
Test if a variable is a interface variable
isPrivateVariable
Test if a variable is a private variable
let
creates an exact copy of a module with the given name
read_module
Reads a file containing Reactive Module descriptions.
read_spec
Read the specification file.
reinit
Reinitializes mocha.
ren
renames an observable variable of a module
rtm_dynamic_var_ordering
control the application of dynamic variable ordering
rtm_init
compute initial set of states of a module (represented as MDD). The build_trans command must be executed prior to executing this command
rtm_search
Performs symbolic (mdd based) state space search on a timed module
rtm_static_order
Orders mdd variables of a module as specified by a file
show_atoms
List all the atoms of the module.
show_mdls
Show all the parsed modules in the current session.
show_spec
show the specifications
show_types
List all types defined in the current Mocha session.
show_vars
shows the variables in side the given module.
sim_choice
Return the choices available to user.
sim_end
Ends the current simulation for the specified module.
sim_info
Provides miscellaneous information about the current simulation.
sim_mode
Changes the mode of simulation.
sim_prev_state_print
Prints the previous state.
sim_select
Select the choice for the current simulation.
sim_start
start simulation for module
state_print
Prints the values of all variables in a state.
sym_dynamic_var_ordering
control the application of dynamic variable ordering
sym_init
compute initial set of states of a module (represented as MDD). The build_trans command must be executed prior to executing this command
sym_post
compute the image of a region with respect to the module's transition relation
sym_print
print the given region
sym_search
Performs symbolic (mdd based) state space search on a module
sym_static_order
write the current ordering into a file
sym_trans
compute transition realtion MDD for the module
sym_union
Computes the union of two regions
sym_write_order
write the current ordering into a file

Last updated on 980624 22h11