Running NuSMV batch

When the -int option is not specified, NuSMV runs as a batch program, in the style of SMV, performing (some of) the steps described in previous section in a fixed sequence.

 system_prompt> NuSMV [command line options] input-file RET

The program described in input-file is processed, and the corresponding finite state machine is built. Then, if input-file contains formulas to verify, their truth in the specified structure is evaluated. For each formula which is not true a counterexample is printed.

The batch mode can be controlled with the following command line options:

NuSMV [-s] [-ctt] [-lp] [-n idx] [-v vl] [-cpp] [-is] [-ic] [-ils]
      [-ii] [-r] [-f] [-int] [-h | -help] [-i iv_file] [-o ov_file]
      [-AG] [-load script_file] [-reorder] [-dynamic] [-m method]
      [[-mono]|[-thresh cp_t]|[-cp cp_t]|[-iwls95 cp_t]] [-coi]
      [-noaffinity] [-iwls95preorder] [-bmc] [-bmc_length k]
      [-ofm fm_file] [-obm bm_file] [input-file]

where the meaning of the options is described below. If input-file is not provided in batch mode, then the model is read from standard input.

-s

Avoids to load the NuSMV commands contained in `~/.nusmvrc' or in `.nusmvrc' or in `$${NuSMV_LIBRARY_PATH}/master.nusmvrc'.

-ctt

Checks whether the transition relation is total.

-lp

Lists all properties in SMV model

-n idx

Specifies which property of SMV model should be checked

-v verbose-level

Enables printing of additional information on the internal operations of NuSMV. Setting verbose-level to 1 gives the basic information. Using this option makes you feel better, since otherwise the program prints nothing until it finishes, and there is no evidence that it is doing anything at all. Setting the verbose-level higher than 1 enables printing of much extra information.

-cpp

Runs preprocessor on SMV files

-is

Does not check SPEC

-ic

Does not check COMPUTE

-ils

Does not check LTLSPEC

-ii

Does not check INVARSPEC

-r

Prints the number of reachable states before exiting. If the -f option is not used, the set of reachable states is computed.

-f

Computes the set of reachable states before evaluating CTL expressions.

-int

Starts interactive shell.

-help

-h

Prints the command line help.

-i iv_file

Reads the variable ordering from file iv_file.

-o ov_file

Reads the variable ordering from file ov_file.

-AG

Verifies only AG formulas using an ad hoc algorithm (see documentation for the ag_only_search environment variable).

-load cmd-file

Interprets NuSMV commands from file cmd-file.

-reorder

Enables variable reordering after having checked all the specification if any.

-dynamic

Enables dynamic reordering of variables

-m method

Uses method when variable ordering is enabled. Possible values for method are those allowed for the reorder_method environment variable (see section Interface to the DD Package).

-mono

Enables monolithic transition relation

-thresh cp_t

conjunctive partitioning with threshold of each partition set to cp_t (DEFAULT, with cp_t=1000)

-cp cp_t

DEPRECATED: use -thresh instead.

-iwls95 cp_t

Enables Iwls95 conjunctive partitioning and sets the threshold of each partition to cp_t

-coi

Enables cone of influence reduction

-noaffinity

Disables affinity clustering

-iwls95preoder

Enables iwls95 preordering

-bmc

Enables BMC instead of BDD model checking

-bmc k

Sets bmc_length variable, used by BMC

-ofm fm_file

prints flattened model to file fn_file

-obm bm_file

Prints boolean model to file bn_file

Go to the first, previous, next, last section, table of contents.