9.8 Invoking dzn simulate

The dzn simulate command starts a simulation run.

Under the hood, dzn simulate uses the Dezyne VM. The simulator can be used to explore Dezyne models (interfaces, components, and systems), and to interpret error traces (witnesses) from the verification engine (See Getting Started). It shows code locations, state, and state transitions and produces friendly error messages. The simulator and verification both report the same errors (See Formal Verification). The simulator, however, only reports errors that it encounters while interpreting a specific event trace. The verifier performs an exhaustive search for errors but only produces a witness and does not report any context information. Its syntax is:

dzn dzn-option… simulate option… FILE

The options can be among the following:

--format=format

-f format

Print trace in format format; one of diagram, event, or trace. The default is trace.

--help

-h

Display help on invoking dzn simulate, and then exit.

--import=dir

-I dir

Add directory dir to the import path.

--internal

-i

Display internal events when using the diagram trace format.

--locations

-l

Display locations in the trace, this implies --format=trace.

--model=model

-m model

Start simulating model. The default is the most “interesting” model.

--no-compliance

-C

Do not run the compliance check.

--no-deadlock

-D

Do not run the deadlock check at the end of the trail (EOT).

--no-interface-determinism

Do not run the observable non-determinism check on interfaces.

--no-interface-livelock

Do not run the interface livelock check at the end of the trail (EOT).

--no-queue-full

-Q

Do not run the external queue-full check at the end of the trail (EOT).

--no-refusals

-R

Do not run the compliance check for the failures model refusals check at the end of the trail (EOT).

--queue-size=size

-q size

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

--queue-size-defer=size

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

--queue-size-external=size

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

--strict

-s

Use strict matching of trail, i.e., the trail must contain all observable events.

--trail=trail

-t trail

Use trail trail. The default is to read from stdin.

--verbose

-v

Display non-communication steps in the trace, this implies --format=trace, --locations.