4.2.11 Invoking ide verify

The ide verify command runs the dzn verify command. If verification errors are found, the ide daemon provides a sequence view that can be viewed with a browser.

ide ide-option… verify option… FILE

Running

ide verify examples/compliance_provides_bool.dzn

will have the trace.html view show

Note: The trace view, which is generated by the simulator, will only show compliance errors when the verificator found a compliance error. This means that when the model has errors such as deadlock, illegal, non-determinism, missing reply, second reply, queue full, or range error, any compliance error is ignored.

The options can be among the following:

--help

-h

Display help on invoking ide verify, and then exit.

--import=dir

-I dir

Add directory dir to import path.

--model=model

-m model

Limit verification to model, and for behavioral component model, to its interfaces.

Note: Verification cannot be applied to system components models; verifying a system model is a no-op.

--queue-size=size

-q size

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

--verbose

-v

Be more verbose, show progress.