diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc index 2c4ba0336..685507112 100644 --- a/spot/twaalgos/cleanacc.cc +++ b/spot/twaalgos/cleanacc.cc @@ -367,7 +367,7 @@ namespace spot return {}; } - acc_cond::mark_t find_interm_rec(acc_cond::acc_word* pos) + acc_cond::mark_t find_interm_rec(const acc_cond::acc_word* pos) { acc_cond::acc_op wanted; auto topop = pos->sub.op; @@ -489,13 +489,13 @@ namespace spot assert(topop == acc_cond::acc_op::Or); } - // Return a vector of "singleton-sets" of + // Build 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}) + // |Inf({5})|Inf({5,6}) // // This returns [({1}, Inf({1})), // ({5}, Inf({5}))]]. @@ -522,9 +522,8 @@ namespace spot 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},...), + // On Fin(a)&(Fin(b)&Inf(c)|Fin(d)) + // we'd like to build [({a},...), // ({b,d},...)] and decide later that // {b,d} can receive {a} if they // (b and d) are both used once. @@ -556,12 +555,18 @@ namespace spot if (p.first != can_receive && p.first.lowest() == p.first) { - to_fuse.emplace_back(p.first, can_receive); + // Mark fused singletons as false, + // so that a future call to + // find_fusable() ignores them. if (p.second->sub.op == acc_cond::acc_op::Fin) p.second->sub.op = acc_cond::acc_op::Inf; - else + else if (p.second->sub.op == + acc_cond::acc_op::Inf) p.second->sub.op = acc_cond::acc_op::Fin; + else + continue; p.second[-1].mark = {}; + to_fuse.emplace_back(p.first, can_receive); } }; diff --git a/tests/python/simplacc.py b/tests/python/simplacc.py index f2cf59099..af8cb9298 100644 --- a/tests/python/simplacc.py +++ b/tests/python/simplacc.py @@ -38,7 +38,19 @@ explicit-labels trans-acc complete properties: deterministic --BODY-- State: 0 [!0&!1] 0 {2} [0&1] 1 {0 5} [0&!1] 1 {0 2 5} [!0&1] 2 {1} State: 1 [0&1] 1 {0} [!0&!1] 1 {2} [0&!1] 1 {0 2} [!0&1] 2 {1} State: 2 [!0&!1] 0 {2 3} [0&!1] 0 {0 2 3 5} [!0&1] 2 {1 4} [0&1] 3 {0 5} State: 3 [!0&!1] 0 {2 3} [0&!1] 0 {0 2 3 5} -[!0&1] 2 {1 4} [0&1] 3 {0} --END--""")) +[!0&1] 2 {1 4} [0&1] 3 {0} --END-- +/* This one caused an infinite loop in the simplification code. */ +HOA: v1 States: 10 Start: 0 AP: 2 "p0" "p1" Acceptance: 6 (((Fin(4) & +(Fin(3) | (Fin(3) & Inf(1))) & (Inf(0)&Inf(5))) | (Fin(5) & Fin(2))) +& Inf(5)) | Inf(5) | Inf(0) properties: trans-labels explicit-labels +trans-acc --BODY-- State: 0 [!0&!1] 2 [!0&!1] 7 {1} [!0&!1] 6 State: +1 [!0&!1] 5 {1 5} [0&!1] 9 {3} [!0&1] 1 {0} [!0&!1] 4 {0 3} State: 2 +[0&1] 1 {1} State: 3 [!0&1] 8 {4} State: 4 [!0&!1] 0 {5} [!0&1] 3 {4} +State: 5 [!0&1] 4 {3 5} [!0&1] 3 {2 4} [!0&1] 2 {2 3} [!0&!1] 0 {0} +[!0&1] 7 {0 4 5} [0&1] 5 {2} State: 6 [0&!1] 7 [0&!1] 1 {1 4} [0&1] +4 {1 4} State: 7 [0&1] 3 {2 3} [0&1] 0 [!0&!1] 6 [0&1] 1 State: 8 [0&1] +3 [!0&!1] 0 [0&1] 9 State: 9 [0&!1] 7 {4 5} [!0&1] 8 {0} [0&1] 9 --END-- +""")) res = [] for a in auts: @@ -62,4 +74,6 @@ assert res == [ '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(1) | Inf(0)', + 'Fin(1) & Fin(0)', ]