diff --git a/NEWS b/NEWS index 595111478..f83b9d645 100644 --- a/NEWS +++ b/NEWS @@ -97,6 +97,12 @@ New in spot 2.0.3a (not yet released) not used anywhere in Spot, and had an obvious bug in its implementation, so it cannot be missed by anyone. + * spot::twa has two new methods that supplement is_empty(): + twa::accepting_run() and twa::accepting_word(). They compute + what their name suggests. Note that twa::accepting_run(), unlike + the two others, is currently restricted to automata with Fin-less + acceptance. + Python: * The __format__() method for formula support the same diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 83ae1d9d3..5c4d8eca3 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -1019,9 +1019,8 @@ namespace if (aut->acc().uses_fin_acceptance()) error(2, 0, "--highlight-word does not yet work with Fin acceptance"); - if (auto res = - spot::couvreur99(spot::product(aut, word_aut.first))->check()) - res->accepting_run()->project(aut)->highlight(word_aut.second); + if (auto run = spot::product(aut, word_aut.first)->accepting_run()) + run->project(aut)->highlight(word_aut.second); } const double conversion_time = sw.stop(); diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh index af0a6a581..9df32fda9 100644 --- a/bin/common_aoutput.hh +++ b/bin/common_aoutput.hh @@ -178,15 +178,10 @@ public: } if (has('w')) { - auto res = spot::couvreur99(aut)->check(); - if (res) + if (auto word = aut->accepting_word()) { - auto run = res->accepting_run(); - assert(run); - spot::twa_word w(run->reduce()); - w.simplify(); std::ostringstream out; - out << w; + out << *word; aut_word_ = out.str(); } else diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index eab9f299a..dd5439b16 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -682,8 +682,8 @@ namespace std::cerr << '\n'; } - auto res = spot::couvreur99(prod)->check(); - if (res) + auto w = prod->accepting_word(); + if (w) { std::ostream& err = global_error(); err << "error: "; @@ -695,24 +695,12 @@ namespace err << "*Comp(P" << j << ')'; else err << "*N" << j; - err << " is nonempty"; - - auto run = res->accepting_run(); - if (run) - { - std::cerr << "; both automata accept the infinite word\n" - << " "; - spot::twa_word w(run->reduce()); - w.simplify(); - example() << w << '\n'; - } - else - { - std::cerr << '\n'; - } + err << " is nonempty; both automata accept the infinite word\n" + << " "; + example() << *w << '\n'; end_error(); } - return !!res; + return !!w; } static bool diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index 2b8b0d169..92d29adb2 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -23,6 +23,7 @@ #include #include #include +#include #include #include @@ -69,6 +70,42 @@ namespace spot return !couvreur99(a)->check(); } + twa_run_ptr + twa::accepting_run() const + { + if (acc().uses_fin_acceptance()) + throw std::runtime_error("twa::accepting_run() does not work with " + "Fin acceptance (but twa:is_empty() and " + "twa::accepting_run() can)"); + auto res = couvreur99(shared_from_this())->check(); + if (!res) + return nullptr; + return res->accepting_run(); + } + + twa_word_ptr + twa::accepting_word() const + { + auto a = shared_from_this(); + if (a->acc().uses_fin_acceptance()) + { + auto aa = std::dynamic_pointer_cast(a); + if (!aa) + aa = make_twa_graph(a, prop_set::all()); + a = remove_fin(aa); + } + if (auto run = a->accepting_run()) + { + auto w = make_twa_word(run->reduce()); + w->simplify(); + return w; + } + else + { + return nullptr; + } + } + void twa::set_named_prop(std::string s, std::nullptr_t) { diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 2a7d707e9..d5f06dbb9 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -39,6 +39,12 @@ namespace spot { + struct twa_run; + typedef std::shared_ptr twa_run_ptr; + + struct twa_word; + typedef std::shared_ptr twa_word_ptr; + /// \ingroup twa_essentials /// \brief Abstract class for states. class SPOT_API state @@ -821,9 +827,28 @@ namespace spot } ///@} - /// Check whether the language of the automaton is empty. + /// \brief Check whether the language of the automaton is empty. virtual bool is_empty() const; + /// \brief Return an accepting run if one exists. + /// + /// Note that this method currently one works for Fin-less + /// acceptance. For acceptance conditions that contain Fin + /// acceptance, you can either rely on is_empty() and not use any + /// accepting run, or remove Fin acceptance using remove_fin() and + /// compute an accepting run on that larger automaton. + /// + /// Return nullptr if no accepting run were found. + virtual twa_run_ptr accepting_run() const; + + /// \brief Return an accepting word if one exists. + /// + /// Note that this method DO works with Fin + /// acceptance. + /// + /// Return nullptr if no accepting word were found. + virtual twa_word_ptr accepting_word() const; + private: acc_cond acc_; diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb index 5804bd265..49703bf95 100644 --- a/tests/python/highlighting.ipynb +++ b/tests/python/highlighting.ipynb @@ -18,7 +18,7 @@ "version": "3.4.3+" }, "name": "", - "signature": "sha256:0f4fb50930c6511a58891626864fe3236e91bb2525f9d8b2b1108f3e2a4c5d28" + "signature": "sha256:f8755e90b26b56799cf6192d76999196f60eefa8307d0d104b73f476904754cc" }, "nbformat": 3, "nbformat_minor": 0, @@ -155,7 +155,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -255,7 +255,7 @@ "\n" ], "text": [ - " *' at 0x7f44a00f88a0> >" + " *' at 0x7f859c0838a0> >" ] } ], @@ -357,7 +357,7 @@ "\n" ], "text": [ - " *' at 0x7f44a006cf30> >" + " *' at 0x7f8595d88f60> >" ] } ], @@ -572,7 +572,7 @@ "\n" ], "text": [ - " *' at 0x7f44a006cfc0> >" + " *' at 0x7f8595d88fc0> >" ] } ], @@ -582,7 +582,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "r = spot.couvreur99(b).check().accepting_run(); r" + "r = b.accepting_run(); r" ], "language": "python", "metadata": {}, @@ -751,7 +751,7 @@ "\n" ], "text": [ - " *' at 0x7f44a006cfc0> >" + " *' at 0x7f8595d88fc0> >" ] } ], @@ -831,7 +831,7 @@ "\n" ], "text": [ - " *' at 0x7f44a68f50f0> >" + " *' at 0x7f85a187e090> >" ] }, { @@ -877,7 +877,7 @@ "\n" ], "text": [ - " *' at 0x7f44a68f50c0> >" + " *' at 0x7f85a187e060> >" ] } ], @@ -963,7 +963,7 @@ "\n" ], "text": [ - " *' at 0x7f44a006cf60> >" + " *' at 0x7f8595d88d20> >" ] } ], @@ -973,7 +973,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "run = spot.couvreur99(prod).check().accepting_run(); run" + "run = prod.accepting_run(); run" ], "language": "python", "metadata": {}, @@ -1088,7 +1088,7 @@ "\n" ], "text": [ - " *' at 0x7f44a006cf60> >" + " *' at 0x7f8595d88d20> >" ] }, { @@ -1145,7 +1145,7 @@ "\n" ], "text": [ - " *' at 0x7f44a68f50f0> >" + " *' at 0x7f85a187e090> >" ] }, { @@ -1191,7 +1191,7 @@ "\n" ], "text": [ - " *' at 0x7f44a68f50c0> >" + " *' at 0x7f85a187e060> >" ] } ], @@ -1211,7 +1211,7 @@ "left2 = spot.translate('!b & FG a')\n", "right2 = spot.translate('XXXb')\n", "prod2 = spot.otf_product(left2, right2) # Note \"otf_product()\"\n", - "run2 = spot.couvreur99(prod2).check().accepting_run()\n", + "run2 = prod2.accepting_run()\n", "run2.project(left2).highlight(5)\n", "run2.project(right2, True).highlight(5)\n", "display(run2, prod2, left2, right2)" @@ -1398,7 +1398,7 @@ "\n" ], "text": [ - " *' at 0x7f44a68f5120> >" + " *' at 0x7f85a187e120> >" ] }, { @@ -1472,7 +1472,7 @@ "\n" ], "text": [ - " *' at 0x7f44a68f5060> >" + " *' at 0x7f85a187e0f0> >" ] }, { @@ -1556,7 +1556,7 @@ "\n" ], "text": [ - " *' at 0x7f44a68f5030> >" + " *' at 0x7f85a187e150> >" ] } ], @@ -1702,7 +1702,7 @@ "\n" ], "text": [ - " *' at 0x7f44a68f5210> >" + " *' at 0x7f85a187e240> >" ] } ], diff --git a/tests/python/word.ipynb b/tests/python/word.ipynb index ad820de94..7e554b7d3 100644 --- a/tests/python/word.ipynb +++ b/tests/python/word.ipynb @@ -1,7 +1,7 @@ { "metadata": { "name": "", - "signature": "sha256:261c16336ba5deefb7e9ebe705cc5c24f1cbba8622030874d2719f5045289c53" + "signature": "sha256:4fc3934cf5fa0e612923dc4253b5e40115b103a93f588595a6706ec77e7994a9" }, "nbformat": 3, "nbformat_minor": 0, @@ -139,7 +139,7 @@ "\n" ], "text": [ - " *' at 0x7fa33c302870> >" + " *' at 0x7fb71c0e18a0> >" ] } ], @@ -149,17 +149,14 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "The call to `couvreur99()` just instanciate the emptiness check, but does not run the check. Calling `check()` will return `None` if no accepting run was found. Otherwise the presence of the accepting run is established, but an accepting run hasn't necessarily been calculated: calling `accepting_run()` on the result will cause this computation to happen.\n", - "\n", - "\n", - "In the example below, we do not check the result of `check()` because we know that the input formula is satisfiable, so the automaton has an accepting run." + "Build an accepting run:" ] }, { "cell_type": "code", "collapsed": false, "input": [ - "run = spot.couvreur99(aut).check().accepting_run(); run" + "run = aut.accepting_run(); run" ], "language": "python", "metadata": {}, @@ -295,6 +292,33 @@ ], "prompt_number": 7 }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Such a simplified word can be created directly from the automaton:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "aut.accepting_word()" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 8, + "text": [ + "cycle{!a & b; a & b}" + ] + } + ], + "prompt_number": 8 + }, { "cell_type": "markdown", "metadata": {}, @@ -323,7 +347,7 @@ ] } ], - "prompt_number": 8 + "prompt_number": 9 }, { "cell_type": "code", @@ -338,13 +362,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 9, + "prompt_number": 10, "text": [ "a; a & b; cycle{!a & !b}" ] } ], - "prompt_number": 9 + "prompt_number": 10 }, { "cell_type": "markdown", @@ -362,7 +386,7 @@ "language": "python", "metadata": {}, "outputs": [], - "prompt_number": 10 + "prompt_number": 11 }, { "cell_type": "code", @@ -376,7 +400,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 11, + "prompt_number": 12, "svg": [ "\n", "\n" ], "text": [ - " *' at 0x7fa33c3028d0> >" + " *' at 0x7fb71c0e1a20> >" ] } ], - "prompt_number": 11 + "prompt_number": 12 }, { "cell_type": "markdown", "metadata": {}, "source": [ - "Test some syntax errors" + "The rest of this pages tests some syntax errors, you (humans) may skip it, but the test suite will not." ] }, { @@ -485,7 +509,7 @@ ] } ], - "prompt_number": 12 + "prompt_number": 13 }, { "cell_type": "code", @@ -505,7 +529,7 @@ ] } ], - "prompt_number": 13 + "prompt_number": 14 }, { "cell_type": "code", @@ -525,7 +549,7 @@ ] } ], - "prompt_number": 14 + "prompt_number": 15 }, { "cell_type": "code", @@ -545,7 +569,7 @@ ] } ], - "prompt_number": 15 + "prompt_number": 16 }, { "cell_type": "code", @@ -557,7 +581,7 @@ "language": "python", "metadata": {}, "outputs": [], - "prompt_number": 16 + "prompt_number": 17 }, { "cell_type": "code", @@ -575,13 +599,13 @@ "output_type": "pyerr", "traceback": [ "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m\n\u001b[0;31mRuntimeError\u001b[0m Traceback (most recent call last)", - "\u001b[0;32m\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[1;32m 1\u001b[0m \u001b[0;31m# ... as long as this word is not printed.\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m----> 2\u001b[0;31m \u001b[0mprint\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mw\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m", - "\u001b[0;32m/home/adl/git/spot/python/spot/impl.py\u001b[0m in \u001b[0;36m__str__\u001b[0;34m(self)\u001b[0m\n\u001b[1;32m 3511\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 3512\u001b[0m \u001b[0;32mdef\u001b[0m \u001b[0m__str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;34m->\u001b[0m \u001b[0;34m\"std::string\"\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m-> 3513\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word___str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 3514\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 3515\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtwa_word\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", + "\u001b[0;32m\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[1;32m 1\u001b[0m \u001b[0;31m# ... as long as this word is not printed.\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m----> 2\u001b[0;31m \u001b[0mprint\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mw\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m", + "\u001b[0;32m/home/adl/git/spot/python/spot/impl.py\u001b[0m in \u001b[0;36m__str__\u001b[0;34m(self)\u001b[0m\n\u001b[1;32m 3599\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 3600\u001b[0m \u001b[0;32mdef\u001b[0m \u001b[0m__str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;34m->\u001b[0m \u001b[0;34m\"std::string\"\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m-> 3601\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word___str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 3602\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 3603\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtwa_word\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", "\u001b[0;31mRuntimeError\u001b[0m: a twa_word may not have an empty cycle" ] } ], - "prompt_number": 17 + "prompt_number": 18 } ], "metadata": {}