Hst hst

Failures refinement

This patch adds support for checking failures refinement. The Refiner

class checks that each (SPEC, IMPL) pair satisfies the following

condition:

∀ α: accs(IMPL) • ∃ β: accs(SPEC) • α ⊇ β

An acceptance is the complement of a refusal, so this is equivalent

to:

∀ α: refs(IMPL) • ∃ β: refs(SPEC) • α ⊆ β

The refs() function only represents the maximal refusals that are

actually stored in the LTS. This corresponds to an allrefs() function

that contains all of refusals, which are subset closed. Thus, the

condition also ensures that

∀ α: allrefs(IMPL) • ∃ β: allrefs(SPEC) • α = β

or, in other words, that

allrefs(IMPL) ⊆ allrefs(SPEC)

Lighthouse: [#3 state:resolved]

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