From 60296317c7952d87bc2675ca08c137b12924ecae Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 2 Nov 2018 17:18:42 +0100 Subject: [PATCH] python: more conventional __repr__ for several types * 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. --- NEWS | 16 ++ python/spot/__init__.py | 29 +- python/spot/impl.i | 71 +++-- tests/python/acc_cond.ipynb | 494 ++++++++++++++------------------ tests/python/accparse.ipynb | 76 ++--- tests/python/atva16-fig2a.ipynb | 6 +- tests/python/automata.ipynb | 48 ++-- tests/python/bdditer.py | 6 +- tests/python/contains.ipynb | 7 +- tests/python/formulas.ipynb | 67 ++++- tests/python/gen.ipynb | 68 ++--- tests/python/highlighting.ipynb | 130 ++++----- tests/python/ltlsimple.py | 2 +- tests/python/ltsmin-dve.ipynb | 59 ++-- tests/python/product.ipynb | 19 +- tests/python/relabel.py | 5 +- tests/python/satmin.ipynb | 179 ++++++------ tests/python/stutter-inv.ipynb | 24 +- tests/python/word.ipynb | 80 +++--- 19 files changed, 686 insertions(+), 700 deletions(-) diff --git a/NEWS b/NEWS index 6b03d9811..d3849af72 100644 --- a/NEWS +++ b/NEWS @@ -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: diff --git a/python/spot/__init__.py b/python/spot/__init__.py index dd979966d..266ee5a48 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -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 diff --git a/python/spot/impl.i b/python/spot/impl.i index a8584ae5e..314305680 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -669,13 +669,42 @@ def state_is_accepting(self, src) -> "bool": %include %include +%extend std::set { + 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; diff --git a/tests/python/acc_cond.ipynb b/tests/python/acc_cond.ipynb index 7300e516b..7fe7e50ad 100644 --- a/tests/python/acc_cond.ipynb +++ b/tests/python/acc_cond.ipynb @@ -3,9 +3,7 @@ { "cell_type": "code", "execution_count": 1, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "import spot\n", @@ -52,67 +50,52 @@ { "cell_type": "code", "execution_count": 2, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { - "data": { - "text/plain": [ - "{}" - ] - }, - "execution_count": 2, - "metadata": {}, - "output_type": "execute_result" + "name": "stdout", + "output_type": "stream", + "text": [ + "{}\n" + ] } ], "source": [ - "spot.mark_t()" + "print(spot.mark_t())" ] }, { "cell_type": "code", "execution_count": 3, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { - "data": { - "text/plain": [ - "{0,2,3}" - ] - }, - "execution_count": 3, - "metadata": {}, - "output_type": "execute_result" + "name": "stdout", + "output_type": "stream", + "text": [ + "{0,2,3}\n" + ] } ], "source": [ - "spot.mark_t([0, 2, 3])" + "print(spot.mark_t([0, 2, 3])) # works with lists" ] }, { "cell_type": "code", "execution_count": 4, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { - "data": { - "text/plain": [ - "{0,2,3}" - ] - }, - "execution_count": 4, - "metadata": {}, - "output_type": "execute_result" + "name": "stdout", + "output_type": "stream", + "text": [ + "{0,2,3}\n" + ] } ], "source": [ - "spot.mark_t((0, 2, 3))" + "print(spot.mark_t((0, 2, 3))) # works with tuples" ] }, { @@ -125,9 +108,7 @@ { "cell_type": "code", "execution_count": 5, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -157,9 +138,7 @@ { "cell_type": "code", "execution_count": 6, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -177,9 +156,7 @@ { "cell_type": "code", "execution_count": 7, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -197,9 +174,7 @@ { "cell_type": "code", "execution_count": 8, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -226,23 +201,18 @@ { "cell_type": "code", "execution_count": 9, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { - "data": { - "text/plain": [ - "{2,4,7}" - ] - }, - "execution_count": 9, - "metadata": {}, - "output_type": "execute_result" + "name": "stdout", + "output_type": "stream", + "text": [ + "{2,4,7}\n" + ] } ], "source": [ - "x << 2" + "print(x << 2)" ] }, { @@ -254,10 +224,8 @@ }, { "cell_type": "code", - "execution_count": 12, - "metadata": { - "collapsed": false - }, + "execution_count": 10, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -287,10 +255,8 @@ }, { "cell_type": "code", - "execution_count": 13, - "metadata": { - "collapsed": false - }, + "execution_count": 11, + "metadata": {}, "outputs": [ { "data": { @@ -298,7 +264,7 @@ "3" ] }, - "execution_count": 13, + "execution_count": 11, "metadata": {}, "output_type": "execute_result" } @@ -316,18 +282,16 @@ }, { "cell_type": "code", - "execution_count": 14, - "metadata": { - "collapsed": false - }, + "execution_count": 12, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "{1}" + "spot.mark_t([1])" ] }, - "execution_count": 14, + "execution_count": 12, "metadata": {}, "output_type": "execute_result" } @@ -338,10 +302,8 @@ }, { "cell_type": "code", - "execution_count": 15, - "metadata": { - "collapsed": false - }, + "execution_count": 13, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -370,10 +332,8 @@ }, { "cell_type": "code", - "execution_count": 16, - "metadata": { - "collapsed": false - }, + "execution_count": 14, + "metadata": {}, "outputs": [ { "data": { @@ -381,7 +341,7 @@ "6" ] }, - "execution_count": 16, + "execution_count": 14, "metadata": {}, "output_type": "execute_result" } @@ -403,24 +363,31 @@ }, { "cell_type": "code", - "execution_count": 17, - "metadata": { - "collapsed": false - }, + "execution_count": 15, + "metadata": {}, "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "(Inf(0) & Fin(1)) | Inf(2)\n" + ] + }, { "data": { "text/plain": [ - "(Inf(0) & Fin(1)) | Inf(2)" + "spot.acc_code(\"(Inf(0) & Fin(1)) | Inf(2)\")" ] }, - "execution_count": 17, + "execution_count": 15, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "spot.acc_code('(Inf(0)&Fin(1))|Inf(2)')" + "acc = spot.acc_code('(Inf(0)&Fin(1))|Inf(2)')\n", + "print(acc) # shows just the formula\n", + "acc # shows the acc_code object" ] }, { @@ -432,18 +399,16 @@ }, { "cell_type": "code", - "execution_count": 18, - "metadata": { - "collapsed": false - }, + "execution_count": 16, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))" + "spot.acc_code(\"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\")" ] }, - "execution_count": 18, + "execution_count": 16, "metadata": {}, "output_type": "execute_result" } @@ -461,10 +426,8 @@ }, { "cell_type": "code", - "execution_count": 19, - "metadata": { - "collapsed": false - }, + "execution_count": 17, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -484,23 +447,21 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "It may also be convenient to generate a random acceptance condition:" + "It may also be convenient to generate a random acceptance condition. Below we require between 3 and 5 acceptance sets:" ] }, { "cell_type": "code", - "execution_count": 20, - "metadata": { - "collapsed": false - }, + "execution_count": 18, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "(Fin(3) | Inf(1)) & Inf(4) & (Fin(0)|Fin(2))" + "spot.acc_code(\"(Fin(3) | Inf(1)) & Inf(4) & (Fin(0)|Fin(2))\")" ] }, - "execution_count": 20, + "execution_count": 18, "metadata": {}, "output_type": "execute_result" } @@ -518,18 +479,16 @@ }, { "cell_type": "code", - "execution_count": 21, - "metadata": { - "collapsed": false - }, + "execution_count": 19, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | Fin(4))))" + "spot.acc_code(\"Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | Fin(4))))\")" ] }, - "execution_count": 21, + "execution_count": 19, "metadata": {}, "output_type": "execute_result" } @@ -541,18 +500,16 @@ }, { "cell_type": "code", - "execution_count": 22, - "metadata": { - "collapsed": false - }, + "execution_count": 20, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "Fin(0) & (Inf(1) | Fin(2)) & (Inf(1) | Inf(3) | Fin(4))" + "spot.acc_code(\"Fin(0) & (Inf(1) | Fin(2)) & (Inf(1) | Inf(3) | Fin(4))\")" ] }, - "execution_count": 22, + "execution_count": 20, "metadata": {}, "output_type": "execute_result" } @@ -563,18 +520,16 @@ }, { "cell_type": "code", - "execution_count": 23, - "metadata": { - "collapsed": false - }, + "execution_count": 21, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "(Fin(0) & Inf(1)) | (Fin(0) & Fin(2) & Inf(3)) | (Fin(0) & Fin(2) & Fin(4))" + "spot.acc_code(\"(Fin(0) & Inf(1)) | (Fin(0) & Fin(2) & Inf(3)) | (Fin(0) & Fin(2) & Fin(4))\")" ] }, - "execution_count": 23, + "execution_count": 21, "metadata": {}, "output_type": "execute_result" } @@ -587,7 +542,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "The manipulation of `acc_code` objects is quite rudimentary at the moment: it easy to build, but it's harder take appart. In fact we won't attempt to disassemble an `acc_code` object in Python: those things are better done in C++\n", + "The manipulation of `acc_code` objects is quite rudimentary at the moment: they are easy to build, but are harder take appart. In fact we won't attempt to disassemble an `acc_code` object in Python: those things are better done in C++\n", "\n", "Operators `|`, `|=`, `&`, `&=`, `<<`, and `<<=` can be used with their obvious semantics.\n", "Whenever possible, the inplace versions (`|=`, `&=`, `<<=`) should be prefered, because they create less temporary acceptance conditions." @@ -595,10 +550,8 @@ }, { "cell_type": "code", - "execution_count": 24, - "metadata": { - "collapsed": false - }, + "execution_count": 22, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -618,10 +571,8 @@ }, { "cell_type": "code", - "execution_count": 25, - "metadata": { - "collapsed": false - }, + "execution_count": 23, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -646,10 +597,8 @@ }, { "cell_type": "code", - "execution_count": 26, - "metadata": { - "collapsed": false - }, + "execution_count": 24, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -679,18 +628,16 @@ }, { "cell_type": "code", - "execution_count": 27, - "metadata": { - "collapsed": false - }, + "execution_count": 25, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "(Fin(3)|Fin(4)|Fin(5)) & (Inf(1)&Inf(2))" + "spot.acc_code(\"(Fin(3)|Fin(4)|Fin(5)) & (Inf(1)&Inf(2))\")" ] }, - "execution_count": 27, + "execution_count": 25, "metadata": {}, "output_type": "execute_result" } @@ -701,18 +648,16 @@ }, { "cell_type": "code", - "execution_count": 28, - "metadata": { - "collapsed": false - }, + "execution_count": 26, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "t" + "spot.acc_code(\"t\")" ] }, - "execution_count": 28, + "execution_count": 26, "metadata": {}, "output_type": "execute_result" } @@ -723,18 +668,16 @@ }, { "cell_type": "code", - "execution_count": 29, - "metadata": { - "collapsed": false - }, + "execution_count": 27, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "t" + "spot.acc_code(\"t\")" ] }, - "execution_count": 29, + "execution_count": 27, "metadata": {}, "output_type": "execute_result" } @@ -745,18 +688,16 @@ }, { "cell_type": "code", - "execution_count": 30, - "metadata": { - "collapsed": false - }, + "execution_count": 28, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "f" + "spot.acc_code(\"f\")" ] }, - "execution_count": 30, + "execution_count": 28, "metadata": {}, "output_type": "execute_result" } @@ -767,18 +708,16 @@ }, { "cell_type": "code", - "execution_count": 31, - "metadata": { - "collapsed": false - }, + "execution_count": 29, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "f" + "spot.acc_code(\"f\")" ] }, - "execution_count": 31, + "execution_count": 29, "metadata": {}, "output_type": "execute_result" } @@ -796,10 +735,8 @@ }, { "cell_type": "code", - "execution_count": 32, - "metadata": { - "collapsed": false - }, + "execution_count": 30, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -833,10 +770,8 @@ }, { "cell_type": "code", - "execution_count": 33, - "metadata": { - "collapsed": false - }, + "execution_count": 31, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -855,6 +790,33 @@ "print(acc.used_sets().max_set())" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The `used_inf_fin_sets()` returns a pair of marks instead, the first one with all sets occuring in `Inf`, and the second one with all sets appearing in `Fin`." + ] + }, + { + "cell_type": "code", + "execution_count": 32, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(spot.mark_t([2]), spot.mark_t([0]))" + ] + }, + "execution_count": 32, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "acc.used_inf_fin_sets()" + ] + }, { "cell_type": "markdown", "metadata": {}, @@ -864,25 +826,23 @@ "Automata store their acceptance condition as an instance of the `acc_cond` class.\n", "This class can be thought of as a pair `(n, code)`, where `n` is an integer that tells how many acceptance sets are used, while the `code` is an instance of `acc_code` and encodes the formula over *a subset* of these acceptance sets. We usually have `n == code.used_sets().max_set())`, but `n` can be larger.\n", "\n", - "It is OK if an automaton declares that is used 3 sets, even if the acceptance condition formula only uses set number 1.\n", + "It is OK if an automaton declares that is uses 3 sets, even if the acceptance condition formula only uses set number 1. The extra two sets will have no impact on the language, even if they are used in the automaton.\n", "\n", "The `acc_cond` objects are usually not created by hand: automata have dedicated methods for that. But for the purpose of this notebook, let's do it:" ] }, { "cell_type": "code", - "execution_count": 34, - "metadata": { - "collapsed": false - }, + "execution_count": 33, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "(4, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))" + "spot.acc_cond(4, \"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\")" ] }, - "execution_count": 34, + "execution_count": 33, "metadata": {}, "output_type": "execute_result" } @@ -901,18 +861,16 @@ }, { "cell_type": "code", - "execution_count": 35, - "metadata": { - "collapsed": false - }, + "execution_count": 34, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "(4, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))" + "spot.acc_cond(4, \"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\")" ] }, - "execution_count": 35, + "execution_count": 34, "metadata": {}, "output_type": "execute_result" } @@ -924,10 +882,8 @@ }, { "cell_type": "code", - "execution_count": 36, - "metadata": { - "collapsed": false - }, + "execution_count": 35, + "metadata": {}, "outputs": [ { "data": { @@ -935,7 +891,7 @@ "4" ] }, - "execution_count": 36, + "execution_count": 35, "metadata": {}, "output_type": "execute_result" } @@ -946,18 +902,16 @@ }, { "cell_type": "code", - "execution_count": 37, - "metadata": { - "collapsed": false - }, + "execution_count": 36, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))" + "spot.acc_code(\"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\")" ] }, - "execution_count": 37, + "execution_count": 36, "metadata": {}, "output_type": "execute_result" } @@ -975,18 +929,16 @@ }, { "cell_type": "code", - "execution_count": 38, - "metadata": { - "collapsed": false - }, + "execution_count": 37, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "(4, t)" + "spot.acc_cond(4, \"t\")" ] }, - "execution_count": 38, + "execution_count": 37, "metadata": {}, "output_type": "execute_result" } @@ -998,18 +950,16 @@ }, { "cell_type": "code", - "execution_count": 39, - "metadata": { - "collapsed": false - }, + "execution_count": 38, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "(6, t)" + "spot.acc_cond(6, \"t\")" ] }, - "execution_count": 39, + "execution_count": 38, "metadata": {}, "output_type": "execute_result" } @@ -1021,18 +971,16 @@ }, { "cell_type": "code", - "execution_count": 40, - "metadata": { - "collapsed": false - }, + "execution_count": 39, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "(6, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))" + "spot.acc_cond(6, \"(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\")" ] }, - "execution_count": 40, + "execution_count": 39, "metadata": {}, "output_type": "execute_result" } @@ -1051,18 +999,16 @@ }, { "cell_type": "code", - "execution_count": 41, - "metadata": { - "collapsed": false - }, + "execution_count": 40, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "(4, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))" + "spot.acc_cond(4, \"(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\")" ] }, - "execution_count": 41, + "execution_count": 40, "metadata": {}, "output_type": "execute_result" } @@ -1081,18 +1027,16 @@ }, { "cell_type": "code", - "execution_count": 42, - "metadata": { - "collapsed": false - }, + "execution_count": 41, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "(4, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))" + "spot.acc_cond(4, \"(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\")" ] }, - "execution_count": 42, + "execution_count": 41, "metadata": {}, "output_type": "execute_result" } @@ -1112,18 +1056,16 @@ }, { "cell_type": "code", - "execution_count": 43, - "metadata": { - "collapsed": false - }, + "execution_count": 42, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))" + "spot.acc_cond(4, \"Inf(0)&Inf(1)&Inf(2)&Inf(3)\")" ] }, - "execution_count": 43, + "execution_count": 42, "metadata": {}, "output_type": "execute_result" } @@ -1143,10 +1085,8 @@ }, { "cell_type": "code", - "execution_count": 44, - "metadata": { - "collapsed": false - }, + "execution_count": 43, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -1178,10 +1118,8 @@ }, { "cell_type": "code", - "execution_count": 45, - "metadata": { - "collapsed": false - }, + "execution_count": 44, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -1209,10 +1147,8 @@ }, { "cell_type": "code", - "execution_count": 46, - "metadata": { - "collapsed": false - }, + "execution_count": 45, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -1243,10 +1179,8 @@ }, { "cell_type": "code", - "execution_count": 47, - "metadata": { - "collapsed": false - }, + "execution_count": 46, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -1275,10 +1209,8 @@ }, { "cell_type": "code", - "execution_count": 48, - "metadata": { - "collapsed": false - }, + "execution_count": 47, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -1302,18 +1234,16 @@ }, { "cell_type": "code", - "execution_count": 49, - "metadata": { - "collapsed": false - }, + "execution_count": 48, + "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "{0,1,2,3}" + "spot.mark_t([0, 1, 2, 3])" ] }, - "execution_count": 49, + "execution_count": 48, "metadata": {}, "output_type": "execute_result" } @@ -1332,10 +1262,8 @@ }, { "cell_type": "code", - "execution_count": 50, - "metadata": { - "collapsed": false - }, + "execution_count": 49, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -1364,17 +1292,15 @@ }, { "cell_type": "code", - "execution_count": 51, - "metadata": { - "collapsed": false - }, + "execution_count": 50, + "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))\n", - "(True, {})\n" + "(True, spot.mark_t([]))\n" ] } ], @@ -1385,17 +1311,15 @@ }, { "cell_type": "code", - "execution_count": 52, - "metadata": { - "collapsed": false - }, + "execution_count": 51, + "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "(0, t)\n", - "(False, {})\n" + "(False, spot.mark_t([]))\n" ] } ], @@ -1407,17 +1331,15 @@ }, { "cell_type": "code", - "execution_count": 53, - "metadata": { - "collapsed": false - }, + "execution_count": 52, + "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "(4, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))\n", - "(True, {2})\n" + "(True, spot.mark_t([2]))\n" ] } ], @@ -1444,7 +1366,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.3" + "version": "3.6.7" } }, "nbformat": 4, diff --git a/tests/python/accparse.ipynb b/tests/python/accparse.ipynb index bb6518461..3122a42ce 100644 --- a/tests/python/accparse.ipynb +++ b/tests/python/accparse.ipynb @@ -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, diff --git a/tests/python/atva16-fig2a.ipynb b/tests/python/atva16-fig2a.ipynb index 66c50b728..2024d5ccd 100644 --- a/tests/python/atva16-fig2a.ipynb +++ b/tests/python/atva16-fig2a.ipynb @@ -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 @@ "\n" ], "text/plain": [ - " *' at 0x7f81a85ea1e0> >" + " *' 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, diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index 3128236d4..9209b6991 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -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 @@ "\n" ], "text/plain": [ - " *' at 0x7effe06cf120> >" + " *' 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 @@ "\n" ], "text/plain": [ - " *' at 0x7effe05eda80> >" + " *' at 0x7f0d1c02c930> >" ] }, "execution_count": 6, @@ -719,7 +719,7 @@ "\n" ], "text/plain": [ - " *' at 0x7effe05edab0> >" + " *' at 0x7f0d1c02c960> >" ] }, "execution_count": 7, @@ -802,7 +802,7 @@ "\n" ], "text/plain": [ - " *' at 0x7effe05edae0> >" + " *' 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 @@ "\n" ], "text/plain": [ - " *' at 0x7effe05edba0> >" + " *' at 0x7f0d1c03ec90> >" ] }, "execution_count": 12, @@ -1435,7 +1435,7 @@ "\n" ], "text/plain": [ - " *' at 0x7effe05edcf0> >" + " *' at 0x7f0d1c03edb0> >" ] }, "execution_count": 13, @@ -1566,7 +1566,7 @@ "\n" ], "text/plain": [ - " *' at 0x7effe05ed930> >" + " *' at 0x7f0d1c03ecf0> >" ] }, "execution_count": 14, @@ -1785,7 +1785,7 @@ "\n" ], "text/plain": [ - " *' at 0x7effe05eda50> >" + " *' at 0x7f0d077c1540> >" ] }, "metadata": {}, @@ -1935,7 +1935,7 @@ "\n" ], "text/plain": [ - " *' at 0x7effe06cf0c0> >" + " *' at 0x7f0d1c02c630> >" ] }, "metadata": {}, @@ -2107,7 +2107,7 @@ "\n" ], "text/plain": [ - " *' at 0x7effe05edb40> >" + " *' at 0x7f0d077c1780> >" ] }, "metadata": {}, @@ -2282,7 +2282,7 @@ "\n" ], "text/plain": [ - " *' at 0x7effe05edbd0> >" + " *' at 0x7f0d077c1660> >" ] }, "metadata": {}, @@ -2468,7 +2468,7 @@ "\n" ], "text/plain": [ - " *' at 0x7effe05ed870> >" + " *' at 0x7f0d077c1810> >" ] }, "execution_count": 19, @@ -2544,7 +2544,7 @@ "\n" ], "text/plain": [ - " *' at 0x7effe05ed8d0> >" + " *' at 0x7f0d077c1930> >" ] }, "execution_count": 20, @@ -3062,7 +3062,7 @@ "\n" ], "text/plain": [ - " *' at 0x7effe05ed9c0> >" + " *' at 0x7f0d077c1e40> >" ] }, "metadata": {}, @@ -3162,7 +3162,7 @@ "\n" ], "text/plain": [ - " *' at 0x7effe05ed9f0> >" + " *' at 0x7f0d1c02c750> >" ] }, "execution_count": 24, @@ -3235,7 +3235,7 @@ "\n" ], "text/plain": [ - " *' at 0x7effe05eda20> >" + " *' at 0x7f0d1c02c780> >" ] }, "execution_count": 25, @@ -3399,7 +3399,7 @@ "\n" ], "text/plain": [ - " *' at 0x7effe05edb40> >" + " *' at 0x7f0d1c03ed80> >" ] }, "execution_count": 27, @@ -3482,7 +3482,7 @@ "\n" ], "text/plain": [ - " *' at 0x7effe05ed9c0> >" + " *' at 0x7f0d077c1e40> >" ] }, "metadata": {}, @@ -3547,7 +3547,7 @@ "\n" ], "text/plain": [ - " *' at 0x7effe05ed9c0> >" + " *' at 0x7f0d077c1e40> >" ] }, "metadata": {}, @@ -3634,7 +3634,7 @@ "\n" ], "text/plain": [ - " *' at 0x7effe05ed9c0> >" + " *' 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, diff --git a/tests/python/bdditer.py b/tests/python/bdditer.py index eea25a761..ea701ac80 100644 --- a/tests/python/bdditer.py +++ b/tests/python/bdditer.py @@ -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) diff --git a/tests/python/contains.ipynb b/tests/python/contains.ipynb index 0e0022b0f..8d2f41ac6 100644 --- a/tests/python/contains.ipynb +++ b/tests/python/contains.ipynb @@ -322,8 +322,11 @@ "outputs": [ { "data": { + "text/latex": [ + "$\\mathsf{cycle}\\{a; \\lnot a\\}$" + ], "text/plain": [ - "cycle{a; !a}" + " *' 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, diff --git a/tests/python/formulas.ipynb b/tests/python/formulas.ipynb index ab47bfb99..69836c91a 100644 --- a/tests/python/formulas.ipynb +++ b/tests/python/formulas.ipynb @@ -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, diff --git a/tests/python/gen.ipynb b/tests/python/gen.ipynb index a6c655a52..832daddde 100644 --- a/tests/python/gen.ipynb +++ b/tests/python/gen.ipynb @@ -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, diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb index 28db29de6..8a558e773 100644 --- a/tests/python/highlighting.ipynb +++ b/tests/python/highlighting.ipynb @@ -240,7 +240,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a44f3f090> >" + " *' at 0x7fc2846aa7b0> >" ] }, "execution_count": 4, @@ -352,7 +352,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a44edacc0> >" + " *' at 0x7fc2846aa780> >" ] }, "execution_count": 5, @@ -462,7 +462,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a44f3f090> >" + " *' at 0x7fc2846aa7b0> >" ] }, "execution_count": 6, @@ -695,7 +695,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a44eec0c0> >" + " *' 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 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a44eec0c0> >" + " *' at 0x7fc2845d2720> >" ] }, "execution_count": 11, @@ -977,7 +975,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a44e7cb70> >" + " *' at 0x7fc2845e4f00> >" ] }, "metadata": {}, @@ -1032,7 +1030,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a44e7c8a0> >" + " *' at 0x7fc2845e4e40> >" ] }, "metadata": {}, @@ -1126,7 +1124,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a44e7c960> >" + " *' 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 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a44e7c960> >" + " *' at 0x7fc2845d2600> >" ] }, "metadata": {}, @@ -1322,7 +1318,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a44e7cb70> >" + " *' at 0x7fc2845e4f00> >" ] }, "metadata": {}, @@ -1377,7 +1373,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a44e7c8a0> >" + " *' 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 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a44e7cf00> >" + " *' at 0x7fc284574690> >" ] }, "metadata": {}, @@ -1694,7 +1689,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a44e7cf60> >" + " *' at 0x7fc2845746f0> >" ] }, "metadata": {}, @@ -1791,7 +1786,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a44e7cdb0> >" + " *' 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 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a44e7cea0> >" + " *' at 0x7fc284574840> >" ] }, "execution_count": 18, @@ -2127,7 +2123,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a44e7cea0> >" + " *' at 0x7fc284574840> >" ] }, "execution_count": 19, @@ -2290,7 +2286,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6a44e7cea0> >" + " *' 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, diff --git a/tests/python/ltlsimple.py b/tests/python/ltlsimple.py index 8b101dfb0..bb3d6c206 100755 --- a/tests/python/ltlsimple.py +++ b/tests/python/ltlsimple.py @@ -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): diff --git a/tests/python/ltsmin-dve.ipynb b/tests/python/ltsmin-dve.ipynb index 62d8bfab8..f2b34d426 100644 --- a/tests/python/ltsmin-dve.ipynb +++ b/tests/python/ltsmin-dve.ipynb @@ -436,7 +436,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f306034fb70> >" + " *' at 0x7f0f044132a0> >" ] }, "execution_count": 9, @@ -1265,7 +1265,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f30602ddba0> >" + " *' at 0x7f0f04381d50> >" ] }, "execution_count": 12, @@ -1453,7 +1453,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f306034f9c0> >" + " *' 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 @@ "\n" ], "text/plain": [ - " *' at 0x7f30602dded0> >" + " *' 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, diff --git a/tests/python/product.ipynb b/tests/python/product.ipynb index de0db966a..269ef1f8a 100644 --- a/tests/python/product.ipynb +++ b/tests/python/product.ipynb @@ -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, diff --git a/tests/python/relabel.py b/tests/python/relabel.py index b658a3fff..9d983eabd 100644 --- a/tests/python/relabel.py +++ b/tests/python/relabel.py @@ -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') diff --git a/tests/python/satmin.ipynb b/tests/python/satmin.ipynb index 16e9e44a5..318981a37 100644 --- a/tests/python/satmin.ipynb +++ b/tests/python/satmin.ipynb @@ -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 @@ "\n" ], "text/plain": [ - " *' at 0x7f79c85a5150> >" + " *' at 0x7f3f787b3690> >" ] }, "execution_count": 3, @@ -444,7 +444,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f79c857fb40> >" + " *' at 0x7f3f78fcd840> >" ] }, "execution_count": 4, @@ -680,7 +680,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f79c85d20f0> >" + " *' at 0x7f3f78761300> >" ] }, "execution_count": 5, @@ -913,7 +913,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f79c857f5d0> >" + " *' 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 @@ "\n" ], "text/plain": [ - " *' at 0x7f79c857fc00> >" + " *' 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 @@ "\n" ], "text/plain": [ - " *' at 0x7f79c857f9c0> >" + " *' 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 @@ "\n" ], "text/plain": [ - " *' at 0x7f79c851b090> >" + " *' 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 @@ " 40\n", " 2760\n", " 224707\n", - " 9\n", + " 8\n", " 0\n", - " 6\n", + " 7\n", " 0\n", " \n", " \n", @@ -1494,7 +1494,7 @@ " 155020\n", " 6\n", " 0\n", - " 7\n", + " 5\n", " 0\n", " \n", " \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 @@ "\n" ], "text/plain": [ - " *' at 0x7f79cdb10330> >" + " *' 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 @@ " 32\n", " 960\n", " 71987\n", - " 3\n", + " 4\n", " 0\n", - " 2\n", + " 1\n", " 0\n", " \n", " \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 @@ "\n" ], "text/plain": [ - " *' at 0x7f79cdb107b0> >" + " *' 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 @@ " 2300\n", " 285287\n", " 13\n", - " 0\n", - " 9\n", + " 1\n", + " 10\n", " 0\n", " \n", " \n", @@ -1981,7 +1981,7 @@ " NaN\n", " 92\n", " 2193\n", - " 0\n", + " 1\n", " 0\n", " 0\n", " 0\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 @@ "\n" ], "text/plain": [ - " *' at 0x7f79cdb108d0> >" + " *' 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 @@ " 40\n", " 2742\n", " 173183\n", - " 6\n", + " 7\n", " 0\n", - " 3\n", + " 2\n", " 0\n", " \n", " \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 @@ "\n" ], "text/plain": [ - " *' at 0x7f79c857fba0> >" + " *' 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 @@ " NaN\n", " 2747\n", " 173427\n", - " 6\n", + " 7\n", " 0\n", - " 1\n", + " 2\n", " 0\n", " \n", " \n", @@ -2445,7 +2445,7 @@ " 173427\n", " 0\n", " 0\n", - " 1\n", + " 0\n", " 0\n", " \n", " \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 @@ "\n" ], "text/plain": [ - " *' at 0x7f79cdb10b10> >" + " *' 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 @@ " 173183\n", " 6\n", " 0\n", - " 3\n", + " 2\n", " 0\n", " \n", " \n", @@ -2704,7 +2704,7 @@ " 2742\n", " 173279\n", " 0\n", - " 1\n", + " 0\n", " 1\n", " 0\n", " \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 @@ "\n" ], "text/plain": [ - " *' at 0x7f79cdb10c30> >" + " *' 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 @@ "\n" ], "text/plain": [ - " *' at 0x7f79cdb109f0> >" + " *' at 0x7f3f5bd9e060> >" ] }, "metadata": {}, @@ -3098,7 +3098,7 @@ " 173183\n", " 7\n", " 0\n", - " 3\n", + " 2\n", " 0\n", " HOA: v1 States: 5 Start: 0 AP: 3 \"a\" \"c\" \"b\" a...\n", " \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 @@ "\n" ], "text/plain": [ - " *' at 0x7f79cdb10a80> >" + " *' at 0x7f3f5bd9e0c0> >" ] }, "metadata": {}, @@ -3484,7 +3484,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f79cdb10e40> >" + " *' at 0x7f3f5bd9e150> >" ] }, "metadata": {}, @@ -3511,7 +3511,7 @@ }, { "cell_type": "code", - "execution_count": 18, + "execution_count": 19, "metadata": {}, "outputs": [ { @@ -3716,10 +3716,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f79c857f5d0> >" + " *' 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 @@ "\n" ], "text/plain": [ - " *' at 0x7f79cdb10e40> >" + " *' 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 @@ " 2\n", " 0\n", " 1\n", - " 1\n", + " 0\n", " \n", " \n", " 1\n", @@ -4034,7 +4034,7 @@ " NaN\n", " 162\n", " 3129\n", - " 0\n", + " 1\n", " 0\n", " 0\n", " 0\n", @@ -4048,7 +4048,7 @@ " NaN\n", " 363\n", " 10496\n", - " 1\n", + " 0\n", " 0\n", " 0\n", " 0\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 @@ "\n" ], "text/plain": [ - " *' at 0x7f79cdae52a0> >" + " *' 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 @@ " 56\n", " 1379\n", " 87992\n", - " 4\n", + " 3\n", " 0\n", - " 1\n", + " 2\n", " 0\n", " \n", " \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 @@ "\n" ], "text/plain": [ - " *' at 0x7f79cdae5270> >" + " *' 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, diff --git a/tests/python/stutter-inv.ipynb b/tests/python/stutter-inv.ipynb index 5c9e12e84..4ad4f5974 100644 --- a/tests/python/stutter-inv.ipynb +++ b/tests/python/stutter-inv.ipynb @@ -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 @@ "\n" ], "text/plain": [ - " *' at 0x7f68605f5630> >" + " *' at 0x7f0a9c1ee180> >" ] }, "metadata": {}, @@ -595,7 +595,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f68605f5ae0> >" + " *' at 0x7f0a9c250300> >" ] }, "metadata": {}, @@ -804,7 +804,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f68605f5ae0> >" + " *' at 0x7f0a9c250300> >" ] }, "metadata": {}, @@ -956,7 +956,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f68605f5a50> >" + " *' at 0x7f0a9c1e1f60> >" ] }, "metadata": {}, @@ -1054,7 +1054,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f68605f5b70> >" + " *' at 0x7f0a9c1e1840> >" ] }, "metadata": {}, @@ -1264,7 +1264,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f68605f5ba0> >" + " *' at 0x7f0a9c1ee990> >" ] }, "metadata": {}, @@ -1393,7 +1393,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f686063ef30> >" + " *' at 0x7f0a9c2502a0> >" ] }, "metadata": {}, @@ -1524,7 +1524,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6860602930> >" + " *' at 0x7f0a9c20eb10> >" ] }, "metadata": {}, @@ -1784,7 +1784,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6860591c30> >" + " *' at 0x7f0a9c20eea0> >" ] }, "metadata": {}, @@ -2098,7 +2098,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f6860591c30> >" + " *' 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, diff --git a/tests/python/word.ipynb b/tests/python/word.ipynb index bab2eb341..668417ed2 100644 --- a/tests/python/word.ipynb +++ b/tests/python/word.ipynb @@ -166,7 +166,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fca777b2090> >" + " *' 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}" + " *' 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}" + " *' 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}" + " *' 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 @@ "\n" ], "text/plain": [ - " *' at 0x7fca7775f690> >" + " *' 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,