Next: Invoking dzn verify
, Previous: Invoking dzn trace
, Up: The Dezyne command-line tools [Contents][Index]
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.
--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.