The NuSMV Interactive Shell Commands

_bmc_test_tableau: Generates a random formula to logically test the equivalent tableau
_memory_profile: It shows the amount of memory used by every package.
_show_help: Provides on-line information for all commands
add_property: Adds a property to the list of properties
alias: Provides an alias for a command
check_ltlspec_sbmc: Finds error up to depth k
check_ltlspec_sbmc_inc: Incremental SBMC LTL model checking
gen_ltlspec_sbmc: Dumps into one or more dimacs files the given LTL specification, or all LTL specifications if no formula is given. Generation and dumping parameters are the maximum bound and the loopback values. Uses Kepa's and Timo's method for doing bmc.
bmc_inc_simulate: Incrementally generates a trace of the model performing a given number of steps.
bmc_pick_state: Picks a state from the set of initial states
bmc_setup: Builds the model in a Boolean Epression format.
bmc_simulate: Generates a trace of the model from 0 (zero) to k
bmc_simulate_check_feasible_constraints: Performs a feasibility check on the list of given constraints. Constraints that are found to be feasible can be safely assumed not to cause deadlocks if used in the following step of incremental simulation.
build_boolean_model: Compiles the flattened hierarchy into boolean SEXP
build_flat_model: Compiles the flattened hierarchy into SEXP
build_model: Compiles the flattened hierarchy into BDD
check_compute: Performs computation of quantitative characteristics
check_ctlspec: Performs fair CTL model checking.
check_invar: Performs model checking of invariants
check_invar_bmc: Generates and solve the given invariant, or all invariants if no formula is given
check_invar_bmc_inc: Generates and solve the given invariant, or all invariants if no formula is given
check_ltlspec: Performs LTL model checking
check_ltlspec_bmc: Checks the given LTL specification, or all LTL specifications if no formula is given. Checking parameters are the maximum length and the loopback values
check_ltlspec_bmc_inc: Checks the given LTL specification, or all LTL specifications if no formula is given, using incremental algorithms. Checking parameters are the maximum length and the loopback values
check_ltlspec_bmc_onepb: Checks the given LTL specification, or all LTL specifications if no formula is given. Checking parameters are the single problem bound and the loopback values
check_property: Checks a property into the current list of properties, or a newly specified property
check_pslspec: Performs fair PSL model checking.
clean_sexp2bdd_cache: Cleans the cache used during evaluation of expressions to ADD and BDD representations.
dump_expr: Dumps a given expression (which can be contextualized) in the specified format. Example of supported format is 'dot'.
dynamic_var_ordering: Deals with the dynamic variable ordering.
echo: Merely echoes the arguments. File redirection is allowed.
encode_variables: Builds the BDD variables necessary to compile the model into BDD.
execute_partial_traces: Executes partial traces on the model FSM
execute_traces: Executes complete traces on the model FSM
flatten_hierarchy: Flattens the hierarchy of modules
check_fsm: Checks the transition relation for totality.
compute_reachable: Computes the set of reachable states
dump_fsm: Dumps (in DOT format) selected parts of the bdd fsm, with optional expression
print_fair_states: Prints out information about fair states
print_fair_transitions: Prints the number of fair transitions
print_reachable_states: Prints out information about reachable states
gen_invar_bmc: Generates the given invariant, or all invariants if no formula is given
gen_ltlspec_bmc: Dumps into one or more dimacs files the given LTL specification, or all LTL specifications if no formula is given. Generation and dumping parameters are the maximum bound and the loopback values
gen_ltlspec_bmc_onepb: Dumps into one dimacs file the problem generated for the given LTL specification, or for all LTL specifications if no formula is explicitly given. Generation and dumping parameters are the problem bound and the loopback values
get_internal_status: Returns the internal status of the system.
go: Initializes the system for the verification.
go_bmc: Initializes the system for the BMC verification.
goto_state: Goes to a given state of a trace
help: Provides on-line information on commands
history: list previous commands and their event numbers
hrc_dump_model: Writes the hrc structure from root node to a given SMV file
hrc_write_model: Writes the hrc structure from root node to a given SMV file
language_emptiness: Checks for language emptiness.
pick_state: Picks a state from the set of initial states
print_bdd_stats: Prints out the BDD statistics and parameters
print_clusterinfo: Prints out information about the clustering. This command is *deprecated* in 2.4
print_current_state: Prints out the current state
print_formula: Prints a formula
print_fsm_stats: Prints out information about the fsm and clustering.
print_iwls95options: Prints the Iwls95 Options.
print_usage: Prints processor and BDD statistics.
process_model: Performs the batch steps and then returns control to the interactive shell.
quit: exits NuSMV
read_model: Reads a NuSMV file into NuSMV.
read_trace: Reads the trace from the specified file into the memory
reset: Resets the whole system.
set: Sets an environment variable
set_bdd_parameters: Creates a table with the value of all currently active NuSMV flags and change accordingly the configurable parameters of the BDD package.
show_dependencies: Shows the expression dependencies
show_plugins: Lists out all the available plugins inside the system. In addition, it prints [D] in front of the default plugin.
show_property: Shows the currently stored properties
show_traces: Shows the traces generated in a NuSMV session
show_vars: Shows model's symbolic variables and their values
simulate: Performs a simulation from the current selected state
source: Executes a sequence of commands from a file
time: Provides a simple CPU elapsed time value
unalias: Removes the definition of an alias.
unset: Unsets an environment variable
usage: Provides a dump of process statistics
which: Looks for a file called "file_name"
write_boolean_model: Writes a flattened and booleanized model of a given SMV file
write_coi_model: Writes a flat model of SMV file, restricted to the COI of the model properties
write_flat_model: Writes a flat model of a given SMV file
write_flat_model_udg: Writes a flat model of a given SMV file in uDraw format
write_order: Writes variable order to file.

NuSMV <nusmv@fbk.eu>