0
@@ -40,9 +40,21 @@ namespace hst
0
         state_t  impl_state;
0
     };
0
 
0
+    struct failures_counterexample_t
0
+    {
0
+        trace_t     trace;
0
+        alphabet_t  acceptance;
0
+        state_t     spec_state;
0
+        state_t     impl_state;
0
+    };
0
+
0
     bool trace_refines(trace_counterexample_t &counter,
0
                        const normalized_lts_t &spec, state_t spec_source,
0
                        const lts_t &impl, state_t impl_source);
0
+
0
+    bool failures_refines(failures_counterexample_t &counter,
0
+                          const normalized_lts_t &spec, state_t spec_source,
0
+                          const lts_t &impl, state_t impl_source);
0
 }
0
 
0
 #endif // HST_ASSERTIONS_H

0
@@ -328,11 +328,6 @@ namespace hst
0
 
0
         bool check_pair(check_pair_cp pair) const
0
         {
0
-            /*
0
-             * TRACES: Check that impl's set of initial events is a
0
-             * subset of spec's (ignoring any τs in impl).
0
-             */
0
-
0
 #if DEBUG_REFINEMENT
0
             alphabet_t  spec_initials
0
                 (spec.state_events_begin(pair->spec),
0
@@ -400,6 +395,142 @@ namespace hst
0
         return refines<__trace_refinement, trace_counterexample_t>
0
             (counter, spec, spec_source, impl, impl_source);
0
     }
0
+
0
+
0
+    //------------------------------------------------------------------
0
+    // Failures refinement
0
+    //
0
+    // For a failures refinement, each (SPEC, IMPL) pair must satisfy
0
+    // the following condition:
0
+    //
0
+    //   ∀ α: accs(IMPL) • ∃ β: accs(SPEC) • α ⊇ β
0
+    //
0
+    // If this doesn't hold, then the counterexample consists of the
0
+    // trace seen so far, along with an alphabet α which failed the
0
+    // existential quantification.
0
+
0
+    struct __failures_refinement
0
+    {
0
+    protected:
0
+        const normalized_lts_t  &spec_norm;
0
+        const lts_t  &spec;
0
+        const lts_t  &impl;
0
+        failures_counterexample_t  &counter;
0
+
0
+        void construct_counterexample(alphabet_t &acceptance,
0
+                                      check_pair_cp pair) const
0
+        {
0
+            failures_counterexample_t  result;
0
+
0
+            for (check_pair_cp  current = pair;
0
+                 current->parent.get() != NULL;
0
+                 current = current->parent)
0
+            {
0
+                result.trace.push_front(current->inbound_event);
0
+            }
0
+
0
+            result.acceptance = acceptance;
0
+            result.spec_state = pair->spec;
0
+            result.impl_state = pair->impl;
0
+
0
+            std::swap(counter, result);
0
+        }
0
+
0
+    public:
0
+        __failures_refinement(const normalized_lts_t &_spec_norm,
0
+                              const lts_t &_impl,
0
+                              failures_counterexample_t &_counter):
0
+            spec_norm(_spec_norm),
0
+            spec(_spec_norm.normalized()),
0
+            impl(_impl),
0
+            counter(_counter)
0
+        {
0
+        }
0
+
0
+        bool check_pair(check_pair_cp pair) const
0
+        {
0
+            alphabet_set_cp  spec_accs =
0
+                spec.get_acceptances(pair->spec);
0
+
0
+            alphabet_set_cp  impl_accs =
0
+                impl.get_acceptances(pair->impl);
0
+
0
+#if DEBUG_REFINEMENT
0
+            cerr << "  Spec: " << *spec_accs << endl
0
+                 << "  Impl: " << *impl_accs << endl;
0
+#endif
0
+
0
+            for (alphabet_set_t::iterator ia_it = impl_accs->begin();
0
+                 ia_it != impl_accs->end();
0
+                 ++ia_it)
0
+            {
0
+#if DEBUG_REFINEMENT
0
+                cerr << "    Checking " << *ia_it << endl;
0
+#endif
0
+
0
+                /*
0
+                 * Verify that there is some SPEC acceptance that this
0
+                 * IMPL acceptance is a superset of.
0
+                 */
0
+
0
+                bool found_one = false;
0
+
0
+                for (alphabet_set_t::iterator sa_it = spec_accs->begin();
0
+                     sa_it != spec_accs->end();
0
+                     ++sa_it)
0
+                {
0
+#if DEBUG_REFINEMENT
0
+                    cerr << "      " << *ia_it << " ?>= "
0
+                         << *sa_it << endl;
0
+#endif
0
+
0
+                    if (is_superset(ia_it->begin(), ia_it->end(),
0
+                                    sa_it->begin(), sa_it->end()))
0
+                    {
0
+                        /*
0
+                         * Excellent, this SPEC acceptance is a subset
0
+                         * of the IMPL acceptance.  We can move on to
0
+                         * the next IMPL acceptance.
0
+                         */
0
+
0
+                        found_one = true;
0
+                        break;
0
+                    }
0
+                }
0
+
0
+                /*
0
+                 * If we didn't find any SPEC acceptances that were a
0
+                 * subset of this IMPL acceptance, so this IMPL
0
+                 * acceptance fails the refinement.
0
+                 */
0
+
0
+                if (!found_one)
0
+                {
0
+#if DEBUG_REFINEMENT
0
+                        cerr << "      Nope!  Refinement fails." << endl;
0
+#endif
0
+
0
+                    construct_counterexample(*ia_it, pair);
0
+                    return false;
0
+                }
0
+            }
0
+
0
+            /*
0
+             * All of the IMPL acceptances passed, so this pair is
0
+             * okay.
0
+             */
0
+
0
+            return true;
0
+        }
0
+    };
0
+
0
+    bool failures_refines(failures_counterexample_t &counter,
0
+                          const normalized_lts_t &spec, state_t spec_source,
0
+                          const lts_t &impl, state_t impl_source)
0
+    {
0
+        return refines<__failures_refinement, failures_counterexample_t>
0
+            (counter, spec, spec_source, impl, impl_source);
0
+    }
0
 }
