Changeset [4754d168e43124cb467c6c82b6333905bd208a7c] by Douglas Creager
Revision 4754d168e43124cb467c6c82b6333905bd208a7c,
committed by Douglas Creager
· May 31st, 2008 @ 06:47 PM
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]
28 changed files
-
A
build-scripts/save-refinement-test -
A
tests/refinement/00-basic1.failures -
A
tests/refinement/00-basic2.failures -
A
tests/refinement/00-basic3.failures -
A
tests/refinement/00-basic4.failures -
A
tests/refinement/00-basic5.csp0 -
A
tests/refinement/00-basic5.failures -
A
tests/refinement/00-basic5.traces -
A
tests/refinement/00-basic6.csp0 -
A
tests/refinement/00-basic6.failures -
A
tests/refinement/00-basic6.traces -
A
tests/refinement/80-roscoe-p40-a.failures -
A
tests/refinement/80-roscoe-p40-b.failures -
A
tests/refinement/80-roscoe-p52-a.failures -
A
tests/refinement/80-roscoe-p52-b.failures -
A
tests/refinement/test-failures-refinement.cc -
M
include/hst/assertions.hh -
M
src/assertions/refine.cc -
M
tests/refinement/00-basic1.csp0 -
M
tests/refinement/00-basic2.csp0 -
M
tests/refinement/00-basic3.csp0 -
M
tests/refinement/00-basic4.csp0 -
M
tests/refinement/80-roscoe-p40-a.csp0 -
M
tests/refinement/80-roscoe-p40-b.csp0 -
M
tests/refinement/80-roscoe-p52-a.csp0 -
M
tests/refinement/80-roscoe-p52-b.csp0 -
M
tests/refinement/CMakeLists.txt -
M
tests/refinement/test-traces-refinement.cc