diff --git a/src/tests/satmin2.test b/src/tests/satmin2.test index b459fa179d54211ffc43c15788e36789c3472166..d7eb8b27212e854e7aa0f78c41f56486f46d82a8 100755 --- a/src/tests/satmin2.test +++ b/src/tests/satmin2.test @@ -165,11 +165,11 @@ State: 0 --END-- EOF -$autfilt --sat-minimize='acc="Inf(0)|Fin(1)",max-states=2' foo.hoa \ +$autfilt --sat-minimize='acc="Streett 1",max-states=2' foo.hoa \ --stats=%s >out test "`cat out`" = 1 -$autfilt --sat-minimize='acc="Inf(0)&Fin(1)",max-states=4' foo.hoa \ +$autfilt --sat-minimize='acc="Rabin 1",max-states=4' foo.hoa \ --stats=%s >out && exit 1 test -z "`cat out`" diff --git a/src/twa/acc.cc b/src/twa/acc.cc index b07f25db17b0ea74fc0e3e48fc25e7a30639bc97..5eeb7eff2815e355c8ac901ca54a6beeae8d13be 100644 --- a/src/twa/acc.cc +++ b/src/twa/acc.cc @@ -1012,8 +1012,6 @@ namespace spot static unsigned parse_num(const char*& input) { - skip_space(input); - expect(input, '('); errno = 0; char* end; @@ -1027,6 +1025,14 @@ namespace spot } input = end; + return num; + } + + static unsigned parse_par_num(const char*& input) + { + skip_space(input); + expect(input, '('); + unsigned num = parse_num(input); skip_space(input); expect(input, ')'); return num; @@ -1056,12 +1062,12 @@ namespace spot else if (!strncmp(input, "Inf", 3)) { input += 3; - res = acc_cond::acc_code::inf({parse_num(input)}); + res = acc_cond::acc_code::inf({parse_par_num(input)}); } else if (!strncmp(input, "Fin", 3)) { input += 3; - res = acc_cond::acc_code::fin({parse_num(input)}); + res = acc_cond::acc_code::fin({parse_par_num(input)}); } else { @@ -1088,7 +1094,65 @@ namespace spot acc_cond::acc_code parse_acc_code(const char* input) { skip_space(input); - acc_cond::acc_code c = parse_acc(input); + acc_cond::acc_code c; + if (!strncmp(input, "all", 3)) + { + input += 3; + c = acc_cond::acc_code::t(); + } + else if (!strncmp(input, "none", 4)) + { + input += 4; + c = acc_cond::acc_code::f(); + } + else if (!strncmp(input, "Buchi", 5)) + { + input += 5; + c = acc_cond::acc_code::buchi(); + } + else if (!strncmp(input, "co-Buchi", 8)) + { + input += 8; + c = acc_cond::acc_code::cobuchi(); + } + else if (!strncmp(input, "generalized-Buchi", 17)) + { + input += 17; + c = acc_cond::acc_code::generalized_buchi(parse_num(input)); + } + else if (!strncmp(input, "generalized-co-Buchi", 20)) + { + input += 20; + c = acc_cond::acc_code::generalized_buchi(parse_num(input)); + } + else if (!strncmp(input, "Rabin", 5)) + { + input += 5; + c = acc_cond::acc_code::rabin(parse_num(input)); + } + else if (!strncmp(input, "Streett", 7)) + { + input += 7; + c = acc_cond::acc_code::streett(parse_num(input)); + } + else if (!strncmp(input, "generalized-Rabin", 17)) + { + input += 17; + unsigned num = parse_num(input); + std::vector v; + v.reserve(num); + while (num > 0) + { + v.push_back(parse_num(input)); + --num; + } + c = acc_cond::acc_code::generalized_rabin(v.begin(), v.end()); + } + else + { + c = parse_acc(input); + } + skip_space(input); if (*input) { std::ostringstream s; diff --git a/src/twa/acc.hh b/src/twa/acc.hh index bf068472c770b61e73973a9e7a9075a968c5e892..97c31e79e65cceb0520e06c13ee2d10b00ffe3a9 100644 --- a/src/twa/acc.hh +++ b/src/twa/acc.hh @@ -451,6 +451,74 @@ namespace spot return inf_neg(mark_t(vals)); } + static acc_code buchi() + { + return inf({0}); + } + + static acc_code cobuchi() + { + return fin({0}); + } + + static acc_code generalized_buchi(unsigned n) + { + acc_cond::mark_t m = (1U << n) - 1; + return inf(m); + } + + static acc_code generalized_co_buchi(unsigned n) + { + acc_cond::mark_t m = (1U << n) - 1; + return fin(m); + } + + // n is a number of pairs. + static acc_code rabin(unsigned n) + { + acc_cond::acc_code res = f(); + while (n > 0) + { + acc_cond::acc_code pair = inf({2*n - 1}); + pair.append_and(fin({2*n - 2})); + res.append_or(std::move(pair)); + --n; + } + return res; + } + + // n is a number of pairs. + static acc_code streett(unsigned n) + { + acc_cond::acc_code res = t(); + while (n > 0) + { + acc_cond::acc_code pair = inf({2*n - 1}); + pair.append_or(fin({2*n - 2})); + res.append_and(std::move(pair)); + --n; + } + return res; + } + + template + static acc_code generalized_rabin(iterator begin, iterator end) + { + acc_cond::acc_code res = f(); + unsigned n = 0; + for (iterator i = begin; i != end; ++i) + { + acc_cond::acc_code pair = fin({n++}); + acc_cond::mark_t m = 0U; + for (unsigned ni = *i; ni > 0; --ni) + m.set({n++}); + pair.append_and(inf(m)); + std::swap(pair, res); + res.append_or(std::move(pair)); + } + return res; + } + void append_and(acc_code&& r) { if (is_true() || r.is_false()) diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 11540780947c8dccc7076a4250f115968a0f1bfc..8753acd65cb2fdf515d15fcffbc9635e0d649531 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -344,6 +344,22 @@ spot::ltl::formula_ptr_less_than>; std::string __str__() { return spot::ltl::to_string(self); } } +%extend spot::acc_cond::acc_code { + std::string __repr__() + { + std::ostringstream os; + os << *self; + return os.str(); + } + + std::string __str__() + { + std::ostringstream os; + os << *self; + return os.str(); + } +} + %nodefaultctor std::ostream; namespace std { class ostream {}; diff --git a/wrap/python/tests/Makefile.am b/wrap/python/tests/Makefile.am index 7dc5e3117d4e811a40a263842fa14fca610c38f3..3be352b07aa02180d15006f478cd363cb7b9e855 100644 --- a/wrap/python/tests/Makefile.am +++ b/wrap/python/tests/Makefile.am @@ -31,6 +31,7 @@ LOG_DRIVER = $(TEST_LOG_DRIVER) check_SCRIPTS = run TESTS = \ + accparse.ipynb \ alarm.py \ automata.ipynb \ automata-io.ipynb \ diff --git a/wrap/python/tests/accparse.ipynb b/wrap/python/tests/accparse.ipynb new file mode 100644 index 0000000000000000000000000000000000000000..ca7e3372dbf347e37ccc457f8f5908e3b3d44940 --- /dev/null +++ b/wrap/python/tests/accparse.ipynb @@ -0,0 +1,150 @@ +{ + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.4.3+" + }, + "name": "" + }, + "nbformat": 3, + "nbformat_minor": 0, + "worksheets": [ + { + "cells": [ + { + "cell_type": "code", + "collapsed": true, + "input": [ + "import spot\n", + "spot.setup()" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 1 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "c = spot.parse_acc_code('Inf(0)&Fin(1)|Inf(2)&Fin(3)'); c" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 2, + "text": [ + "(Fin(1) & Inf(0)) | (Fin(3) & Inf(2))" + ] + } + ], + "prompt_number": 2 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "c.to_dnf()" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 3, + "text": [ + "(Fin(1) & Inf(0)) | (Fin(3) & Inf(2))" + ] + } + ], + "prompt_number": 3 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "c.to_cnf()" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 4, + "text": [ + "(Inf(0) | Inf(2)) & (Fin(3) | Inf(0)) & (Fin(1) | Inf(2)) & (Fin(1)|Fin(3))" + ] + } + ], + "prompt_number": 4 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "for acc in ['all', 't', \n", + " 'Buchi', 'generalized-Buchi 3', 'generalized-Buchi 0',\n", + " 'co-Buchi', 'generalized-co-Buchi 3', 'generalized-co-Buchi 0',\n", + " 'Rabin 2', 'Rabin 0',\n", + " 'Streett 2', 'Streett 0',\n", + " 'generalized-Rabin 3 1 2 3', 'generalized-Rabin 0']:\n", + " print(acc, ': ', spot.parse_acc_code(acc), sep='')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "all: t\n", + "t: t\n", + "Buchi: Inf(0)\n", + "generalized-Buchi 3: Inf(0)&Inf(1)&Inf(2)\n", + "generalized-Buchi 0: t\n", + "co-Buchi: Fin(0)\n", + "generalized-co-Buchi 3: Inf(0)&Inf(1)&Inf(2)\n", + "generalized-co-Buchi 0: t\n", + "Rabin 2: (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\n", + "Rabin 0: f\n", + "Streett 2: (Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\n", + "Streett 0: t\n", + "generalized-Rabin 3 1 2 3: (Fin(0) & Inf(1)) | (Fin(2) & (Inf(3)&Inf(4))) | (Fin(5) & (Inf(6)&Inf(7)&Inf(8)))\n", + "generalized-Rabin 0: f\n" + ] + } + ], + "prompt_number": 5 + }, + { + "cell_type": "code", + "collapsed": true, + "input": [], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": null + } + ], + "metadata": {} + } + ] +} \ No newline at end of file