9.2 Invoking dzn code

While the simulator (See Invoking dzn simulate) can interpret Dezyne code directly, to create an executable program Dezyne uses a code generator.

This code generator, the command dzn code, generates compilable or runnable code for a Dezyne file, such as C++. Usually—i.e., except for trivial cases—this generated Dezyne code is combined with “handwritten” code in the target language to create a Dezyne application, See Code Integration.

dzn dzn-option… code option… FILE

The options can be among the following:

--calling-context=type

-c type

Generate an extra parameter of type for every event.

--help

-h

Display help on invoking dzn code, and then exit.

--import=dir

-I dir

Add directory dir to the import path.

--init=PROCESS

When generating mCRL2 code, use init PROCESS. For other language backends, this options is ignored.

--language=language

-l language

Generate code for language language.

--model=model

-m model

Generate a trivial main for model. This “generated main” can execute an event trace read from stdin, and writes a code trace to stderr. See Getting Started.

--no-comstaint

-C

Do not use a constraining process.

--no-non-compliance

-D

Do not generate ‘constraint-any’ processes.

--no-unreachable

-U

Do not generate tags for the unreachable code check.

--output=dir

-o dir

Write output to directory dir (use - for standard output).

--queue-size=size

-q size

When generating mCRL2 code, use component queue size size for verification, the default is 3. For other language backends, this options is ignored.

--queue-size-defer=size

When generating mCRL2 code, use defer queue size size for verification, the default is 2. For other language backends, this options is ignored.

--queue-size-external=size

When generating mCRL2 code, use extternal queue size size for verification, the default is 1. For other language backends, this options is ignored.

--shell=model

-s model

Generate thread-safe system shell for model model. See Thread-safe Shell.