Previous: Invoking dzn traces, Up: The Dezyne command-line tools [Contents][Index]
dzn verify
The dzn verify
command exhaustively checks a Dezyne file for
verification errors in Dezyne models. See Formal Verification.
dzn dzn-option… verify option… FILE
The options can be among the following:
--all
-a
Show all errors, i.e., keep going after finding an error. By default, verification stops after finding a verification error.
--help
-h
Display help on invoking dzn verify
, and then exit.
--import=dir
-I dir
Add directory dir to the import path.
--model=model
-m model
Limit verification to model, and for a behavioral component model, to its interfaces.
Note: Verification cannot be limited to
system
component models; verifying a system model is a no-op10.
--no-interface-determinism
Do not run the observable non-determinism check on interfaces.
--out=format
Run a partial verification pipeline to produce format.
Interesting formats are mcrl2
, aut
,
aut-dpweak-bisim
, aut-weak-trace
, and
aut+provides-aut
. Use --out=help for a full list.
The verification pipeline starts by generating mCRL2
code, which
is converted into an lps and then into an lts
(See Invoking dzn lts). The lts is then manipulated further.
Using the --debug on dzn
(See Invoking dzn) shows
the pipelines with all their commands that are being used, ready for
use on the command line.
--queue-size=size
-q size
Use queue size size for verification, the default is 3
.
The compositional property
of the Dezyne component-based programming paradigm guarantees that the
verification of a system
component model amounts to the
verification of all its interface
models and behavioral
component
models.