alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

gfguarantee: fix selection of moved init state

Browse source 
Fixes #357.

* spot/twaalgos/gfguarantee.cc: Decide that a moved init state is to
close from the terminal state *before* actually modifying the
automaton.
* tests/core/ltl2tgba2.test: Add a test.
This commit is contained in:
Alexandre Duret-Lutz 2018-06-30 16:38:56 +02:00
parent 04d05104fa
commit c1b7497f84
2 changed files with 27 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

20
spot/twaalgos/gfguarantee.cc
View file

@ -255,11 +255,22 @@ namespace spot
moved: moved:
continue; 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 // we have successfully played all history
// to a non-terminal state. // to a non-terminal state.
// //
// Combine this edge with any compatible edge from // Combine this edge with any compatible
// the initial state. // edge from the initial state.
first = true; first = true;
for (auto& ei: aut->out(moved_init)) for (auto& ei: aut->out(moved_init))
{ {
@ -272,10 +283,11 @@ namespace spot
// the initial state without any // the initial state without any
// combination. // combination.
bool ts = term[si.scc_of(ei.dst)]; bool ts = term[si.scc_of(ei.dst)];
if (ts && hlen > 0)
goto failed;
if (ts) if (ts)
{
assert(hlen == 0);
want_merge_edges = true; want_merge_edges = true;
}
if (first) if (first)
{ {
e.acc = {0}; e.acc = {0};

10
tests/core/ltl2tgba2.test
View file

@ -378,3 +378,13 @@ ltl2tgba -Fformulas/1 --stats='%f, %s,%t' |
ltl2tgba -BD -F-/1 --stats='%f,%>, %s,%t' > output ltl2tgba -BD -F-/1 --stats='%f,%>, %s,%t' > output
diff formulas 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 <<EOF
3,5,1
4,12,1
EOF
diff out expected