VERIFY(1)  Local Manual  VERIFY(1) 
NAME
verify — modelcheck a system of communicating machinesSYNOPSIS
verify  [option ...] [scmfile] 
DESCRIPTION
The verify tool reads the model given in the specified scmfile and modelchecks it. If scmfile is omitted, the model is read from the standard input.The model contains the description of a system of communicating machines along with, optionally, the specification of a set of bad configurations. See scm(5) for a description of the scm input language.
Upon succesful termination, verify either reports that the model is safe (if no bad configuration is reachable), or provides a counterexample trace (leading to some bad configuration).
Note that, depending on the input model and on the options that are used, verify may abort, or compute indefinitely. This problem cannot be avoided due to the undecidability of the modelchecking problem for systems of communicating machines.
OPTIONS
Main Options
 mcengine engine

Specifies the main algorithm used for modelchecking. The following engines are available:
 absint
 Static analysis based on abstract interpretation.
 armc
 Abstract regular modelchecking.
 cegar
 Counterexample guided abstraction refinement. This algorithm maintains an abstract graph whose nodes form a partition of the model's configuration space. Refinement consists in splitting abstract nodes visited by a spurious counterexample, according to a generated trace invariant. This is the default.
 lart
 Lazy abstraction refinement tree. This algorithm builds an abstract reachability tree, and maintains node covering information to truncate the tree. Branches leading to bad configurations are refined by strengthening nodes according to a generated trace invariant.
 tcengine engine

Specifies the tracechecking algorithm used by some modelcheckers. Here, tracechecking consists in analyzing a given abstract counterexample to determine whether it is feasible or spurious, and, in the latter case, provide a trace invariant “explaining” spuriousness. The following engines are available:
 apinvbwd
 Perform an adaptive extrapolated symbolic pre computation along the abstract counterexample, starting from the failure abstract node. This is the default.
 apinvfwd
 Reversed version of apinvbwd (uses post).
 upinvfwd
 Perform a uniform extrapolated symbolic post computation along the abstract counterexample.
 upinvbwd
 Reversed version of upinvfwd (uses pre).
 kmin start

The extrapolation operator is parameterized by a nonnegative integer k. This option specifies the starting value of k. The model/tracechecking algorithms first try with k = start (which produces the coarsest overapproximation) and then iteratively increase k until the analysis is precise enough (or k becomes greater than the bound specified by kmax). The start must be a nonnegative integer. The default is 0.
As an exception (a hack), it is also possible to specify a start of 1 (see option extrapolation below).
 kmax stop
 Specifies the largest value that model/tracechecking algorithms may use for the extrapolation parameter k. The stop must be a nonnegative integer. The default is 2.
 tcdiscardstates
 Removes abstract states from the trace before passing it to the tracechecking engine. With this option, abstract counterexamples are more likely to be feasible. But, for spurious counterexamples, trace invariant generation may require more precision (i.e., a higher extrapolation parameter).
 tcvalidate
 Validates each result provided by the tracechecking engine, and print an error message when validation fails.
 limit limit

Limit the number of modelchecker iterations to limit. Note that iterations are not comparable between modelchecking engines. The limit must be a nonnegative integer. OCaml's
max_int
is used by default.  novalidation
 The modelchecking engine returns either a safe inductive invariant, or a counterexample trace. By default, this result is validated by a simple, independent algorithm. This option disables this validation.
 statistics
 Upon succesful termination, verify displays detailed statistics about execution time and memory consumption.
Scm Wrapper Options
 scmrel method

The symbolic onestep binary reachability relation of the model is not (directly) provided by the Scm library. This option specifies the method used to compute this binary relation. The following methods are supported:
 post
 Use the symbolic post operator of the Scm library.
 pre
 Use the symbolic pre operator of the Scm library.
 mixed
 Use post for send actions and pre for receive actions. This is the default.
 extrapolation operator

Specifies the extrapolation operator used for overapproximation of queue decision diagrams. The overapproximations provided by the Scm library are based on state equivalences. The following extrapolation operators are available:
 bisimfwd
 Forward kdepth bisimulation equivalence. This is the default.
 bisimbwd
 Backward kdepth bisimulation equivalence.
 bisimboth
 Conjunction of the two previous equivalences.
 langfwd
 Forward kdepth language equivalence.
 langbwd
 Backward kdepth language equivalence.
 langboth
 Conjunction of the two previous equivalences.
 identity
 Identity function (no overapproximation).
