NAME

smv - symbolic model verifier

SYNOPSIS

smv [options] [input-file]

DESCRIPTION

smv is a program that uses a symbolic model checking algorithm to evaluate formulas of CTL (Computational Tree Logic - a branching time temporal logic) with respect to a finite state model. The model and the specifications are described in input-file (default is the standard input). The language for describing the model is a simple parallel assignment. For complete definition of CTL and the model description language, please refer to the document "The SMV system."

OPTIONS

-version

Prints version information on stdout and exits.

-c cache-size

Set the size of the cache for BDD operations. It should be a prime or nearly prime number. Default is 32749. There is a tradeoff here between performance and memory. Up to a point, a larger cache can speed up operations by orders of magnitude. Each cache entry uses 16 bytes, so a quarter million entries use about four megabytes, which is reasonable if you have about 12 megabytes of real memory available. Virtual memory is of practically no use.

Some suggested values for the -c parameter: 16381, 32749, 65521, 262063, 522713, 1046429 2090867, 4186067, 8363639, 16777207

-k key-table-size

Set the size of the key table for BDD nodes. It should be a prime or nearly prime number, and should be at least 1/10 the number of BDD nodes in use at any given time. The default is 32749, which should be enough for most applications.

-m mini-cache-size

Sets the size of the portion of the cache for BDD operations which is used by the less expensive (non-iterative) BDD operations. It should be a prime or nearly prime number not larger than the cache-size. The default is 32749, same as the default cache-size.

-f

-nof

With -f, search the reachable state space of the model before evaluating the CTL operators. This can result in improved performance for models with sparse state spaces. It is on by default, and -nof disables it.

-AG

Verify Universal CTL formulas only. Uses an algorithm without fixpoints, and is generally faster. May take somewhat more memory.

-early

-noearly

With -early SMV evaluates AG specs while building the set of reachable states (-noearly turns it off, and is the default). This often helps in finding bugs earlier before the complete model is built. Has an effect only with -AG and -f options (that is, no -nof specified, since -f is on by default). At every iteration in the forward search SMV evaluates all the specs. If a spec is false, prints a counterexample and removes the spec from the list, so it won't be evaluated again. If no specs are left, exits immediately.

This option together with -inc supports a "lazy" construction of the transition relation. That is, it is computed only if it is necessary for evaluating a spec or for constructing a counterexample.

This option may also slow down verification if -inc option is used, since it may build the restricted transition relation at every iteration.

USE IT WITH CAUTION! Only *true* AG properties can be early evaluated. If your formulas contain other than the topmost AG temporal operators, the results may be wrong.

-cp part-limit

Perform conjunctive partitioning of the transition relation. The transition relation is not evaluated as a whole, instead the various next(variable) assignments are collected into partitions. When the size of a partition exceeds part-limit, the remaining assignments are collected into a new partition. When a forward (or backward) traversal of the transition relation is needed, each partition is used in turn. After the use of each partition, early quantification is done on unnecessary variables in order to reduce the size of the intermediate BDD [This option currently may make smv run slower, but on large examples it saves a lot of memory].

-h heuristic-factor

The variable ordering is determined by a heuristic procedure which is based on the syntactic structure of the program, and a floating point heuristic-factor between 0.0 and 1.0 [This option is currently broken].

-inc

Perform incremental evaluation of the transition relation. At each step in the forward search, the transition relation is being restricted to the reached state set. This can cut down on the size of the transition relation, although at the expense of some overhead to reevaluate at each step.

-simp n

n = 0, 1 or 2.

