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.
check_invar_bmc: Generates and solve the given invariant, or all invariants if no formula is given
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_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
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
_bmc_test_tableau: Generates a random formula to logically test the equivalent tableau
check_pslspec_bmc_inc: Performs fair PSL model checking using incremental BMC.
add_property: Adds a property to the list of properties
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_fsm: Checks the transition relation for totality.
check_invar: Performs model checking of invariants
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.
reset: Resets the whole system.
compute: Performs computation of quantitative characteristics
compute_reachable: Computes the set of reachable states
convert_property_to_invar:
print_clusterinfo: Prints out information about the clustering. This command is *deprecated* in 2.4
dump_fsm: Dumps (in DOT format) selected parts of the bdd fsm, with optional expression
dynamic_var_ordering: Deals with the dynamic variable ordering.
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
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
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
print_iwls95options: Prints the Iwls95 Options.
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_current_state: Prints out the current state
_print_fair_state_input_pairs: Prints the number of fair state/input pairs
print_fair_states: Prints out information about fair states
print_fair_transitions: Prints the number of fair transitions, and list transitions in verbose mode.
print_fsm_stats: Prints out information about the fsm and clustering.
print_reachable_states: Prints out information about reachable states
print_usage: Prints processor and BDD statistics.
process_model: Performs the batch steps and then returns control to the interactive shell.
read_trace: Reads the trace from the specified file into the memory
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
optional: optional
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_boolean_model: Writes a flattened and booleanized 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.
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.
check_ltlspec_sbmc_inc: Incremental SBMC LTL model checking
1.6.1
