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

5 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 interaction can be (partially) controlled with the following command line options:

NuSMV [-int] [-s] [-load cmd-file] [-h|-help] [-v verbose-level]
      [-r] [-f] [-AG] [-ctt] [-is] [-ils] [-ii]
      [-i order-file] [-o order-file] [-reorder] [-m method]
      [[-cp part-limit]|[-dp]|[-iwls95 part-limit]] [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.

-AG

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

-cp part-limit

Build a conjunctively partitioned transition relation.

-ctt

Check whether the transition relation is total.

-dp

Build a disjunctively partitioned transition relation.

-f

Compute the set of reachable states before evaluating CTL expressions.

-help

-h

Print the command line help.

-i order-file

Read the variable ordering from file order-file.

-ii

Do not check INVARSPECs.

-ils

Do not check LTLSPECs.

-int

Start interactive shell.

-is

Do not check SPECs and COMPUTEs.

-iwls95 part-limit

Build a conjunctively partitioned transition relation, using [RAP+95] clustering heuristics, with threshold part-limit.

-load cmd-file

Interpret NuSMV commands from file cmd-file.

-m method

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

-o order-file

Write the variable ordering to file order-file. No evaluation occurs when only the -o command option is used in batch mode.

-r

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

-reorder

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

-s

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

-v verbose-level

Enable 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.

Bibliography

[CCGR98]

A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a reimplementation of SMV. Proceeding of the International Workshop on Software Tools for Technology Transfer (STTT-98), BRICS Notes Series, NS-98-4, pages 25--31. Also IRST Technical Report 9801-06.

[BCLM+94]

J.R. Burch, E.M. Clarke, D.E. Long, K.L. McMillan, and D.L. Dill. Symbolic Model Checking for Sequential Circuit Verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(4):401--424, April 1994.

[CGH97]

E. Clarke, O. Grumberg and K. Hamaguchi. Another Look at LTL Model Checking. Formal Methods in System Design, 10(1):57--71, February 1997.

[CMB90]

O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines based on symbolic execution. In J. Sifakis, editor, Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of LNCS, pages 365--373, Berlin, June 1990. Springer.

[Dil88]

D. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. ACM Distinguished Dissertations. MIT Press, 1988.

[EMSS91]

E. Allen Emerson, A. K. Mok, A. Prasad Sistla, and Jai Srinivasan. Quantitative temporal reasoning. In Edmund M. Clarke and Robert P. Kurshan, editors, Proceedings of Computer-Aided Verification (CAV '90), volume 531 of LNCS, pages 136--145, Berlin, Germany, June 1991. Springer.

[McMil92]

K.L. McMillan. The SMV system -- DRAFT. 1992.
Available at http://www.cs.cmu.edu/~modelcheck/smv/smvmanual.r2.2.ps.

[McMil93]

K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publ., 1993.

[Mart85]

A.J. Martin. The design of a self-timed circuit for distributed mutual exclusion. In H. Fuchs and W.H. Freeman, editors, Proceedings of the 1985 Chapel Hill Conference on VLSI, pages 245--260, New York, 1985.

[RAP+95]

R. K. Ranjan, A. Aziz, B. Plessier, C. Pixley, and R. K. Brayton. Efficient BDD algorithms for FSM synthesis and verification. In IEEE/ACM Proceedings International Workshop on Logic Synthesis, Lake Tahoe (NV), May 1995.

[Som98]

F. Somenzi. CUDD: CU Decision Diagram package -- release 2.2.0 Department of Electrical and Computer Engineering -- University of Colorado at Boulder, May 1998.

[Vis96]

"VIS: A system for Verification and Synthesis", The VIS Group, In the Proceedings of the 8th International Conference on Computer Aided Verification, p428-432, Springer Lecture Notes in Computer Science, #1102, Edited by R. Alur and T. Henzinger, New Brunswick, NJ, July 1996