Next: , Previous: , Up: The Dezyne command-line tools   [Contents][Index]

9.6 Invoking dzn lts

The dzn lts command can be used to manipulate and query a labeled transition system (lts) in Aldebaran (aut) format (See Invoking dzn graph, See Invoking dzn verify, See Invoking dzn traces).

dzn dzn-option… lts option… [FILE]…

The options can be among the following:


Rewrite mCRL2 labels to Dezyne, optionally remove prefix as specified with --prefix.


Detect deadlock in lts (after introduction of failures) and produce a witness.


Remove edges leading to illegal (in combination with --failures).


Introduce a failure for each ’optional’ event into the lts.


Display help on invoking dzn lts, and then exit.


Detect whether lts contains <illegal> labels.


Detect tau-loops in lts and produce a witness.

-n label[,label…]

Detect whether lts is deterministic by detecting multiple edges of label from a single state, and produce a witness.


Optional prefix for --cleanup

-t event[,event…]

Hide all events from lts.


Exclude given events from ’--tau’ list.


Report each error including its trace (witness) on a single line.