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.

--jitty

-j

Run lts2lps with --rewriter=jittyc. The jittyc rewriter can be much faster but it adds a performance penalty of a couple of minutes and it needs a functional compilation environment. For large models this may result in better performance.

--lts

-l

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

--model=model

-m model

Generate traces for model model.

--no-comstaint

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