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

python: more conventional __repr__ for several types

Browse source 
* NEWS: Mention the change.
* python/spot/__init__.py: Add _repr_latex_ for twa_word, and
remove __repr__ and __str__ for atomic_prop_set.
* python/spot/impl.i: Implement __repr__ and __str__ for
atomic_prop_set.  Fix __repr__ for trival, acc_code, acc_cond,
mark_t.  Remove __repr__ for twa_run and twa_word.
* tests/python/acc_cond.ipynb, tests/python/accparse.ipynb,
tests/python/atva16-fig2a.ipynb, tests/python/automata.ipynb,
tests/python/bdditer.py, tests/python/contains.ipynb,
tests/python/gen.ipynb, tests/python/highlighting.ipynb,
tests/python/ltlsimple.py, tests/python/ltsmin-dve.ipynb,
tests/python/product.ipynb, tests/python/relabel.py,
tests/python/satmin.ipynb tests/python/stutter-inv.ipynb,
tests/python/word.ipynb: Adjust test cases.
* tests/python/formulas.ipynb: Add test for atomic_prop_set.
This commit is contained in:
Alexandre Duret-Lutz 2018-11-02 17:18:42 +01:00
parent c3b7a691e4
commit 60296317c7
19 changed files with 686 additions and 700 deletions
Download patch file Download diff file Expand all files Collapse all files

16
NEWS
View file

@ -82,6 +82,22 @@ New in spot 2.6.3.dev (not yet released)
vector_rs_pairs) by acc_cond::is_rabin_like() and
acc_cond::is_streett_like() were not usable in Python.
- Many object types had __repr__() methods that would return the
same string as __str__(), contrary to Python usage where repr(x)
should try to show how to rebuild x. The following types have
been changed to follow this convention:
spot.acc_code
spot.acc_cond
spot.atomic_prop_set
spot.formula
spot.mark_t
spot.twa_run (__repr__ shows type and address)
spot.twa_word (likewise, but _repr_latex_ used in notebooks)
Note that this you were relying on the fact that Jupyter calls
repr() to display returned values, you may want to call print()
explicitely if you prefer the old representation.
New in spot 2.6.3 (2018-10-17)
Bugs fixed:

29
python/spot/__init__.py
View file

