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-op11.
--no-constraint
-C
Do not use a constraining process.
--no-interfaces
Do not verify interfaces.
--no-unreachable
-U
Disable the unreachable code check. For large models the unreachable code check may have a serious performance impact.
--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 component queue size size for verification, the default is
3
.
--queue-size-defer=size
Use defer queue size size for verification, the default is
2
.
--queue-size-external=size
Use external queue size size for verification, the default is
1
.
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.
Previous: Invoking dzn traces
, Up: The Dezyne command-line tools [Contents][Index]