9.10 Invoking dzn traces

The dzn traces command generates an exhaustive set of event traces or trails for a behavioral Dezyne model. It can also be used to generate an lts in Aldebaran format (See Invoking dzn lts, See Invoking dzn graph, See Invoking dzn verify).

Under the hood, dzn traces uses dzn code and mCRL2.

dzn dzn-option… traces option… FILE

The options can be among the following:

--flush

-f

Include <flush> events in trace.

--help

-h

Display help on invoking dzn traces, and then exit.

--illegal

-i

Include traces that lead to an illegal.

--import=dir

-I dir

Add directory dir to the import path.

--lts

-l

Instead of generating trace files, generate an lts in Aldebaran format.

--model=model

-m model

Generate traces for model model.

--no-constraint

-C

Do not use a constraining process.

--no-non-compliance

-D

Report deadlock upon a non-compliance error.

--output=dir

-o dir

Write trace files to directory dir.

--queue-size=size

-q size

Use component queue size size for generation, the default is 3.

--queue-size-defer=size

Use defer queue size size for trace generation, the default is 2.

--queue-size-external=size

Use external queue size size for trace generation, the default is 1.

--traces

-t

Generate trace files, this is the default. Using --traces will generate trace files even when --lts is used.