9.11 Invoking 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-op¹¹.

--no-comstaint

-C

Do not use a constraining process.

--no-interfaces

Do not verify a model’s interfaces.

--no-non-compliance

-D

Report deadlock upon a non-compliance error.

--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.