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_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_bdd_cache
Cleans the cache used during evaluation of expressions to ADD and BDD representations.
compute
Performs computation of quantitative characteristics
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
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_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_order
Writes variable order to file.

NuSMV <nusmv@fbk.eu>