As an exception, the extrapolation for k = 1 is the same for all operators, and consists in merging all states of the queue decision diagram. In other words, this extrapolation is equal to the 0depth bisimulation/language equivalence without state coloring.
 extrapolcoloring coloring

Specifies the state coloring applied by the extrapolation operator on queue decision diagrams. The state equivalence induced by this coloring defines the 0depth equivalence (see extrapolation). The following state colorings are available:
 final
 Distinguish final states from the others (2 colors).
 init
 Distinguish initial states from the others (2 colors).
 both
 Conjunction of the two previous equivalences (4 colors).
 none
 Merge all states (1 color).
 auto
 Behave as final for forward extrapolations, as init for backward extrapolations, and as both for extrapolations that use both directions. This is the default.
 channelpolicy policy

Channels in an scm model can be either perfect or lossy (see scm(5)). This option allows to override the reliability policy of the channels. The following reliability policies are supported:
 alllossy
 Make all channels lossy.
 allperfect
 Make all channels perfect.
 normal
 Keep the policy specified in the scm input. This is the default.
Cegar Options
 graphexploration search

Specifies the exploration algorithm used to find a counterexample in the abstract graph. The following graph search algorithms are supported:
 fwddfs
 Forward depthfirst search.
 fwdbfs
 Forward breadthfirst search.
 bwddfs
 Backward depthfirst search.
 bwdbfs
 Backward breadthfirst search.
 mixed
 Use only breadthfirst search and select the direction with the smallest set of initial nodes. This is the default.
 graphrefinement method

When an abstract node is split into n refined nodes, the abstract edges that enter or leave this node must be refined. This option specifies the method used to compute the refined edges. The following methods are supported:
 rel
 Use the model's symbolic onestep binary reachability relation rel. This method requires, for each edge refinement, n rel computations.
 postpre
 Use the model's symbolic post and pre operators. This method requires, for each edge refinement, 1 post/pre computation and n emptiness tests. This is the default.
Lazy Abstraction Options
 treeexploration exploration

Specifies the exploration strategy used to build the abstract reachability tree. The following exploration strategies are supported:
 dfs
 Depthfirst exploration.
 bfs
 Breadthfirst exploration. This is the default.
 notreepruning
 By default, nodes being refined with an empty region are removed from the tree. This option disables this pruning.
APInv Options
 safeapproximation algorithm

Adaptive trace invariant generation relies on a simplification procedure that, given a pair (r1, r2) of disjoint regions, returns an overapproximation of r1 that is still disjoint from r2. This option selects the algorithm used for the computation of this safe overapproximation. The following algorithms are available:
 split
 Given (r1, r2), return the extrapolation of r1 for the smallest parameter k that leads to an empty intersection with r2. This is the default.
 cosplit
 Given (r1, r2), return the complement of the region obtained with split on (r2, r1).
Logging Options
 columns width

Use width columns for prettyprinting. In other words, set the value of the prettyprinter's right margin to width (in characters). The default is the value of the environment variable COLUMNS if set, or
78
otherwise.  boxdepth depth

Set the prettyprinter's box depth to depth. Boxes nested deeper than depth are printed as an ellipsis. OCaml's
max_int
is used by default.
AUTHORS
The verify tool is mainly written, maintained and tested by:
See the AUTHORS file in the source distribution for the full list of contributors.
Web site: ../../../projects/mcscm/wiki.html
CAVEATS
Numerical values held by messages or local variables are currently ignored by verify. Conditions in transitions and bad configurations are discarded and assumed to be true.
 Assignments in transitions are ignored.
These rules guarantee that the analysis performed by verify is “safetyconservative”.
BUGS
Please visit the following page for bug reports and feature requests: ../../../projects/mcscm/issuesACKNOWLEDGEMENTS
The verify tool is programmed in Objective Caml and uses several 3rdparty libraries: Camllib, Fixpoint, LatticeAutomata, and Scm. By and . Licensed under the LGPL. Web site: http://gforge.inria.fr/projects/bjeannet/.
October 12, 2011  Linux 3.0.01amd64 