9.9 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:

--no-deadlock

-D

Do not run the deadlock check.

--no-interface-determinism

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

--no-refusals

-R

Do not run the compliance check for the failures model refusals check.

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

--queue-size=size

-q size

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

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