Previous: , Up: Formal Verification   [Contents][Index]

6.3 Interpreting Verification Errors

Understanding why a certain verification error occurs, or how to fix it, is not always easy. The simulator can help to interpret the error and identify what is going on (See Invoking dzn simulate): It can show the source locations where the error occurs and the state the interface(s) and/or the component(s) are in.

The simulator can interpret the counter example from the verifier:

$ dzn verify doc/examples/illegal-requires.dzn \
  | dzn simulate doc/examples/illegal-requires.dzn
error: illegal action performed in model illegal_requires
(header ((h) ihello provides) ((sut) illegal_requires component) ((w) ihello requires))
(state ((h)) ((sut)) ((w)))
doc/examples/illegal-requires.dzn:6:3: error: illegal
<external>.h.hello -> ...
... -> sut.h.hello -> ...
... -> <external>
(state ((h)) ((sut)) ((w)))
doc/examples/illegal-requires.dzn:6:3: error: illegal
(trail "h.hello" "" "<illegal>")
(labels "h.hello" "")