DragonFly On-Line Manual Pages
SMV(1) DragonFly General Commands Manual SMV(1)
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.
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)