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.

When generating code for C++, a dependency file is generated as <output-directory>/.deps/<base>.dzn.dep for use by the build system.

dzn dzn-option… code option… FILE…

If FILE is a directory, code is generated for all .dzn files in that directory.

The options can be among the following:

--calling-context=type

-c type

Generate an extra parameter of type for every event.

--touch-empty-files

-t

When generating C++ code, if an execution unit is empty, touch it, creating an empty file for consistency. This may remove an irregularity from the build system.

--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-constraint

-C

Do not use a constraining process.

--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 external 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. This option can be used multiple times. See Thread-safe Shell.