alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

twa: introduce exclusive_word() and exclusive_run()

Browse source 
* spot/twa/twa.cc, spot/twa/twa.hh: Add these methods.
* NEWS, tests/python/contains.ipynb: Document them.
This commit is contained in:
Alexandre Duret-Lutz 2018-06-29 20:50:19 +02:00
parent 3c12015181
commit 4e8b35d7ca
4 changed files with 298 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
NEWS
View file

@ -192,7 +192,14 @@ New in spot 2.5.3.dev (not yet released)
- spot::contains() and spot::are_equivalent() can be used to
check language containement between two automata or formulas.
They are most welcome in Python, since we used to redefine
them every now and them.
them every now and them. Some examples are shown in
https://spot.lrde.epita.fr/ipynb/contains.html
- aut1->exclusive_word(aut2) is a new method that returns a word
accepted by aut1 or aut2 but not both. The exclusive_run()
variant will return. This is useful when comparing automata and
looking for differences. See also
https://spot.lrde.epita.fr/ipynb/contains.html
- spot::remove_alternation() was slightly improved on very-weak
alternating automata: the labeling of the outgoing transitions in

56
spot/twa/twa.cc
View file

@ -28,6 +28,9 @@
#include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/alternation.hh>
#include <spot/twa/twaproduct.hh>
#include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/postproc.hh>
#include <spot/twaalgos/isdet.hh>
#include <utility>
namespace spot
@ -117,7 +120,7 @@ namespace spot
twa::intersecting_run(const_twa_ptr other, bool from_other) const
{
auto a = shared_from_this();
if (from_other)
if (!from_other)
other = remove_fin_maybe(other);
else
a = remove_fin_maybe(a);
@ -135,6 +138,57 @@ namespace spot
return otf_product(a1, a2)->accepting_word();
}
namespace
{
static const_twa_graph_ptr
ensure_deterministic(const const_twa_ptr& aut_in)
{
const_twa_graph_ptr aut =
std::dynamic_pointer_cast<const twa_graph>(aut_in);
if (!aut)
aut = make_twa_graph(aut_in, twa::prop_set::all());
if (is_deterministic(aut))
return aut;
postprocessor p;
p.set_type(postprocessor::Generic);
p.set_pref(postprocessor::Deterministic);
p.set_level(postprocessor::Low);
return p.run(std::const_pointer_cast<twa_graph>(aut));
}
}
twa_run_ptr
twa::exclusive_run(const_twa_ptr other) const
{
const_twa_ptr a = shared_from_this();
const_twa_ptr b = other;
// We have to find a run in A\B or in B\A. When possible, let's
// make sure the first automaton we complement is deterministic.
if (auto aa = std::dynamic_pointer_cast<const twa_graph>(a))
if (is_deterministic(aa))
std::swap(a, b);
if (auto run = a->intersecting_run(dualize(ensure_deterministic(b))))
return run;
return b->intersecting_run(dualize(ensure_deterministic(a)));
}
twa_word_ptr
twa::exclusive_word(const_twa_ptr other) const
{
const_twa_ptr a = shared_from_this();
const_twa_ptr b = other;
// We have to find a word in A\B or in B\A. When possible, let's
// make sure the first automaton we complement is deterministic.
if (auto aa = std::dynamic_pointer_cast<const twa_graph>(a))
if (is_deterministic(aa))
std::swap(a, b);
if (auto word = a->intersecting_word(dualize(ensure_deterministic(b))))
return word;
return b->intersecting_word(dualize(ensure_deterministic(a)));
}
void
twa::set_named_prop(std::string s, std::nullptr_t)
{

24
spot/twa/twa.hh
View file

@ -888,6 +888,30 @@ namespace spot
/// Return nullptr if no accepting word were found.
virtual twa_word_ptr intersecting_word(const_twa_ptr other) const;
/// \brief Return an accepting run recognizing a word accepted by
/// exactly one of the two automata.
///
/// If \a from_other is true, the returned run will be over the
/// \a other automaton. Otherwise, the run will be over this
/// automaton.
///
/// Note that this method currently only works if the automaton
/// from which the accepting run is extracted uses Fin-less acceptance.
/// (The other automaton can have any acceptance condition.)
///
/// Return nullptr iff the two automata recognize the same
/// language.
virtual twa_run_ptr exclusive_run(const_twa_ptr other) const;
/// \brief Return a word accepted by exactly one of the two
/// automata.
///
/// Note that this method DOES works with Fin acceptance.
///
/// Return nullptr iff the two automata recognize the same
/// language.
virtual twa_word_ptr exclusive_word(const_twa_ptr other) const;
private:
acc_cond acc_;

212
tests/python/contains.ipynb
View file

@ -7,6 +7,7 @@
"outputs": [],
"source": [
"import spot\n",
"from spot.jupyter import display_inline\n",
"spot.setup(show_default='.a')"
]
},
@ -302,6 +303,215 @@
"source": [
"lcc.are_equivalent(f, g)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Help for distinguishing languages\n",
"\n",
"Assume you have computed two automata, that `are_equivalent(a1, a2)` returns `False`, and you want to know why. (This often occur when debugging some algorithm that produce an automaton that is not equivalent to which it should.) The automaton class has a method called `a1.exclusive_run(a2)` that can help with this task: it returns a run that recognizes a word is is accepted by one of the two automata but not by both. The method `a1.exclusive_run(a2)` will return just a word.\n",
"\n",
"For instance let's find a word that is exclusive between `aut_f` and `aut_g`. (The adjective *exlusive* is a reference to the *exclusive or* operator: the word belongs to L(aut_f) \"xor\" it belongs to L(aut_g).)"
]
},
{
"cell_type": "code",
"execution_count": 16,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"cycle{a; !a}"
]
},
"execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"aut_f.exclusive_word(aut_g)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We can even write a small function that highlights one difference between two automata. Note that the `run` returned will belong to either `left` or `right`, so calling the `highlight()` method will colorize one of those two automata."
]
},
{
"cell_type": "code",
"execution_count": 34,
"metadata": {},
"outputs": [],
"source": [
"def show_one_difference(left, right):\n",
" run = left.exclusive_run(right)\n",
" if not run:\n",
" print(\"The two automata are equivalent.\")\n",
" else:\n",
" print(\"The following word is only accepted by one automaton:\", spot.make_twa_word(run))\n",
" run.highlight(5)\n",
" display_inline(left, right)"
]
},
{
"cell_type": "code",
"execution_count": 35,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"The following word is only accepted by one automaton: cycle{!a; a; !a}\n"
]
},
{
"data": {
"text/html": [
"<div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
" -->\n",
"<!-- Pages: 1 -->\n",
"<svg width=\"82pt\" height=\"161pt\"\n",
" viewBox=\"0.00 0.00 82.00 161.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 157)\">\n",
"<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-157 78,-157 78,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"16\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"38\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"54\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n",
"<text text-anchor=\"start\" x=\"14\" y=\"-124.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>I&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-18C4.178,-18 17.9448,-18 30.9241,-18\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-18 30.9808,-21.1501 34.4807,-18 30.9807,-18.0001 30.9807,-18.0001 30.9807,-18.0001 34.4807,-18 30.9807,-14.8501 37.9807,-18 37.9807,-18\"/>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"#e31a1c\" stroke-width=\"2\" d=\"M52.7643,-35.7817C52.2144,-45.3149 53.293,-54 56,-54 57.988,-54 59.0977,-49.3161 59.3292,-43.0521\"/>\n",
"<polygon fill=\"#e31a1c\" stroke=\"#e31a1c\" stroke-width=\"2\" points=\"59.2357,-35.7817 62.4756,-42.7406 59.7808,-39.275 59.8258,-42.7747 59.3258,-42.7812 58.8259,-42.7876 58.7808,-39.2879 56.1761,-42.8217 59.2357,-35.7817 59.2357,-35.7817\"/>\n",
"<text text-anchor=\"start\" x=\"50.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">!a</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"#e31a1c\" stroke-width=\"2\" d=\"M50.6841,-35.4203C47.6538,-52.791 49.4258,-72 56,-72 61.7011,-72 63.7908,-57.5545 62.2691,-42.3894\"/>\n",
"<polygon fill=\"#e31a1c\" stroke=\"#e31a1c\" stroke-width=\"2\" points=\"61.3159,-35.4203 65.3856,-41.9288 62.2856,-38.8202 62.76,-42.2879 62.2646,-42.3557 61.7692,-42.4235 61.2949,-38.9558 59.1437,-42.7826 61.3159,-35.4203 61.3159,-35.4203\"/>\n",
"<text text-anchor=\"start\" x=\"52.5\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a</text>\n",
"<text text-anchor=\"start\" x=\"48\" y=\"-75.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n",
"</div><div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
" -->\n",
"<!-- Pages: 1 -->\n",
"<svg width=\"169pt\" height=\"125pt\"\n",
" viewBox=\"0.00 0.00 169.00 124.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 120.8)\">\n",
"<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-120.8 165,-120.8 165,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"57.5\" y=\"-86.6\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Büchi]</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>I&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M1.1233,-22C4.178,-22 17.9448,-22 30.9241,-22\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"37.9807,-22 30.9808,-25.1501 34.4807,-22 30.9807,-22.0001 30.9807,-22.0001 30.9807,-22.0001 34.4807,-22 30.9807,-18.8501 37.9807,-22 37.9807,-22\"/>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n",
"<text text-anchor=\"start\" x=\"51.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"#000000\" cx=\"139\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
"<ellipse fill=\"none\" stroke=\"#000000\" cx=\"139\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
"<text text-anchor=\"start\" x=\"134.5\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M74.0098,-22C84.4333,-22 97.8048,-22 109.7062,-22\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"116.887,-22 109.887,-25.1501 113.387,-22 109.887,-22.0001 109.887,-22.0001 109.887,-22.0001 113.387,-22 109.8869,-18.8501 116.887,-22 116.887,-22\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M131.3173,-42.9908C130.3688,-53.0872 132.9297,-62 139,-62 143.5527,-62 146.1314,-56.9866 146.7361,-50.2204\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"146.6827,-42.9908 149.8844,-49.9673 146.7086,-46.4907 146.7345,-49.9906 146.7345,-49.9906 146.7345,-49.9906 146.7086,-46.4907 143.5846,-50.0139 146.6827,-42.9908 146.6827,-42.9908\"/>\n",
"<text text-anchor=\"start\" x=\"135.5\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">a</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n",
"</div>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"show_one_difference(aut_f, aut_g)"
]
},
{
"cell_type": "code",
"execution_count": 36,
"metadata": {},
"outputs": [
{
"ename": "NameError",
"evalue": "name 'run' is not defined",
"output_type": "error",
"traceback": [
"\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
"\u001b[0;31mNameError\u001b[0m Traceback (most recent call last)",
"\u001b[0;32m<ipython-input-36-d7d1b4bd9ffe>\u001b[0m in \u001b[0;36m<module>\u001b[0;34m()\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mrun\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mget_aut\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
"\u001b[0;31mNameError\u001b[0m: name 'run' is not defined"
]
}
],
"source": [
"run.get_aut()"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
@ -320,7 +530,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.6.5"
"version": "3.6.6"
}
},
"nbformat": 4,