From 04171207e6c3528e875b11893f94c930cec49557 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 19 May 2015 22:22:53 +0200 Subject: [PATCH] acc: recognize parity acceptance It has two modes: strict or not. In strict mode (tested in hoaparse.test), the acceptance formula has to match exactly the one given in the HOA spec. In non-strict mode (tested in accparse2.py) any equivalent formula is accepted. * src/twa/acc.cc, src/twa/acc.hh (acc_cond::is_parity): New method. * src/twaalgos/hoa.cc: Use it. * src/tests/hoaparse.test: Test it. * wrap/python/spot_impl.i: Bind it. * wrap/python/tests/accparse2.py: New file. * wrap/python/tests/Makefile.am: Add it. --- src/tests/hoaparse.test | 164 +++++++++++++++++++++++++++++++++ src/twa/acc.cc | 70 ++++++++++++++ src/twa/acc.hh | 7 ++ src/twaalgos/hoa.cc | 10 ++ wrap/python/spot_impl.i | 2 + wrap/python/tests/Makefile.am | 1 + wrap/python/tests/accparse2.py | 33 +++++++ 7 files changed, 287 insertions(+) create mode 100644 wrap/python/tests/accparse2.py diff --git a/src/tests/hoaparse.test b/src/tests/hoaparse.test index 1c44d1574..da4885b58 100755 --- a/src/tests/hoaparse.test +++ b/src/tests/hoaparse.test @@ -1789,6 +1789,54 @@ State: 0 [!0&1] 0 {2} [0&1] 0 {} --END-- +HOA: v1 +States: 1 +Start: 0 +AP: 2 "a" "b" +Acceptance: 4 Inf(0)|Fin(1)&Inf(2) /* min even 4 */ +--BODY-- +State: 0 +[!0&!1] 0 {0 1} +[0&!1] 0 {1} +[!0&1] 0 {2} +[0&1] 0 {} +--END-- +HOA: v1 +States: 1 +Start: 0 +AP: 2 "a" "b" +Acceptance: 4 Inf(3)|Fin(2)&Inf(1) /* max odd 4 */ +--BODY-- +State: 0 +[!0&!1] 0 {0 1} +[0&!1] 0 {1} +[!0&1] 0 {2} +[0&1] 0 {} +--END-- +HOA: v1 +States: 1 +Start: 0 +AP: 2 "a" "b" +Acceptance: 4 Fin(3) & (Inf(2) | (Fin(1) & Inf(0))) /* max even 4 */ +--BODY-- +State: 0 +[!0&!1] 0 {0 1} +[0&!1] 0 {1} +[!0&1] 0 {2} +[0&1] 0 {} +--END-- +HOA: v1 +States: 1 +Start: 0 +AP: 2 "a" "b" +Acceptance: 4 Inf(0) | (Fin(1) & Inf(2)) /* min even 4 (reorderd) */ +--BODY-- +State: 0 +[!0&!1] 0 {0 1} +[0&!1] 0 {1} +[!0&1] 0 {2} +[0&1] 0 {} +--END-- EOF expectok input < r; + for (unsigned i = 0; r.size() < umax; ++i) + if (used.has(i)) + r.push_back(bdd_ithvar(base++)); + else + r.push_back(bddfalse); + return to_bdd_rec(&lhs.back(), &r[0]) == to_bdd_rec(&rhs.back(), &r[0]); + } + } + + bool acc_cond::is_parity(bool& max, bool& odd, bool equiv) const + { + unsigned sets = num_; + if (sets == 0) + { + max = false; + odd = false; + return is_false(); + } + if (is_true()) + return false; + acc_cond::mark_t u_inf; + acc_cond::mark_t u_fin; + std::tie(u_inf, u_fin) = code_.used_inf_fin_sets(); + + odd = !u_inf.has(0); + for (auto s: u_inf.sets()) + if ((s & 1) != odd) + return false; + + auto max_code = acc_code::parity(true, odd, sets); + if (max_code == code_) + { + max = true; + return true; + } + auto min_code = acc_code::parity(false, odd, sets); + if (min_code == code_) + { + max = false; + return true; + } + + if (!equiv) + return false; + + if (equiv_codes(code_, max_code)) + { + max = true; + return true; + } + if (equiv_codes(code_, min_code)) + { + max = false; + return true; + } + return false; } acc_cond::acc_code acc_cond::acc_code::to_dnf() const diff --git a/src/twa/acc.hh b/src/twa/acc.hh index 8d5a85d2c..d31b56496 100644 --- a/src/twa/acc.hh +++ b/src/twa/acc.hh @@ -905,6 +905,13 @@ namespace spot // Return the number of Inf in each pair. bool is_generalized_rabin(std::vector& pairs) const; + // If EQUIV is false, this return true iff the acceptance + // condition is a parity condition written in the canonical way + // given in the HOA specifications. If EQUIV is true, then we + // check whether the condition is logically equivalent to some + // parity acceptance condition. + bool is_parity(bool& max, bool& odd, bool equiv = false) const; + static acc_code generalized_buchi(unsigned n) { mark_t m((1U << n) - 1); diff --git a/src/twaalgos/hoa.cc b/src/twaalgos/hoa.cc index d95216b6b..499bff7dd 100644 --- a/src/twaalgos/hoa.cc +++ b/src/twaalgos/hoa.cc @@ -328,6 +328,16 @@ namespace spot os << ' ' << p; os << nl; } + else + { + bool max = false; + bool odd = false; + if (aut->acc().is_parity(max, odd)) + os << "acc-name: parity " + << (max ? "max " : "min ") + << (odd ? "odd " : "even ") + << num_acc << nl; + } } } } diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 8753acd65..37ea3d80d 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -33,6 +33,7 @@ %include "std_list.i" %include "std_set.i" %include "exception.i" +%include "typemaps.i" // git grep 'typedef.*std::shared_ptr' | grep -v const | // sed 's/.*<\(.*\)>.*/%shared_ptr(spot::\1)/g' @@ -234,6 +235,7 @@ using namespace spot; %include "twa/fwd.hh" %feature("flatnested") spot::acc_cond::mark_t; %feature("flatnested") spot::acc_cond::acc_code; +%apply bool* OUTPUT {bool& max, bool& odd}; %include "twa/acc.hh" %include "twa/twa.hh" diff --git a/wrap/python/tests/Makefile.am b/wrap/python/tests/Makefile.am index 3be352b07..139dd5e6b 100644 --- a/wrap/python/tests/Makefile.am +++ b/wrap/python/tests/Makefile.am @@ -32,6 +32,7 @@ check_SCRIPTS = run TESTS = \ accparse.ipynb \ + accparse2.py \ alarm.py \ automata.ipynb \ automata-io.ipynb \ diff --git a/wrap/python/tests/accparse2.py b/wrap/python/tests/accparse2.py new file mode 100644 index 000000000..9b05c84b8 --- /dev/null +++ b/wrap/python/tests/accparse2.py @@ -0,0 +1,33 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2015 Laboratoire de Recherche et Développement +# de l'Epita +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +import spot + +a = spot.acc_cond(5) +a.set_acceptance(spot.parse_acc_code('parity min odd 5')) +assert(a.is_parity() == [True, False, True]) +a.set_acceptance(spot.parse_acc_code('parity max even 5')) +assert(a.is_parity() == [True, True, False]) +a.set_acceptance(spot.parse_acc_code('generalized-Buchi 5')) +assert(a.is_parity() == [False, False, False]) +assert(a.is_parity(True) == [False, False, False]) +a.set_acceptance(spot.parse_acc_code( + 'Inf(4) | (Fin(3)&Inf(2)) | (Fin(3)&Fin(1)&Inf(0))')) +assert(a.is_parity() == [False, False, False]) +assert(a.is_parity(True) == [True, True, False]) -- GitLab