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.
--output=dir
-o dir
Write trace files to directory dir.
--queue-size=size
-q size
Use queue size size for generation, the default is 3
.
--traces
-t
Generate trace files, this is the default. Using --traces will generate trace files even when --lts is used.