0
 
0
 #endif // HST_CSP_INTERLEAVE_CC

0
@@ -2,6 +2,7 @@
0
 # Q = a -> Q
0
 #
0
 # assert P [T= Q
0
+# assert P [F= Q
0
 
0
 event a;
0
 event b;

0
@@ -2,6 +2,7 @@
0
 # Q = a -> b -> Q
0
 #
0
 # assert P [T= Q
0
+# assert P [F= Q
0
 
0
 event a;
0
 event b;

0
@@ -2,6 +2,7 @@
0
 # Q = a -> b -> Q
0
 #
0
 # assert P [T= P
0
+# assert P [F= P
0
 
0
 event a;
0
 event b;

0
@@ -2,6 +2,7 @@
0
 # Q = a -> b -> Q
0
 #
0
 # assert not Q [T= P
0
+# assert not Q [F= P
0
 
0
 event a;
0
 event b;

0
@@ -2,6 +2,7 @@
0
 # P2 = up -> down -> up -> down -> P2
0
 #
0
 # assert P1 [T= P2
0
+# assert P1 [F= P2
0
 
0
 event up;
0
 event down;

0
@@ -2,6 +2,7 @@
0
 # P2 = up -> down -> up -> down -> P2
0
 #
0
 # assert P2 [T= P1
0
+# assert P2 [F= P1
0
 
0
 event up;
0
 event down;

0
@@ -2,6 +2,7 @@
0
 # Q = (a -> STOP) [] (c -> a -> STOP)
0
 #
0
 # assert (P || Q) [T= (a -> STOP)
0
+# assert (P || Q) [F= (a -> STOP)
0
 
0
 event a;
0
 event b;

0
@@ -2,6 +2,7 @@
0
 # Q = (a -> STOP) [] (c -> a -> STOP)
0
 #
0
 # assert (a -> STOP) [T= (P || Q)
0
+# assert (a -> STOP) [F= (P || Q)
0
 
0
 event a;
0
 event b;

0
@@ -3,6 +3,8 @@ set(TESTS
0
   00-basic2
0
   00-basic3
0
   00-basic4
0
+  00-basic5
0
+  00-basic6
0
   80-roscoe-p40-a
0
   80-roscoe-p40-b
0
   80-roscoe-p52-a
0
@@ -12,7 +14,7 @@ set(TESTS
0
 # Copy the test data from the source directory to the build directory.
0
 
0
 foreach(_test ${TESTS})
0
-  foreach(_ext csp0 traces)
0
+  foreach(_ext csp0 traces failures)
0
     configure_file(
0
       ${CMAKE_CURRENT_SOURCE_DIR}/${_test}.${_ext}
0
       ${CMAKE_CURRENT_BINARY_DIR}/${_test}.${_ext}
0
@@ -32,3 +34,13 @@ foreach(_test ${TESTS})
0
        cmp - ${_test}.traces"
0
   )
0
 endforeach(_test)
0
+
0
+add_executable(test-failures-refinement test-failures-refinement.cc)
0
+target_link_libraries(test-failures-refinement hst)
0
+foreach(_test ${TESTS})
0
+  add_test(
0
+    refinement:failures:${_test}
0
+    bash -c "./test-failures-refinement < ${_test}.csp0 |
0
+       cmp - ${_test}.failures"
0
+  )
0
+endforeach(_test)

0
@@ -39,6 +39,8 @@ int main()
0
 
0
     if (!cin.fail())
0
     {
0
+        csp.normalized_lts()->clear(TRACES);
0
+
0
         state_t  SPEC;
0
 
0
         {