The NuSMV Interactive Shell 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

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.

optional

optional

bmc_setup

Builds the model in a Boolean Epression format.

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.

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.

flatten_hierarchy

Flattens the hierarchy of modules

check_fsm

Checks the transition relation for totality.

compute_reachable

Enables the future computation of the set of reachable states

print_fair_states

Prints out the number of fair states. In verbose mode, prints also the list of fair states.

print_fair_transitions

Prints the number of fair transitions. In verbose mode, prints also the list of fair states. NOTE: THESE ARE NOT REALLY TRANSITIONS, BUT RATHER STATE_INPUT PAIRS.

print_reachable_states

Prints out the number of reachable states. In verbose mode, prints also the list of 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

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_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_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_flat_model

Writes a flat model of a given SMV file

write_order

Writes variable order to file.