From 60f046a574533bbdce3e154d7d7cd4de3d925a84 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 29 Feb 2024 16:54:14 +0100 Subject: [PATCH] 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 | 5 ++++ THANKS | 1 + spot/twa/fwd.hh | 4 +++ spot/twa/twa.cc | 6 +++++ spot/twa/twa.hh | 7 +++++ spot/twaalgos/forq_contains.cc | 6 ++--- spot/twaalgos/word.hh | 12 +++++++-- tests/python/word.ipynb | 49 +++++++++++++++++++++++++++++----- 8 files changed, 78 insertions(+), 12 deletions(-) diff --git a/NEWS b/NEWS index 7508311ea..81a5272a7 100644 --- a/NEWS +++ b/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. diff --git a/THANKS b/THANKS index 4eb4a598c..cf923eaec 100644 --- a/THANKS +++ b/THANKS @@ -57,6 +57,7 @@ Reuben Rowe Roei Nahum Rüdiger Ehlers Samuel Judson +Scott Buckley Shachar Itzhaky Shengping Shaw Shufang Zhu diff --git a/spot/twa/fwd.hh b/spot/twa/fwd.hh index 839844875..59f6853fd 100644 --- a/spot/twa/fwd.hh +++ b/spot/twa/fwd.hh @@ -36,4 +36,8 @@ namespace spot class twa_product; typedef std::shared_ptr const_twa_product_ptr; typedef std::shared_ptr twa_product_ptr; + + struct twa_word; + typedef std::shared_ptr const_twa_word_ptr; + typedef std::shared_ptr twa_word_ptr; } diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index ab4c12ef6..66d518f65 100644 --- a/spot/twa/twa.cc +++ b/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 { diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 85ce382e3..85a755873 100644 --- a/spot/twa/twa.hh +++ b/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. /// diff --git a/spot/twaalgos/forq_contains.cc b/spot/twaalgos/forq_contains.cc index 106553160..4d4264ae2 100644 --- a/spot/twaalgos/forq_contains.cc +++ b/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; diff --git a/spot/twaalgos/word.hh b/spot/twaalgos/word.hh index 68538d2d3..171b14ce3 100644 --- a/spot/twaalgos/word.hh +++ b/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_ptr; - /// \brief Create an empty twa_word /// /// Note that empty twa_word are invalid and cannot be printed. diff --git a/tests/python/word.ipynb b/tests/python/word.ipynb index dec900dd0..e2e9441ca 100644 --- a/tests/python/word.ipynb +++ b/tests/python/word.ipynb @@ -307,7 +307,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f8f5c19e5e0> >" + " *' at 0x7f1f80568c60> >" ] }, "execution_count": 2, @@ -405,7 +405,7 @@ "$\\lnot a; \\lnot a; \\mathsf{cycle}\\{a \\land b; \\lnot a \\land b\\}$" ], "text/plain": [ - " *' at 0x7f8f5c19e040> >" + " *' at 0x7f1f805686f0> >" ] }, "execution_count": 5, @@ -530,7 +530,7 @@ "$\\lnot a; \\mathsf{cycle}\\{\\lnot a \\land b; a \\land b\\}$" ], "text/plain": [ - " *' at 0x7f8f5c19f8d0> >" + " *' 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": [ - " *' at 0x7f8f5c19e250> >" + " *' at 0x7f1f8060df80> >" ] }, "execution_count": 11, @@ -790,7 +790,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f8f5c19fab0> >" + " *' 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,