From c0e1b3e52a68dc660e564a2a9cc6885ba0c6693a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 18 Apr 2020 22:05:43 +0200 Subject: [PATCH] cleanacc: keep acceptance order when removing complementary colors * spot/twaalgos/cleanacc.cc (remove_compl_rec): Rewrite to preserve the original order of the acceptance condition while rewriting it. * tests/core/sccdot.test, tests/python/merge.py, tests/python/simplacc.py, tests/python/toparity.py: Adjust test cases. --- spot/twaalgos/cleanacc.cc | 170 +++++++++++++++++++------------------- tests/core/sccdot.test | 4 +- tests/python/merge.py | 11 ++- tests/python/simplacc.py | 27 +++--- tests/python/toparity.py | 5 +- 5 files changed, 109 insertions(+), 108 deletions(-) diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc index 87a42917c..ff663596a 100644 --- a/spot/twaalgos/cleanacc.cc +++ b/spot/twaalgos/cleanacc.cc @@ -157,101 +157,99 @@ namespace spot return aut; } - // Eventually remove complementary marks from the acceptance condition. + // Remove complementary marks from the acceptance condition. acc_cond::acc_code remove_compl_rec(const acc_cond::acc_word* pos, const std::vector& complement) { auto start = pos - pos->sub.size; + auto boolop = + [&](acc_cond::acc_op opand, acc_cond::acc_op opfin, + acc_cond::acc_op opinf, + acc_cond::acc_code&& truecode, + acc_cond::acc_code&& falsecode) + { + --pos; + acc_cond::acc_code res = truecode; + acc_cond::mark_t seen_fin = {}; + do + { + auto tmp = remove_compl_rec(pos, complement); + + if (!tmp.empty() && (tmp.back().sub.op == opfin + && tmp.front().mark.count() == 1)) + seen_fin |= tmp.front().mark; + + if (opand == acc_cond::acc_op::And) + tmp &= std::move(res); + else + tmp |= std::move(res); + std::swap(tmp, res); + pos -= pos->sub.size + 1; + } + while (pos > start); + if (res.empty() || res.back().sub.op != opand) + return res; + // Locate the position of any Inf element. + // A property of the &= operator is that there + // is only one Inf in a conjunction. + auto rbegin = &res.back(); + auto rend = rbegin - rbegin->sub.size; + --rbegin; + do + { + if (rbegin->sub.op == opinf) + break; + rbegin -= rbegin->sub.size + 1; + } + while (rbegin > rend); + if (rbegin <= rend) + return res; + // Fin(i) & Inf(i) = f; + if (rbegin[-1].mark & seen_fin) + return std::move(falsecode); + for (auto m: seen_fin.sets()) + { + acc_cond::mark_t cm = complement[m]; + // Fin(i) & Fin(!i) = f; + if (cm & seen_fin) + return std::move(falsecode); + // Inf({!i}) & Fin({i}) = Fin({i}) + rbegin[-1].mark -= complement[m]; + } + if (rbegin[-1].mark) + return res; + // Inf(i) has been rewritten as t, we need to remove it. Sigh! + acc_cond::acc_code res2 = std::move(truecode); + rbegin = &res.back() - 1; + do + { + acc_cond::acc_code tmp(rbegin); + if (opand == acc_cond::acc_op::And) + tmp &= std::move(res); + else + tmp |= std::move(res); + std::swap(tmp, res2); + rbegin -= rbegin->sub.size + 1; + } + while (rbegin > rend); + return res2; + }; + switch (pos->sub.op) { case acc_cond::acc_op::And: - { - --pos; - auto res = acc_cond::acc_code::t(); - acc_cond::mark_t seen_fin = {}; - auto inf = acc_cond::acc_code::inf({}); - do - { - auto tmp = remove_compl_rec(pos, complement); - - if (!tmp.empty()) - { - if (tmp.back().sub.op == acc_cond::acc_op::Fin - && tmp.front().mark.count() == 1) - seen_fin |= tmp.front().mark; - - if (tmp.back().sub.op == acc_cond::acc_op::Inf) - { - inf &= std::move(tmp); - pos -= pos->sub.size + 1; - continue; - } - } - tmp &= std::move(res); - std::swap(tmp, res); - pos -= pos->sub.size + 1; - } - while (pos > start); - - // Fin(i) & Inf(i) = f; - if (inf.front().mark & seen_fin) - return acc_cond::acc_code::f(); - for (auto m: seen_fin.sets()) - { - acc_cond::mark_t cm = complement[m]; - // Fin(i) & Fin(!i) = f; - if (cm & seen_fin) - return acc_cond::acc_code::f(); - // Inf({!i}) & Fin({i}) = Fin({i}) - inf.front().mark -= complement[m]; - } - - return inf & res; - } + return boolop(acc_cond::acc_op::And, + acc_cond::acc_op::Fin, + acc_cond::acc_op::Inf, + acc_cond::acc_code::t(), + acc_cond::acc_code::f()); case acc_cond::acc_op::Or: - { - --pos; - auto res = acc_cond::acc_code::f(); - acc_cond::mark_t seen_inf = {}; - auto fin = acc_cond::acc_code::f(); - do - { - auto tmp = remove_compl_rec(pos, complement); - - if (!tmp.empty()) - { - if (tmp.back().sub.op == acc_cond::acc_op::Inf - && tmp.front().mark.count() == 1) - seen_inf |= tmp.front().mark; - - if (tmp.back().sub.op == acc_cond::acc_op::Fin) - { - fin |= std::move(tmp); - pos -= pos->sub.size + 1; - continue; - } - } - tmp |= std::move(res); - std::swap(tmp, res); - pos -= pos->sub.size + 1; - } - while (pos > start); - - // Fin(i) | Inf(i) = t; - if (fin.front().mark & seen_inf) - return acc_cond::acc_code::t(); - for (auto m: seen_inf.sets()) - { - acc_cond::mark_t cm = complement[m]; - // Inf({i}) | Inf({!i}) = t; - if (cm & seen_inf) - return acc_cond::acc_code::t(); - // Fin({!i}) | Inf({i}) = Inf({i}) - fin.front().mark -= complement[m]; - } - return res | fin; - } + return boolop(acc_cond::acc_op::Or, + acc_cond::acc_op::Inf, + acc_cond::acc_op::Fin, + acc_cond::acc_code::f(), + acc_cond::acc_code::t()); case acc_cond::acc_op::Fin: return acc_cond::acc_code::fin(pos[-1].mark); case acc_cond::acc_op::Inf: diff --git a/tests/core/sccdot.test b/tests/core/sccdot.test index 03fb2318a..69c75e8d6 100755 --- a/tests/core/sccdot.test +++ b/tests/core/sccdot.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2017, 2018 Laboratoire de Recherche et +# Copyright (C) 2015, 2017, 2018, 2020 Laboratoire de Recherche et # Développement de l'Epita # # This file is part of Spot, a model checking library. @@ -156,7 +156,7 @@ HOA: v1 States: 8 Start: 0 AP: 2 "a" "b" -Acceptance: 3 Fin(2) & (Inf(0)&Inf(1)) +Acceptance: 3 (Inf(0)&Inf(1)) & Fin(2) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 diff --git a/tests/python/merge.py b/tests/python/merge.py index 7fa888859..c69ec4028 100644 --- a/tests/python/merge.py +++ b/tests/python/merge.py @@ -43,7 +43,8 @@ assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" -Acceptance: 2 Fin(1) | Inf(0) +acc-name: parity min even 2 +Acceptance: 2 Inf(0) | Fin(1) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 @@ -78,7 +79,8 @@ assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" -Acceptance: 2 Fin(1) | Inf(0) +acc-name: parity min even 2 +Acceptance: 2 Inf(0) | Fin(1) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 @@ -149,7 +151,8 @@ assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" -Acceptance: 2 Fin(1) | Inf(0) +acc-name: parity min even 2 +Acceptance: 2 Inf(0) | Fin(1) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 @@ -289,7 +292,7 @@ assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" -Acceptance: 2 (Fin(1) & Inf(0)) | (Fin(1) & Inf(0)) +Acceptance: 2 (Inf(0) & Fin(1)) | (Inf(0) & Fin(1)) properties: trans-labels explicit-labels state-acc --BODY-- State: 0 {0} diff --git a/tests/python/simplacc.py b/tests/python/simplacc.py index 024bccd56..e4e902dbd 100644 --- a/tests/python/simplacc.py +++ b/tests/python/simplacc.py @@ -67,18 +67,17 @@ for a in auts: c = spot.simplify_acceptance(b) assert b.get_acceptance() == c.get_acceptance() - assert res == [ - 'Inf(0)', - 'Fin(0)', - 'Fin(0) & Inf(1)', - 'Fin(1) | Inf(0)', - '(Fin(0) | Inf(2)) & Inf(1)', - 'Fin(1) | (Fin(2) & Inf(0))', - '(Fin(1) | Inf(2)) & Inf(0)', - 'Fin(0) | (Fin(2) & Inf(1))', - '((Fin(1) | Inf(2)) & Inf(5)) | (Fin(0) & (Fin(1) | (Fin(3) & Inf(4))))', - '(Fin(5) | (Fin(2) & Inf(1))) & (Inf(0) | ((Fin(4) | Inf(3)) & Inf(1)))', - 'Inf(0)', - 'Fin(0)', - ] + 'Inf(0)', + 'Fin(0)', + 'Inf(1) & Fin(0)', + 'Fin(1) | Inf(0)', + 'Inf(1) & (Fin(0) | Inf(2))', + 'Fin(1) | (Inf(0) & Fin(2))', + 'Inf(0) & (Inf(2) | Fin(1))', + 'Fin(0) | (Fin(2) & Inf(1))', + '((Fin(1) | Inf(2)) & Inf(5)) | (Fin(0) & (Fin(1) | (Fin(3) & Inf(4))))', + '((Inf(1) & Fin(2)) | Fin(5)) & (Inf(0) | (Inf(1) & (Inf(3) | Fin(4))))', + 'Inf(0)', + 'Fin(0)', + ] diff --git a/tests/python/toparity.py b/tests/python/toparity.py index c3b193be8..091292ffb 100644 --- a/tests/python/toparity.py +++ b/tests/python/toparity.py @@ -112,7 +112,8 @@ def test(aut, expected_num_states=[], full=True): spot.reduce_parity_here(p1) assert spot.are_equivalent(aut, p1) if expected_num is not None: - assert p1.num_states() == expected_num + # print(p1.num_states(), expected_num) + assert p1.num_states() == expected_num if full: # Make sure passing opt is the same as setting # each argument individually @@ -292,7 +293,7 @@ State: 4 [0&!1] 4 [0&1] 4 {1 2 4} --END-- -"""), [9, 6, 6, 6, 7, 6, 6]) +"""), [9, 6, 7, 7, 6, 6, 6]) test(spot.automaton(""" HOA: v1