9.3 Invoking dzn graph

The dzn graph command can be used to generate different graphs from a Dezyne model.

dzn dzn-option… graph option… FILE

The options can be among the following:

--backend=type

-b type

Generate a diagram using backend type; one of dependency, lts, state, or system and write it to standard output. The default is system.

The state diagram can simplified using options --hide and --remove.

Under the hood, lts and state use the Dezyne VM. LTSs can be queried and manipulated using dzn lts (Invoking dzn lts) and the mCRL2 tooling.

Note: Generating an LTS for a large component or system using the VM can be very time-consuming. For generating an LTS using the verification engine, see (Invoking dzn verify) and (Invoking dzn traces).

--format=format

-f format

Print trace in format format; one of aut, dot, or json. For --lts the default is aut, for other formats the default is dot.

Note: The json can be processed by Dezyne-P5 to draw state and system diagrams in a browser.

--help

-h

Display help on invoking dzn graph, and then exit.

--hide=hide

-H hide

Generate a state diagram and hide hide from the transitions; one of labels (hide everything), actions or returns.

--import=dir

-I dir

Add directory dir to the import path.

--model=model

-m model

Generate graph for model model. The default is to use the most “interesting” model.

--queue-size=size

-q size

Use component queue size size for exploration, the default is 3.

--queue-size-defer=size

Use defer queue size size for exploration, the default is 2.

--queue-size-external=size

Use external queue size size for exploration, the default is 1.

--remove=vars

-R vars

Generate a state diagram and remove variables from nodes remove; one of ports or extended.

ports Hides the state of the component’s or system’s ports, extended hides the interface’s or component’s extended state, i.e., all but the main (first) state variable and implies ports.