Hst hst

Refactoring refinement code to support multiple semantic models

As another step towards implementing failures refinement, this patch

refactors the refinement code to have better support for different

semantic models. Part of the refinement code is identical regardless

of semantic model. Mostly, this is the scaffolding of the

breadth-first search, where we examine each pair of (SPEC, IMPL)

states from the original processes. The only model-specific code is

the part that checks whether a particular (SPEC, IMPL) pair is part of

a valid refinement, and that constructs a counterexample object if

it's not.

This new design has the model-independent code as a templated

function. There are two template parameters: Refiner and

Counterexample. Counterexample is the type of the counterexample

object that's created if the refinement fails. The refine function

does not need to know any details of this type. The Refiner type

contains the model-specific code for checking a pair of states and

constructing a Counterexample object if needed. The API of the

Refiner object is described in the refine.cc file.

With this modification, we should be able to implement failures

refinement simply by defining a new Refiner class.

Lighthouse: [#3]

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