0
@@ -32,7 +32,16 @@ using namespace std;
0
 
0
 namespace hst
0
 {
0
-    bool refines(const normalized_lts_t spec, state_t spec_source,
0
+    struct trace_counterexample_t
0
+    {
0
+        trace_t  trace;
0
+        event_t  event;
0
+        state_t  spec_state;
0
+        state_t  impl_state;
0
+    };
0
+
0
+    bool 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
 

0
@@ -24,6 +24,7 @@
0
 #ifndef HST_TYPES_HH
0
 #define HST_TYPES_HH
0
 
0
+#include <deque>
0
 #include <tr1/memory>
0
 
0
 #include <hst/intset.hh>
0
@@ -68,6 +69,10 @@ namespace hst
0
         }
0
     };
0
 
0
+    typedef deque<event_t>             trace_t;
0
+    typedef shared_ptr<trace_t>        trace_p;
0
+    typedef shared_ptr<const trace_t>  trace_cp;
0
+
0
     typedef pair<state_t, state_t>           state_state_t;
0
     typedef shared_ptr<state_state_t>        state_state_p;
0
     typedef shared_ptr<const state_state_t>  state_state_cp;

0
@@ -44,35 +44,96 @@ using namespace std;
0
 
0
 namespace hst
0
 {
0
-    typedef pair<state_t, state_t>  check_pair_t;
0
+    struct check_pair_t;
0
+    typedef shared_ptr<check_pair_t>        check_pair_p;
0
+    typedef shared_ptr<const check_pair_t>  check_pair_cp;
0
+
0
+    struct check_pair_t
0
+    {
0
+        state_t  spec;
0
+        state_t  impl;
0
+        event_t  inbound_event;
0
+        check_pair_cp  parent;
0
+
0
+        check_pair_t(state_t _spec, state_t _impl):
0
+            spec(_spec),
0
+            impl(_impl),
0
+            inbound_event(HST_ERROR_EVENT)
0
+        {
0
+        }
0
+
0
+        check_pair_t(state_t _spec, state_t _impl,
0
+                     event_t _inbound_event,
0
+                     check_pair_cp _parent):
0
+            spec(_spec),
0
+            impl(_impl),
0
+            inbound_event(_inbound_event),
0
+            parent(_parent)
0
+        {
0
+        }
0
+
0
+        bool operator == (const check_pair_t &other) const
0
+        {
0
+            return (spec == other.spec) && (impl == other.impl);
0
+        }
0
+    };
0
 
0
     struct check_pair_t_hasher
0
     {
0
         unsigned long operator () (const check_pair_t &pair) const
0
         {
0
-            return (pair.first * 33) + pair.second;
0
+            return (pair.spec * 33) + pair.impl;
0
+        }
0
+
0
+        unsigned long operator () (check_pair_cp pair) const
0
+        {
0
+            return (pair->spec * 33) + pair->impl;
0
         }
0
+
0
     };
0
 
0
+    static
0
+    void construct_counterexample(trace_counterexample_t &counter,
0
+                                  event_t event,
0
+                                  check_pair_cp pair)
0
+    {
0
+        trace_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.event = event;
0
+        result.spec_state = pair->spec;
0
+        result.impl_state = pair->impl;
0
+
0
+        std::swap(counter,result);
0
+    }
0
+
0
     typedef judy_set_l<check_pair_t, check_pair_t_hasher>
0
         check_pair_set_t;
0
 
0
-    bool refines(const normalized_lts_t spec_norm, state_t spec_source,
0
+    bool refines(trace_counterexample_t &counter,
0
+                 const normalized_lts_t spec_norm, state_t spec_source,
0
                  const lts_t impl, state_t impl_source)
0
     {
0
         const lts_t  &spec = spec_norm.normalized();
0
 
0
-        check_pair_set_t     seen;
0
-        deque<check_pair_t>  pending;
0
+        check_pair_set_t      seen;
0
+        deque<check_pair_cp>  pending;
0
 
0
         /*
0
          * Initialize the BFS sets with the source pair.
0
          */
0
 
0
         {
0
-            check_pair_t  source(spec_source, impl_source);
0
+            check_pair_cp  source
0
+                (new check_pair_t(spec_source, impl_source));
0
 
0
-            seen.insert(source);
0
+            seen.insert(*source);
0
             pending.push_back(source);
0
         }
0
 
0
@@ -82,12 +143,12 @@ namespace hst
0
 
0
         while (!pending.empty())
0
         {
0
-            check_pair_t  pair = pending.front();
0
+            check_pair_cp  pair = pending.front();
0
             pending.pop_front();
0
 
0
 #if DEBUG_REFINEMENT
0
-            cerr << "Checking (" << pair.first
0
-                 << "," << pair.second << ")" << endl;
0
+            cerr << "Checking (" << pair->spec
0
+                 << "," << pair->impl << ")" << endl;
0
 #endif
0
 
0
             /*
0
@@ -97,12 +158,12 @@ namespace hst
0
 
0
             {
0
                 alphabet_t  spec_initials
0
-                    (spec.state_events_begin(pair.first),
0
-                     spec.state_events_end(pair.first));
0
+                    (spec.state_events_begin(pair->spec),
0
+                     spec.state_events_end(pair->spec));
0
 
0
                 alphabet_t  impl_initials
0
-                    (impl.state_events_begin(pair.second),
0
-                     impl.state_events_end(pair.second));
0
+                    (impl.state_events_begin(pair->impl),
0
+                     impl.state_events_end(pair->impl));
0
 
0
                 impl_initials -= spec_norm.tau();
0
 
0
@@ -111,11 +172,26 @@ namespace hst
0
                      << impl_initials << endl;
0
 #endif
0
 
0
-                if (!(spec_initials >= impl_initials))
0
+                /*
0
+                 * Remove all of the events that both IMPL and SPEC
0
+                 * can do.  If any are left over, the refinement
0
+                 * fails.
0
+                 */
0
+
0
+                impl_initials -= spec_initials;
0
+
0
+                if (impl_initials.size() > 0)
0
                 {
0
 #if DEBUG_REFINEMENT
0
                     cerr << "  Nope!  Refinement fails." << endl;
0
 #endif
0
+                    /*
0
+                     * We can use any of the events left in the set as
0
+                     * the counterexample event.
0
+                     */
0
+
0
+                    event_t  event = *(impl_initials.begin());
0
+                    construct_counterexample(counter, event, pair);
0
                     return false;
0
                 }
0
             }
0
@@ -126,8 +202,8 @@ namespace hst
0
              */
0
 
0
             for (lts_t::state_pairs_iterator sp_it =
0
-                     impl.state_pairs_begin(pair.second);
0
-                 sp_it != impl.state_pairs_end(pair.second);
0
+                     impl.state_pairs_begin(pair->impl);
0
+                 sp_it != impl.state_pairs_end(pair->impl);
0
                  ++sp_it)
0
             {
0
                 event_t  event = sp_it->first;
0
@@ -141,11 +217,13 @@ namespace hst
0
                      * includes a τ-closure.
0
                      */
0
 
0
-                    check_pair_t  next(pair.first, impl_prime);
0
+                    check_pair_cp  next
0
+                        (new check_pair_t(pair->spec, impl_prime,
0
+                                          spec_norm.tau(), pair));
0
 
0
-                    if (seen.find(next) == seen.end())
0
+                    if (seen.find(*next) == seen.end())
0
                     {
0
-                        seen.insert(next);
0
+                        seen.insert(*next);
0
                         pending.push_back(next);
0
                     }
0
                 } else {
0
@@ -159,9 +237,9 @@ namespace hst
0
                      */
0
 
0
                     lts_t::event_target_iterator  et_it =
0
-                        spec.event_targets_begin(pair.first, event);
0
+                        spec.event_targets_begin(pair->spec, event);
0
 
0
-                    if (et_it == spec.event_targets_end(pair.first,
0
+                    if (et_it == spec.event_targets_end(pair->spec,
0
                                                         event))
0
                     {
0
 #if DEBUG_REFINEMENT
0
@@ -174,7 +252,7 @@ namespace hst
0
                     state_t  spec_prime = *et_it;
0
                     ++et_it;
0
 
0
-                    if (et_it != spec.event_targets_end(pair.first,
0
+                    if (et_it != spec.event_targets_end(pair->spec,
0
                                                         event))
0
                     {
0
 #if DEBUG_REFINEMENT
0
@@ -184,11 +262,13 @@ namespace hst
0
                         return false;
0
                     }
0
 
0
-                    check_pair_t  next(spec_prime, impl_prime);
0
+                    check_pair_cp  next
0
+                        (new check_pair_t(spec_prime, impl_prime,
0
+                                          event, pair));
0
 
0
-                    if (seen.find(next) == seen.end())
0
+                    if (seen.find(*next) == seen.end())
0
                     {
0
-                        seen.insert(next);
0
+                        seen.insert(*next);
0
                         pending.push_back(next);
0
                     }
0
                 }

0
@@ -271,12 +271,46 @@ int do_assert(int argc, const char **argv)
0
 
0
             // Check the refinement.
0
 
0
-            bool  result = refines(*csp.normalized_lts(), spec,
0
+            trace_counterexample_t  counter;
0
+            bool  result = refines(counter, 
0
+                                   *csp.normalized_lts(), spec,
0
                                    *csp.lts(), impl);
0
 
0
             cout << spec_name << " [T= " << impl_name
0
                  << ": " << (result? "true": "false")
0
                  << endl;
0
+
0
+            if (!result)
0
+            {
0
+                cout << "After trace <";
0
+
0
+                trace_t::const_iterator  tit;
0
+                bool  first = true;
0
+
0
+                for (tit = counter.trace.begin();
0
+                     tit != counter.trace.end();
0
+                     ++tit)
0
+                {
0
+                    event_t  event = *tit;
0
+
0
+                    if (event != csp.tau())
0
+                    {
0
+                        if (first)
0
+                            first = false;
0
+                        else
0
+                            cout << ",";
0
+
0
+                        cout << csp.lts()->get_event_name(*tit);
0
+                    }
0
+                }
0
+
0
+                cout << ">," << endl
0
+                     << impl_name << " can execute "
0
+                     << csp.lts()->get_event_name(counter.event)
0
+                     << " but " << spec_name << " cannot."
0
+                     << endl;
0
+            }
0
+
0
         } else {
0
             cerr << "Unknown assertion flag " << flag << endl;
0
             return 2;

0
@@ -1,24 +1,21 @@
0
 set(TESTS
0
-  "00-basic1 1"
0
-  "00-basic2 1"
0
-  "00-basic3 1"
0
-  "00-basic4 0"
0
-  "80-roscoe-p40-a 1"
0
-  "80-roscoe-p40-b 1"
0
-  "80-roscoe-p52-a 1"
0
-  "80-roscoe-p52-b 1"
0
+  00-basic1
0
+  00-basic2
0
+  00-basic3
0
+  00-basic4
0
+  80-roscoe-p40-a
0
+  80-roscoe-p40-b
0
+  80-roscoe-p52-a
0
+  80-roscoe-p52-b
0
 )
0
 
0
 # Copy the test data from the source directory to the build directory.
0
 
0
 foreach(_test ${TESTS})
0
-  separate_arguments(_test)
0
-  list(GET _test 0 _test_file)
0
-
0
-  foreach(_ext csp0)
0
+  foreach(_ext csp0 traces)
0
     configure_file(
0
-      ${CMAKE_CURRENT_SOURCE_DIR}/${_test_file}.${_ext}
0
-      ${CMAKE_CURRENT_BINARY_DIR}/${_test_file}.${_ext}
0
+      ${CMAKE_CURRENT_SOURCE_DIR}/${_test}.${_ext}
0
+      ${CMAKE_CURRENT_BINARY_DIR}/${_test}.${_ext}
0
       COPYONLY
0
     )
0
   endforeach(_ext)
0
@@ -29,12 +26,9 @@ endforeach(_test)
0
 add_executable(test-traces-refinement test-traces-refinement.cc)
0
 target_link_libraries(test-traces-refinement hst)
0
 foreach(_test ${TESTS})
0
-  separate_arguments(_test)
0
-  list(GET _test 0 _test_file)
0
-  list(GET _test 1 _traces_result)
0
-
0
   add_test(
0
-    refinement:traces:${_test_file}
0
-    bash -c "[ `./test-traces-refinement < ${_test_file}.csp0` == '${_traces_result}' ]"
0
+    refinement:traces:${_test}
0
+    bash -c "./test-traces-refinement < ${_test}.csp0 |
0
+       cmp - ${_test}.traces"
0
   )
0
 endforeach(_test)

0
@@ -64,9 +64,39 @@ int main()
0
 
0
         // Check the refinement
0
 
0
-        bool  result = refines(*csp.normalized_lts(), SPEC,
0
+        trace_counterexample_t  counter;
0
+        bool  result = refines(counter,
0
+                               *csp.normalized_lts(), SPEC,
0
                                *csp.lts(), IMPL);
0
 
0
         cout << result << endl;
0
+        if (!result)
0
+        {
0
+            trace_t::const_iterator  tit;
0
+            bool  first = true;
0
+
0
+            cout << "<";
0
+
0
+            for (tit = counter.trace.begin();
0
+                 tit != counter.trace.end();
0
+                 ++tit)
0
+            {
0
+                event_t  event = *tit;
0
+
0
+                if (event != csp.tau())
0
+                {
0
+                    if (first)
0
+                        first = false;
0
+                    else
0
+                        cout << ",";
0
+
0
+                    cout << csp.lts()->get_event_name(*tit);
0
+                }
0
+            }
0
+
0
+            cout << ">: "
0
+                 << csp.lts()->get_event_name(counter.event)
0
+                 << endl;
0
+        }
0
     }
0
 }