6.2 Verification Counter Examples

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. This implies there is an inconsistency in the behavior of the component and its interface, the contract is violated. This can either be fixed by a change to the interface behavior contract or by changing the component behavior.