Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages

  
 
  

home | help
SMV(1)			    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 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 in-
       put).   The  language for describing the	model is a simple parallel as-
       signment.  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  de-
	      fault, 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 ev-
	      ery 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 re-
	      maining 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  be-
	      ing  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.

       -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.  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 or-
	      dering 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  re-
	      sults.   It  is always recommended to use	-oo instead of -o, un-
	      less 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 re-
	      order 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 re-
	      ordering.	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.  De-
	      fault is n = 2000.

       -reorderfactor n
	      Reorder  when  the  BDD size exceeds the size after the last re-
	      ordering 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 re-
	      ordering 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 ORDERING
       smv  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  or-
       dering.	Instead, the variables appear in the BDDs in the same order in
       which they are declared in the program.	This means that	variables  de-
       clared  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 ar-
       range  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-in-
       teractive  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  re-
	      mains 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  in-
	      put-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"  as-
	      signments	 (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  re-
	      ordering	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)

NAME | SYNOPSIS | DESCRIPTION | OPTIONS | VARIABLE ORDERING | INTERACTIVE MODE | NEW FEATURES | SIGNAL HANDLING | SEE ALSO | BUGS | AUTHOR | MAINTAINER

Want to link to this manual page? Use this URL:
<https://www.freebsd.org/cgi/man.cgi?query=smv&sektion=1&manpath=FreeBSD+12.0-RELEASE+and+Ports>

home | help