diff --git a/spot/twaalgos/gfguarantee.cc b/spot/twaalgos/gfguarantee.cc index 9d6ab7d98..aa26fb88b 100644 --- a/spot/twaalgos/gfguarantee.cc +++ b/spot/twaalgos/gfguarantee.cc @@ -255,11 +255,22 @@ namespace spot moved: continue; } + + // Make sure no successor of the new initial + // state will reach a terminal state; if + // that is the case, we have to shorten the + // history further. + if (hlen > 0) + for (auto& ei: aut->out(moved_init)) + if ((ei.cond & econd) != bddfalse + && term[si.scc_of(ei.dst)]) + goto failed; + // we have successfully played all history // to a non-terminal state. // - // Combine this edge with any compatible edge from - // the initial state. + // Combine this edge with any compatible + // edge from the initial state. first = true; for (auto& ei: aut->out(moved_init)) { @@ -272,10 +283,11 @@ namespace spot // the initial state without any // combination. bool ts = term[si.scc_of(ei.dst)]; - if (ts && hlen > 0) - goto failed; if (ts) - want_merge_edges = true; + { + assert(hlen == 0); + want_merge_edges = true; + } if (first) { e.acc = {0}; diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index b48c1b448..fcd004f6e 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -378,3 +378,13 @@ ltl2tgba -Fformulas/1 --stats='%f, %s,%t' | ltl2tgba -BD -F-/1 --stats='%f,%>, %s,%t' > output diff formulas output + +# Regression test for issue #357. The second formula used to +# incorrectly produce 13 edges when translated after the first one +# because the transition were explored in a different order. +ltl2tgba -D 'a | Fb' 'GF(d & (!c | XXc))' --stats=%s,%e,%d >out +cat >expected <