Implemented 2 more levels of simplification operators (`constrain'). n = 0 is the default and original SMV setup. n = 1 is generally faster on big examples but takes more memory. n = 2 is a combination of the two, which is usually slower but supposed to take even less memory. Has a real effect only with -cp option.

-int

smv enters interactive mode after the processing of input-file is completed. See INTERACTIVE MODE below.

-r

The number of reachable states to be printed at termination. This can involve some extra work if the -f option is not used.

-v verbose-level

A large amount of gibberish printed on the standard error. Setting verbose-level to 1 should give you all the information you need. 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 2 has the same affect as 2.

-reorder dynamic-variable-reordering

The dynamic variable reordering algorithm will work with this option. Every time when the garbage collection routine is called with the total BDD size large enough, dynamic-reordering tries to change the variable order in order to reduce the total bdd node number. This option also sets -noquit option.

-final-reorder

-no-final-reorder

Reoreder (or not) at the very end of SMV run (default - off). This is useful to generate a good variable ordering file, as the reordering is forced to happen, even if BDDs are small.

-i input-order

The variable ordering is read from file input-order. This overrides the -h option. This is most useful in combination with the -o option: The variable ordering (with or without heuristic ordering) can be written to a file using the -o option, the file can be inspected and reordered by the user, then read back in using the -i option. See VARIABLE ORDERING below.

-o output-order

-oo output-order

The variable ordering is written to file output-order, after parsing, and optional application of the heuristic variable ordering procedure (-h). No evaluation occurs when the -o or -oo option is used, unless -noquit or -reorder is specified.

The -oo is basically the same as the -o option, except that while reordering SMV will dump the output-order file every time after placing each variable, not only after the whole reordering is complete. This comes handy when you reorder a huge BDD and it already did half of the work in several hours, and then it suddenly runs out of memory and you lose all of the partial results. It is always recommended to use -oo instead of -o, unless you have a very strong reason otherwise.

-quit

-noquit

If -noquit is specified together with -o or -oo, SMV does not quit after dumping the order file. Useful with dynamic toggling of reordering. See `signal handling' for details. `-quit' is the opposite and is the default behavior.

-reorderbits bits-for-dynamic-variable-reordering

This option gives the limit for the number of bits of the variable to be reordered. The reorder routine will skip the variables that exceeds this limit. The default value is 10.

-reordersize starting-size-for-dynamic-variable-reordering

This option gives the minimal total bdd node number that the reorder routine will start working. Current default value is 5000.

-reordermaxsize n

Set the maximal size of BDDs to reorder. Useful if BDDs grow too large and reordering takes forever. Default is n = 300000.

-reorderminsize n

Set the minimal size of BDDs below which SMV should stop reordering. Useful if there are too many BDD variables, but the size of the BDDs quickly becomes small after moving a few first variables, and continuing to reorder becomes waste of time. Default is n = 2000.

-reorderfactor n

Reorder when the BDD size exceeds the size after the last reordering times n. NOTE: n is float (default n = 1.25).

-drip

Don't Reorder Intermediate [relational] Products.

Disables reordering while computing forward or backward relational products with -cp option. My observation is that intermediate relational products are often of a random nature and reordering variables for them may severly screw up the BDD size of the reachable state set.

-gcfactor n

-gclimit L

Set the desired frequency n and memory limit L (in MB) for garbage collection. Defaults are n = 3 and L = 32. Next garbage collection will be called when the number of nodes exceeds a certain curve that behaves close to y=n*x at small x and goes flatter as it approaches the limit L. Here x is the number of nodes after the last GC. This behavior corresponds to rare garbage collection when memory is sufficient, and more frequent collections with high memory demands.

Don't put n = 1 or too small L, it'll kill you.

Reason for the options: I found that sometimes garbage collection takes too large a fraction of time. Bigger n reduces this dramatically, but it may take much more memory. Be sure to set -gclimit to no more (and better no less) than the actual memory size on your machine. The memory limit will be adjusted if SMV goes beyond it and doesn't crash. If you feel you really need to garbage collect at some point, you may force SMV by sending it signal 12 (SIGUSR2). See SIGNAL HANDLING for details.

-checktrans

-nochecktrans

Default is -checktrans. If on, checks that the transition relation is total, and if not, prints a deadlock state. Very useful if you are using TRANS or INVAR to specify the transition relation. Note, that SMV can not check the totalness of the transition relation with CTL formulas (no idea why), and some formulas may be wrong if it's not total. May slow things down. If it bothers you, use -nochecktrans.

-l

-long

Print all the variables in each state in the counterexample traces. Normally, only the variables that have changed from the previous state are printed out. This can be useful if SMV is used as a decision procedure in a bigger system and the counterexamples are processed automatically.

-dumpspace file-name

Dumps the bdd for the set of reachable states in the file file-name. Works only with the -f option enabled (default).

-cols n

Sets the max number of characters for printing specs on stdout to n. If a spec is longer than that, SMV will put ... after n first characters. Default n = 40.

-width n

Sets the width of the terminal to n characters. Default n = 79.

VARIABLE ORDERING

smv uses Boolean Decision Diagrams (BDDs) to represent sets and relations in the CTL model checking algorithm. A BDD is a decision tree, in which variables always appear in the same order as the tree is traversed from root to leaf. The efficiency of BDDs is obtained by always combining isomorphic subtrees, and by eliminating redundant decision nodes in the tree. The degree storage efficiency obtained in this way is closely related to the variable ordering. The present version of the program has no built-in heuristics for selecting the variable ordering. Instead, the variables appear in the BDDs in the same order in which they are declared in the program. This means that variables declared in the same module are grouped together, which is generally a good practice, but this alone is not generally sufficient to obtain good performance in the evaluation. Usually, the variable ordering must be adjusted by hand, in an ad hoc way. A good heuristic is to arrange the ordering so that variables which often appear close to each other in formulas are close together in the order of declaration, and global variables should appear first in the program. The number of BDD nodes currently in use is printed on standard error each time the program performs garbage collection, if verbose-level is greater than zero. Also, as each evaluation is made, the number of BDD nodes representing the result is printed. An important number to look at is the number of BDD nodes representing the transition relation. It is very important to minimize this number. Iterations are used to solved the fixed point equations which characterize the CTL operators, and also to search for counterexamples. With each iteration, the number of BDD nodes used to represent the result is printed, as well as the number of corresponding states. Some of the options can improve performance. Experiment with them if the run time starts getting out of hand.

INTERACTIVE MODE

When the -int option is used, smv goes into interactive mode after the specifications in input-file has been checked. In this mode, the model described in input-file is used as a basis for interactive debugging and modifications. Moreover, specific states of the model can be reached using any trace created by smv in either interactive or non-interactive mode. A trace is a sequence of states corresponding to a possible execution of the model. Each trace produced by smv has a number, and the states are numbered within the trace. Trace number n has states numbered n.1, n.2, n.3, ... If additional traces are needed, say from state n.i, these traces are numbered n.i.1, n.i.2, n.i.3, ... Within these traces, the states are numbered n.i.m.1, n.i.m.2, n.i.m.3, ... In the interactive mode smv associates a current state with one of the states of the model. Most of the commands operate on the current state. The current trace is the trace the current state belongs to.

Interactive Commands

The following commands are recognized in interactive mode:

EVAL expression;: expression is evaluated in the current state. expression may be a CTL formula, and therefore, can produce a trace, from current state, to be used by later commands.
FAIR expression;: Add a new fairness constraint to the existing list of fairness constraints (See "The SMV System").
GOTO state;: Make state the current state.
INIT expression;: Add a constraint on the initial states. expression should hold for all initial states. This command is equivalent to the INIT declaration in input-file (See "The SMV System").
LET variable := expression;: Assign the value of expression, as evaluated in the current state, to variable. This command changes the current state. The value of all other variables in the new current state remains the same as it was in the old current state.
RESET ;: Discard all additions made to the model in interactive mode. This command cancels the effect of all FAIR, INIT, and TRANS commands issued in interactive mode.
SPEC expression;: The specification expression is evaluated in all of the initial states. This command is equivalent to the SPEC declaration in the input-file.
STEP ;: Move to the next state in the current trace.
TRANS expression;: Add expression to the constraints on the transition relation. This command is equivalent to the TRANS declaration in the input-file (See "The SMV System").

NEW FEATURES

Algorithmic additions

Conjuntive partitioning now splits "normal assignments" (invariant) as: well. Before SMV was building a monolithic BDD for the invariant, which could be very big.

Changes in the input language.

INVAR <formula>

A counterpart to TRANS, but uses only *current* state variables (NEVER use next(x) in it! Even if it parses...). To make the long story short, it has the same effect as using "normal" assignments (ASSIGN x := something(x,y,z);), but allows you to write it as a formula directly. Use it only if you know exactly what you are doing!

PRINT <hspec>

<hspec> ::= <spec> | hide <varlist>: <spec> | expose <varlist>: <spec>

Dumps on stdout a propositional formula obtained from the bdd for <hspec>. If used without -nof option, intersects the bdd with the set of reachable states. The <spec> is any valid CTL formula, and <varlist> is a non-empty list of variables that have to be excluded from the formula (hide) or whose complement have to be excluded (expose). There is no nesting of hide or expose. The "irrelevant" variables are being existentially quantified out and do not appear in the formula.

An example:

PRINT hide x,y: z < y & state in {1,2,3}

This feature can be useful for examining slices of your reachable state space to get a better idea of what your system actually does. One can use the formula as an initial state predicate to save on the computation of the reachable state space in further runs.

It is also valuable if SMV is used as a part of a bigger system to calculate the strongest invariants, for example.

Be careful with it, BDDs can be too big to be printed out! :)