@ -352,19 +352,6 @@ class formula:
@_extend(atomic_prop_set)
class atomic_prop_set:
def __repr__(self):
res = '{'
comma = ''
for ap in self:
res += comma
comma = ', '
res += '"' + ap.ap_name() + '"'
res += '}'
return res
def __str__(self):
return self.__repr__()
def _repr_latex_(self):
res = '$\{'
comma = ''
@ -1147,6 +1134,22 @@ formula.show_mp_hierarchy = show_mp_hierarchy
@_extend(twa_word)
class twa_word:
def _repr_latex_(self):
bd = self.get_dict()
res = '$'
for idx, letter in enumerate(self.prefix):
if idx:
res += '; '
res += bdd_to_formula(letter, bd).to_str('j')
if len(res) > 1:
res += '; ';
res += '\\mathsf{cycle}\\{';
for idx, letter in enumerate(self.cycle):
if idx:
res += '; '
res += bdd_to_formula(letter, bd).to_str('j')
return res + '\\}$'
def as_svg(self):
"""
Build an SVG picture representing the word as a collection of

71
python/spot/impl.i
View file

@ -669,13 +669,42 @@ def state_is_accepting(self, src) -> "bool":
%include <spot/taalgos/stats.hh>
%include <spot/taalgos/minimize.hh>
%extend std::set<spot::formula> {
std::string __str__()
{
std::ostringstream os;
os << '{';
const char* sep = "";
for (spot::formula s: *self)
{
os << sep << '"' << spot::escape_str(spot::str_psl(s)) << '"';
sep = ", ";
}
os << '}';
return os.str();
}
std::string __repr__()
{
std::ostringstream os;
os << "spot.atomic_prop_set([";
const char* sep = "";
for (spot::formula s: *self)
{
os << sep
<< "spot.formula(\"" << spot::escape_str(spot::str_psl(s)) << "\")";
sep = ", ";
}
os << "])";
return os.str();
}
}
%extend spot::acc_cond::rs_pair {
std::string __repr__()
{
std::ostringstream os;
os << "spot.rs_pair(fin=[";
char* sep = "";
const char* sep = "";
for (unsigned s: self->fin.sets())
{
os << sep << s;
@ -696,9 +725,11 @@ def state_is_accepting(self, src) -> "bool":
%extend spot::trival {
std::string __repr__()
{
std::ostringstream os;
os << *self;
return os.str();
if (self->is_true())
return "spot.trival(True)";
if (self->is_false())
return "spot.trival(False)";
return "spot.trival_maybe()";
}
std::string __str__()
@ -752,7 +783,9 @@ def state_is_accepting(self, src) -> "bool":
unsigned __len__() { return self->size(); }
formula __getitem__(unsigned pos) { return (*self)[pos]; }
std::string __repr__() { return spot::str_psl(*self); }
std::string __repr__() {
return "spot.formula(\"" + spot::escape_str(spot::str_psl(*self)) + "\")";
}
std::string __str__() { return spot::str_psl(*self); }
}
@ -929,7 +962,7 @@ def state_is_accepting(self, src) -> "bool":
std::string __repr__()
{
std::ostringstream os;
os << *self;
os << "spot.acc_code(\"" << *self << "\")";
return os.str();
}
@ -951,7 +984,14 @@ def state_is_accepting(self, src) -> "bool":
std::string __repr__()
{
std::ostringstream os;
os << *self;
os << "spot.mark_t([";
const char* sep = "";
for (unsigned s: self->sets())
{
os << sep << s;
sep = ", ";
}
os << "])";
return os.str();
}
@ -967,7 +1007,8 @@ def state_is_accepting(self, src) -> "bool":
std::string __repr__()
{
std::ostringstream os;
os << *self;
os << "spot.acc_cond(" << self->num_sets() << ", \""
<< self->get_acceptance() << "\")";
return os.str();
}
@ -980,13 +1021,6 @@ def state_is_accepting(self, src) -> "bool":
}
%extend spot::twa_run {
std::string __repr__()
{
std::ostringstream os;
os << *self;
return os.str();
}
std::string __str__()
{
std::ostringstream os;
@ -996,13 +1030,6 @@ def state_is_accepting(self, src) -> "bool":
}
%extend spot::twa_word {
std::string __repr__()
{
std::ostringstream os;
os << *self;
return os.str();
}
std::string __str__()
{
std::ostringstream os;

494
tests/python/acc_cond.ipynb
View file

File diff suppressed because it is too large Load diff

76
tests/python/accparse.ipynb
View file

@ -3,9 +3,7 @@
{
"cell_type": "code",
"execution_count": 1,
"metadata": {
"collapsed": true
},
"metadata": {},
"outputs": [],
"source": [
"import spot\n",
@ -15,75 +13,58 @@
{
"cell_type": "code",
"execution_count": 2,
"metadata": {
"collapsed": false
},
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(Inf(0) & Fin(1)) | (Inf(2) & Fin(3))"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
"name": "stdout",
"output_type": "stream",
"text": [
"(Inf(0) & Fin(1)) | (Inf(2) & Fin(3))\n"
]
}
],
"source": [
"c = spot.acc_code('Inf(0)&Fin(1)|Inf(2)&Fin(3)'); c"
"c = spot.acc_code('Inf(0)&Fin(1)|Inf(2)&Fin(3)'); print(c)"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {
"collapsed": false
},
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(Fin(1) & Inf(0)) | (Fin(3) & Inf(2))"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
"name": "stdout",
"output_type": "stream",
"text": [
"(Fin(1) & Inf(0)) | (Fin(3) & Inf(2))\n"
]
}
],
"source": [
"c.to_dnf()"
"print(c.to_dnf())"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {
"collapsed": false
},
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(Inf(0) | Inf(2)) & (Inf(0) | Fin(3)) & (Inf(2) | Fin(1)) & (Fin(1)|Fin(3))"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
"name": "stdout",
"output_type": "stream",
"text": [
"(Inf(0) | Inf(2)) & (Inf(0) | Fin(3)) & (Inf(2) | Fin(1)) & (Fin(1)|Fin(3))\n"
]
}
],
"source": [
"c.to_cnf()"
"print(c.to_cnf())"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {
"collapsed": false
},
"metadata": {},
"outputs": [
{
"name": "stdout",
@ -141,15 +122,6 @@
" ]:\n",
" print(acc, ': ', spot.acc_code(acc), sep='')"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {
"collapsed": false
},
"outputs": [],
"source": []
}
],
"metadata": {
@ -168,7 +140,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.5.3+"
"version": "3.6.7"
}
},
"nbformat": 4,

6
tests/python/atva16-fig2a.ipynb
View file

@ -28,7 +28,7 @@
"$\\mathsf{G} \\mathsf{F} a \\leftrightarrow \\mathsf{G} \\mathsf{F} b$"
],
"text/plain": [
"GFa <-> GFb"
"spot.formula(\"GFa <-> GFb\")"
]
},
"execution_count": 2,
@ -155,7 +155,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f81a85ea1e0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f62d41ff690> >"
]
},
"execution_count": 3,
@ -238,7 +238,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.6.5"
"version": "3.6.7"
}
},
"nbformat": 4,

48
tests/python/automata.ipynb
View file

@ -16,7 +16,7 @@
"cell_type": "markdown",
"metadata": {},
"source": [
"To build an automaton, simply call `translate()` with a formula, and a list of options to characterize the automaton you want (those options have the same name as the long options name of the `ltl2tgba` tool, and they can be abbreviated)."
"To build an automaton from an LTL formula, simply call `translate()` with a formula, and a list of options to characterize the automaton you want (those options have the same name as the long options name of the `ltl2tgba` tool, and they can be abbreviated)."
]
},
{
@ -178,7 +178,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe06cf120> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d1c0b2de0> >"
]
},
"execution_count": 2,
@ -567,7 +567,7 @@
"$a \\mathbin{\\mathsf{U}} b$"
],
"text/plain": [
"a U b"
"spot.formula(\"a U b\")"
]
},
"execution_count": 5,
@ -643,7 +643,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe05eda80> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d1c02c930> >"
]
},
"execution_count": 6,
@ -719,7 +719,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe05edab0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d1c02c960> >"
]
},
"execution_count": 7,
@ -802,7 +802,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe05edae0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d1c02ca80> >"
]
},
"execution_count": 8,
@ -832,7 +832,7 @@
"$\\mathsf{G} a \\lor \\mathsf{G} b \\lor \\mathsf{G} c$"
],
"text/plain": [
"Ga | Gb | Gc"
"spot.formula(\"Ga | Gb | Gc\")"
]
},
"execution_count": 9,
@ -1321,7 +1321,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe05edba0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d1c03ec90> >"
]
},
"execution_count": 12,
@ -1435,7 +1435,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe05edcf0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d1c03edb0> >"
]
},
"execution_count": 13,
@ -1566,7 +1566,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe05ed930> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d1c03ecf0> >"
]
},
"execution_count": 14,
@ -1785,7 +1785,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe05eda50> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d077c1540> >"
]
},
"metadata": {},
@ -1935,7 +1935,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe06cf0c0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d1c02c630> >"
]
},
"metadata": {},
@ -2107,7 +2107,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe05edb40> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d077c1780> >"
]
},
"metadata": {},
@ -2282,7 +2282,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe05edbd0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d077c1660> >"
]
},
"metadata": {},
@ -2468,7 +2468,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe05ed870> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d077c1810> >"
]
},
"execution_count": 19,
@ -2544,7 +2544,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe05ed8d0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d077c1930> >"
]
},
"execution_count": 20,
@ -3062,7 +3062,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe05ed9c0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d077c1e40> >"
]
},
"metadata": {},
@ -3162,7 +3162,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe05ed9f0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d1c02c750> >"
]
},
"execution_count": 24,
@ -3235,7 +3235,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe05eda20> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d1c02c780> >"
]
},
"execution_count": 25,
@ -3399,7 +3399,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe05edb40> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d1c03ed80> >"
]
},
"execution_count": 27,
@ -3482,7 +3482,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe05ed9c0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d077c1e40> >"
]
},
"metadata": {},
@ -3547,7 +3547,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe05ed9c0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d077c1e40> >"
]
},
"metadata": {},
@ -3634,7 +3634,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effe05ed9c0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d077c1e40> >"
]
},
"execution_count": 29,
@ -3667,7 +3667,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.6.6"
"version": "3.6.7"
}
},
"nbformat": 4,

6
tests/python/bdditer.py
View file

@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita
# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de l'Epita
# (LRDE).
#
# This file is part of Spot, a model checking library.
@ -44,8 +44,8 @@ assert res == [0, -1]
res2 = []
for i in run.aut.ap():
res2.append((i, run.aut.register_ap(i)))
assert str(res2) == '[(a, 0), (b, 1)]'
res2.append((str(i), run.aut.register_ap(i)))
assert str(res2) == "[('a', 0), ('b', 1)]"
f = spot.bdd_to_formula(b)

7
tests/python/contains.ipynb
View file

@ -322,8 +322,11 @@
"outputs": [
{
"data": {
"text/latex": [
"$\\mathsf{cycle}\\{a; \\lnot a\\}$"
],
"text/plain": [
"cycle{a; !a}"
"<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7faa9424d9c0> >"
]
},
"execution_count": 16,
@ -502,7 +505,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.6.6"
"version": "3.6.7"
}
},
"nbformat": 4,

67
tests/python/formulas.ipynb
View file

@ -14,7 +14,8 @@
"metadata": {},
"outputs": [],
"source": [
"import spot"
"import spot\n",
"from IPython.display import display # not needed with recent Jupyter"
]
},
{
@ -35,7 +36,7 @@
"$p_{1} \\mathbin{\\mathsf{U}} (p_{2} \\mathbin{\\mathsf{R}} (p_{3} \\land \\lnot p_{4}))$"
],
"text/plain": [
"p1 U (p2 R (p3 & !p4))"
"spot.formula(\"p1 U (p2 R (p3 & !p4))\")"
]
},
"execution_count": 2,
@ -59,7 +60,7 @@
"$\\{a \\mathbin{\\mathsf{;}} b^{\\star} \\mathbin{\\mathsf{;}} c^+\\}\\mathrel{\\Diamond\\kern-1.7pt\\raise.4pt\\hbox{$\\mathord{\\rightarrow}$}} \\mathsf{G} \\mathsf{F} b$"
],
"text/plain": [
"{a;b[*];c[+]}<>-> GFb"
"spot.formula(\"{a;b[*];c[+]}<>-> GFb\")"
]
},
"execution_count": 3,
@ -89,7 +90,7 @@
"$c \\land (a \\lor b)$"
],
"text/plain": [
"c & (a | b)"
"spot.formula(\"c & (a | b)\")"
]
},
"execution_count": 4,
@ -119,7 +120,7 @@
"$c \\land (a \\lor b)$"
],
"text/plain": [
"c & (a | b)"
"spot.formula(\"c & (a | b)\")"
]
},
"execution_count": 5,
@ -422,7 +423,7 @@
"$\\unicode{x201C}\\mathit{a > b}\\unicode{x201D} \\land \\unicode{x201C}\\mathit{proc[2]@init}\\unicode{x201D} \\land \\mathsf{G} \\mathsf{F} \\mathit{\\_foo\\_}$"
],
"text/plain": [
"\"a > b\" & \"proc[2]@init\" & GF_foo_"
"spot.formula(\"\\\"a > b\\\" & \\\"proc[2]@init\\\" & GF_foo_\")"
]
},
"execution_count": 15,
@ -445,7 +446,7 @@
"$a \\land b \\land \\mathsf{G} \\mathsf{F} c$"
],
"text/plain": [
"a & b & GFc"
"spot.formula(\"a & b & GFc\")"
]
},
"execution_count": 16,
@ -468,7 +469,7 @@
"$p_{0} \\land p_{1} \\land \\mathsf{G} \\mathsf{F} p_{2}$"
],
"text/plain": [
"p0 & p1 & GFp2"
"spot.formula(\"p0 & p1 & GFp2\")"
]
},
"execution_count": 17,
@ -719,7 +720,7 @@
"$\\mathsf{F} (a \\land \\mathsf{X} (\\lnot a \\land b))$"
],
"text/plain": [
"F(a & X(!a & b))"
"spot.formula(\"F(a & X(!a & b))\")"
]
},
"execution_count": 21,
@ -749,7 +750,7 @@
"$\\mathsf{F} (a \\land ((a \\land (a \\mathbin{\\mathsf{U}} (\\lnot a \\land b)) \\land ((\\lnot b \\mathbin{\\mathsf{U}} \\lnot a) \\lor (b \\mathbin{\\mathsf{U}} \\lnot a))) \\lor (\\lnot a \\land (\\lnot a \\mathbin{\\mathsf{U}} (a \\land \\lnot a \\land b)) \\land ((\\lnot b \\mathbin{\\mathsf{U}} a) \\lor (b \\mathbin{\\mathsf{U}} a))) \\lor (b \\land (b \\mathbin{\\mathsf{U}} (\\lnot a \\land b \\land \\lnot b)) \\land ((\\lnot a \\mathbin{\\mathsf{U}} \\lnot b) \\lor (a \\mathbin{\\mathsf{U}} \\lnot b))) \\lor (\\lnot b \\land (\\lnot b \\mathbin{\\mathsf{U}} (\\lnot a \\land b)) \\land ((\\lnot a \\mathbin{\\mathsf{U}} b) \\lor (a \\mathbin{\\mathsf{U}} b))) \\lor (\\lnot a \\land b \\land (\\mathsf{G} \\lnot a \\lor \\mathsf{G} a) \\land (\\mathsf{G} \\lnot b \\lor \\mathsf{G} b))))$"
],
"text/plain": [
"F(a & ((a & (a U (!a & b)) & ((!b U !a) | (b U !a))) | (!a & (!a U (a & !a & b)) & ((!b U a) | (b U a))) | (b & (b U (!a & b & !b)) & ((!a U !b) | (a U !b))) | (!b & (!b U (!a & b)) & ((!a U b) | (a U b))) | (!a & b & (G!a | Ga) & (G!b | Gb))))"
"spot.formula(\"F(a & ((a & (a U (!a & b)) & ((!b U !a) | (b U !a))) | (!a & (!a U (a & !a & b)) & ((!b U a) | (b U a))) | (b & (b U (!a & b & !b)) & ((!a U !b) | (a U !b))) | (!b & (!b U (!a & b)) & ((!a U b) | (a U b))) | (!a & b & (G!a | Ga) & (G!b | Gb))))\")"
]
},
"execution_count": 22,
@ -779,7 +780,7 @@
"$(\\bot \\mathbin{\\mathsf{R}} \\lnot (a \\leftrightarrow b)) \\rightarrow (\\top \\mathbin{\\mathsf{U}} (a \\leftrightarrow b))$"
],
"text/plain": [
"(0 R !(a <-> b)) -> (1 U (a <-> b))"
"spot.formula(\"(0 R !(a <-> b)) -> (1 U (a <-> b))\")"
]
},
"execution_count": 23,
@ -803,7 +804,7 @@
"$(\\top \\mathbin{\\mathsf{U}} ((a \\land b) \\lor (\\lnot a \\land \\lnot b))) \\lor \\lnot (\\bot \\mathbin{\\mathsf{R}} ((\\lnot a \\land b) \\lor (a \\land \\lnot b)))$"
],
"text/plain": [
"(1 U ((a & b) | (!a & !b))) | !(0 R ((!a & b) | (a & !b)))"
"spot.formula(\"(1 U ((a & b) | (!a & !b))) | !(0 R ((!a & b) | (a & !b)))\")"
]
},
"execution_count": 24,
@ -850,6 +851,46 @@
"# operator, you can count both with\n",
"print(\"FU\", spot.nesting_depth(f, \"FU\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Collecting the set of atomic propositions used by a formula:"
]
},
{
"cell_type": "code",
"execution_count": 26,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"spot.atomic_prop_set([spot.formula(\"a\"), spot.formula(\"b\"), spot.formula(\"c\"), spot.formula(\"d\")])\n",
"{\"a\", \"b\", \"c\", \"d\"}\n"
]
},
{
"data": {
"text/latex": [
"$\\{\\unicode{x201C}a\\unicode{x201D}, \\unicode{x201C}b\\unicode{x201D}, \\unicode{x201C}c\\unicode{x201D}, \\unicode{x201C}d\\unicode{x201D}\\}$"
],
"text/plain": [
"spot.atomic_prop_set([spot.formula(\"a\"), spot.formula(\"b\"), spot.formula(\"c\"), spot.formula(\"d\")])"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"ap = spot.atomic_prop_collect(f)\n",
"print(repr(ap)) # print as an atomic_prop_set object\n",
"print(ap) # print as a string\n",
"display(ap) # LaTeX-style, for notebooks"
]
}
],
"metadata": {
@ -868,7 +909,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.6.5"
"version": "3.6.7"
}
},
"nbformat": 4,

68
tests/python/gen.ipynb
View file

@ -41,7 +41,7 @@
"$\\mathsf{G} \\mathsf{F} p_{1} \\land \\mathsf{G} \\mathsf{F} p_{2} \\land \\mathsf{G} \\mathsf{F} p_{3}$"
],
"text/plain": [
"GFp1 & GFp2 & GFp3"
"spot.formula(\"GFp1 & GFp2 & GFp3\")"
]
},
"execution_count": 2,
@ -64,7 +64,7 @@
"$\\mathsf{F} (p \\land \\mathsf{X} p \\land \\mathsf{X} \\mathsf{X} p \\land \\mathsf{X} \\mathsf{X} \\mathsf{X} p) \\land \\mathsf{F} (q \\land \\mathsf{X} q \\land \\mathsf{X} \\mathsf{X} q \\land \\mathsf{X} \\mathsf{X} \\mathsf{X} q)$"
],
"text/plain": [
"F(p & Xp & XXp & XXXp) & F(q & Xq & XXq & XXXq)"
"spot.formula(\"F(p & Xp & XXp & XXXp) & F(q & Xq & XXq & XXXq)\")"
]
},
"execution_count": 3,
@ -103,7 +103,7 @@
"$(\\mathsf{G} \\mathsf{F} p_{1} \\lor \\mathsf{F} \\mathsf{G} p_{2}) \\land (\\mathsf{G} \\mathsf{F} p_{2} \\lor \\mathsf{F} \\mathsf{G} p_{3}) \\land (\\mathsf{G} \\mathsf{F} p_{3} \\lor \\mathsf{F} \\mathsf{G} p_{4})$"
],
"text/plain": [
"(GFp1 | FGp2) & (GFp2 | FGp3) & (GFp3 | FGp4)"
"spot.formula(\"(GFp1 | FGp2) & (GFp2 | FGp3) & (GFp3 | FGp4)\")"
]
},
"metadata": {},
@ -115,7 +115,7 @@
"$\\mathsf{F} \\mathsf{G} p_{1}$"
],
"text/plain": [
"FGp1"
"spot.formula(\"FGp1\")"
]
},
"metadata": {},
@ -127,7 +127,7 @@
"$\\mathsf{F} \\mathsf{G} p_{1} \\land \\mathsf{F} \\mathsf{G} p_{2}$"
],
"text/plain": [
"FGp1 & FGp2"
"spot.formula(\"FGp1 & FGp2\")"
]
},
"metadata": {},
@ -139,7 +139,7 @@
"$\\mathsf{F} \\mathsf{G} p_{1} \\land \\mathsf{F} \\mathsf{G} p_{2} \\land \\mathsf{F} \\mathsf{G} p_{3}$"
],
"text/plain": [
"FGp1 & FGp2 & FGp3"
"spot.formula(\"FGp1 & FGp2 & FGp3\")"
]
},
"metadata": {},
@ -151,7 +151,7 @@
"$p_{0} \\mathbin{\\mathsf{U}} (p_{1} \\land \\mathsf{G} p_{2})$"
],
"text/plain": [
"p0 U (p1 & Gp2)"
"spot.formula(\"p0 U (p1 & Gp2)\")"
]
},
"metadata": {},
@ -163,7 +163,7 @@
"$p_{0} \\mathbin{\\mathsf{U}} (p_{1} \\land \\mathsf{X} (p_{2} \\mathbin{\\mathsf{U}} p_{3}))$"
],
"text/plain": [
"p0 U (p1 & X(p2 U p3))"
"spot.formula(\"p0 U (p1 & X(p2 U p3))\")"
]
},
"metadata": {},
@ -175,7 +175,7 @@
"$p_{0} \\mathbin{\\mathsf{U}} (p_{1} \\land \\mathsf{X} (p_{2} \\land \\mathsf{F} (p_{3} \\land \\mathsf{X} \\mathsf{F} (p_{4} \\land \\mathsf{X} \\mathsf{F} (p_{5} \\land \\mathsf{X} \\mathsf{F} p_{6})))))$"
],
"text/plain": [
"p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)))))"
"spot.formula(\"p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)))))\")"
]
},
"metadata": {},
@ -187,7 +187,7 @@
"$\\mathsf{F} (p_{0} \\land \\mathsf{X} \\mathsf{G} p_{1})$"
],
"text/plain": [
"F(p0 & XGp1)"
"spot.formula(\"F(p0 & XGp1)\")"
]
},
"metadata": {},
@ -199,7 +199,7 @@
"$\\mathsf{F} (p_{0} \\land \\mathsf{X} (p_{1} \\land \\mathsf{X} \\mathsf{F} p_{2}))$"
],
"text/plain": [
"F(p0 & X(p1 & XFp2))"
"spot.formula(\"F(p0 & X(p1 & XFp2))\")"
]
},
"metadata": {},
@ -211,7 +211,7 @@
"$\\mathsf{F} (p_{0} \\land \\mathsf{X} (p_{1} \\mathbin{\\mathsf{U}} p_{2}))$"
],
"text/plain": [
"F(p0 & X(p1 U p2))"
"spot.formula(\"F(p0 & X(p1 U p2))\")"
]
},
"metadata": {},
@ -223,7 +223,7 @@
"$\\mathsf{G} \\mathsf{F} p_{0} \\lor \\mathsf{F} \\mathsf{G} p_{1}$"
],
"text/plain": [
"GFp0 | FGp1"
"spot.formula(\"GFp0 | FGp1\")"
]
},
"metadata": {},
@ -235,7 +235,7 @@
"$\\mathsf{G} (p_{0} \\rightarrow (p_{1} \\mathbin{\\mathsf{U}} p_{2}))$"
],
"text/plain": [
"G(p0 -> (p1 U p2))"
"spot.formula(\"G(p0 -> (p1 U p2))\")"
]
},
"metadata": {},
@ -247,7 +247,7 @@
"$\\mathsf{G} (p_{0} \\land \\mathsf{X} \\mathsf{F} (p_{1} \\land \\mathsf{X} \\mathsf{F} (p_{2} \\land \\mathsf{X} \\mathsf{F} p_{3})))$"
],
"text/plain": [
"G(p0 & XF(p1 & XF(p2 & XFp3)))"
"spot.formula(\"G(p0 & XF(p1 & XF(p2 & XFp3)))\")"
]
},
"metadata": {},
@ -259,7 +259,7 @@
"$\\mathsf{G} \\mathsf{F} p_{1} \\land \\mathsf{G} \\mathsf{F} p_{2} \\land \\mathsf{G} \\mathsf{F} p_{3} \\land \\mathsf{G} \\mathsf{F} p_{0} \\land \\mathsf{G} \\mathsf{F} p_{4}$"
],
"text/plain": [
"GFp1 & GFp2 & GFp3 & GFp0 & GFp4"
"spot.formula(\"GFp1 & GFp2 & GFp3 & GFp0 & GFp4\")"
]
},
"metadata": {},
@ -271,7 +271,7 @@
"$(p_{0} \\mathbin{\\mathsf{U}} (p_{1} \\mathbin{\\mathsf{U}} p_{2})) \\lor (p_{1} \\mathbin{\\mathsf{U}} (p_{2} \\mathbin{\\mathsf{U}} p_{0})) \\lor (p_{2} \\mathbin{\\mathsf{U}} (p_{0} \\mathbin{\\mathsf{U}} p_{1}))$"
],
"text/plain": [
"(p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1))"
"spot.formula(\"(p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1))\")"
]
},
"metadata": {},
@ -283,7 +283,7 @@
"$\\mathsf{G} (p_{0} \\rightarrow (p_{1} \\mathbin{\\mathsf{U}} (\\mathsf{G} p_{2} \\lor \\mathsf{G} p_{3})))$"
],
"text/plain": [
"G(p0 -> (p1 U (Gp2 | Gp3)))"
"spot.formula(\"G(p0 -> (p1 U (Gp2 | Gp3)))\")"
]
},
"metadata": {},
@ -317,7 +317,7 @@
"$\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} b)$"
],
"text/plain": [
"GFa1 U G(GFa0 U Xb)"
"spot.formula(\"GFa1 U G(GFa0 U Xb)\")"
]
},
"metadata": {},
@ -329,7 +329,7 @@
"$\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} b)$"
],
"text/plain": [
"GFa1 U G(GFa0 U XXb)"
"spot.formula(\"GFa1 U G(GFa0 U XXb)\")"
]
},
"metadata": {},
@ -341,7 +341,7 @@
"$\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} \\mathsf{X} b)$"
],
"text/plain": [
"GFa1 U G(GFa0 U XXXb)"
"spot.formula(\"GFa1 U G(GFa0 U XXXb)\")"
]
},
"metadata": {},
@ -353,7 +353,7 @@
"$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} b))$"
],
"text/plain": [
"GFa2 U G(GFa1 U G(GFa0 U Xb))"
"spot.formula(\"GFa2 U G(GFa1 U G(GFa0 U Xb))\")"
]
},
"metadata": {},
@ -365,7 +365,7 @@
"$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} b))$"
],
"text/plain": [
"GFa2 U G(GFa1 U G(GFa0 U XXb))"
"spot.formula(\"GFa2 U G(GFa1 U G(GFa0 U XXb))\")"
]
},
"metadata": {},
@ -377,7 +377,7 @@
"$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} \\mathsf{X} b))$"
],
"text/plain": [
"GFa2 U G(GFa1 U G(GFa0 U XXXb))"
"spot.formula(\"GFa2 U G(GFa1 U G(GFa0 U XXXb))\")"
]
},
"metadata": {},
@ -389,7 +389,7 @@
"$\\mathsf{G} \\mathsf{F} a_{3} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} b)))$"
],
"text/plain": [
"GFa3 U G(GFa2 U G(GFa1 U G(GFa0 U Xb)))"
"spot.formula(\"GFa3 U G(GFa2 U G(GFa1 U G(GFa0 U Xb)))\")"
]
},
"metadata": {},
@ -401,7 +401,7 @@
"$\\mathsf{G} \\mathsf{F} a_{3} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} b)))$"
],
"text/plain": [
"GFa3 U G(GFa2 U G(GFa1 U G(GFa0 U XXb)))"
"spot.formula(\"GFa3 U G(GFa2 U G(GFa1 U G(GFa0 U XXb)))\")"
]
},
"metadata": {},
@ -413,7 +413,7 @@
"$\\mathsf{G} \\mathsf{F} a_{3} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} \\mathsf{X} b)))$"
],
"text/plain": [
"GFa3 U G(GFa2 U G(GFa1 U G(GFa0 U XXXb)))"
"spot.formula(\"GFa3 U G(GFa2 U G(GFa1 U G(GFa0 U XXXb)))\")"
]
},
"metadata": {},
@ -436,7 +436,7 @@
"$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} \\mathsf{X} b))$"
],
"text/plain": [
"GFa2 U G(GFa1 U G(GFa0 U XXXb))"
"spot.formula(\"GFa2 U G(GFa1 U G(GFa0 U XXXb))\")"
]
},
"metadata": {},
@ -448,7 +448,7 @@
"$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} b))$"
],
"text/plain": [
"GFa2 U G(GFa1 U G(GFa0 U XXb))"
"spot.formula(\"GFa2 U G(GFa1 U G(GFa0 U XXb))\")"
]
},
"metadata": {},
@ -460,7 +460,7 @@
"$\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} b)$"
],
"text/plain": [
"GFa1 U G(GFa0 U Xb)"
"spot.formula(\"GFa1 U G(GFa0 U Xb)\")"
]
},
"metadata": {},
@ -472,7 +472,7 @@
"$\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} b)$"
],
"text/plain": [
"GFa1 U G(GFa0 U XXb)"
"spot.formula(\"GFa1 U G(GFa0 U XXb)\")"
]
},
"metadata": {},
@ -484,7 +484,7 @@
"$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} b))$"
],
"text/plain": [
"GFa2 U G(GFa1 U G(GFa0 U Xb))"
"spot.formula(\"GFa2 U G(GFa1 U G(GFa0 U Xb))\")"
]
},
"metadata": {},
@ -496,7 +496,7 @@
"$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} b))$"
],
"text/plain": [
"GFa2 U G(GFa1 U G(GFa0 U XXb))"
"spot.formula(\"GFa2 U G(GFa1 U G(GFa0 U XXb))\")"
]
},
"metadata": {},
@ -1232,7 +1232,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.6.5"
"version": "3.6.7"
}
},
"nbformat": 4,

130
tests/python/highlighting.ipynb
View file

@ -240,7 +240,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6a44f3f090> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc2846aa7b0> >"
]
},
"execution_count": 4,
@ -352,7 +352,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7f6a44edacc0> >"
"<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7fc2846aa780> >"
]
},
"execution_count": 5,
@ -462,7 +462,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6a44f3f090> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc2846aa7b0> >"
]
},
"execution_count": 6,
@ -695,7 +695,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6a44eec0c0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc2845d2720> >"
]
},
"execution_count": 8,
@ -713,25 +713,23 @@
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Prefix:\n",
" 4\n",
" | 1\n",
" 0\n",
" | !a & !b\n",
"Cycle:\n",
" 1\n",
" | !b\t{0}"
]
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
"name": "stdout",
"output_type": "stream",
"text": [
"Prefix:\n",
" 4\n",
" | 1\n",
" 0\n",
" | !a & !b\n",
"Cycle:\n",
" 1\n",
" | !b\t{0}\n",
"\n"
]
}
],
"source": [
"r = b.accepting_run(); r"
"r = b.accepting_run(); print(r)"
]
},
{
@ -892,7 +890,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6a44eec0c0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc2845d2720> >"
]
},
"execution_count": 11,
@ -977,7 +975,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6a44e7cb70> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc2845e4f00> >"
]
},
"metadata": {},
@ -1032,7 +1030,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6a44e7c8a0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc2845e4e40> >"
]
},
"metadata": {},
@ -1126,7 +1124,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6a44e7c960> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc2845d2600> >"
]
},
"execution_count": 13,
@ -1144,23 +1142,21 @@
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Prefix:\n",
" 1,0\n",
" | !a & b\n",
"Cycle:\n",
" 0,0\n",
" | a\t{0}"
]
},
"execution_count": 14,
"metadata": {},
"output_type": "execute_result"
"name": "stdout",
"output_type": "stream",
"text": [
"Prefix:\n",
" 1,0\n",
" | !a & b\n",
"Cycle:\n",
" 0,0\n",
" | a\t{0}\n",
"\n"
]
}
],
"source": [
"run = prod.accepting_run(); run"
"run = prod.accepting_run(); print(run)"
]
},
{
@ -1257,7 +1253,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6a44e7c960> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc2845d2600> >"
]
},
"metadata": {},
@ -1322,7 +1318,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6a44e7cb70> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc2845e4f00> >"
]
},
"metadata": {},
@ -1377,7 +1373,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6a44e7c8a0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc2845e4e40> >"
]
},
"metadata": {},
@ -1401,24 +1397,23 @@
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Prefix:\n",
" 0 * 3\n",
" | a & !b\n",
" 1 * 2\n",
" | a\t{0}\n",
" 1 * 1\n",
" | a\t{0}\n",
" 1 * 0\n",
" | a & b\t{0}\n",
"Cycle:\n",
" 1 * 4\n",
" | a\t{0,1}"
]
},
"metadata": {},
"output_type": "display_data"
"name": "stdout",
"output_type": "stream",
"text": [
"Prefix:\n",
" 0 * 3\n",
" | a & !b\n",
" 1 * 2\n",
" | a\t{0}\n",
" 1 * 1\n",
" | a\t{0}\n",
" 1 * 0\n",
" | a & b\t{0}\n",
"Cycle:\n",
" 1 * 4\n",
" | a\t{0,1}\n",
"\n"
]
},
{
"data": {
@ -1609,7 +1604,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f6a44e7cf00> >"
"<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7fc284574690> >"
]
},
"metadata": {},
@ -1694,7 +1689,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6a44e7cf60> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc2845746f0> >"
]
},
"metadata": {},
@ -1791,7 +1786,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6a44e7cdb0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc284574570> >"
]
},
"metadata": {},
@ -1805,7 +1800,8 @@
"run2 = prod2.accepting_run()\n",
"run2.project(left2).highlight(5)\n",
"run2.project(right2, True).highlight(5)\n",
"display(run2, prod2, left2, right2)"
"print(run2)\n",
"display(prod2, left2, right2)"
]
},
{
@ -1959,7 +1955,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6a44e7cea0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc284574840> >"
]
},
"execution_count": 18,
@ -2127,7 +2123,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6a44e7cea0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc284574840> >"
]
},
"execution_count": 19,
@ -2290,7 +2286,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6a44e7cea0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc284574840> >"
]
},
"metadata": {},
@ -2765,7 +2761,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.6.6"
"version": "3.6.7"
}
},
"nbformat": 4,

2
tests/python/ltlsimple.py
View file

@ -73,7 +73,7 @@ del a, b, c, T, F, f1, f2, f4, f5
assert spot.fnode_instances_check()
#----------------------------------------------------------------------
assert str([x for x in spot.formula('a &b & c')]) == '[a, b, c]'
assert str([str(x) for x in spot.formula('a &b & c')]) == "['a', 'b', 'c']"
def switch_g_f(x):

59
tests/python/ltsmin-dve.ipynb
View file

@ -436,7 +436,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f306034fb70> >"
"<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f0f044132a0> >"
]
},
"execution_count": 9,
@ -1265,7 +1265,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f30602ddba0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0f04381d50> >"
]
},
"execution_count": 12,
@ -1453,7 +1453,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f306034f9c0> >"
"<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f0f04381b10> >"
]
},
"execution_count": 13,
@ -1483,7 +1483,7 @@
"$\\{\\unicode{x201C}\\mathit{a < 2}\\unicode{x201D}, \\unicode{x201C}\\mathit{b == 1}\\unicode{x201D}\\}$"
],
"text/plain": [
"{\"a < 2\", \"b == 1\"}"
"spot.atomic_prop_set([spot.formula(\"\\\"a < 2\\\"\"), spot.formula(\"\\\"b == 1\\\"\")])"
]
},
"execution_count": 14,
@ -1548,31 +1548,29 @@
},
{
"cell_type": "code",
"execution_count": 18,
"execution_count": 19,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Prefix:\n",
" a=0, b=0, Q=0\n",
" | \"a<1\" & !\"b > 1\" & !dead\n",
" a=1, b=0, Q=0\n",
" | !\"a<1\" & !\"b > 1\" & !dead\n",
" a=2, b=0, Q=0\n",
" | !\"a<1\" & !\"b > 1\" & !dead\n",
"Cycle:\n",
" a=3, b=0, Q=0\n",
" | !\"a<1\" & !\"b > 1\" & dead"
]
},
"execution_count": 18,
"metadata": {},
"output_type": "execute_result"
"name": "stdout",
"output_type": "stream",
"text": [
"Prefix:\n",
" a=0, b=0, Q=0\n",
" | \"a<1\" & !\"b > 1\" & !dead\n",
" a=1, b=0, Q=0\n",
" | !\"a<1\" & !\"b > 1\" & !dead\n",
" a=2, b=0, Q=0\n",
" | !\"a<1\" & !\"b > 1\" & !dead\n",
"Cycle:\n",
" a=3, b=0, Q=0\n",
" | !\"a<1\" & !\"b > 1\" & dead\n",
"\n"
]
}
],
"source": [
"run = model_debug('\"a<1\" R \"b > 1\"', m); run"
"run = model_debug('\"a<1\" R \"b > 1\"', m); print(run)"
]
},
{
@ -1584,7 +1582,7 @@
},
{
"cell_type": "code",
"execution_count": 19,
"execution_count": 20,
"metadata": {},
"outputs": [
{
@ -1665,10 +1663,10 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f30602dded0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0f04392d80> >"
]
},
"execution_count": 19,
"execution_count": 20,
"metadata": {},
"output_type": "execute_result"
}
@ -1676,6 +1674,13 @@
"source": [
"run.as_twa(True)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
@ -1694,7 +1699,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.6.5"
"version": "3.6.7"
}
},
"nbformat": 4,

19
tests/python/product.ipynb
View file

@ -1192,8 +1192,8 @@
"name": "stdout",
"output_type": "stream",
"text": [
"(a, b)\n",
"(c, b)\n",
"(spot.formula(\"a\"), spot.formula(\"b\"))\n",
"(spot.formula(\"c\"), spot.formula(\"b\"))\n",
"()\n"
]
}
@ -1585,7 +1585,7 @@
"name": "stdout",
"output_type": "stream",
"text": [
"(a, b, c)\n"
"(spot.formula(\"a\"), spot.formula(\"b\"), spot.formula(\"c\"))\n"
]
}
],
@ -2426,7 +2426,7 @@
"name": "stdout",
"output_type": "stream",
"text": [
"219 µs ± 5.11 µs per loop (mean ± std. dev. of 7 runs, 1000 loops each)\n"
"200 µs ± 2.74 µs per loop (mean ± std. dev. of 7 runs, 1000 loops each)\n"
]
}
],
@ -2443,7 +2443,7 @@
"name": "stdout",
"output_type": "stream",
"text": [
"5.23 µs ± 532 ns per loop (mean ± std. dev. of 7 runs, 100000 loops each)\n"
"3.35 µs ± 52.4 ns per loop (mean ± std. dev. of 7 runs, 100000 loops each)\n"
]
}
],
@ -2468,13 +2468,6 @@
"\n",
"Finally, note that `spot.product()` actually does a bit more: it has some specializations for when one of the argument of the product is marked as weak (as indicated by `prop_weak()`). In this case, the resulting acceptance condition can be simplified a bit."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
@ -2493,7 +2486,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.6.5+"
"version": "3.6.7"
}
},
"nbformat": 4,

5
tests/python/relabel.py
View file

@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement
# Copyright (C) 2015, 2017, 2018 Laboratoire de Recherche et Développement
# de l'Epita
#
# This file is part of Spot, a model checking library.
@ -34,7 +34,8 @@ GFp0 -> (FGp0 & Gp1)""")
autg = g.translate()
spot.relabel_here(autg, m)
assert str(autg.ap()) == '(a, b, c)'
assert str(autg.ap()) == \
'(spot.formula("a"), spot.formula("b"), spot.formula("c"))'
assert spot.isomorphism_checker.are_isomorphic(autg, f.translate())
a = spot.formula('a')

