The NuSMV Interactive Shell Commands
-
add_property
- Adds a property to the list of properties
-
alias
- Provides an alias for a command
-
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
-
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_setup
- Builds the model in a Boolean Epression format.
-
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.
-
bmc_simulate
- Generates a trace of the model from 0 (zero) to k
-
_bmc_test_tableau
- Generates a random formula to logically test the equivalent tableau
-
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_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_invar
- Performs model checking of invariants
-
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_ltlspec
- Performs LTL model checking
-
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_bmc
- Initializes the system for the BMC verification.
-
go
- Initializes the system for the 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.
-
_memory_profile
- It shows the amount of memory used by every package.
-
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_bdd_parameters
- Creates a table with the value of all currently active NuSMV flags and change accordingly the configurable parameters of the BDD package.
-
set
- Sets an environment variable
-
show_dependencies
- Shows the expression dependencies
-
_show_help
- Provides on-line information for all commands
-
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>