Next: Interpreting Verification Errors, Previous: Verification Checks and Errors, Up: Formal Verification [Contents][Index]
A verification error does not only show the error it has detected, it
also shows where it occurs. Where an error occurs is specified
by means of a counter example, or an event trace.
Verifying
interface ihello
{
in void hello ();
in void world ();
behavior
{
on hello: {}
}
}
component illegal_requires
{
provides ihello h;
requires ihello w;
behavior
{
on h.hello (): w.world ();
}
}
gives:
$ dzn verify doc/examples/illegal-requires.dzn model: hello h.hello w.hello <illegal>
at the end of running this trace, an illegal action occurs.