From df1ef302e86d6a6889468284ff8d34eee488a6d5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 18 Dec 2015 17:47:16 +0100 Subject: [PATCH] acc_code: parse from the constructor * spot/twa/acc.hh, spot/twa/acc.cc (parse_acc_code): Rename as... (acc_cond::acc_code): ... this, making it a lot easier to build acceptance conditions from strings. * NEWS: Mention the change. * spot/twaalgos/dtwasat.cc, spot/bin/randaut.cc, spot/tests/acc.cc: Adjust. * wrap/python/tests/acc_cond.ipynb, wrap/python/tests/accparse.ipynb, wrap/python/tests/accparse2.py: Simplify, but not completely to exercise all variants. * wrap/python/spot_impl.i: Make acc_code's constructor implicit. --- NEWS | 3 +- spot/bin/randaut.cc | 2 +- spot/tests/acc.cc | 16 ++-- spot/twa/acc.cc | 4 +- spot/twa/acc.hh | 52 +++++++----- spot/twaalgos/dtwasat.cc | 2 +- wrap/python/spot_impl.i | 1 + wrap/python/tests/acc_cond.ipynb | 133 ++++++++++++++++++++----------- wrap/python/tests/accparse.ipynb | 16 +++- wrap/python/tests/accparse2.py | 49 +++++------- 10 files changed, 167 insertions(+), 111 deletions(-) diff --git a/NEWS b/NEWS index 94a7c4f24..51a1921da 100644 --- a/NEWS +++ b/NEWS @@ -48,10 +48,11 @@ New in spot 1.99.6a (not yet released) acc_cond::cap(l, r) -> use l & r acc_cond::set_minus(l, r) -> use l - r - Additionally, the following methods have been renamed: + Additionally, the following methods/functions have been renamed: acc_cond::is_tt() -> acc_cond::is_t() acc_cond::is_ff() -> acc_cond::is_f() + parse_acc_code() -> acc_cond::acc_code(...) Python: diff --git a/spot/bin/randaut.cc b/spot/bin/randaut.cc index 2effda970..f0ce89313 100644 --- a/spot/bin/randaut.cc +++ b/spot/bin/randaut.cc @@ -347,7 +347,7 @@ main(int argc, char** argv) spot::acc_cond::acc_code code; if (opt_acceptance) { - code = spot::parse_acc_code(opt_acceptance); + code = spot::acc_cond::acc_code(opt_acceptance); accs = code.used_sets().max_set(); if (opt_colored && accs == 0) error(2, 0, "--colored requires at least one acceptance set; " diff --git a/spot/tests/acc.cc b/spot/tests/acc.cc index f1aa8270e..e624b8b9a 100644 --- a/spot/tests/acc.cc +++ b/spot/tests/acc.cc @@ -158,14 +158,14 @@ int main() std::cout << code3 << ' ' << "{0} false\n"; print(code3.missing(m, false)); - std::cout << spot::parse_acc_code("t") << '\n'; - std::cout << spot::parse_acc_code("f") << '\n'; - std::cout << spot::parse_acc_code("Fin(2)") << '\n'; - std::cout << spot::parse_acc_code("Inf(2)") << '\n'; - std::cout << spot::parse_acc_code("Fin(2) | Inf(2)") << '\n'; - std::cout << spot::parse_acc_code("Inf(2) & Fin(2)") << '\n'; - auto c1 = spot::parse_acc_code("Fin(0)|Inf(1)&Fin(2)|Fin(3)"); - auto c2 = spot::parse_acc_code + std::cout << spot::acc_cond::acc_code("t") << '\n'; + std::cout << spot::acc_cond::acc_code("f") << '\n'; + std::cout << spot::acc_cond::acc_code("Fin(2)") << '\n'; + std::cout << spot::acc_cond::acc_code("Inf(2)") << '\n'; + std::cout << spot::acc_cond::acc_code("Fin(2) | Inf(2)") << '\n'; + std::cout << spot::acc_cond::acc_code("Inf(2) & Fin(2)") << '\n'; + auto c1 = spot::acc_cond::acc_code("Fin(0)|Inf(1)&Fin(2)|Fin(3)"); + auto c2 = spot::acc_cond::acc_code ("( Fin ( 0 )) | (Inf ( 1) & Fin(2 ))| Fin (3) "); std::cout << c1 << '\n'; std::cout << c2 << '\n'; diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 02abc56ca..8860d2fe6 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -1544,7 +1544,7 @@ namespace spot } - acc_cond::acc_code parse_acc_code(const char* input) + acc_cond::acc_code::acc_code(const char* input) { skip_space(input); acc_cond::acc_code c; @@ -1630,6 +1630,6 @@ namespace spot s << "syntax error at '" << input << "', unexpected character."; throw parse_error(s.str()); } - return c; + std::swap(c, *this); } } diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 496dd4ceb..d8eca7ba4 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -889,6 +889,38 @@ namespace spot std::function set_printer = nullptr) const; + + /// \brief Construct an acc_code from a string. + /// + /// The string can follow the following grammar: + /// + ///
+      ///   acc ::= "t"
+      ///         | "f"
+      ///         | "Inf" "(" num ")"
+      ///         | "Fin" "(" num ")"
+      ///         | "(" acc ")"
+      ///         | acc "&" acc
+      ///         | acc "|" acc
+      /// 
+ /// + /// Where num is an integer and "&" has priority over "|". Note that + /// "Fin(!x)" and "Inf(!x)" are not supported by this parser. + /// + /// Or the string can be the name of an acceptance condition, as + /// speficied in the HOA format. (E.g. "Rabin 2", "parity max odd 3", + /// "generalized-Rabin 4 2 1", etc.). + /// + /// A spot::parse_error is thrown on syntax error. + acc_code(const char* input); + + /// \brief Build an empty acceptance condition. + /// + /// This is the same as t(). + acc_code() + { + } + // Calls to_text SPOT_API friend std::ostream& operator<<(std::ostream& os, const acc_code& code); @@ -1167,26 +1199,6 @@ namespace spot }; - /// \brief Parse a string into an acc_code - /// - /// The string should follow the following grammar: - /// - ///
-  ///   acc ::= "t"
-  ///         | "f"
-  ///         | "Inf" "(" num ")"
-  ///         | "Fin" "(" num ")"
-  ///         | "(" acc ")"
-  ///         | acc "&" acc
-  ///         | acc "|" acc
-  /// 
- /// - /// Where num is an integer and "&" has priority over "|". Note that - /// "Fin(!x)" and "Inf(!x)" are not supported by this parser. - /// - /// A spot::parse_error is thrown on syntax error. - SPOT_API acc_cond::acc_code parse_acc_code(const char* input); - SPOT_API std::ostream& operator<<(std::ostream& os, const acc_cond& acc); } diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc index ac3c8c7c2..c1f3e9fa0 100644 --- a/spot/twaalgos/dtwasat.cc +++ b/spot/twaalgos/dtwasat.cc @@ -1313,7 +1313,7 @@ namespace spot if (!accstr.empty()) { user_supplied_acc = true; - target_acc = parse_acc_code(accstr.c_str()); + target_acc = acc_cond::acc_code(accstr.c_str()); // Just in case we were given something like // Fin(1) | Inf(3) // Rewrite it as diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 5622b5c82..a7fbe43c5 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -353,6 +353,7 @@ namespace std { %include %include %implicitconv spot::acc_cond::mark_t; +%implicitconv spot::acc_cond::acc_code; %feature("flatnested") spot::acc_cond::mark_t; %feature("flatnested") spot::acc_cond::acc_code; %apply bool* OUTPUT {bool& max, bool& odd}; diff --git a/wrap/python/tests/acc_cond.ipynb b/wrap/python/tests/acc_cond.ipynb index 4ad9c85c8..b18513672 100644 --- a/wrap/python/tests/acc_cond.ipynb +++ b/wrap/python/tests/acc_cond.ipynb @@ -18,7 +18,7 @@ "version": "3.4.3+" }, "name": "", - "signature": "sha256:c447381803e03318b0d23c721f53fa232f91ec81af26a7c09c817463eee5d417" + "signature": "sha256:9abaa081794db5d5479c8c9c179c8518aa52b60abdb4b7a106045646e277d43a" }, "nbformat": 3, "nbformat_minor": 0, @@ -473,14 +473,14 @@ "\n", "`acc_code` encodes the formula of the acceptance condition using a kind of bytecode that basically corresponds to an encoding in [reverse Polish notation](http://en.wikipedia.org/wiki/Reverse_Polish_notation) in which conjunctions of `Inf(n)` terms, and disjunctions of `Fin(n)` terms are grouped. In particular, the frequently-used genaralized-B\u00fcchi acceptance conditions (like `Inf(0)&Inf(1)&Inf(2)`) are always encoded as a single term (like `Inf({0,1,2})`).\n", "\n", - "The simplest way to construct an `acc_code` is via the `parse_acc_code()` function." + "The simplest way to construct an `acc_code` by passing a string that represent the formula to build." ] }, { "cell_type": "code", "collapsed": false, "input": [ - "spot.parse_acc_code('(Inf(0)&Fin(1))|Inf(2)')" + "spot.acc_code('(Inf(0)&Fin(1))|Inf(2)')" ], "language": "python", "metadata": {}, @@ -507,7 +507,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "spot.parse_acc_code('Rabin 2')" + "spot.acc_code('Rabin 2')" ], "language": "python", "metadata": {}, @@ -534,8 +534,8 @@ "cell_type": "code", "collapsed": false, "input": [ - "print(spot.parse_acc_code('Streett 2..4'))\n", - "print(spot.parse_acc_code('Streett 2..4'))" + "print(spot.acc_code('Streett 2..4'))\n", + "print(spot.acc_code('Streett 2..4'))" ], "language": "python", "metadata": {}, @@ -562,7 +562,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "spot.parse_acc_code('random 3..5')" + "spot.acc_code('random 3..5')" ], "language": "python", "metadata": {}, @@ -589,7 +589,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "a = spot.parse_acc_code('parity min odd 5')\n", + "a = spot.acc_code('parity min odd 5')\n", "a" ], "language": "python", @@ -660,8 +660,8 @@ "cell_type": "code", "collapsed": false, "input": [ - "x = spot.parse_acc_code('Rabin 2')\n", - "y = spot.parse_acc_code('Rabin 2') << 4\n", + "x = spot.acc_code('Rabin 2')\n", + "y = spot.acc_code('Rabin 2') << 4\n", "print(x)\n", "print(y)" ], @@ -732,7 +732,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Instead of using `parse_acc_code()`, it is also possible to build a formula from atoms like `Inf({...})`, `Fin({...})`, `t`, or `f`.\n", + "Instead of using `acc_code('string')`, it is also possible to build an acceptance formula from atoms like `Inf({...})`, `Fin({...})`, `t`, or `f`.\n", "\n", "Remember that in our encoding for the formula, terms like `Inf(1)&Inf(2)` and `Fin(3)|Fin(4)|Fin(5)` are actually stored as `Inf({1,2})` and `Fin({3,4,5})`, where `{1,2}` and `{3,4,5}` are instance of `mark_t`. These terms can be generated with the\n", "functions `spot.acc_code.inf(mark)` and `spot.acc_code.fin(mark)`.\n", @@ -851,7 +851,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "acc = spot.parse_acc_code('Fin(0) & Inf(1) | Inf(2)')\n", + "acc = spot.acc_code('Fin(0) & Inf(1) | Inf(2)')\n", "print(\"acc =\", acc)\n", "for x in ([0, 1, 2], [1, 2], [0, 1], [0, 2], [0], [1], [2], []):\n", " print(\"acc.accepting({}) = {}\".format(x, acc.accepting(x)))" @@ -888,7 +888,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "acc = spot.parse_acc_code('Fin(0) & Inf(2)')\n", + "acc = spot.acc_code('Fin(0) & Inf(2)')\n", "print(acc)\n", "print(acc.used_sets())\n", "print(acc.used_sets().max_set())" @@ -926,7 +926,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "acc = spot.acc_cond(4, spot.parse_acc_code('Rabin 2'))\n", + "acc = spot.acc_cond(4, spot.acc_code('Rabin 2'))\n", "acc" ], "language": "python", @@ -943,11 +943,19 @@ ], "prompt_number": 34 }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "For convenience, you can pass the string directly:" + ] + }, { "cell_type": "code", "collapsed": false, "input": [ - "acc.num_sets()" + "acc = spot.acc_cond(4, 'Rabin 2')\n", + "acc" ], "language": "python", "metadata": {}, @@ -957,7 +965,7 @@ "output_type": "pyout", "prompt_number": 35, "text": [ - "4" + "(4, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))" ] } ], @@ -967,7 +975,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "acc.get_acceptance()" + "acc.num_sets()" ], "language": "python", "metadata": {}, @@ -977,12 +985,32 @@ "output_type": "pyout", "prompt_number": 36, "text": [ - "(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))" + "4" ] } ], "prompt_number": 36 }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "acc.get_acceptance()" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 37, + "text": [ + "(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))" + ] + } + ], + "prompt_number": 37 + }, { "cell_type": "markdown", "metadata": {}, @@ -1003,13 +1031,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 37, + "prompt_number": 38, "text": [ "(4, t)" ] } ], - "prompt_number": 37 + "prompt_number": 38 }, { "cell_type": "code", @@ -1024,19 +1052,19 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 38, + "prompt_number": 39, "text": [ "(6, t)" ] } ], - "prompt_number": 38 + "prompt_number": 39 }, { "cell_type": "code", "collapsed": false, "input": [ - "acc.set_acceptance(spot.parse_acc_code('Streett 2'))\n", + "acc.set_acceptance('Streett 2')\n", "acc" ], "language": "python", @@ -1045,26 +1073,26 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 39, + "prompt_number": 40, "text": [ "(6, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))" ] } ], - "prompt_number": 39 + "prompt_number": 40 }, { "cell_type": "markdown", "metadata": {}, "source": [ - "Calling the constructor of `acc_cond` by passing just an instance of `acc_code` will automatically set the number of acceptance sets to the minimum needed by the formula:" + "Calling the constructor of `acc_cond` by passing just an instance of `acc_code` (or a string that will be passed to the `acc_code` constructor) will automatically set the number of acceptance sets to the minimum needed by the formula:" ] }, { "cell_type": "code", "collapsed": false, "input": [ - "acc = spot.acc_cond(spot.parse_acc_code('Streett 2'))\n", + "acc = spot.acc_cond('Streett 2')\n", "acc" ], "language": "python", @@ -1073,13 +1101,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 40, + "prompt_number": 41, "text": [ "(4, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))" ] } ], - "prompt_number": 40 + "prompt_number": 41 }, { "cell_type": "markdown", @@ -1092,7 +1120,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "code = spot.parse_acc_code('Streett 2')\n", + "code = spot.acc_code('Streett 2')\n", "acc = spot.acc_cond(code.used_sets().max_set(), code)\n", "acc" ], @@ -1102,13 +1130,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 41, + "prompt_number": 42, "text": [ "(4, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))" ] } ], - "prompt_number": 41 + "prompt_number": 42 }, { "cell_type": "markdown", @@ -1131,13 +1159,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 42, + "prompt_number": 43, "text": [ "(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))" ] } ], - "prompt_number": 42 + "prompt_number": 43 }, { "cell_type": "markdown", @@ -1170,7 +1198,7 @@ ] } ], - "prompt_number": 43 + "prompt_number": 44 }, { "cell_type": "markdown", @@ -1185,7 +1213,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "acc = spot.acc_cond(spot.parse_acc_code('Rabin 2'))\n", + "acc = spot.acc_cond('Rabin 2')\n", "print(acc)\n", "print(acc.is_rabin())\n", "print(acc.is_streett())" @@ -1203,7 +1231,7 @@ ] } ], - "prompt_number": 44 + "prompt_number": 45 }, { "cell_type": "markdown", @@ -1216,7 +1244,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "acc = spot.acc_cond(spot.parse_acc_code('parity min odd 4'))\n", + "acc = spot.acc_cond('parity min odd 4')\n", "print(acc)\n", "print(acc.is_parity())\n", "acc.set_generalized_buchi()\n", @@ -1237,7 +1265,7 @@ ] } ], - "prompt_number": 45 + "prompt_number": 46 }, { "cell_type": "markdown", @@ -1266,7 +1294,7 @@ ] } ], - "prompt_number": 46 + "prompt_number": 47 }, { "cell_type": "markdown", @@ -1287,13 +1315,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 47, + "prompt_number": 48, "text": [ "{0,1,2,3}" ] } ], - "prompt_number": 47 + "prompt_number": 48 }, { "cell_type": "markdown", @@ -1324,7 +1352,7 @@ ] } ], - "prompt_number": 48 + "prompt_number": 49 }, { "cell_type": "markdown", @@ -1354,13 +1382,13 @@ ] } ], - "prompt_number": 49 + "prompt_number": 50 }, { "cell_type": "code", "collapsed": false, "input": [ - "acc = spot.acc_cond(0)\n", + "acc = spot.acc_cond(0) # use 0 acceptance sets, and the default formula (t)\n", "print(acc)\n", "print(acc.unsat_mark())" ], @@ -1376,13 +1404,13 @@ ] } ], - "prompt_number": 50 + "prompt_number": 51 }, { "cell_type": "code", "collapsed": false, "input": [ - "acc = spot.acc_cond(spot.parse_acc_code('Streett 2'))\n", + "acc = spot.acc_cond('Streett 2')\n", "print(acc)\n", "print(acc.unsat_mark())" ], @@ -1398,7 +1426,16 @@ ] } ], - "prompt_number": 51 + "prompt_number": 52 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 52 } ], "metadata": {} diff --git a/wrap/python/tests/accparse.ipynb b/wrap/python/tests/accparse.ipynb index 031d02090..3b6c6ca63 100644 --- a/wrap/python/tests/accparse.ipynb +++ b/wrap/python/tests/accparse.ipynb @@ -17,7 +17,8 @@ "pygments_lexer": "ipython3", "version": "3.4.3+" }, - "name": "" + "name": "", + "signature": "sha256:1ee7951bed30652ae110a14b210541829221552eb944ff01f25236179673dd5b" }, "nbformat": 3, "nbformat_minor": 0, @@ -40,7 +41,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "c = spot.parse_acc_code('Inf(0)&Fin(1)|Inf(2)&Fin(3)'); c" + "c = spot.acc_code('Inf(0)&Fin(1)|Inf(2)&Fin(3)'); c" ], "language": "python", "metadata": {}, @@ -112,7 +113,7 @@ " 'parity min even 1', 'parity max odd 1', 'parity max even 1', 'parity min odd 1',\n", " 'parity min even 0', 'parity max odd 0', 'parity max even 0', 'parity min odd 0',\n", " ]:\n", - " print(acc, ': ', spot.parse_acc_code(acc), sep='')" + " print(acc, ': ', spot.acc_code(acc), sep='')" ], "language": "python", "metadata": {}, @@ -159,6 +160,15 @@ } ], "prompt_number": 5 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 5 } ], "metadata": {} diff --git a/wrap/python/tests/accparse2.py b/wrap/python/tests/accparse2.py index 38efae552..3bcf6a96e 100644 --- a/wrap/python/tests/accparse2.py +++ b/wrap/python/tests/accparse2.py @@ -20,79 +20,74 @@ import spot a = spot.acc_cond(5) -a.set_acceptance(spot.parse_acc_code('parity min odd 5')) +a.set_acceptance(spot.acc_code('parity min odd 5')) assert(a.is_parity() == [True, False, True]) -a.set_acceptance(spot.parse_acc_code('parity max even 5')) +a.set_acceptance('parity max even 5') assert(a.is_parity() == [True, True, False]) -a.set_acceptance(spot.parse_acc_code('generalized-Buchi 5')) +a.set_acceptance('generalized-Buchi 5') assert(a.is_parity()[0] == False) assert(a.is_parity(True)[0] == False) -a.set_acceptance(spot.parse_acc_code( - 'Inf(4) | (Fin(3)&Inf(2)) | (Fin(3)&Fin(1)&Inf(0))')) +a.set_acceptance('Inf(4) | (Fin(3)&Inf(2)) | (Fin(3)&Fin(1)&Inf(0))') assert(a.is_parity()[0] == False) assert(a.is_parity(True) == [True, True, False]) a = spot.acc_cond(0) -a.set_acceptance(spot.parse_acc_code('all')) +a.set_acceptance('all') assert(a.is_rabin() == -1) assert(a.is_streett() == 0) assert(a.is_parity() == [True, True, True]) -a.set_acceptance(spot.parse_acc_code('none')) +a.set_acceptance('none') assert(a.is_rabin() == 0) assert(a.is_streett() == -1) assert(a.is_parity() == [True, True, False]) -a = spot.acc_cond(2) -a.set_acceptance(spot.parse_acc_code('(Fin(0)&Inf(1))')) +a = spot.acc_cond('(Fin(0)&Inf(1))') assert(a.is_rabin() == 1) assert(a.is_streett() == -1) -a.set_acceptance(spot.parse_acc_code('Inf(1)&Fin(0)')) +a.set_acceptance('Inf(1)&Fin(0)') assert(a.is_rabin() == 1) assert(a.is_streett() == -1) -a.set_acceptance(spot.parse_acc_code('(Fin(0)|Inf(1))')) +a.set_acceptance('(Fin(0)|Inf(1))') assert(a.is_rabin() == -1) assert(a.is_streett() == 1) -a.set_acceptance(spot.parse_acc_code('Inf(1)|Fin(0)')) +a.set_acceptance('Inf(1)|Fin(0)') assert(a.is_rabin() == -1) assert(a.is_streett() == 1) -a = spot.acc_cond(4) -a.set_acceptance(spot.parse_acc_code('(Fin(0)&Inf(1))|(Fin(2)&Inf(3))')) +a = spot.acc_cond('(Fin(0)&Inf(1))|(Fin(2)&Inf(3))') assert(a.is_rabin() == 2) assert(a.is_streett() == -1) -a.set_acceptance(spot.parse_acc_code('(Inf(3)&Fin(2))|(Fin(0)&Inf(1))')) +a.set_acceptance(spot.acc_code('(Inf(3)&Fin(2))|(Fin(0)&Inf(1))')) assert(a.is_rabin() == 2) assert(a.is_streett() == -1) -a.set_acceptance(spot.parse_acc_code('(Inf(2)&Fin(3))|(Fin(0)&Inf(1))')) +a.set_acceptance(spot.acc_code('(Inf(2)&Fin(3))|(Fin(0)&Inf(1))')) assert(a.is_rabin() == -1) assert(a.is_streett() == -1) -a.set_acceptance(spot.parse_acc_code('(Inf(3)&Fin(2))|(Fin(2)&Inf(1))')) +a.set_acceptance(spot.acc_code('(Inf(3)&Fin(2))|(Fin(2)&Inf(1))')) assert(a.is_rabin() == -1) assert(a.is_streett() == -1) -a.set_acceptance(spot.parse_acc_code('(Inf(1)&Fin(0))|(Fin(0)&Inf(1))')) +a.set_acceptance(spot.acc_code('(Inf(1)&Fin(0))|(Fin(0)&Inf(1))')) assert(a.is_rabin() == -1) assert(a.is_streett() == -1) -r = spot.parse_acc_code('(Fin(0)&Inf(1))|(Inf(1)&Fin(0))|(Inf(3)&Fin(2))') -a.set_acceptance(r) +a.set_acceptance('(Fin(0)&Inf(1))|(Inf(1)&Fin(0))|(Inf(3)&Fin(2))') assert(a.is_rabin() == 2) assert(a.is_streett() == -1) -a.set_acceptance(spot.parse_acc_code('(Fin(0)|Inf(1))&(Fin(2)|Inf(3))')) +a.set_acceptance('(Fin(0)|Inf(1))&(Fin(2)|Inf(3))') assert(a.is_rabin() == -1) assert(a.is_streett() == 2) -a.set_acceptance(spot.parse_acc_code('(Inf(3)|Fin(2))&(Fin(0)|Inf(1))')) +a.set_acceptance('(Inf(3)|Fin(2))&(Fin(0)|Inf(1))') assert(a.is_rabin() == -1) assert(a.is_streett() == 2) -a.set_acceptance(spot.parse_acc_code('(Inf(2)|Fin(3))&(Fin(0)|Inf(1))')) +a.set_acceptance('(Inf(2)|Fin(3))&(Fin(0)|Inf(1))') assert(a.is_rabin() == -1) assert(a.is_streett() == -1) -a.set_acceptance(spot.parse_acc_code('(Inf(3)|Fin(2))&(Fin(2)|Inf(1))')) +a.set_acceptance('(Inf(3)|Fin(2))&(Fin(2)|Inf(1))') assert(a.is_rabin() == -1) assert(a.is_streett() == -1) -a.set_acceptance(spot.parse_acc_code('(Inf(1)|Fin(0))&(Fin(0)|Inf(1))')) +a.set_acceptance('(Inf(1)|Fin(0))&(Fin(0)|Inf(1))') assert(a.is_rabin() == -1) assert(a.is_streett() == -1) -r = spot.parse_acc_code('(Fin(0)|Inf(1))&(Inf(1)|Fin(0))&(Inf(3)|Fin(2))') -a.set_acceptance(r) +a.set_acceptance('(Fin(0)|Inf(1))&(Inf(1)|Fin(0))&(Inf(3)|Fin(2))') assert(a.is_rabin() == -1) assert(a.is_streett() == 2) -- GitLab