From 704eaf26c2b3db820469db9cbe83b9aed03691af Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 19 May 2015 20:54:03 +0200 Subject: [PATCH] acc: add support for generating parity conditions * src/twa/acc.cc, src/twa/acc.hh: Here. * wrap/python/tests/accparse.ipynb: Test it. --- src/twa/acc.cc | 72 ++++++++++++++++++++++++++++++++ src/twa/acc.hh | 2 + wrap/python/tests/accparse.ipynb | 39 ++++++++++++----- 3 files changed, 102 insertions(+), 11 deletions(-) diff --git a/src/twa/acc.cc b/src/twa/acc.cc index efdf8f474..198ac5c2e 100644 --- a/src/twa/acc.cc +++ b/src/twa/acc.cc @@ -445,6 +445,32 @@ namespace spot return true; } + acc_cond::acc_code + acc_cond::acc_code::parity(bool max, bool odd, unsigned sets) + { + if (sets == 0) + return f(); + // When you look at something like + // acc-name: parity min even 5 + // Acceptance: 5 Inf(0) | (Fin(1) & (Inf(2) | (Fin(3) & Inf(4)))) + // remember that we build it from right to left. + int start = max ? 0 : sets - 1; + int inc = max ? 1 : -1; + int end = max ? sets : -1; + // Do not start with a Fin term, the right-most term is always Inf. + if ((start & 1) != odd) + start += inc; + acc_cond::acc_code res = f(); + for (int i = start; i != end; i += inc) + { + if ((i & 1) == odd) + res.append_or(inf({(unsigned)i})); + else + res.append_and(fin({(unsigned)i})); + } + return res; + } + namespace { bdd to_bdd_rec(const acc_cond::acc_word* c, const bdd* map) @@ -1186,6 +1212,44 @@ namespace spot return res; } + static bool max_or_min(const char*& input) + { + skip_space(input); + if (!strncmp(input, "max", 3)) + { + input += 3; + return true; + } + if (!strncmp(input, "min", 3)) + { + input += 3; + return false; + } + std::ostringstream s; + s << "syntax error at '" << input + << "': expecting 'min' or 'max'"; + throw parse_error(s.str()); + } + + static bool odd_or_even(const char*& input) + { + skip_space(input); + if (!strncmp(input, "odd", 3)) + { + input += 3; + return true; + } + if (!strncmp(input, "even", 4)) + { + input += 4; + return false; + } + std::ostringstream s; + s << "syntax error at '" << input + << "': expecting 'odd' or 'even'"; + throw parse_error(s.str()); + } + } acc_cond::acc_code parse_acc_code(const char* input) @@ -1245,6 +1309,14 @@ namespace spot } c = acc_cond::acc_code::generalized_rabin(v.begin(), v.end()); } + else if (!strncmp(input, "parity", 6)) + { + input += 6; + bool max = max_or_min(input); + bool odd = odd_or_even(input); + unsigned num = parse_num(input); + c = acc_cond::acc_code::parity(max, odd, num); + } else { c = parse_acc(input); diff --git a/src/twa/acc.hh b/src/twa/acc.hh index b76efcd57..8d5a85d2c 100644 --- a/src/twa/acc.hh +++ b/src/twa/acc.hh @@ -519,6 +519,8 @@ namespace spot return res; } + static acc_code parity(bool max, bool odd, unsigned sets); + void append_and(acc_code&& r) { if (is_true() || r.is_false()) diff --git a/wrap/python/tests/accparse.ipynb b/wrap/python/tests/accparse.ipynb index ca7e3372d..75fcf7f5d 100644 --- a/wrap/python/tests/accparse.ipynb +++ b/wrap/python/tests/accparse.ipynb @@ -105,7 +105,13 @@ " '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", + " 'generalized-Rabin 3 1 2 3', 'generalized-Rabin 0',\n", + " 'parity min even 6', 'parity max odd 6', 'parity max even 6', 'parity min odd 6',\n", + " 'parity min even 5', 'parity max odd 5', 'parity max even 5', 'parity min odd 5',\n", + " 'parity min even 2', 'parity max odd 2', 'parity max even 2', 'parity min odd 2',\n", + " '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='')" ], "language": "python", @@ -128,20 +134,31 @@ "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" + "generalized-Rabin 0: f\n", + "parity min even 6: Inf(0) | (Fin(1) & (Inf(2) | (Fin(3) & Inf(4))))\n", + "parity max odd 6: Inf(5) | (Fin(4) & (Inf(3) | (Fin(2) & Inf(1))))\n", + "parity max even 6: Fin(5) & (Inf(4) | (Fin(3) & (Inf(2) | (Fin(1) & Inf(0)))))\n", + "parity min odd 6: Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | (Fin(4) & Inf(5)))))\n", + "parity min even 5: Inf(0) | (Fin(1) & (Inf(2) | (Fin(3) & Inf(4))))\n", + "parity max odd 5: Fin(4) & (Inf(3) | (Fin(2) & Inf(1)))\n", + "parity max even 5: Inf(4) | (Fin(3) & (Inf(2) | (Fin(1) & Inf(0))))\n", + "parity min odd 5: Fin(0) & (Inf(1) | (Fin(2) & Inf(3)))\n", + "parity min even 2: Inf(0)\n", + "parity max odd 2: Inf(1)\n", + "parity max even 2: Fin(1) & Inf(0)\n", + "parity min odd 2: Fin(0) & Inf(1)\n", + "parity min even 1: Inf(0)\n", + "parity max odd 1: f\n", + "parity max even 1: Inf(0)\n", + "parity min odd 1: f\n", + "parity min even 0: f\n", + "parity max odd 0: f\n", + "parity max even 0: f\n", + "parity min odd 0: f\n" ] } ], "prompt_number": 5 - }, - { - "cell_type": "code", - "collapsed": true, - "input": [], - "language": "python", - "metadata": {}, - "outputs": [], - "prompt_number": null } ], "metadata": {}