Commit 04171207 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 704eaf26
......@@ -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 <<EOF
......@@ -1853,6 +1901,66 @@ State: 0
[!0&1] 0 {2}
[0&1] 0
--END--
HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
acc-name: parity min even 4
Acceptance: 4 Inf(0) | (Fin(1) & Inf(2))
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--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"
acc-name: parity max odd 4
Acceptance: 4 Inf(3) | (Fin(2) & Inf(1))
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--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"
acc-name: parity max even 4
Acceptance: 4 Fin(3) & (Inf(2) | (Fin(1) & Inf(0)))
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--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"
acc-name: parity min even 4
Acceptance: 4 Inf(0) | (Fin(1) & Inf(2))
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[!0&!1] 0 {0 1}
[0&!1] 0 {1}
[!0&1] 0 {2}
[0&1] 0
--END--
EOF
# The complements are Streett and Rabin, but the acceptance set are
......@@ -1917,4 +2025,60 @@ State: 0
[!0&1] 0 {2}
[0&1] 0
--END--
HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
Acceptance: 4 Fin(0) & (Inf(1) | Fin(2))
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--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))
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--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) | Fin(0)))
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--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(0) & (Inf(1) | Fin(2))
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[!0&!1] 0 {0 1}
[0&!1] 0 {1}
[!0&1] 0 {2}
[0&1] 0
--END--
EOF
......@@ -526,6 +526,76 @@ namespace spot
SPOT_UNREACHABLE();
return bddfalse;
}
static bool
equiv_codes(const acc_cond::acc_code& lhs,
const acc_cond::acc_code& rhs)
{
auto used = lhs.used_sets() | rhs.used_sets();
unsigned c = used.count();
unsigned umax = used.max_set();
bdd_allocator ba;
int base = ba.allocate_variables(c);
assert(base == 0);
std::vector<bdd> 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
......
......@@ -905,6 +905,13 @@ namespace spot
// Return the number of Inf in each pair.
bool is_generalized_rabin(std::vector<unsigned>& 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);
......
......@@ -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;
}
}
}
}
......
......@@ -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"
......
......@@ -32,6 +32,7 @@ check_SCRIPTS = run
TESTS = \
accparse.ipynb \
accparse2.py \
alarm.py \
automata.ipynb \
automata-io.ipynb \
......
# -*- 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 <http://www.gnu.org/licenses/>.
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])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment