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:

--cleanup
-c

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

--deadlock
-d

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

--exclude-illegal

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

--failures
-f

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

--help
-h

Display help on invoking dzn lts, and then exit.

--illegal
-i

Detect whether lts contains <illegal> labels.

--livelock
-l

Detect tau-loops in lts and produce a witness.

--deterministic-labels=label[,label…]
-n label[,label…]

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

--prefix=prefix

Optional prefix for --cleanup

--tau=event[,event…]
-t event[,event…]

Hide all events from lts.

--exclude-tau=event[,event…]

Exclude given events from ’--tau’ list.

--single-line
-s

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