179
tests/python/satmin.ipynb
View file

@ -42,7 +42,7 @@
"$\\mathsf{G} \\mathsf{F} (a \\leftrightarrow \\mathsf{X} \\mathsf{X} b)$"
],
"text/plain": [
"GF(a <-> XXb)"
"spot.formula(\"GF(a <-> XXb)\")"
]
},
"execution_count": 2,
@ -256,7 +256,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79c85a5150> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f787b3690> >"
]
},
"execution_count": 3,
@ -444,7 +444,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79c857fb40> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f78fcd840> >"
]
},
"execution_count": 4,
@ -680,7 +680,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79c85d20f0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f78761300> >"
]
},
"execution_count": 5,
@ -913,7 +913,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79c857f5d0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f78761db0> >"
]
},
"execution_count": 6,
@ -938,7 +938,7 @@
"cell_type": "markdown",
"metadata": {},
"source": [
"It can be minimized as a 2-state transition-based Rabin:"
"It can be minimized as a 2-state transition-based Rabin automaton:"
]
},
{
@ -1061,7 +1061,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79c857fc00> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f78761ba0> >"
]
},
"execution_count": 7,
@ -1077,12 +1077,12 @@
"cell_type": "markdown",
"metadata": {},
"source": [
"Or as a 4-state state-based Rabin:"
"Or as a 4-state state-based Rabin automaton:"
]
},
{
"cell_type": "code",
"execution_count": 8,
"execution_count": 9,
"metadata": {},
"outputs": [
{
@ -1233,10 +1233,10 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79c857f9c0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f78761b70> >"
]
},
"execution_count": 8,
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
@ -1254,7 +1254,7 @@
},
{
"cell_type": "code",
"execution_count": 9,
"execution_count": 10,
"metadata": {},
"outputs": [
{
@ -1392,10 +1392,10 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79c851b090> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f787b3720> >"
]
},
"execution_count": 9,
"execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
@ -1417,7 +1417,7 @@
},
{
"cell_type": "code",
"execution_count": 10,
"execution_count": 11,
"metadata": {},
"outputs": [
{
@ -1478,9 +1478,9 @@
" <td>40</td>\n",
" <td>2760</td>\n",
" <td>224707</td>\n",
" <td>9</td>\n",
" <td>8</td>\n",
" <td>0</td>\n",
" <td>6</td>\n",
" <td>7</td>\n",
" <td>0</td>\n",
" </tr>\n",
" <tr>\n",
@ -1494,7 +1494,7 @@
" <td>155020</td>\n",
" <td>6</td>\n",
" <td>0</td>\n",
" <td>7</td>\n",
" <td>5</td>\n",
" <td>0</td>\n",
" </tr>\n",
" </tbody>\n",
@ -1509,8 +1509,8 @@
"\n",
" clauses enc.user enc.sys sat.user sat.sys \n",
"0 48806 2 0 1 0 \n",
"1 224707 9 0 6 0 \n",
"2 155020 6 0 7 0 "
"1 224707 8 0 7 0 \n",
"2 155020 6 0 5 0 "
]
},
"metadata": {},
@ -1651,10 +1651,10 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79cdb10330> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f5be97960> >"
]
},
"execution_count": 10,
"execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
@ -1672,7 +1672,7 @@
},
{
"cell_type": "code",
"execution_count": 11,
"execution_count": 12,
"metadata": {},
"outputs": [
{
@ -1733,9 +1733,9 @@
" <td>32</td>\n",
" <td>960</td>\n",
" <td>71987</td>\n",
" <td>3</td>\n",
" <td>4</td>\n",
" <td>0</td>\n",
" <td>2</td>\n",
" <td>1</td>\n",
" <td>0</td>\n",
" </tr>\n",
" </tbody>\n",
@ -1749,7 +1749,7 @@
"\n",
" clauses enc.user enc.sys sat.user sat.sys \n",
"0 15542 1 0 0 0 \n",
"1 71987 3 0 2 0 "
"1 71987 4 0 1 0 "
]
},
"metadata": {},
@ -1883,10 +1883,10 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79cdb107b0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f5bdc5cc0> >"
]
},
"execution_count": 11,
"execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
@ -1906,7 +1906,7 @@
},
{
"cell_type": "code",
"execution_count": 12,
"execution_count": 13,
"metadata": {},
"outputs": [
{
@ -1954,8 +1954,8 @@
" <td>2300</td>\n",
" <td>285287</td>\n",
" <td>13</td>\n",
" <td>0</td>\n",
" <td>9</td>\n",
" <td>1</td>\n",
" <td>10</td>\n",
" <td>0</td>\n",
" </tr>\n",
" <tr>\n",
@ -1981,7 +1981,7 @@
" <td>NaN</td>\n",
" <td>92</td>\n",
" <td>2193</td>\n",
" <td>0</td>\n",
" <td>1</td>\n",
" <td>0</td>\n",
" <td>0</td>\n",
" <td>0</td>\n",
@ -1997,9 +1997,9 @@
"2 2 1 NaN NaN NaN 92 \n",
"\n",
" clauses enc.user enc.sys sat.user sat.sys \n",
"0 285287 13 0 9 0 \n",
"0 285287 13 1 10 0 \n",
"1 17993 1 0 0 0 \n",
"2 2193 0 0 0 0 "
"2 2193 1 0 0 0 "
]
},
"metadata": {},
@ -2097,10 +2097,10 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79cdb108d0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f78761d20> >"
]
},
"execution_count": 12,
"execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
@ -2118,7 +2118,7 @@
},
{
"cell_type": "code",
"execution_count": 13,
"execution_count": 14,
"metadata": {},
"outputs": [
{
@ -2165,9 +2165,9 @@
" <td>40</td>\n",
" <td>2742</td>\n",
" <td>173183</td>\n",
" <td>6</td>\n",
" <td>7</td>\n",
" <td>0</td>\n",
" <td>3</td>\n",
" <td>2</td>\n",
" <td>0</td>\n",
" </tr>\n",
" <tr>\n",
@ -2209,7 +2209,7 @@
"2 4 3 NaN NaN NaN 363 \n",
"\n",
" clauses enc.user enc.sys sat.user sat.sys \n",
"0 173183 6 0 3 0 \n",
"0 173183 7 0 2 0 \n",
"1 45412 2 0 0 0 \n",
"2 10496 1 0 0 0 "
]
@ -2348,10 +2348,10 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79c857fba0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f5bdc5d20> >"
]
},
"execution_count": 13,
"execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
@ -2382,7 +2382,7 @@
},
{
"cell_type": "code",
"execution_count": 14,
"execution_count": 15,
"metadata": {},
"outputs": [
{
@ -2429,9 +2429,9 @@
" <td>NaN</td>\n",
" <td>2747</td>\n",
" <td>173427</td>\n",
" <td>6</td>\n",
" <td>7</td>\n",
" <td>0</td>\n",
" <td>1</td>\n",
" <td>2</td>\n",
" <td>0</td>\n",
" </tr>\n",
" <tr>\n",
@ -2445,7 +2445,7 @@
" <td>173427</td>\n",
" <td>0</td>\n",
" <td>0</td>\n",
" <td>1</td>\n",
" <td>0</td>\n",
" <td>0</td>\n",
" </tr>\n",
" <tr>\n",
@ -2473,8 +2473,8 @@
"2 6 4 4 12 32 2747 \n",
"\n",
" clauses enc.user enc.sys sat.user sat.sys \n",
"0 173427 6 0 1 0 \n",
"1 173427 0 0 1 0 \n",
"0 173427 7 0 2 0 \n",
"1 173427 0 0 0 0 \n",
"2 173427 0 0 0 0 "
]
},
@ -2619,10 +2619,10 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79cdb10b10> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f5bdc5f00> >"
]
},
"execution_count": 14,
"execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
@ -2642,7 +2642,7 @@
},
{
"cell_type": "code",
"execution_count": 15,
"execution_count": 16,
"metadata": {},
"outputs": [
{
@ -2691,7 +2691,7 @@
" <td>173183</td>\n",
" <td>6</td>\n",
" <td>0</td>\n",
" <td>3</td>\n",
" <td>2</td>\n",
" <td>0</td>\n",
" </tr>\n",
" <tr>\n",
@ -2704,7 +2704,7 @@
" <td>2742</td>\n",
" <td>173279</td>\n",
" <td>0</td>\n",
" <td>1</td>\n",
" <td>0</td>\n",
" <td>1</td>\n",
" <td>0</td>\n",
" </tr>\n",
@ -2733,8 +2733,8 @@
"2 4 3 NaN NaN NaN 2742 \n",
"\n",
" clauses enc.user enc.sys sat.user sat.sys \n",
"0 173183 6 0 3 0 \n",
"1 173279 0 1 1 0 \n",
"0 173183 6 0 2 0 \n",
"1 173279 0 0 1 0 \n",
"2 173327 0 0 0 0 "
]
},
@ -2879,10 +2879,10 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79cdb10c30> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f78fcd630> >"
]
},
"execution_count": 15,
"execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
@ -2904,7 +2904,7 @@
},
{
"cell_type": "code",
"execution_count": 16,
"execution_count": 17,
"metadata": {},
"outputs": [
{
@ -3045,7 +3045,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79cdb109f0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f5bd9e060> >"
]
},
"metadata": {},
@ -3098,7 +3098,7 @@
" <td>173183</td>\n",
" <td>7</td>\n",
" <td>0</td>\n",
" <td>3</td>\n",
" <td>2</td>\n",
" <td>0</td>\n",
" <td>HOA: v1 States: 5 Start: 0 AP: 3 \"a\" \"c\" \"b\" a...</td>\n",
" </tr>\n",
@ -3143,7 +3143,7 @@
"2 4 3 NaN NaN NaN 2742 \n",
"\n",
" clauses enc.user enc.sys sat.user sat.sys \\\n",
"0 173183 7 0 3 0 \n",
"0 173183 7 0 2 0 \n",
"1 173279 0 0 1 0 \n",
"2 173327 0 0 0 0 \n",
"\n",
@ -3172,7 +3172,7 @@
},
{
"cell_type": "code",
"execution_count": 17,
"execution_count": 18,
"metadata": {},
"outputs": [
{
@ -3333,7 +3333,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79cdb10a80> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f5bd9e0c0> >"
]
},
"metadata": {},
@ -3484,7 +3484,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79cdb10e40> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f5bd9e150> >"
]
},
"metadata": {},
@ -3511,7 +3511,7 @@
},
{
"cell_type": "code",
"execution_count": 18,
"execution_count": 19,
"metadata": {},
"outputs": [
{
@ -3716,10 +3716,10 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79c857f5d0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f78761db0> >"
]
},
"execution_count": 18,
"execution_count": 19,
"metadata": {},
"output_type": "execute_result"
}
@ -3737,7 +3737,7 @@
},
{
"cell_type": "code",
"execution_count": 19,
"execution_count": 20,
"metadata": {},
"outputs": [
{
@ -3958,10 +3958,10 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79cdb10e40> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f5bd9e180> >"
]
},
"execution_count": 19,
"execution_count": 20,
"metadata": {},
"output_type": "execute_result"
}
@ -3973,7 +3973,7 @@
},
{
"cell_type": "code",
"execution_count": 20,
"execution_count": 21,
"metadata": {},
"outputs": [
{
@ -4023,7 +4023,7 @@
" <td>2</td>\n",
" <td>0</td>\n",
" <td>1</td>\n",
" <td>1</td>\n",
" <td>0</td>\n",
" </tr>\n",
" <tr>\n",
" <th>1</th>\n",
@ -4034,7 +4034,7 @@
" <td>NaN</td>\n",
" <td>162</td>\n",
" <td>3129</td>\n",
" <td>0</td>\n",
" <td>1</td>\n",
" <td>0</td>\n",
" <td>0</td>\n",
" <td>0</td>\n",
@ -4048,7 +4048,7 @@
" <td>NaN</td>\n",
" <td>363</td>\n",
" <td>10496</td>\n",
" <td>1</td>\n",
" <td>0</td>\n",
" <td>0</td>\n",
" <td>0</td>\n",
" <td>0</td>\n",
@ -4064,9 +4064,9 @@
"2 4 3 NaN NaN NaN 363 \n",
"\n",
" clauses enc.user enc.sys sat.user sat.sys \n",
"0 51612 2 0 1 1 \n",
"1 3129 0 0 0 0 \n",
"2 10496 1 0 0 0 "
"0 51612 2 0 1 0 \n",
"1 3129 1 0 0 0 \n",
"2 10496 0 0 0 0 "
]
},
"metadata": {},
@ -4210,10 +4210,10 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79cdae52a0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f5bdc5ea0> >"
]
},
"execution_count": 20,
"execution_count": 21,
"metadata": {},
"output_type": "execute_result"
}
@ -4234,7 +4234,7 @@
},
{
"cell_type": "code",
"execution_count": 21,
"execution_count": 22,
"metadata": {},
"outputs": [
{
@ -4281,9 +4281,9 @@
" <td>56</td>\n",
" <td>1379</td>\n",
" <td>87992</td>\n",
" <td>4</td>\n",
" <td>3</td>\n",
" <td>0</td>\n",
" <td>1</td>\n",
" <td>2</td>\n",
" <td>0</td>\n",
" </tr>\n",
" </tbody>\n",
@ -4295,7 +4295,7 @@
"0 2 7 7 22 56 1379 \n",
"\n",
" clauses enc.user enc.sys sat.user sat.sys \n",
"0 87992 4 0 1 0 "
"0 87992 3 0 2 0 "
]
},
"metadata": {},
@ -4529,10 +4529,10 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79cdae5270> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3f5bdc5f30> >"
]
},
"execution_count": 21,
"execution_count": 22,
"metadata": {},
"output_type": "execute_result"
}
@ -4540,13 +4540,6 @@
"source": [
"spot.sat_minimize(small, acc=\"co-Buchi\", states=7, state_based=True, display_log=True)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
@ -4565,7 +4558,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.6.5+"
"version": "3.6.7"
}
},
"nbformat": 4,

