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

ltl-split: deal with suspendable formulas that are false

Browse source 
Fixes #358.

* spot/twaalgos/translate.cc: Fix the assert().
* tests/core/ltl2tgba2.test: Add a test case.
This commit is contained in:
Alexandre Duret-Lutz 2018-06-30 20:39:30 +02:00
parent d82419de1a
commit e48c6c40d0
2 changed files with 10 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

10
spot/twaalgos/translate.cc
View file

@ -266,8 +266,14 @@ namespace spot
scc_info si(susp_aut, scc_info_options::NONE);
if (si.is_trivial(si.scc_of(susp_aut->get_init_state_number())))
{
assert(!si.is_trivial(0));
susp_aut->set_init_state(si.one_state_of(0));
unsigned st = si.one_state_of(0);
// The bottom SCC can actually be trivial if it
// has no successor because the formula is
// equivalent to false.
assert(!si.is_trivial(0) ||
susp_aut->out(st).begin()
== susp_aut->out(st).end());
susp_aut->set_init_state(st);
susp_aut->purge_unreachable_states();
}
}

2
tests/core/ltl2tgba2.test
View file

@ -364,12 +364,14 @@ diff output expected
# The first four formulas appear in a NEWS entry for Spot 2.6
# The 5th one is from issue #267.
# The 6th one is from issue #358.
cat >formulas <<EOF
GF((a & XXa) | (!a & XX!a)), 4,8, 4,8, 6,14, 7,14
GF((a & XXXa) | (!a & XXX!a)), 7,14, 8,16, 8,18, 15,30
GF(((a & Xb) | XXc) & Xd), 4,64, 4,64, 5,80, 5,80
GF((b | Fa) & (b R Xb)), 2,4, 2,4, 3,6, 3,12
G(F(a & Xa) & F(a & X!a)), 2,4, 2,4, 4,8, 4,8
G(!p0 & F(p1 & XG!p1)), 1,0, 1,0, 1,0, 1,0
EOF
ltl2tgba -Fformulas/1 --stats='%f, %s,%t' |