add intersection checks between words and automata

Several people have asked for a way to check whether a word is
accepted by an automaton, including at least Jonah Romero and Scott
Buckley.  So it's time we have it.

* spot/twa/twa.hh, spot/twa/twa.cc,
spot/twaalgos/word.hh (intersects): Add the new variant.
* spot/twa/fwd.hh: Forward declare twa_word, so that
we can use it in twa.hh.
* spot/twaalgos/forq_contains.cc: Use the new intersection check.
* tests/python/word.ipynb, NEWS: Mention it.
* THANKS: Add Scott Buckley.

NEWS

@@ -114,6 +114,11 @@ New in spot 2.11.6.dev  (not yet released)
 
     The above also impacts autfilt --included-in option.
 
+  - Given a twa_word_ptr W and a twa_ptr A both sharing the same
+    alphabet, one can now write W->intersects(A) or A->intersects(W)
+    instead of the longuer W->as_automaton()->intersects(A) or
+    A->intersects(W->as_automaton()).
+
   - spot::scc_info has a new option PROCESS_UNREACHABLE_STATES that
     causes it to enumerate even unreachable SCCs.
 

THANKS

@@ -57,6 +57,7 @@ Reuben Rowe
 Roei Nahum
 Rüdiger Ehlers
 Samuel Judson
+Scott Buckley
 Shachar Itzhaky
 Shengping Shaw
 Shufang Zhu

spot/twa/fwd.hh

@@ -36,4 +36,8 @@ namespace spot
   class twa_product;
   typedef std::shared_ptr<const twa_product> const_twa_product_ptr;
   typedef std::shared_ptr<twa_product> twa_product_ptr;
+
+  struct twa_word;
+  typedef std::shared_ptr<const twa_word> const_twa_word_ptr;
+  typedef std::shared_ptr<twa_word> twa_word_ptr;
 }

spot/twa/twa.cc

@@ -155,6 +155,12 @@ namespace spot
     return !otf_product(self, other)->is_empty();
   }
 
+  bool
+  twa::intersects(const_twa_word_ptr w) const
+  {
+    return intersects(w->as_automaton());
+  }
+
   twa_run_ptr
   twa::intersecting_run(const_twa_ptr other) const
   {

spot/twa/twa.hh

@@ -865,6 +865,13 @@ namespace spot
     /// this case an explicit product is performed.
     virtual bool intersects(const_twa_ptr other) const;
 
+    /// \brief Check if this automaton _word intersects a word.
+    ///
+    /// If the twa_word actually represent a word (i.e., if each
+    /// Boolean formula that label its steps have a unique satisfying
+    /// valuation), this is equivalent to a membership test.
+    virtual bool intersects(const_twa_word_ptr w) const;
+
     /// \brief Return an accepting run recognizing a word accepted by
     /// two automata.
     ///

spot/twaalgos/forq_contains.cc

@@ -578,10 +578,8 @@ namespace spot::forq
           auto shared_dict = setup.context.A.aut->get_dict();
           auto current_word = util::as_twa_word_ptr(shared_dict, word_of_u,
                                                     word_of_v);
-          if (!setup.context.B.aut->intersects(current_word->as_automaton()))
-            {
-              return current_word;
-            }
+          if (!current_word->intersects(setup.context.B.aut))
+            return current_word;
         }
     }
     return nullptr;

spot/twaalgos/word.hh

@@ -85,6 +85,16 @@ namespace spot
     /// This is useful to evaluate a word on an automaton.
     twa_graph_ptr as_automaton() const;
 
+    /// \brief Check if a the twa_word intersect another automaton.
+    ///
+    /// If the twa_word actually represent a word (i.e., if each
+    /// Boolean formula that label its steps have a unique satisfying
+    /// valuation), this is equivalent to a membership test.
+    bool intersects(const_twa_ptr aut) const
+    {
+      return as_automaton()->intersects(aut);
+    }
+
     /// \brief Print a twa_word
     ///
     /// Words are printed as
@@ -101,8 +111,6 @@ namespace spot
     bdd_dict_ptr dict_;
   };
 
-  typedef std::shared_ptr<twa_word> twa_word_ptr;
-
   /// \brief Create an empty twa_word
   ///
   /// Note that empty twa_word are invalid and cannot be printed.

tests/python/word.ipynb

@@ -307,7 +307,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8f5c19e5e0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1f80568c60> >"
       ]
      },
      "execution_count": 2,
@@ -405,7 +405,7 @@
        "$\\lnot a; \\lnot a; \\mathsf{cycle}\\{a \\land b; \\lnot a \\land b\\}$"
       ],
       "text/plain": [
-       "<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f8f5c19e040> >"
+       "<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f1f805686f0> >"
       ]
      },
      "execution_count": 5,
@@ -530,7 +530,7 @@
        "$\\lnot a; \\mathsf{cycle}\\{\\lnot a \\land b; a \\land b\\}$"
       ],
       "text/plain": [
-       "<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f8f5c19f8d0> >"
+       "<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f1f8060d770> >"
       ]
      },
      "execution_count": 9,
@@ -581,7 +581,7 @@
        "$a; a \\land b; \\mathsf{cycle}\\{\\lnot a \\land \\lnot b; \\lnot a \\land b\\}$"
       ],
       "text/plain": [
-       "<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f8f5c19e250> >"
+       "<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f1f8060df80> >"
       ]
      },
      "execution_count": 11,
@@ -790,7 +790,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8f5c19fab0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1f8060d800> >"
       ]
      },
      "execution_count": 13,
@@ -801,6 +801,43 @@
    "source": [
     "w.as_automaton()"
    ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "To check if a word is accepted by an automaton, you can use `intersects`.   The name `intersects` actually makes more sense than `accepts` or `accepted`, because a word actually describes a set of words because of the don't care atomic propositions."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 16,
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "False\n",
+      "False\n",
+      "True\n",
+      "True\n"
+     ]
+    }
+   ],
+   "source": [
+    "print(w.intersects(aut))\n",
+    "print(aut.intersects(w))\n",
+    "print(word.intersects(aut))\n",
+    "print(aut.intersects(word))"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
   }
  ],
  "metadata": {
@@ -819,7 +856,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.11.7"
+   "version": "3.11.8"
   }
  },
  "nbformat": 4,