24
tests/python/stutter-inv.ipynb
View file

@ -119,7 +119,7 @@
"$\\mathsf{F} (a \\land ((a \\land (a \\mathbin{\\mathsf{U}} (\\lnot a \\land \\mathsf{G} b)) \\land ((\\lnot b \\mathbin{\\mathsf{U}} \\lnot a) \\lor (b \\mathbin{\\mathsf{U}} \\lnot a))) \\lor (\\lnot a \\land (\\lnot a \\mathbin{\\mathsf{U}} (a \\land \\lnot a \\land \\mathsf{G} b)) \\land ((\\lnot b \\mathbin{\\mathsf{U}} a) \\lor (b \\mathbin{\\mathsf{U}} a))) \\lor (b \\land (b \\mathbin{\\mathsf{U}} (\\lnot a \\land \\lnot b \\land \\mathsf{G} b)) \\land ((\\lnot a \\mathbin{\\mathsf{U}} \\lnot b) \\lor (a \\mathbin{\\mathsf{U}} \\lnot b))) \\lor (\\lnot b \\land (\\lnot b \\mathbin{\\mathsf{U}} (\\lnot a \\land b \\land \\mathsf{G} b)) \\land ((\\lnot a \\mathbin{\\mathsf{U}} b) \\lor (a \\mathbin{\\mathsf{U}} b))) \\lor (\\lnot a \\land \\mathsf{G} b \\land (\\mathsf{G} \\lnot a \\lor \\mathsf{G} a) \\land (\\mathsf{G} b \\lor \\mathsf{G} \\lnot b))))$"
],
"text/plain": [
"F(a & ((a & (a U (!a & Gb)) & ((!b U !a) | (b U !a))) | (!a & (!a U (a & !a & Gb)) & ((!b U a) | (b U a))) | (b & (b U (!a & !b & Gb)) & ((!a U !b) | (a U !b))) | (!b & (!b U (!a & b & Gb)) & ((!a U b) | (a U b))) | (!a & Gb & (G!a | Ga) & (Gb | G!b))))"
"spot.formula(\"F(a & ((a & (a U (!a & Gb)) & ((!b U !a) | (b U !a))) | (!a & (!a U (a & !a & Gb)) & ((!b U a) | (b U a))) | (b & (b U (!a & !b & Gb)) & ((!a U !b) | (a U !b))) | (!b & (!b U (!a & b & Gb)) & ((!a U b) | (a U b))) | (!a & Gb & (G!a | Ga) & (Gb | G!b))))\")"
]
},
"execution_count": 5,
@ -302,7 +302,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f68605f5630> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0a9c1ee180> >"
]
},
"metadata": {},
@ -595,7 +595,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f68605f5ae0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0a9c250300> >"
]
},
"metadata": {},
@ -804,7 +804,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f68605f5ae0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0a9c250300> >"
]
},
"metadata": {},
@ -956,7 +956,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f68605f5a50> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0a9c1e1f60> >"
]
},
"metadata": {},
@ -1054,7 +1054,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f68605f5b70> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0a9c1e1840> >"
]
},
"metadata": {},
@ -1264,7 +1264,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f68605f5ba0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0a9c1ee990> >"
]
},
"metadata": {},
@ -1393,7 +1393,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f686063ef30> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0a9c2502a0> >"
]
},
"metadata": {},
@ -1524,7 +1524,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6860602930> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0a9c20eb10> >"
]
},
"metadata": {},
@ -1784,7 +1784,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6860591c30> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0a9c20eea0> >"
]
},
"metadata": {},
@ -2098,7 +2098,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6860591c30> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0a9c20eea0> >"
]
},
"metadata": {},
@ -2339,7 +2339,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.6.6"
"version": "3.6.7"
}
},
"nbformat": 4,