!= and notin

Added disequality != and notin as the negation of in. Before one had to write "!(x = y)" or "!(x in {1,2})", now it's "x != y" and "x notin {1,2}" respectively.

next restrictions

Now only legal variable names are allowed in next() operator.

SIGNAL HANDLING

SMV now catches all the UNIX signals it can catch and prints the standard report (signal number, number of BDD nodes, memory usage etc.) before exiting. The only exceptions are:

Signal 10 (user defined 1)

toggles the dynamic variable reordering ON and OFF on the fly. This proved to be useful in one of my examples, however generally it just creates an ellusion of `more control' over SMV while it's running. The option -reordermaxsize is usually sufficient.

Signal 12 (user defined 2)

forces garbage collection next appropriate time. This is useful if you specified too big -gcfactor or -gclimit.

Note: signal numbers are different under Solaris. Currently SMV uses the standard numbers (not macros like SIGUSR1) for handling the signals. This may change in future when I figure out how to change the emacs interface accordingly.

Also, SMV writes its own process id in a file .smv-pid in the current directory. This allows SMV interfaces (like smv-mode.el for emacs) to send signals to SMV more conveniently. In particular, in emacs it makes the toggling of reordering just a key stroke.

If you turn off the dynamic reordering in the middle of the reordering process, by default SMV will finish the reordering, write the order file and quit. Use option `-noquit' to avoid that.

BUGS

Arguments of the wrong type specified for certain options and commands may produce cryptic (and fatal) error messages. See also the NEW file in the distribution for the up-to-date list of bugs.

AUTHOR

Kenneth L. McMillan, Carnegie Mellon University.
Kenneth.McMillan@cs.cmu.edu [may be outdated]

MAINTAINER

Sergey Berezin, Carnegie Mellon University.
Sergey.Berezin@cs.cmu.edu