Commit 5a5f83f4 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

python: add missing bindings for twa_word and twa_run

Fixes #133.

* python/spot/impl.i: Add bindings for twa_word.  Add a __repr__
for twa_run, and instantiate templates for twa_run's members.
* tests/python/word.ipynb: New file with examples.
* tests/Makefile.am, doc/org/tut.org: Add it.
parent eb0a0b6b
......@@ -63,3 +63,4 @@ real notebooks instead.
automaton
- [[https://spot.lrde.epita.fr/ipynb/ltsmin.html][=ltsmin.ipynb=]] minimal test for loading a DiVinE model using
the LTSmin interface.
- [[https://spot.lrde.epita.fr/ipynb/ltsmin.html][=word.ipynb=]] example for the =twa_run= and =twa_word= classes.
......@@ -63,6 +63,7 @@
%shared_ptr(spot::taa_tgba_formula)
%shared_ptr(spot::twa_safra_complement)
%shared_ptr(spot::twa_run)
%shared_ptr(spot::twa_word)
%shared_ptr(spot::emptiness_check_result)
%shared_ptr(spot::emptiness_check)
%shared_ptr(spot::emptiness_check_instantiator)
......@@ -140,6 +141,7 @@
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/dtwasat.hh>
#include <spot/twaalgos/relabel.hh>
#include <spot/twaalgos/word.hh>
#include <spot/parseaut/public.hh>
......@@ -411,7 +413,9 @@ namespace std {
%include <spot/twaalgos/copy.hh>
%include <spot/twaalgos/complete.hh>
%include <spot/twaalgos/complement.hh>
%feature("flatnested") spot::twa_run::step;
%include <spot/twaalgos/emptiness.hh>
%template(list_step) std::list<spot::twa_run::step>;
%include <spot/twaalgos/gtec/gtec.hh>
%include <spot/twaalgos/lbtt.hh>
%include <spot/twaalgos/ltl2taa.hh>
......@@ -434,6 +438,9 @@ namespace std {
%include <spot/twaalgos/hoa.hh>
%include <spot/twaalgos/dtwasat.hh>
%include <spot/twaalgos/relabel.hh>
%include <spot/twaalgos/word.hh>
%template(list_bdd) std::list<bdd>;
%include <spot/parseaut/public.hh>
......@@ -605,6 +612,29 @@ namespace std {
}
%extend spot::twa_run {
std::string __repr__()
{
std::ostringstream os;
os << *self;
return os.str();
}
std::string __str__()
{
std::ostringstream os;
os << *self;
return os.str();
}
}
%extend spot::twa_word {
std::string __repr__()
{
std::ostringstream os;
os << *self;
return os.str();
}
std::string __str__()
{
std::ostringstream os;
......
......@@ -313,7 +313,8 @@ TESTS_python = \
python/satmin.py \
python/setxor.py \
python/testingaut.ipynb \
python/trival.py
python/trival.py \
python/word.ipynb
endif
CLEANFILES = python/test1.dve python/test1.dve2C python/test1.dve.cpp
......
{
"metadata": {
"name": "",
"signature": "sha256:e975b9a64657f38248c434a89f29b28f0bf90f9c40b7e8afdd7459734cbdcd38"
},
"nbformat": 3,
"nbformat_minor": 0,
"worksheets": [
{
"cells": [
{
"cell_type": "code",
"collapsed": false,
"input": [
"import spot\n",
"spot.setup()"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 1
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Let's build a small automaton to use as example."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"aut = spot.translate('G(Fa <-> Xb)'); aut"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 2,
"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.38.0 (20140413.2041)\n",
" -->\n",
"<!-- Title: G Pages: 1 -->\n",
"<svg width=\"386pt\" height=\"155pt\"\n",
" viewBox=\"0.00 0.00 385.50 155.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 151)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-151 381.5,-151 381.5,4 -4,4\"/>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\"><title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-45\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-41.3\" 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=\"M1.15491,-45C2.79388,-45 17.1543,-45 30.6317,-45\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-45 30.9419,-48.1501 34.4419,-45 30.9419,-45.0001 30.9419,-45.0001 30.9419,-45.0001 34.4419,-45 30.9418,-41.8501 37.9419,-45 37.9419,-45\"/>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\"><title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"139\" cy=\"-96\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"139\" y=\"-92.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M71.8566,-54.3542C84.5306,-62.3341 102.896,-73.8976 117.061,-82.816\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"123.238,-86.7051 115.636,-85.641 120.276,-84.8402 117.314,-82.9754 117.314,-82.9754 117.314,-82.9754 120.276,-84.8402 118.992,-80.3097 123.238,-86.7051 123.238,-86.7051\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node4\" class=\"node\"><title>2</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"248\" cy=\"-61\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"248\" y=\"-57.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;2 -->\n",
"<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M74.1963,-46.4481C108.109,-49.3039 183.696,-55.6692 222.691,-58.953\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"229.979,-59.5667 222.74,-62.1181 226.492,-59.2729 223.004,-58.9792 223.004,-58.9792 223.004,-58.9792 226.492,-59.2729 223.268,-55.8403 229.979,-59.5667 229.979,-59.5667\"/>\n",
"<text text-anchor=\"start\" x=\"135.5\" y=\"-56.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node5\" class=\"node\"><title>3</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"357\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"357\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;3 -->\n",
"<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M74.3679,-43.4317C125.166,-38.8446 273.551,-25.4452 331.97,-20.17\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"338.957,-19.539 332.268,-23.3059 335.471,-19.8538 331.985,-20.1687 331.985,-20.1687 331.985,-20.1687 335.471,-19.8538 331.702,-17.0314 338.957,-19.539 338.957,-19.539\"/>\n",
"<text text-anchor=\"start\" x=\"188\" y=\"-37.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M131.969,-112.664C130.406,-122.625 132.75,-132 139,-132 143.688,-132 146.178,-126.727 146.471,-119.888\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"146.031,-112.664 149.601,-119.46 146.244,-116.158 146.456,-119.651 146.456,-119.651 146.456,-119.651 146.244,-116.158 143.312,-119.842 146.031,-112.664 146.031,-112.664\"/>\n",
"<text text-anchor=\"start\" x=\"120.5\" y=\"-135.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M157,-98.8379C172.054,-100.594 194.318,-101.307 212,-94 219.178,-91.0336 225.76,-85.8674 231.231,-80.4911\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"236.314,-75.1185 233.791,-82.3685 233.908,-77.6611 231.503,-80.2038 231.503,-80.2038 231.503,-80.2038 233.908,-77.6611 229.215,-78.039 236.314,-75.1185 236.314,-75.1185\"/>\n",
"<text text-anchor=\"start\" x=\"176.5\" y=\"-118.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"185.5\" y=\"-103.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;1 -->\n",
"<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M229.954,-62.6225C215.066,-64.4327 193.072,-68.0686 175,-75 169.996,-76.9191 164.895,-79.5369 160.19,-82.2732\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"154.066,-86.0235 158.39,-79.6814 157.05,-84.1956 160.035,-82.3677 160.035,-82.3677 160.035,-82.3677 157.05,-84.1956 161.68,-85.054 154.066,-86.0235 154.066,-86.0235\"/>\n",
"<text text-anchor=\"start\" x=\"175\" y=\"-78.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;2 -->\n",
"<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M238.767,-76.5414C236.169,-86.9087 239.246,-97 248,-97 254.702,-97 258.077,-91.0847 258.124,-83.6591\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"257.233,-76.5414 261.229,-83.0955 257.668,-80.0143 258.103,-83.4871 258.103,-83.4871 258.103,-83.4871 257.668,-80.0143 254.977,-83.8788 257.233,-76.5414 257.233,-76.5414\"/>\n",
"<text text-anchor=\"start\" x=\"231\" y=\"-115.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"240\" y=\"-100.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;3 -->\n",
"<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M265.251,-54.4692C283.425,-47.1658 312.983,-35.2873 333.402,-27.0815\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"339.947,-24.4513 334.626,-29.9844 336.699,-25.7565 333.452,-27.0616 333.452,-27.0616 333.452,-27.0616 336.699,-25.7565 332.277,-24.1388 339.947,-24.4513 339.947,-24.4513\"/>\n",
"<text text-anchor=\"start\" x=\"284\" y=\"-48.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;3 -->\n",
"<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M347.767,-33.5414C345.169,-43.9087 348.246,-54 357,-54 363.702,-54 367.077,-48.0847 367.124,-40.6591\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"366.233,-33.5414 370.229,-40.0955 366.668,-37.0143 367.103,-40.4871 367.103,-40.4871 367.103,-40.4871 366.668,-37.0143 363.977,-40.8788 366.233,-33.5414 366.233,-33.5414\"/>\n",
"<text text-anchor=\"start\" x=\"336.5\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
"<text text-anchor=\"start\" x=\"349\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f4f0c2e0810> >"
]
}
],
"prompt_number": 2
},
{
"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."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"run = spot.couvreur99(aut).check().accepting_run(); run"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 3,
"text": [
"Prefix:\n",
" 0\n",
" | !a\n",
"Cycle:\n",
" 1\n",
" | a & b\t{0}\n",
" 2\n",
" | !a & b"
]
}
],
"prompt_number": 3
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Accessing the contents of the run can be done via the `prefix` and `cycle` lists."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"print(spot.bdd_format_formula(aut.get_dict(), run.prefix[0].label))\n",
"print(run.cycle[0].acc)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"!a\n",
"{0}\n"
]
}
],
"prompt_number": 4
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"To convert the run into a word, using `spot.twa_word()`. Note that our runs are labeled by Boolean formulas that are not necessarily a conjunction of all involved litterals. The word is just the projection of the run on its labels."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"word = spot.twa_word(run); word"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 5,
"text": [
"!a; cycle{a & b; !a & b}"
]
}
],
"prompt_number": 5
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Accessing the different formulas (stored as BDDs) can be done again via the `prefix` and `cycle` lists."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"print(spot.bdd_format_formula(aut.get_dict(), word.prefix[0]))\n",
"print(spot.bdd_format_formula(aut.get_dict(), word.cycle[0]))\n",
"print(spot.bdd_format_formula(aut.get_dict(), word.cycle[1]))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"!a\n",
"a & b\n",
"!a & b\n"
]
}
],
"prompt_number": 6
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Calling `simplifify()` will produce a shorter word that is compatible with the original word. For instance in the above word, the initial `!a` is compatible with both `a & b` and `!a & b`. The word obtained by restricting `!a` to `!a & b` is therefore still accepted, but it allows removing the prefix by rotating the cycle:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"word.simplify()\n",
"word"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 7,
"text": [
"cycle{!a & b; a & b}"
]
}
],
"prompt_number": 7
}
],
"metadata": {}
}
]
}
\ No newline at end of file
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