SMV(1)SMV(1)NAMEsmv - symbolic model verifier
SYNOPSISsmv [options] [input-file]
DESCRIPTIONsmv is a program that uses a symbolic model checking algorithm to eval‐
uate formulas of CTL (Computational Tree Logic - a branching time tem‐
poral 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 prac‐
tically 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 opera‐
tions. 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 per‐
formance 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 mem‐
ory.
-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 counterex‐
ample.
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 parti‐
tions. 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 (`con‐
strain'). 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 sup‐
posed to take even less memory. Has a real effect only with -cp
option.
-intsmv 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. Set‐
ting 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 over‐
rides 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 vari‐
able to be reordered. The reorder routine will skip the vari‐
ables 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 rela‐
tional products with -cp option. My observation is that inter‐
mediate 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 collec‐
tion 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 rela‐
tion is total, and if not, prints a deadlock state. Very useful
if you are using TRANS or INVAR to specify the transition rela‐
tion. Note, that SMV can not check the totalness of the transi‐
tion 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 coun‐
terexamples 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 ORDERINGsmv uses Boolean Decision Diagrams (BDDs) to represent sets and rela‐
tions 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 tra‐
versed 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 pro‐
gram performs garbage collection, if verbose-level is greater than
zero. Also, as each evaluation is made, the number of BDD nodes repre‐
senting 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 num‐
ber, 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 invari‐
ant, 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 reach‐
able
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 sys‐
tem 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 stan‐
dard 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 gener‐
ally it just creates an ellusion of `more control' over SMV
while it's running. The option -reordermaxsize is usually suf‐
ficient.
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 particu‐
lar, 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.
SEE ALSO
The SMV system,
Symbolic Model Checking - an approach to the state explosion problem by
K. McMillan, CMU-CS-92-131
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
SMV 2.5 March 23, 1999 SMV(1)
