From 50c0f880dc9987a7ae5f590ac7d5be57bb3d1338 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 27 Jan 2020 22:50:17 +0100 Subject: [PATCH] Inf(i)|Inf(j) -> Inf(k) and Fin(i)&Fin(j) -> Fin(k) Implement those rules in simplify_acceptance_here(). * NEWS: Mention the change. * spot/twa/acc.cc, spot/twa/acc.hh (acc_cond::acc_code::used_once_sets): New method. * spot/twaalgos/cleanacc.cc, spot/twaalgos/cleanacc.hh: Implement the above rule. * tests/core/remfin.test: Adjust expected results. * tests/python/simplacc.py: New file. * tests/Makefile.am: Add it. --- NEWS | 7 + spot/twa/acc.cc | 33 ++++- spot/twa/acc.hh | 12 +- spot/twaalgos/cleanacc.cc | 294 +++++++++++++++++++++++++++++++++++++- spot/twaalgos/cleanacc.hh | 7 +- tests/Makefile.am | 4 +- tests/core/remfin.test | 28 ++-- tests/python/simplacc.py | 54 +++++++ 8 files changed, 416 insertions(+), 23 deletions(-) create mode 100644 tests/python/simplacc.py diff --git a/NEWS b/NEWS index 975da9cad..67278dc05 100644 --- a/NEWS +++ b/NEWS @@ -61,6 +61,13 @@ New in spot 2.8.5.dev (not yet released) degeneralization to get rid of conjunction of Inf terms in acceptance conditions. + - simplify_acceptance_here() and simplify_acceptance() learned to + simplify subformulas like Fin(i)&Fin(j) or Inf(i)|Inf(j), or some + more complex variants of those. If i us uniquely used in the + acceptance condition these become respectively Fin(i) or Inf(i), + and the automaton is adjusted to that i also appears where j + appeared. + New in spot 2.8.5 (2020-01-04) Bugs fixed: diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index a564c4968..3ef185403 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2020 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -2340,6 +2340,7 @@ namespace spot std::swap(c, *this); } + int acc_cond::acc_code::fin_one() const { if (empty() || is_f()) @@ -2398,4 +2399,34 @@ namespace spot while (pos >= &front()); return res; } + + acc_cond::mark_t acc_cond::acc_code::used_once_sets() const + { + mark_t seen = {}; + mark_t dups = {}; + if (empty()) + return {}; + const acc_cond::acc_word* pos = &back(); + do + { + switch (pos->sub.op) + { + case acc_cond::acc_op::And: + case acc_cond::acc_op::Or: + --pos; + break; + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::InfNeg: + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::Fin: + auto m = pos[-1].mark; + pos -= 2; + dups |= m & seen; + seen |= m; + break; + } + } + while (pos >= &front()); + return seen - dups; + } } diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 6192e9dba..10513ac87 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -1199,7 +1199,7 @@ namespace spot /// /// If multiple unit-Fin appear as unit-clauses, the set of /// those will be returned. For instance applied to - /// `Fin(0)&Fin(1)&(Inf(2)|Fin(3))``, this will return `{0,1}`. + /// `Fin(0)&Fin(1)&(Inf(2)|Fin(3))`, this will return `{0,1}`. mark_t fin_unit() const; /// \brief Return one acceptance set i that appear as `Fin(i)` @@ -1286,6 +1286,14 @@ namespace spot /// \brief Return the set of sets appearing in the condition. acc_cond::mark_t used_sets() const; + /// \brief Return the sets that appears only once in the + /// acceptance. + /// + /// For instance if the condition is + /// `Fin(0)&(Inf(1)|(Fin(1)&Inf(2)))`, this returns `{0,2}`, + /// because set `1` is used more than once. + mark_t used_once_sets() const; + /// \brief Return the sets used as Inf or Fin in the acceptance condition std::pair used_inf_fin_sets() const; diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc index c36175a20..2c4d76d93 100644 --- a/spot/twaalgos/cleanacc.cc +++ b/spot/twaalgos/cleanacc.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2017-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2015, 2017-2020 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -320,6 +320,292 @@ namespace spot complement)); return aut; } + + + acc_cond::acc_code acc_rewrite_rec(const acc_cond::acc_word* pos) + { + auto start = pos - pos->sub.size; + switch (pos->sub.op) + { + case acc_cond::acc_op::And: + { + --pos; + auto res = acc_cond::acc_code::t(); + do + { + auto tmp = acc_rewrite_rec(pos); + tmp &= std::move(res); + std::swap(tmp, res); + pos -= pos->sub.size + 1; + } + while (pos > start); + return res; + } + case acc_cond::acc_op::Or: + { + --pos; + auto res = acc_cond::acc_code::f(); + do + { + auto tmp = acc_rewrite_rec(pos); + tmp |= std::move(res); + std::swap(tmp, res); + pos -= pos->sub.size + 1; + } + while (pos > start); + return res; + } + case acc_cond::acc_op::Fin: + return acc_cond::acc_code::fin(pos[-1].mark); + case acc_cond::acc_op::Inf: + return acc_cond::acc_code::inf(pos[-1].mark); + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::InfNeg: + SPOT_UNREACHABLE(); + }; + SPOT_UNREACHABLE(); + return {}; + } + + acc_cond::mark_t find_interm_rec(acc_cond::acc_word* pos) + { + acc_cond::acc_op wanted; + auto topop = pos->sub.op; + if (topop == acc_cond::acc_op::Or) + { + wanted = acc_cond::acc_op::Fin; + } + else + { + wanted = acc_cond::acc_op::Inf; + assert(topop == acc_cond::acc_op::And); + } + acc_cond::mark_t res = {}; + const acc_cond::acc_word* rend = pos - (pos->sub.size + 1); + --pos; + do + switch (auto op = pos->sub.op) + { + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::InfNeg: + case acc_cond::acc_op::FinNeg: + { + auto m = pos[-1].mark; + if (op == wanted && m == m.lowest()) + { + res |= m; + } + else + { + return {}; + } + pos -= 2; + break; + } + case acc_cond::acc_op::And: + case acc_cond::acc_op::Or: + if (op == topop) + { + if (auto m = find_interm_rec(pos)) + res |= m; + else + return {}; + pos -= pos->sub.size + 1; + } + else + { + auto posend = pos - (pos->sub.size + 1); + --pos; + bool seen = false; + do + { + switch (auto op = pos->sub.op) + { + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::InfNeg: + case acc_cond::acc_op::FinNeg: + if (op == wanted) + { + auto m = pos[-1].mark; + if (!seen && m == m.lowest()) + { + seen = true; + res |= m; + } + else + { + return {}; + } + } + pos -= 2; + break; + case acc_cond::acc_op::And: + case acc_cond::acc_op::Or: + return {}; + } + } + while (pos > posend); + } + break; + } + while (pos > rend); + return res; + } + + // Replace Inf(i)|Inf(j) by Inf(k) + // or Fin(i)&Fin(j) by Fin(k) + // For this to work, k must be one of i or j, + // k must be used only once in the acceptance + // the transitions have to be updated: every transition marked + // by i or j should be marked by k. + void fuse_marks_here(twa_graph_ptr aut) + { + acc_cond::acc_code acccopy = aut->get_acceptance(); + acc_cond::mark_t once = acccopy.used_once_sets(); + if (!once) + return; + + acc_cond::acc_word* pos = &acccopy.back(); + const acc_cond::acc_word* front = &acccopy.front(); + + // a list of pairs ({i}, {j, k, l, ...}) where i is a set + // occurring once that can be removed if all transitions in set + // i are added to sets j,k,l, ... + std::vector> to_fuse; + + auto find_fusable = [&](acc_cond::acc_word* pos) + { + acc_cond::acc_op wanted; + auto topop = pos->sub.op; + if (topop == acc_cond::acc_op::And) + { + wanted = acc_cond::acc_op::Fin; + } + else + { + wanted = acc_cond::acc_op::Inf; + assert(topop == acc_cond::acc_op::Or); + } + + // Return a vector of "singleton-sets" of + // the wanted type in the operand of the + // pointed Or/And operator. For instance, + // assuming wanted=Inf and pos points to + // + // Inf({1})|Inf({2,3})|Fin({4}) + // |Inf({5})|Inf({5})|Inf({6}) + // + // This returns [({1}, Inf({1})), + // ({5}, Inf({5}))]]. + std::vector> + singletons; + const acc_cond::acc_word* rend = + pos - (pos->sub.size + 1); + --pos; + do + { + switch (auto op = pos->sub.op) + { + case acc_cond::acc_op::InfNeg: + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::Fin: + { + auto m = pos[-1].mark; + if (op == wanted && m == m.lowest()) + singletons.emplace_back(m, pos); + pos -= 2; + } + break; + case acc_cond::acc_op::And: + case acc_cond::acc_op::Or: + // On + // Fin(a)&(Fin(b)&Inf(c)|Fin(d)) + // where we'd like to return [{a}, + // {b,d}] and decide later that + // {b,d} can receive {a} if they + // (b and d) are both used once. + if (auto m = find_interm_rec(pos)) + { + singletons.emplace_back(m, pos); + // move this to the front, to + // be sure it is the first + // recipient tried. + swap(singletons.front(), + singletons.back()); + } + pos -= pos->sub.size + 1; + break; + } + } + while (pos > rend); + + acc_cond::mark_t can_receive = {}; + for (auto p: singletons) + if ((p.first & once) == p.first) + { + can_receive = p.first; + break; + } + if (!can_receive) + return; + for (auto p: singletons) + if (p.first != can_receive) + { + to_fuse.emplace_back(p.first, can_receive); + if (p.second->sub.op == acc_cond::acc_op::Fin) + p.second->sub.op = acc_cond::acc_op::Inf; + else + p.second->sub.op = acc_cond::acc_op::Fin; + p.second[-1].mark = {}; + } + }; + + do + { + switch (pos->sub.op) + { + case acc_cond::acc_op::And: + case acc_cond::acc_op::Or: + find_fusable(pos); + // Don't skip to entire operands, as we might find + // fusable sub-parts. + --pos; + break; + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::InfNeg: + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::Fin: + pos -= 2; + break; + } + } + while (pos >= front); + + if (to_fuse.empty()) + return; + + // Update the transition according to to_fuse. + for (auto pair: to_fuse) + if (pair.first & once) // can we remove pair.first? + { + for (auto& e: aut->edges()) + if (e.acc & pair.first) + e.acc = (e.acc - pair.first) | pair.second; + } + else + { + for (auto& e: aut->edges()) + if (e.acc & pair.first) + e.acc |= pair.second; + } + + // Now rewrite the acceptance condition, removing all the "to_kill" terms. + aut->set_acceptance(aut->num_sets(), acc_rewrite_rec(&acccopy.back())); + } } twa_graph_ptr simplify_acceptance_here(twa_graph_ptr aut) @@ -327,9 +613,11 @@ namespace spot cleanup_acceptance_here(aut, false); merge_identical_marks_here(aut); if (!aut->acc().is_generalized_buchi()) - simplify_complementary_marks_here(aut); + { + simplify_complementary_marks_here(aut); + fuse_marks_here(aut); + } cleanup_acceptance_here(aut, true); - return aut; } diff --git a/spot/twaalgos/cleanacc.hh b/spot/twaalgos/cleanacc.hh index 2200cc186..de637c63b 100644 --- a/spot/twaalgos/cleanacc.hh +++ b/spot/twaalgos/cleanacc.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2017-2019 Laboratoire de Recherche et +// Copyright (C) 2015, 2017-2020 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -57,6 +57,11 @@ namespace spot /// - `Fin(i) | Inf(j) = Inf(j)` /// - `Inf(i) | Inf(j) = t` /// - `Fin(i) | Inf(i) = t` + /// And also merge terms like `Inf(i)|Inf(j)` or `Fin(i)&Fin(j)` + /// provided at least i or j is used uniquely in the formula. + /// (for instance if i is unique, `Inf(i)|Inf(j)` is rewritten + /// as `Inf(i)`, and `i` is added on all transitions where `j` is present + /// in the automaton.) /// /// simplify_acceptance_here() works in place, simplify_acceptance() /// returns a new automaton that has been simplified. diff --git a/tests/Makefile.am b/tests/Makefile.am index 26d5f1b46..a577c76ec 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -1,6 +1,5 @@ ## -*- coding: utf-8 -*- - -## Copyright (C) 2009-2019 Laboratoire de Recherche et Développement +## Copyright (C) 2009-2020 Laboratoire de Recherche et Développement ## de l'Epita (LRDE). ## Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6 ## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -410,6 +409,7 @@ TESTS_python = \ python/semidet.py \ python/setacc.py \ python/setxor.py \ + python/simplacc.py \ python/simstate.py \ python/split.py \ python/streett_totgba.py \ diff --git a/tests/core/remfin.test b/tests/core/remfin.test index c3835d294..c50272339 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -1,8 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- - -# Copyright (C) 2015-2018 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2015-2018, 2020 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -340,7 +339,7 @@ HOA: v1 States: 4 Start: 0 AP: 2 "a" "b" -Acceptance: 5 (Inf(0)&Inf(1)&Inf(4)) | Inf(0) | (Inf(2)&Inf(3)) +Acceptance: 4 (Inf(0)&Inf(1)) | Inf(0) | (Inf(2)&Inf(3)) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 @@ -357,7 +356,7 @@ State: 2 [!0&!1] 2 {0} [!0&!1] 3 State: 3 -[!0&!1] 3 {0 1 4} +[!0&!1] 3 {0 1} --END-- HOA: v1 States: 1 @@ -402,7 +401,8 @@ HOA: v1 States: 10 Start: 2 AP: 1 "p1" -Acceptance: 2 Inf(1) | Inf(0) +acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc --BODY-- State: 0 @@ -410,29 +410,29 @@ State: 0 [!0] 6 [0] 8 [0] 9 -State: 1 {0 1} +State: 1 [t] 3 -State: 2 {0 1} +State: 2 [0] 1 [!0] 5 -State: 3 {0 1} +State: 3 [0] 0 [!0] 6 -State: 4 {0 1} +State: 4 {0} [0] 4 [!0] 6 -State: 5 {0 1} +State: 5 [0] 3 [!0] 7 State: 6 [0] 0 [!0] 6 -State: 7 {1} +State: 7 [0] 4 [!0] 6 State: 8 [0] 8 -State: 9 {1} +State: 9 {0} [0] 9 --END-- HOA: v1 @@ -765,7 +765,7 @@ acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc --BODY-- -State: 0 {0} +State: 0 [!0&1] 5 [!0&1] 7 State: 1 diff --git a/tests/python/simplacc.py b/tests/python/simplacc.py new file mode 100644 index 000000000..064ff9fbf --- /dev/null +++ b/tests/python/simplacc.py @@ -0,0 +1,54 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). +# +# 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 + + +auts = list(spot.automata(""" +HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" Acceptance: 2 Inf(0) | Inf(1) --BODY-- +State: 0 [1] 0 [0] 1 {0} State: 1 [0] 1 [1] 0 {1} --END-- +HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" Acceptance: 2 (Inf(0) | Inf(1)) & +Fin(0) --BODY-- State: 0 [1] 0 [0] 1 {0} State: 1 [0] 1 [1] 0 {1} --END-- +HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" Acceptance: 3 (Inf(0) | Inf(1)) & +(Fin(0) | Inf(2)) --BODY-- State: 0 [1] 0 [0] 1 {0} State: 1 [0] 1 {2} [1] 0 +{1} --END-- +HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" Acceptance: 4 (Inf(0) | +(Inf(1)&(Inf(3)|Fin(2)))) --BODY-- State: 0 [1] 0 {3} [0] 1 {0} State: 1 [0] 1 +{2} [1] 0 {1} --END-- +""")) + +res = [] +for a in auts: + b = spot.simplify_acceptance(a) + assert b.equivalent_to(a) + res.append(str(b.get_acceptance())) + + a.set_acceptance(a.num_sets(), a.get_acceptance().complement()) + b = spot.simplify_acceptance(a) + assert b.equivalent_to(a) + res.append(str(b.get_acceptance())) + +assert res == ['Inf(0)', + 'Fin(0)', + 'Inf(1) & Fin(0)', + 'Fin(1) | Inf(0)', + 'Inf(1) & (Fin(0) | Inf(2))', + 'Fin(1) | (Fin(2) & Inf(0))', + '(Fin(1) | Inf(2)) & Inf(0)', + 'Fin(0) | (Fin(2) & Inf(1))']