Previous: , Up: Verum-Dezyne View Commands   [Contents][Index]


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 optionFILE

Running

ide verify examples/compliance_provides_bool.dzn

will have the trace.html view show

images/ide-verify-compliance_provides_bool

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.

--no-constraint
-C

Do not use a constraining process.

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

--no-interfaces

Do not verify a model’s interfaces.

--no-unreachable
-U

Disable the unreachable code check. For large models the unreachable code check may have a serious performance impact.

--queue-size=size
-q size

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

--queue-size-defer=size

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

--queue-size-external=size

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

--verbose
-v

Be more verbose, show progress.


Previous: , Up: Verum-Dezyne View Commands   [Contents][Index]