Commit 65a729ab authored by Etienne Renault's avatar Etienne Renault

Add remove_fin Python binding.

* wrap/python/spot_impl.i: here.
* wrap/python/tests/automata.ipynb: tests here.
parent f067dd78
......@@ -129,6 +129,7 @@ namespace std {
#include "tgbaalgos/magic.hh"
#include "tgbaalgos/minimize.hh"
#include "tgbaalgos/neverclaim.hh"
#include "tgbaalgos/remfin.hh"
#include "tgbaalgos/safety.hh"
#include "tgbaalgos/sccfilter.hh"
#include "tgbaalgos/stats.hh"
......@@ -271,6 +272,7 @@ using namespace spot;
%include "tgbaalgos/minimize.hh"
%include "tgbaalgos/neverclaim.hh"
%include "tgbaalgos/safety.hh"
%include "tgbaalgos/remfin.hh"
%include "tgbaalgos/sccfilter.hh"
%include "tgbaalgos/stats.hh"
%include "tgbaalgos/isdet.hh"
......
......@@ -18,7 +18,7 @@
"version": "3.4.2"
},
"name": "",
"signature": "sha256:a45a88a09bb68e3c3ea4856e0dc7ab83ccc4afa607806beb1fa902de88e28792"
"signature": "sha256:a5b3af236b0c8dbdebad89d23ca023434c02a55b30bf8f5afd206daabc92c25b"
},
"nbformat": 3,
"nbformat_minor": 0,
......@@ -171,7 +171,7 @@
"</svg>\n"
],
"text": [
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x10f07d3c0> >"
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x105ac14b0> >"
]
}
],
......@@ -303,7 +303,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x10ea65390>"
"<IPython.core.display.SVG at 0x1054d1390>"
]
}
],
......@@ -449,7 +449,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x110a75a20>"
"<IPython.core.display.SVG at 0x1074df668>"
]
}
],
......@@ -542,7 +542,7 @@
"</svg>\n"
],
"text": [
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x110aae060> >"
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x10747f180> >"
]
}
],
......@@ -612,7 +612,7 @@
"</svg>\n"
],
"text": [
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x110aae120> >"
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x10747f210> >"
]
}
],
......@@ -681,7 +681,7 @@
"</svg>\n"
],
"text": [
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x110aae030> >"
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x10747f0f0> >"
]
}
],
......@@ -797,7 +797,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x110ab21d0>"
"<IPython.core.display.SVG at 0x107519198>"
]
}
],
......@@ -987,7 +987,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG at 0x110ac49e8>"
"<IPython.core.display.SVG at 0x10752c9e8>"
]
}
],
......@@ -1080,7 +1080,7 @@
"</svg>\n"
],
"text": [
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x10f0ecfc0> >"
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x10747f2d0> >"
]
}
],
......@@ -1554,7 +1554,7 @@
"</svg>\n"
],
"text": [
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x10f0ecba0> >"
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x105b2ed80> >"
]
}
],
......@@ -1579,6 +1579,193 @@
}
],
"prompt_number": 14
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"%%file example1.aut\n",
"HOA: v1\n",
"States: 3\n",
"Start: 0\n",
"AP: 2 \"a\" \"b\"\n",
"acc-name: Buchi\n",
"Acceptance: 4 Inf(0)&Fin(1)&Fin(3) | Inf(2)&Inf(3) | Inf(1)\n",
"--BODY--\n",
"State: 0 {3}\n",
"[t] 0\n",
"[0] 1 {1}\n",
"[!0] 2 {0}\n",
"State: 1 {3}\n",
"[1] 0\n",
"[0&1] 1 {0}\n",
"[!0&1] 2 {2}\n",
"State: 2\n",
"[!1] 0\n",
"[0&!1] 1 {0}\n",
"[!0&!1] 2 {0}\n",
"--END--"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"Writing example1.aut\n"
]
}
],
"prompt_number": 15
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"a = spot.automaton('example1.aut')\n",
"spot.remove_fin(a)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 16,
"svg": [
"<?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.36.0 (20140111.2315)\n",
" -->\n",
"<!-- Title: G Pages: 1 -->\n",
"<svg width=\"410pt\" height=\"160pt\"\n",
" viewBox=\"0.00 0.00 409.73 159.96\" 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 155.955)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-155.955 405.733,-155.955 405.733,4 -4,4\"/>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\"><title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"58\" cy=\"-26.3554\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"58\" y=\"-23.5553\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M2.15778,-26.3554C3.85328,-26.3554 18.9155,-26.3554 32.8257,-26.3554\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"39.9179,-26.3554 32.918,-29.5055 36.4179,-26.3554 32.9179,-26.3555 32.9179,-26.3555 32.9179,-26.3555 36.4179,-26.3554 32.9179,-23.2055 39.9179,-26.3554 39.9179,-26.3554\"/>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M51.6208,-43.3927C50.3189,-53.2133 52.4453,-62.3554 58,-62.3554 62.166,-62.3554 64.4036,-57.2129 64.7128,-50.4987\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"64.3792,-43.3927 67.8541,-50.2372 64.5434,-46.8888 64.7076,-50.385 64.7076,-50.385 64.7076,-50.385 64.5434,-46.8888 61.561,-50.5327 64.3792,-43.3927 64.3792,-43.3927\"/>\n",
"<text text-anchor=\"start\" x=\"53.94\" y=\"-84.7553\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"<text text-anchor=\"start\" x=\"50.2615\" y=\"-67.9553\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#b276b2\">\u2778</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\"><title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"162\" cy=\"-82.3554\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"162\" y=\"-79.5553\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M65.4225,-43.0425C71.0198,-55.1011 80.3931,-70.5826 94,-78.3554 106.891,-85.7193 123.546,-86.7442 137.025,-85.9157\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"144.143,-85.2933 137.444,-89.0412 140.656,-85.5983 137.17,-85.9032 137.17,-85.9032 137.17,-85.9032 140.656,-85.5983 136.895,-82.7652 144.143,-85.2933 144.143,-85.2933\"/>\n",
"<text text-anchor=\"start\" x=\"106.521\" y=\"-104.155\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
"<text text-anchor=\"start\" x=\"94.523\" y=\"-90.1554\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
"<text text-anchor=\"start\" x=\"110\" y=\"-90.1554\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#b276b2\">\u2778</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node4\" class=\"node\"><title>2</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"270\" cy=\"-26.3554\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"270\" y=\"-23.5553\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;2 -->\n",
"<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M76.2453,-25.1482C93.4101,-24.0112 120.511,-22.3906 144,-21.7555 179.018,-20.8086 219.537,-22.8815 244.72,-24.5444\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"252.02,-25.0435 244.821,-27.7086 248.528,-24.8047 245.036,-24.5659 245.036,-24.5659 245.036,-24.5659 248.528,-24.8047 245.251,-21.4233 252.02,-25.0435 252.02,-25.0435\"/>\n",
"<text text-anchor=\"start\" x=\"156.638\" y=\"-44.7553\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
"<text text-anchor=\"start\" x=\"154.262\" y=\"-27.9553\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#b276b2\">\u2778</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M151.834,-67.0501C145.648,-58.0367 136.676,-47.1772 126,-40.7555 113.097,-32.994 96.5758,-29.3872 83.1681,-27.7241\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"76.0825,-26.9861 83.3712,-24.5783 79.5637,-27.3487 83.0448,-27.7113 83.0448,-27.7113 83.0448,-27.7113 79.5637,-27.3487 82.7185,-30.8444 76.0825,-26.9861 76.0825,-26.9861\"/>\n",
"<text text-anchor=\"start\" x=\"106.08\" y=\"-63.7553\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
"<text text-anchor=\"start\" x=\"102.261\" y=\"-46.9553\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#b276b2\">\u2778</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M153.021,-98.2714C150.679,-108.506 153.672,-118.355 162,-118.355 168.376,-118.355 171.625,-112.582 171.746,-105.282\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"170.979,-98.2714 174.872,-104.887 171.36,-101.751 171.741,-105.23 171.741,-105.23 171.741,-105.23 171.36,-101.751 168.61,-105.573 170.979,-98.2714 170.979,-98.2714\"/>\n",
"<text text-anchor=\"start\" x=\"146.033\" y=\"-140.755\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"154.262\" y=\"-123.955\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#b276b2\">\u2778</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M180.023,-79.7742C195.037,-76.9453 217.096,-71.4076 234,-61.3554 241.012,-57.1855 247.637,-51.2949 253.197,-45.5333\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"257.985,-40.3314 255.562,-47.6152 255.615,-42.9067 253.244,-45.4819 253.244,-45.4819 253.244,-45.4819 255.615,-42.9067 250.927,-43.3487 257.985,-40.3314 257.985,-40.3314\"/>\n",
"<text text-anchor=\"start\" x=\"198.15\" y=\"-94.1554\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"200.523\" y=\"-80.1554\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#faa43a\">\u2777</text>\n",
"<text text-anchor=\"start\" x=\"216\" y=\"-80.1554\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#b276b2\">\u2778</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;0 -->\n",
"<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M252.914,-19.6064C229.206,-10.4711 183.423,4.07831 144,-1.55541 122.429,-4.63797 98.6856,-11.9104 81.7891,-17.7876\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"74.9932,-20.2048 80.5328,-14.8911 78.2908,-19.0318 81.5885,-17.8589 81.5885,-17.8589 81.5885,-17.8589 78.2908,-19.0318 82.6441,-20.8268 74.9932,-20.2048 74.9932,-20.2048\"/>\n",
"<text text-anchor=\"start\" x=\"156.197\" y=\"-7.95533\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;1 -->\n",
"<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M251.801,-26.6353C236.67,-27.5854 214.54,-30.7406 198,-40.5554 189.438,-45.6361 182.003,-53.5987 176.214,-61.2171\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"172.117,-66.9224 173.642,-59.3991 174.159,-64.0795 176.2,-61.2365 176.2,-61.2365 176.2,-61.2365 174.159,-64.0795 178.759,-63.0739 172.117,-66.9224 172.117,-66.9224\"/>\n",
"<text text-anchor=\"start\" x=\"198.15\" y=\"-46.9553\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;2 -->\n",
"<g id=\"edge10\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M260.767,-41.8968C258.169,-52.2641 261.246,-62.3554 270,-62.3554 276.702,-62.3554 280.077,-56.44 280.124,-49.0144\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"279.233,-41.8968 283.229,-48.4508 279.668,-45.3697 280.103,-48.8425 280.103,-48.8425 280.103,-48.8425 279.668,-45.3697 276.977,-49.2342 279.233,-41.8968 279.233,-41.8968\"/>\n",
"<text text-anchor=\"start\" x=\"250.267\" y=\"-67.9553\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node5\" class=\"node\"><title>3</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"382\" cy=\"-26.3554\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"382\" y=\"-23.5553\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;3 -->\n",
"<g id=\"edge11\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M288.188,-26.3554C306.593,-26.3554 335.947,-26.3554 356.709,-26.3554\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"363.933,-26.3554 356.933,-29.5055 360.433,-26.3554 356.933,-26.3555 356.933,-26.3555 356.933,-26.3555 360.433,-26.3554 356.933,-23.2055 363.933,-26.3554 363.933,-26.3554\"/>\n",
"<text text-anchor=\"start\" x=\"306.267\" y=\"-31.9553\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;3 -->\n",
"<g id=\"edge12\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M372.425,-41.8968C369.73,-52.2641 372.922,-62.3554 382,-62.3554 388.95,-62.3554 392.45,-56.44 392.499,-49.0144\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"391.575,-41.8968 395.6,-48.4325 392.026,-45.3676 392.477,-48.8385 392.477,-48.8385 392.477,-48.8385 392.026,-45.3676 389.353,-49.2444 391.575,-41.8968 391.575,-41.8968\"/>\n",
"<text text-anchor=\"start\" x=\"362.267\" y=\"-84.7553\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
"<text text-anchor=\"start\" x=\"374.262\" y=\"-67.9553\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text": [
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x105b2ec90> >"
]
}
],
"prompt_number": 16
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"!rm example1.aut"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 17
}
],
"metadata": {}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment