twa_run: let as_twa work on the result of intersecting_run

Reported by Philipp Schlehuber-Caissier.

* spot/twaalgos/emptiness.cc (as_twa): Simplify considerably.  Don't
try to replay the run, and don't merge identical states.
* spot/twaalgos/word.hh, spot/twaalgos/emptiness.hh: Improve
documentation.
* tests/python/intrun.py: Add a test case.
* NEWS: Mention the bug.

NEWS

@@ -25,6 +25,11 @@ New in spot 2.11.4.dev  (not yet released)
   - Building from the git repository would fail to report a missing
     emacs (issue #528).
 
+  - Fix exception raised by aut1.intersecting_run(aut2).as_twa()
+    because the run did not match transitions present in aut1
+    verbatim.  We also changed the behavior of as_twa() to not merge
+    identical states.
+
 New in spot 2.11.4  (2023-02-10)
 
   Python:

spot/twaalgos/emptiness.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2011-2019, 2021 Laboratoire de Recherche et
+// Copyright (C) 2009, 2011-2019, 2021, 2023 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -570,7 +570,7 @@ namespace spot
         if (debug)
           os << "ERROR: First state of run (in " << in << "): "
              << aut->format_state(i->s)
-             << "\ndoes not match initial state of automata: "
+             << "\ndoes not match initial state of automaton: "
              << aut->format_state(s) << '\n';
         s->destroy();
         return false;
@@ -802,38 +802,38 @@ namespace spot
         res->set_named_prop("state-names", names);
       }
 
-    const state* s = aut->get_init_state();
     unsigned src;
     unsigned dst;
     const twa_run::steps* l;
-    acc_cond::mark_t seen_acc = {};
+    unsigned cycle_entry = 0;
-
-    state_map<unsigned> seen;
 
     if (prefix.empty())
-        l = &cycle;
+      l = &cycle;
     else
-        l = &prefix;
+      l = &prefix;
 
     twa_run::steps::const_iterator i = l->begin();
 
-    assert(s->compare(i->s) == 0);
+#if NDEBUG
+    const state* init = aut->get_init_state();
+    assert(init->compare(i->s) == 0);
+    init->destroy();
+#endif
+
     src = res->new_state();
-    seen.emplace(i->s, src);
     if (names)
-      names->push_back(aut->format_state(s));
+      names->push_back(aut->format_state(i->s));
 
     for (; i != l->end();)
       {
-        // expected outgoing transition
         bdd label = i->label;
         acc_cond::mark_t acc = i->acc;
-
         // compute the next expected state
         const state* next;
         ++i;
         if (i != l->end())
           {
+            dst = res->new_state();
             next = i->s;
           }
         else
@@ -842,57 +842,24 @@ namespace spot
               {
                 l = &cycle;
                 i = l->begin();
+                cycle_entry = dst = res->new_state();
+              }
+            else
+              {
+                dst = cycle_entry;
               }
             next = l->begin()->s;
           }
 
-        // browse the actual outgoing transitions and
+        if (names && i != l->end())
-        // look for next;
-        const state* the_next = nullptr;
-        for (auto j: aut->succ(s))
           {
-            if (j->cond() != label
+            assert(dst == names->size());
-                || j->acc() != acc)
+            names->push_back(aut->format_state(next));
-              continue;
-
-            const state* s2 = j->dst();
-            if (s2->compare(next) == 0)
-              {
-                the_next = s2;
-                break;
-              }
-            s2->destroy();
           }
-        s->destroy();
-        if (!the_next)
-          throw std::runtime_error("twa_run::as_twa() unable to replay run");
-        s = the_next;
-
-
-        auto p = seen.emplace(next, 0);
-        if (p.second)
-          {
-            unsigned ns = res->new_state();
-            p.first->second = ns;
-            if (names)
-              {
-                assert(ns == names->size());
-                names->push_back(aut->format_state(next));
-              }
-          }
-        dst = p.first->second;
-
         res->new_edge(src, dst, label, acc);
         src = dst;
-
-        // Sum acceptance conditions.
-        if (l == &cycle && i != l->begin())
-          seen_acc |= acc;
       }
 
-    s->destroy();
-
-    assert(aut->acc().accepting(seen_acc));
     return res;
   }
 

spot/twaalgos/emptiness.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2013-2018, 2020-2021 Laboratoire de
+// Copyright (C) 2011, 2013-2018, 2020-2021, 2023 Laboratoire de
 // Recherche et Developpement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -451,9 +451,9 @@ namespace spot
     /// Note that this works only if the automaton is a twa_graph_ptr.
     void highlight(unsigned color);
 
-    /// \brief Return a twa_graph_ptr corresponding to \a run
+    /// \brief Convert the run into a lasso-shaped automaton
     ///
-    /// Identical states are merged.
+    /// This preserves the original acceptance condition.
     ///
     /// If \a preserve_names is set, the created states are named
     /// using the format_state() result from the original state.

spot/twaalgos/word.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014, 2015, 2016, 2018, 2019 Laboratoire de Recherche et
+// Copyright (C) 2013-2016, 2018-2019, 2023 Laboratoire de Recherche
-// Développement de l'Epita (LRDE).
+// et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -80,6 +80,9 @@ namespace spot
 
     /// \brief Convert the twa_word as an automaton.
     ///
+    /// Convert the twa_word into a lasso-shapred automaton
+    /// with "true" acceptance condition.
+    ///
     /// This is useful to evaluate a word on an automaton.
     twa_graph_ptr as_automaton() const;
 

tests/python/intrun.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement
+# Copyright (C) 2020, 2022, 2023 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -38,3 +38,41 @@ r = b.intersecting_run(spot.complement(a));
 c = spot.twa_word(r).as_automaton()
 tc.assertTrue(c.intersects(b))
 tc.assertFalse(c.intersects(a))
+
+# The next test came from Philipp Schlehuber-Caissier: running
+# as_twa() on a run built from a A.intersecting_run(B) failed to build
+# the automaton because it tried to rebuild the run on A and did not
+# find transitions matching exactly.  Additionally the idea of merging
+# states in as_twa() seems to be a way to create some disasters, so we
+# removed that too.
+a = spot.translate("a");
+b = spot.translate("{a;1;a}");
+r = a.intersecting_run(b)
+tc.assertEqual(str(r), """Prefix:
+  1
+  |  a
+  0
+  |  1	{0}
+  0
+  |  a	{0}
+Cycle:
+  0
+  |  1	{0}
+""")
+tc.assertEqual(r.as_twa().to_str(), """HOA: v1
+States: 4
+Start: 0
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0
+[0] 1
+State: 1 {0}
+[t] 2
+State: 2 {0}
+[0] 3
+State: 3 {0}
+[t] 3
+--END--""")