From e5a37ff98f38f1d3258ae3af7756165833fa8397 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 6 Nov 2017 17:25:38 +0100 Subject: [PATCH] symplify_acceptance: More rules Fixes #297. Implement the following rules. Fin(i) & Fin(j) by f if i and j are complementary Fin(i) & Inf(i) by f Inf(i) | Inf(j) by t if i and j are complementary Fin(i) | Inf(i) by t. * spot/twaalgos/cleanacc.cc, spot/twaalgos/cleanacc.hh: Here. * tests/python/merge.py: Add more test cases. * NEWS: Mention the change. --- NEWS | 10 +++ spot/twaalgos/cleanacc.cc | 63 +++++++++++----- spot/twaalgos/cleanacc.hh | 30 ++++++-- tests/python/merge.py | 148 ++++++++++++++++++++++++++++++++++++-- 4 files changed, 222 insertions(+), 29 deletions(-) diff --git a/NEWS b/NEWS index 229ac9476..cc33f9857 100644 --- a/NEWS +++ b/NEWS @@ -160,6 +160,16 @@ New in spot 2.4.1.dev (not yet released) conditions. The fmt parameter specify the format to use for that name (e.g. to the style used in HOA, or that used by print_dot()). + - spot::simplify_acceptance() was already merging identical acceptance + sets, and detecting complementary sets i and j to perform the following + simplifications + Fin(i) & Inf(j) = Fin(i) + Fin(i) | Inf(j) = Inf(i) + It now additionally applies the following rules (again assuming i + and j are complementary): + Fin(i) & Fin(j) = f Inf(i) | Inf(j) = t + Fin(i) & Inf(i) = f Fin(i) | Inf(i) = t + Deprecation notices: (These functions still work but compilers emit warnings.) diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc index 2d9233a31..145ff915a 100644 --- a/spot/twaalgos/cleanacc.cc +++ b/spot/twaalgos/cleanacc.cc @@ -174,15 +174,18 @@ namespace spot { auto tmp = remove_compl_rec(pos, complement); - 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) + if (!tmp.empty()) { - inf &= std::move(tmp); - pos -= pos->sub.size + 1; - continue; + 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); @@ -190,8 +193,18 @@ namespace spot } 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()) - inf.front().mark -= complement[m]; + { + 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; } @@ -205,15 +218,18 @@ namespace spot { auto tmp = remove_compl_rec(pos, complement); - 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) + if (!tmp.empty()) { - fin |= std::move(tmp); - pos -= pos->sub.size + 1; - continue; + 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); @@ -221,9 +237,18 @@ namespace spot } 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()) - fin.front().mark -= complement[m]; - + { + 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; } case acc_cond::acc_op::Fin: diff --git a/spot/twaalgos/cleanacc.hh b/spot/twaalgos/cleanacc.hh index d58e01fd0..461dad9d3 100644 --- a/spot/twaalgos/cleanacc.hh +++ b/spot/twaalgos/cleanacc.hh @@ -23,28 +23,48 @@ namespace spot { + /// \ingroup twa_algorithms /// \brief Remove useless acceptance sets /// + /// This removes from the automaton the acceptance marks that are + /// not used in the acceptance condition. This also removes from + /// the acceptance conditions the terms that corresponds to empty + /// or full sets. + /// /// If \a strip is true (the default), the remaining acceptance set /// numbers will be shifted down to reduce maximal number of /// acceptance sets used. SPOT_API twa_graph_ptr cleanup_acceptance_here(twa_graph_ptr aut, bool strip = true); + /// \ingroup twa_algorithms /// \brief Remove useless acceptance sets + /// + /// This removes from the automaton the acceptance marks that are + /// not used in the acceptance condition. This also removes from + /// the acceptance conditions the terms that corresponds to empty + /// or full sets. + /// SPOT_API twa_graph_ptr cleanup_acceptance(const_twa_graph_ptr aut); + /// @{ + /// \ingroup twa_algorithms /// \brief Simplify an acceptance condition /// - /// Remove useless acceptance sets. - /// Merge identical sets. - /// If some sets are complement to each other, might result in the - /// simplification of some clause in the acceptance condition. + /// Does evereything cleanup_acceptance() does, but additionally: + /// merge identical sets, detect whether to sets i and j are + /// complementary to apply the following reductions: + /// - `Fin(i) & Inf(j) = Fin(i)` + /// - `Fin(i) & Fin(j) = f` + /// - `Fin(i) & Inf(i) = f` + /// - `Fin(i) | Inf(j) = Inf(j)` + /// - `Inf(i) | Inf(j) = t` + /// - `Fin(i) | Inf(i) = t` SPOT_API twa_graph_ptr simplify_acceptance_here(twa_graph_ptr aut); - /// \brief Simplify an acceptance condition SPOT_API twa_graph_ptr simplify_acceptance(const_twa_graph_ptr aut); + /// @} } diff --git a/tests/python/merge.py b/tests/python/merge.py index c0601e7bb..5d0997a25 100644 --- a/tests/python/merge.py +++ b/tests/python/merge.py @@ -113,16 +113,88 @@ assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" -Acceptance: 2 (Fin(0) & Inf(0)) | (Fin(1) & Inf(1)) +acc-name: none +Acceptance: 0 f +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 +[0] 1 +State: 1 +[0] 1 +[1] 2 +State: 2 +[1] 0 +--END--""" + +aut = spot.automaton(""" +HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 4 (Inf(0) | Fin(1)) & (Inf(2) | Fin(3)) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 -[0] 1 {0} +[0] 1 {0 1} State: 1 -[0] 1 {1} -[1] 2 {0 1} +[0] 1 {2 3} +[1] 2 {0 1 3} State: 2 -[1] 0 {1} +[1] 0 {2 3} +--END--""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') + +assert hoa == """HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 2 Fin(1) | Inf(0) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0] 1 +State: 1 +[0] 1 {0 1} +[1] 2 {1} +State: 2 +[1] 0 {0 1} +--END--""" + +aut = spot.automaton(""" +HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 4 (Inf(0) | Fin(1)) & (Inf(2) | Fin(3)) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0] 1 {0 1} +State: 1 +[0] 1 {2 3} +[1] 2 {0 1 2 3} +State: 2 +[1] 0 {2 3} +--END--""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') + +assert hoa == """HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 +[0] 1 +State: 1 +[0] 1 +[1] 2 +State: 2 +[1] 0 --END--""" aut = spot.automaton("""HOA: v1 @@ -645,3 +717,69 @@ State: 1 [0] 1 [!0] 0 --END--""" + +aut = spot.automaton("""HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 4 Fin(0) & Fin(1) & Inf(2) +--BODY-- +State: 0 +[0] 1 {0} +State: 1 +[0] 1 {1 2} +[1] 2 {0 2} +State: 2 +[1] 0 {1} +--END--""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') +assert hoa == """HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +acc-name: none +Acceptance: 0 f +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 +[0] 1 +State: 1 +[0] 1 +[1] 2 +State: 2 +[1] 0 +--END--""" + +aut = spot.automaton("""HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 4 Inf(0) | Inf(1) | Inf(2) +--BODY-- +State: 0 +[0] 1 {0} +State: 1 +[0] 1 {1 2} +[1] 2 {0 2} +State: 2 +[1] 0 {1} +--END--""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') +assert hoa == """HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 +[0] 1 +State: 1 +[0] 1 +[1] 2 +State: 2 +[1] 0 +--END--"""