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.