Previous: Verification Counter Examples, Up: Formal Verification [Contents][Index]
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 sut.w.world -> ... ... -> <external>.w.world <illegal> (state ((h)) ((sut)) ((w))) doc/examples/illegal-requires.dzn:6:3: error: illegal (trail "h.hello" "w.world" "<illegal>") (labels "h.hello" "h.world") (eligible)