0
@@ -96,6 +96,7 @@ void print_assert_usage(ostream &stream)
0
            << "be of the following form:" << endl
0
            << endl
0
            << "    --traces-refinement [spec] [impl]" << endl
0
+           << "    --failures-refinement [spec] [impl]" << endl
0
         ;
0
 }
0
 
0
@@ -180,6 +181,180 @@ int do_lts(int argc, const char **argv)
0
  * The “assert” command tests assertions on a CSP0 script.
0
  */
0
 
0
+int do_traces_refinement(csp_t &csp,
0
+                         const char *spec_name,
0
+                         const char *impl_name)
0
+{
0
+    // Look up the process names in the CSP script.
0
+
0
+    state_t  spec, impl;
0
+
0
+    spec = csp.get_process(spec_name);
0
+    if (spec == HST_ERROR_STATE)
0
+    {
0
+        cerr << "Specification process "
0
+             << spec_name << " does not exist."
0
+             << endl;
0
+        return 3;
0
+    }
0
+
0
+    impl = csp.get_process(impl_name);
0
+    if (impl == HST_ERROR_STATE)
0
+    {
0
+        cerr << "Implementation process "
0
+             << impl_name << " does not exist."
0
+             << endl;
0
+        return 3;
0
+    }
0
+
0
+    // Normalize the spec process.
0
+
0
+    csp.normalized_lts()->clear(TRACES);
0
+    csp.normalized_lts()->prenormalize(spec);
0
+    csp.normalized_lts()->normalize();
0
+    spec = csp.normalized_lts()->initial_normal_state(spec);
0
+
0
+    // Check the refinement.
0
+
0
+    trace_counterexample_t  counter;
0
+    bool  result = trace_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
+    return 0;
0
+}
0
+
0
+int do_failures_refinement(csp_t &csp,
0
+                           const char *spec_name,
0
+                           const char *impl_name)
0
+{
0
+    // Look up the process names in the CSP script.
0
+
0
+    state_t  spec, impl;
0
+
0
+    spec = csp.get_process(spec_name);
0
+    if (spec == HST_ERROR_STATE)
0
+    {
0
+        cerr << "Specification process "
0
+             << spec_name << " does not exist."
0
+             << endl;
0
+        return 3;
0
+    }
0
+
0
+    impl = csp.get_process(impl_name);
0
+    if (impl == HST_ERROR_STATE)
0
+    {
0
+        cerr << "Implementation process "
0
+             << impl_name << " does not exist."
0
+             << endl;
0
+        return 3;
0
+    }
0
+
0
+    // Normalize the spec process.
0
+
0
+    csp.normalized_lts()->clear(FAILURES);
0
+    csp.normalized_lts()->prenormalize(spec);
0
+    csp.normalized_lts()->normalize();
0
+    spec = csp.normalized_lts()->initial_normal_state(spec);
0
+
0
+    // Check the refinement.
0
+
0
+    failures_counterexample_t  counter;
0
+    bool  result = failures_refines(counter,
0
+                                    *csp.normalized_lts(), spec,
0
+                                    *csp.lts(), impl);
0
+
0
+    cout << spec_name << " [F= " << impl_name
0
+         << ": " << (result? "true": "false")
0
+         << endl;
0
+
0
+    if (!result)
0
+    {
0
+        cout << "After trace <";
0
+
0
+        bool first = true;
0
+
0
+        for (trace_t::const_iterator 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(event);
0
+            }
0
+        }
0
+
0
+        cout << ">," << endl
0
+             << impl_name << " can accept {";
0
+
0
+        first = true;
0
+
0
+        for (alphabet_t::iterator ait = counter.acceptance.begin();
0
+             ait != counter.acceptance.end();
0
+             ++ait)
0
+        {
0
+            event_t  event = *ait;
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(event);
0
+            }
0
+        }
0
+
0
+        cout << "} but " << spec_name << " cannot."
0
+             << endl;
0
+    }
0
+
0
+    return 0;
0
+}
0
+
0
 int do_assert(int argc, const char **argv)
0
 {
0
     if (argc < 1)
0
@@ -240,77 +415,28 @@ int do_assert(int argc, const char **argv)
0
             const char  *impl_name = *argv++;
0
             argc -= 2;
0
 
0
-            // Look up the process names in the CSP script.
0
+            int result = do_traces_refinement(csp, spec_name, impl_name);
0
+            if (result != 0)
0
+                return result;
0
 
0
-            state_t  spec, impl;
0
+        } else if (strcmp(flag, "--failures-refinement") == 0) {
0
 
0
-            spec = csp.get_process(spec_name);
0
-            if (spec == HST_ERROR_STATE)
0
-            {
0
-                cerr << "Specification process "
0
-                     << spec_name << " does not exist."
0
-                     << endl;
0
-                return 3;
0
-            }
0
+            // We need two process names
0
 
0
-            impl = csp.get_process(impl_name);
0
-            if (impl == HST_ERROR_STATE)
0
+            if (argc < 2)
0
             {
0
-                cerr << "Implementation process "
0
-                     << impl_name << " does not exist."
0
+                cerr << "Need two processes for a failures refinement!"
0
                      << endl;
0
-                return 3;
0
+                return 2;
0
             }
0
 
0
-            // Normalize the spec process.
0
-
0
-            csp.normalized_lts()->clear(TRACES);
0
-            csp.normalized_lts()->prenormalize(spec);
0
-            csp.normalized_lts()->normalize();
0
-            spec = csp.normalized_lts()->initial_normal_state(spec);
0
-
0
-            // Check the refinement.
0
-
0
-            trace_counterexample_t  counter;
0
-            bool  result = trace_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
+            const char  *spec_name = *argv++;
0
+            const char  *impl_name = *argv++;
0
+            argc -= 2;
0
 
0
+            int result = do_failures_refinement(csp, spec_name, impl_name);
0
+            if (result != 0)
0
+                return result;
0
         } else {
0
             cerr << "Unknown assertion flag " << flag << endl;
0
             return 2;