diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index 323a5ad0d..f6b418b17 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -26,7 +26,6 @@ #include #include - #include #include #include @@ -34,7 +33,7 @@ #include #include #include - +#include namespace spot { @@ -448,15 +447,6 @@ namespace spot return res; } - // Used to remove all acceptance whose value is above or equal to max_acc - void remove_dead_acc(twa_graph_ptr& aut, unsigned max_acc) - { - assert(max_acc < 32); - unsigned mask = (1 << max_acc) - 1; - for (auto& t: aut->edges()) - t.acc &= mask; - } - struct compare { bool @@ -961,20 +951,23 @@ namespace spot if (s.color_ != -1U) { res->new_edge(src_num, dst_num, s.cond(), {s.color_}); - // We only care about green acc which are odd - if (s.color_ % 2 == 1) - sets = std::max(s.color_ + 1, sets); + sets = std::max(s.color_ + 1, sets); } else res->new_edge(src_num, dst_num, s.cond()); } } - remove_dead_acc(res, sets); + // Green and red colors work in pairs, so the number of parity conditions is + // necessarily even. + if (sets % 2 == 1) + sets += 1; // Acceptance is now min(odd) since we can emit Red on paths 0 with new opti res->set_acceptance(sets, acc_cond::acc_code::parity(false, true, sets)); res->prop_universal(true); res->prop_state_acc(false); + cleanup_parity_here(res); + if (pretty_print) res->set_named_prop("state-names", print_debug(aut, seen)); return res; diff --git a/tests/core/safra.test b/tests/core/safra.test index 85a304911..c5b2277ff 100755 --- a/tests/core/safra.test +++ b/tests/core/safra.test @@ -45,15 +45,15 @@ HOA: v1 States: 4 Start: 0 AP: 2 "a" "b" -acc-name: Rabin 1 -Acceptance: 2 Fin(0) & Inf(1) +acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc deterministic --BODY-- State: 0 [0] 1 State: 1 [!0&1] 2 -[0] 3 {1} +[0] 3 {0} State: 2 [0&!1] 0 [!0&1] 2 @@ -90,27 +90,27 @@ HOA: v1 States: 5 Start: 0 AP: 2 "a" "b" -acc-name: Rabin 1 -Acceptance: 2 Fin(0) & Inf(1) +acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc deterministic --BODY-- State: 0 [0] 1 State: 1 [0&!1] 1 -[!0&1] 2 {1} +[!0&1] 2 {0} [0&1] 3 State: 2 [0&!1] 0 -[!0&1] 2 {1} +[!0&1] 2 {0} [0&1] 3 State: 3 -[0&1] 1 {1} -[!0&1] 2 {1} +[0&1] 1 {0} +[!0&1] 2 {0} [0&!1] 4 State: 4 -[0] 1 {1} -[!0&1] 2 {1} +[0] 1 {0} +[!0&1] 2 {0} --END-- EOF diff --git a/tests/python/simstate.py b/tests/python/simstate.py index ee014ebbe..e2bf5330e 100644 --- a/tests/python/simstate.py +++ b/tests/python/simstate.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement +# Copyright (C) 2015, 2017-2018 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -70,26 +70,26 @@ assert daut.to_str() == """HOA: v1 States: 3 Start: 0 AP: 2 "p1" "p0" -acc-name: parity min odd 4 -Acceptance: 4 Fin(0) & (Inf(1) | (Fin(2) & Inf(3))) +acc-name: parity min even 3 +Acceptance: 3 Inf(0) | (Fin(1) & Inf(2)) properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 "{₀[0]₀}" [!0&!1] 0 [!0&1] 0 -[0&!1] 0 {1} -[0&1] 1 {3} +[0&!1] 0 {0} +[0&1] 1 {2} State: 1 "{₀[0]{₂[2]₂}₀}{₁[1]₁}" -[!0&!1] 0 {2} +[!0&!1] 0 {1} [!0&1] 2 -[0&!1] 0 {1} -[0&1] 1 {3} +[0&!1] 0 {0} +[0&1] 1 {2} State: 2 "{₀[0]₀}{₁[1]₁}" -[!0&!1] 0 {2} +[!0&!1] 0 {1} [!0&1] 2 -[0&!1] 0 {1} -[0&1] 1 {3} +[0&!1] 0 {0} +[0&1] 1 {2} --END--""" aut = spot.automaton(""" @@ -113,8 +113,8 @@ assert daut.to_str() == """HOA: v1 States: 12 Start: 0 AP: 2 "a" "b" -acc-name: parity min odd 4 -Acceptance: 4 Fin(0) & (Inf(1) | (Fin(2) & Inf(3))) +acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc deterministic --BODY-- State: 0 "{₀[0#0,0#1]₀}" @@ -123,7 +123,7 @@ State: 0 "{₀[0#0,0#1]₀}" [0&1] 2 State: 1 "{₀[1#1]₀}" [!0&1] 0 -[0&!1] 3 {1} +[0&!1] 3 {0} [0&1] 4 State: 2 "{₀[0#0,0#1] [1#1]₀}" [!0&1] 2 @@ -147,24 +147,24 @@ State: 6 "{₀[0#0,0#1] [1#0]₀}" [0&1] 9 State: 7 "{₀[1#1]{₁[0#0,0#1]₁}₀}" [!0&1] 10 -[0&!1] 6 {1} -[0&1] 9 {1} +[0&!1] 6 {0} +[0&1] 9 {0} State: 8 "{₀[1#1]{₁[0#0,0#1] [1#0]₁}₀}" -[!0&1] 2 {1} -[0&!1] 6 {1} -[0&1] 9 {1} +[!0&1] 2 {0} +[0&!1] 6 {0} +[0&1] 9 {0} State: 9 "{₀[0#0,0#1] [1#1] [1#0]₀}" [!0&1] 2 [0&!1] 4 [0&1] 5 State: 10 "{₀[0#0,0#1]{₁[1#1]₁}₀}" [!0&1] 7 -[0&!1] 4 {3} +[0&!1] 4 {0} [0&1] 11 State: 11 "{₀[1#1]{₁[0#0,0#1]{₂[1#0]₂}₁}₀}" -[!0&1] 2 {1} -[0&!1] 6 {1} -[0&1] 9 {1} +[!0&1] 2 {0} +[0&!1] 6 {0} +[0&1] 9 {0} --END--""" a = spot.translate('!Gp0 xor FG((p0 W Gp1) M p1)')