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

* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Clone and then

Browse source 
free all formulae entered into canonical_succ, to avoid errors
when a formula is entered into canonical_succ but not into
formulae_seen.
* src/tgbatest/ltl2tgba.test: Add a new test, and check with -f.
Report from Thomas Martinez.
This commit is contained in:
Alexandre Duret-Lutz 2004-05-03 16:41:00 +00:00
parent 22912b6db7
commit ca80561ad5
3 changed files with 42 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

9
ChangeLog
View file

@ -1,3 +1,12 @@
2004-05-03 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Clone and then
free all formulae entered into canonical_succ, to avoid errors
when a formula is entered into canonical_succ but not into
formulae_seen.
* src/tgbatest/ltl2tgba.test: Add a new test, and check with -f.
Report from Thomas Martinez.
2004-04-23 Alexandre Duret-Lutz <adl@src.lip6.fr>
* configure.ac, NEWS: Bump version to 0.0u.

19
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -431,9 +431,14 @@ namespace spot
formulae_to_translate.erase(formulae_to_translate.begin());
// Translate it into a BDD to simplify it.
// FIXME: Currently the same formula can be converted into a
// BDD twice. Once in the symb_merge block below, and then
// once here.
f->accept(v);
bdd res = v.result();
canonical_succ[res] = f;
succ_to_formula::iterator cs = canonical_succ.find(res);
if (cs == canonical_succ.end())
canonical_succ[res] = clone(f);
std::string now = to_string(f);
@ -514,7 +519,7 @@ namespace spot
}
else
{
canonical_succ[succbdd] = dest;
canonical_succ[succbdd] = clone(dest);
}
}
@ -539,9 +544,10 @@ namespace spot
// way it will be explored before the other during the model
// checking.
dest_map::const_iterator i = dests.find(constant::true_instance());
// conditions of the True arc, so when can remove them from
// all other arcs. It might sounds that this is not needed
// when exprop is used, but it fact it is complementary.
// COND_FOR_TRUE is the conditions of the True arc, so when
// can remove them from all other arcs. It might sounds that
// this is not needed when exprop is used, but in fact it is
// complementary.
//
// Consider
// f = r(X(1) R p) = p.(1 + r(X(1) R p))
@ -615,6 +621,9 @@ namespace spot
for (std::set<const formula*>::iterator i = formulae_seen.begin();
i != formulae_seen.end(); ++i)
destroy(*i);
for (succ_to_formula::iterator i = canonical_succ.begin();
i != canonical_succ.end(); ++i)
destroy(i->second);
// Turn all promises into real acceptance conditions.
a->complement_all_acceptance_conditions();

30
src/tgbatest/ltl2tgba.test
View file

@ -25,17 +25,25 @@
set -e
check ()
{
run 0 ./ltl2tgba "$1"
run 0 ./ltl2tgba -f "$1"
}
# We don't check the output, but just running these might be enough to
# trigger assertions.
run 0 ./ltl2tgba a
run 0 ./ltl2tgba 'a U b'
run 0 ./ltl2tgba 'X a'
run 0 ./ltl2tgba 'a & b & c'
run 0 ./ltl2tgba 'a | b | (c U (d & (g U (h ^ i))))'
run 0 ./ltl2tgba 'Xa & (b U !a) & (b U !a)'
run 0 ./ltl2tgba 'Fa & Xb & GFc & Gd'
run 0 ./ltl2tgba 'Fa & Xa & GFc & Gc'
run 0 ./ltl2tgba 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
run 0 ./ltl2tgba 'a R (b R c)'
run 0 ./ltl2tgba '(a U b) U (c U d)'
check a
check 'a U b'
check 'X a'
check 'a & b & c'
check 'a | b | (c U (d & (g U (h ^ i))))'
check 'Xa & (b U !a) & (b U !a)'
check 'Fa & Xb & GFc & Gd'
check 'Fa & Xa & GFc & Gc'
check 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
check 'a R (b R c)'
check '(a U b) U (c U d)'
check '((Xp2)U(X(1)))*(p1 R(p2 R p0))'