80
tests/python/word.ipynb
View file

@ -166,7 +166,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fca777b2090> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f4e4c5e8de0> >"
]
},
"execution_count": 2,
@ -191,25 +191,24 @@
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Prefix:\n",
" 0\n",
" | !a\n",
" 1\n",
" | a\n",
"Cycle:\n",
" 2\n",
" | a & b\t{0}"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
"name": "stdout",
"output_type": "stream",
"text": [
"Prefix:\n",
" 0\n",
" | !a\n",
" 1\n",
" | a\n",
"Cycle:\n",
" 2\n",
" | a & b\t{0}\n",
"\n"
]
}
],
"source": [
"run = aut.accepting_run(); run"
"run = aut.accepting_run()\n",
"print(run)"
]
},
{
@ -250,10 +249,20 @@
"execution_count": 5,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"!a; a; cycle{a & b}\n"
]
},
{
"data": {
"text/latex": [
"$\\lnot a; a; \\mathsf{cycle}\\{a \\land b\\}$"
],
"text/plain": [
"!a; a; cycle{a & b}"
"<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f4e4c5e8b70> >"
]
},
"execution_count": 5,
@ -262,7 +271,9 @@
}
],
"source": [
"word = spot.twa_word(run); word"
"word = spot.twa_word(run)\n",
"print(word) # print as a string\n",
"word # LaTeX-style representation in notebooks"
]
},
{
@ -341,19 +352,16 @@
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"!a; cycle{a & b}"
]
},
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
"name": "stdout",
"output_type": "stream",
"text": [
"!a; cycle{a & b}\n"
]
}
],
"source": [
"word.simplify()\n",
"word"
"print(word)"
]
},
{
@ -370,8 +378,11 @@
"outputs": [
{
"data": {
"text/latex": [
"$\\lnot a; \\mathsf{cycle}\\{a \\land b\\}$"
],
"text/plain": [
"!a; cycle{a & b}"
"<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f4e4c652810> >"
]
},
"execution_count": 9,
@ -418,8 +429,11 @@
"outputs": [
{
"data": {
"text/latex": [
"$a; a \\land b; \\mathsf{cycle}\\{\\lnot a \\land \\lnot b; \\lnot a \\land b\\}$"
],
"text/plain": [
"a; a & b; cycle{!a & !b; !a & b}"
"<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f4e4c574600> >"
]
},
"execution_count": 11,
@ -464,7 +478,7 @@
"cell_type": "markdown",
"metadata": {},
"source": [
"Words can be easily converted as automata"
"Words can be easily converted to automata"
]
},
{
@ -550,7 +564,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fca7775f690> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f4e4c6528a0> >"
]
},
"execution_count": 13,
@ -579,7 +593,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.6.5"
"version": "3.6.7"
}
},
"nbformat": 4,