Changeset [04ffccc1b5572d80415bac200d0544576e8078b9] by Douglas Creager

Adding counterexamples to the traces refinement check

Instead of just giving a yes/no answer for a traces refinement, we now

provide a counterexample when the refinement fails. The

counterexample consists of a trace of visible events, after which the

IMPL process can perform some event that SPEC cannot perform. (This

event is provided in the counterexample, as well.) There will often

me many possible counterexamples for a particular failed refinement;

the current implementation uses a breadth-first search, so we know

that the returned counterexample will be one with the smallest trace.

If there are many counterexamples of this length, an arbitrary one

will be returned.

The csp0 utility has also been modified to display this

counterexample, as have the traces refinement test cases.

As currently defined, the counterexample might not be especially

useful, since it only includes visible events. If the high-level SPEC

and IMPL processes involve a lot of hiding, then you won't actually be

able to see any useful detail in the counterexample trace. We'll need

to add some logic for drilling down into the syntax tree of a CSP

process to fix this.

http://github.com/dcreager/hst/c...