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

* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Refine

Browse source 
fair_loop_approximation when branching postponement is not used.
This commit is contained in:
Alexandre Duret-Lutz 2004-05-10 13:43:22 +00:00
parent 040f8beec7
commit faf4a2af26
2 changed files with 10 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
ChangeLog
View file

@ -1,5 +1,8 @@
2004-05-10 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-05-10 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Refine
fair_loop_approximation when branching postponement is not used.
Cache formula translations, and canonize formulae before doing Cache formula translations, and canonize formulae before doing
branching postponement. branching postponement.
* src/tgbaalgos/ltl2tgba_fm.cc (formula_canonizer): New class, with * src/tgbaalgos/ltl2tgba_fm.cc (formula_canonizer): New class, with

9
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -684,6 +684,11 @@ namespace spot
std::string now = to_string(f); std::string now = to_string(f);
// When branching_postponement is used, we must assume that
// the source state is in a fair loop.
bool pflc_from =
(fair_loop_approx && !branching_postponement) ? pflc.check(f) : true;
// We used to factor only Next and A variables while computing // We used to factor only Next and A variables while computing
// prime implicants, with // prime implicants, with
// minato_isop isop(res, d.next_set & d.a_set); // minato_isop isop(res, d.next_set & d.a_set);
@ -752,8 +757,8 @@ namespace spot
// If the destination cannot possibly be part of a fair // If the destination cannot possibly be part of a fair
// loop, make all possible promises. // loop, make all possible promises.
if (fair_loop_approx if (fair_loop_approx
&& dest != constant::true_instance() && !(dest == constant::true_instance()
&& !pflc.check(dest)) || (pflc_from && pflc.check(dest))))
label &= all_promises; label &= all_promises;
// If we are not postponing the branching, we can // If we are not postponing the branching, we can