Commit 014a9dbd authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

twa: add accepting_run() and accepting_word() methods

Fixes #153.

* spot/twa/twa.cc, spot/twa/twa.hh: Add the methods.
* bin/autfilt.cc, bin/common_aoutput.hh, bin/ltlcross.cc,
tests/python/highlighting.ipynb, tests/python/word.ipynb: Use
them to simplify the code.
* NEWS: Mention them.
parent 3836ea8d
...@@ -97,6 +97,12 @@ New in spot 2.0.3a (not yet released) ...@@ -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 not used anywhere in Spot, and had an obvious bug in its
implementation, so it cannot be missed by anyone. 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: Python:
* The __format__() method for formula support the same * The __format__() method for formula support the same
......
...@@ -1019,9 +1019,8 @@ namespace ...@@ -1019,9 +1019,8 @@ namespace
if (aut->acc().uses_fin_acceptance()) if (aut->acc().uses_fin_acceptance())
error(2, 0, error(2, 0,
"--highlight-word does not yet work with Fin acceptance"); "--highlight-word does not yet work with Fin acceptance");
if (auto res = if (auto run = spot::product(aut, word_aut.first)->accepting_run())
spot::couvreur99(spot::product(aut, word_aut.first))->check()) run->project(aut)->highlight(word_aut.second);
res->accepting_run()->project(aut)->highlight(word_aut.second);
} }
const double conversion_time = sw.stop(); const double conversion_time = sw.stop();
......
...@@ -178,15 +178,10 @@ public: ...@@ -178,15 +178,10 @@ public:
} }
if (has('w')) if (has('w'))
{ {
auto res = spot::couvreur99(aut)->check(); if (auto word = aut->accepting_word())
if (res)
{ {
auto run = res->accepting_run();
assert(run);
spot::twa_word w(run->reduce());
w.simplify();
std::ostringstream out; std::ostringstream out;
out << w; out << *word;
aut_word_ = out.str(); aut_word_ = out.str();
} }
else else
......
...@@ -682,8 +682,8 @@ namespace ...@@ -682,8 +682,8 @@ namespace
std::cerr << '\n'; std::cerr << '\n';
} }
auto res = spot::couvreur99(prod)->check(); auto w = prod->accepting_word();
if (res) if (w)
{ {
std::ostream& err = global_error(); std::ostream& err = global_error();
err << "error: "; err << "error: ";
...@@ -695,24 +695,12 @@ namespace ...@@ -695,24 +695,12 @@ namespace
err << "*Comp(P" << j << ')'; err << "*Comp(P" << j << ')';
else else
err << "*N" << j; err << "*N" << j;
err << " is nonempty"; err << " is nonempty; both automata accept the infinite word\n"
<< " ";
auto run = res->accepting_run(); example() << *w << '\n';
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';
}
end_error(); end_error();
} }
return !!res; return !!w;
} }
static bool static bool
......
...@@ -23,6 +23,7 @@ ...@@ -23,6 +23,7 @@
#include <spot/twa/twa.hh> #include <spot/twa/twa.hh>
#include <spot/twa/twagraph.hh> #include <spot/twa/twagraph.hh>
#include <spot/twaalgos/gtec/gtec.hh> #include <spot/twaalgos/gtec/gtec.hh>
#include <spot/twaalgos/word.hh>
#include <spot/twaalgos/remfin.hh> #include <spot/twaalgos/remfin.hh>
#include <utility> #include <utility>
...@@ -69,6 +70,42 @@ namespace spot ...@@ -69,6 +70,42 @@ namespace spot
return !couvreur99(a)->check(); 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<const twa_graph>(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 void
twa::set_named_prop(std::string s, std::nullptr_t) twa::set_named_prop(std::string s, std::nullptr_t)
{ {
......
...@@ -39,6 +39,12 @@ ...@@ -39,6 +39,12 @@
namespace spot namespace spot
{ {
struct twa_run;
typedef std::shared_ptr<twa_run> twa_run_ptr;
struct twa_word;
typedef std::shared_ptr<twa_word> twa_word_ptr;
/// \ingroup twa_essentials /// \ingroup twa_essentials
/// \brief Abstract class for states. /// \brief Abstract class for states.
class SPOT_API state class SPOT_API state
...@@ -821,9 +827,28 @@ namespace spot ...@@ -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; 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: private:
acc_cond acc_; acc_cond acc_;
......
...@@ -18,7 +18,7 @@ ...@@ -18,7 +18,7 @@
"version": "3.4.3+" "version": "3.4.3+"
}, },
"name": "", "name": "",
"signature": "sha256:0f4fb50930c6511a58891626864fe3236e91bb2525f9d8b2b1108f3e2a4c5d28" "signature": "sha256:f8755e90b26b56799cf6192d76999196f60eefa8307d0d104b73f476904754cc"
}, },
"nbformat": 3, "nbformat": 3,
"nbformat_minor": 0, "nbformat_minor": 0,
...@@ -155,7 +155,7 @@ ...@@ -155,7 +155,7 @@
"</svg>" "</svg>"
], ],
"text": [ "text": [
"<IPython.core.display.SVG at 0x7f44a034f208>" "<IPython.core.display.SVG at 0x7f859c2ba588>"
] ]
} }
], ],
...@@ -255,7 +255,7 @@ ...@@ -255,7 +255,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a00f88a0> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f859c0838a0> >"
] ]
} }
], ],
...@@ -357,7 +357,7 @@ ...@@ -357,7 +357,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7f44a006cf30> >" "<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7f8595d88f60> >"
] ]
} }
], ],
...@@ -572,7 +572,7 @@ ...@@ -572,7 +572,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a006cfc0> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8595d88fc0> >"
] ]
} }
], ],
...@@ -582,7 +582,7 @@ ...@@ -582,7 +582,7 @@
"cell_type": "code", "cell_type": "code",
"collapsed": false, "collapsed": false,
"input": [ "input": [
"r = spot.couvreur99(b).check().accepting_run(); r" "r = b.accepting_run(); r"
], ],
"language": "python", "language": "python",
"metadata": {}, "metadata": {},
...@@ -751,7 +751,7 @@ ...@@ -751,7 +751,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a006cfc0> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8595d88fc0> >"
] ]
} }
], ],
...@@ -831,7 +831,7 @@ ...@@ -831,7 +831,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a68f50f0> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f85a187e090> >"
] ]
}, },
{ {
...@@ -877,7 +877,7 @@ ...@@ -877,7 +877,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a68f50c0> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f85a187e060> >"
] ]
} }
], ],
...@@ -963,7 +963,7 @@ ...@@ -963,7 +963,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a006cf60> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8595d88d20> >"
] ]
} }
], ],
...@@ -973,7 +973,7 @@ ...@@ -973,7 +973,7 @@
"cell_type": "code", "cell_type": "code",
"collapsed": false, "collapsed": false,
"input": [ "input": [
"run = spot.couvreur99(prod).check().accepting_run(); run" "run = prod.accepting_run(); run"
], ],
"language": "python", "language": "python",
"metadata": {}, "metadata": {},
...@@ -1088,7 +1088,7 @@ ...@@ -1088,7 +1088,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a006cf60> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8595d88d20> >"
] ]
}, },
{ {
...@@ -1145,7 +1145,7 @@ ...@@ -1145,7 +1145,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a68f50f0> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f85a187e090> >"
] ]
}, },
{ {
...@@ -1191,7 +1191,7 @@ ...@@ -1191,7 +1191,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a68f50c0> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f85a187e060> >"
] ]
} }
], ],
...@@ -1211,7 +1211,7 @@ ...@@ -1211,7 +1211,7 @@
"left2 = spot.translate('!b & FG a')\n", "left2 = spot.translate('!b & FG a')\n",
"right2 = spot.translate('XXXb')\n", "right2 = spot.translate('XXXb')\n",
"prod2 = spot.otf_product(left2, right2) # Note \"otf_product()\"\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(left2).highlight(5)\n",
"run2.project(right2, True).highlight(5)\n", "run2.project(right2, True).highlight(5)\n",
"display(run2, prod2, left2, right2)" "display(run2, prod2, left2, right2)"
...@@ -1398,7 +1398,7 @@ ...@@ -1398,7 +1398,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f44a68f5120> >" "<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f85a187e120> >"
] ]
}, },
{ {
...@@ -1472,7 +1472,7 @@ ...@@ -1472,7 +1472,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a68f5060> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f85a187e0f0> >"
] ]
}, },
{ {
...@@ -1556,7 +1556,7 @@ ...@@ -1556,7 +1556,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a68f5030> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f85a187e150> >"
] ]
} }
], ],
...@@ -1702,7 +1702,7 @@ ...@@ -1702,7 +1702,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f44a68f5210> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f85a187e240> >"
] ]
} }
], ],
......
{ {
"metadata": { "metadata": {
"name": "", "name": "",
"signature": "sha256:261c16336ba5deefb7e9ebe705cc5c24f1cbba8622030874d2719f5045289c53" "signature": "sha256:4fc3934cf5fa0e612923dc4253b5e40115b103a93f588595a6706ec77e7994a9"
}, },
"nbformat": 3, "nbformat": 3,
"nbformat_minor": 0, "nbformat_minor": 0,
...@@ -139,7 +139,7 @@ ...@@ -139,7 +139,7 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa33c302870> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb71c0e18a0> >"
] ]
} }
], ],
...@@ -149,17 +149,14 @@ ...@@ -149,17 +149,14 @@
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "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", "Build an accepting run:"
"\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."
] ]
}, },
{ {
"cell_type": "code", "cell_type": "code",
"collapsed": false, "collapsed": false,
"input": [ "input": [
"run = spot.couvreur99(aut).check().accepting_run(); run" "run = aut.accepting_run(); run"
], ],
"language": "python", "language": "python",
"metadata": {}, "metadata": {},
...@@ -295,6 +292,33 @@ ...@@ -295,6 +292,33 @@
], ],
"prompt_number": 7 "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", "cell_type": "markdown",
"metadata": {}, "metadata": {},
...@@ -323,7 +347,7 @@ ...@@ -323,7 +347,7 @@
] ]
} }
], ],
"prompt_number": 8 "prompt_number": 9
}, },
{ {
"cell_type": "code", "cell_type": "code",
...@@ -338,13 +362,13 @@ ...@@ -338,13 +362,13 @@
{ {
"metadata": {}, "metadata": {},
"output_type": "pyout", "output_type": "pyout",
"prompt_number": 9, "prompt_number": 10,
"text": [ "text": [
"a; a & b; cycle{!a & !b}" "a; a & b; cycle{!a & !b}"
] ]
} }
], ],
"prompt_number": 9 "prompt_number": 10
}, },
{ {
"cell_type": "markdown", "cell_type": "markdown",
...@@ -362,7 +386,7 @@ ...@@ -362,7 +386,7 @@
"language": "python", "language": "python",
"metadata": {}, "metadata": {},
"outputs": [], "outputs": [],
"prompt_number": 10 "prompt_number": 11
}, },
{ {
"cell_type": "code", "cell_type": "code",
...@@ -376,7 +400,7 @@ ...@@ -376,7 +400,7 @@
{ {
"metadata": {}, "metadata": {},
"output_type": "pyout", "output_type": "pyout",
"prompt_number": 11, "prompt_number": 12,
"svg": [ "svg": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
...@@ -454,17 +478,17 @@ ...@@ -454,17 +478,17 @@
"</svg>\n" "</svg>\n"
], ],
"text": [ "text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa33c3028d0> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fb71c0e1a20> >"
] ]
} }
], ],
"prompt_number": 11 "prompt_number": 12
},