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

ltl2tgba: apply -R3 before -D or -DS.

Browse source 
* src/tgbatest/ltl2tgba.cc (main): Call scc_filter() before the
degeneralization, because it might remove useless acceptance
conditions.  I realized this while looking at experiments from
Rdiger Ehlers.
This commit is contained in:
Alexandre Duret-Lutz 2010-03-03 08:40:21 +01:00
parent 2598f794d8
commit efb15a9171
3 changed files with 21 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

9
ChangeLog
View file

@ -1,3 +1,12 @@
2010-03-03 Alexandre Duret-Lutz <adl@lrde.epita.fr>
ltl2tgba: apply -R3 before -D or -DS.
* src/tgbatest/ltl2tgba.cc (main): Call scc_filter() before the
degeneralization, because it might remove useless acceptance
conditions. I realized this while looking at experiments from
Rüdiger Ehlers.
2010-02-24 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-02-24 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/sanity/style.test: Better fix for the previous error. * src/sanity/style.test: Better fix for the previous error.

1
THANKS
View file

@ -5,4 +5,5 @@ Heikki Tauriainen
Jean-Michel Couvreur Jean-Michel Couvreur
Jean-Michel Ilié Jean-Michel Ilié
Kristin Y. Rozier Kristin Y. Rozier
Rüdiger Ehlers
Yann Thierry-Mieg Yann Thierry-Mieg

21
src/tgbatest/ltl2tgba.cc
View file

@ -800,6 +800,16 @@ main(int argc, char** argv)
} }
} }
// Remove dead SCCs and useless acceptance conditions before
// degeneralization.
spot::tgba* aut_scc = 0;
if (reduc_aut & spot::Reduce_Scc)
{
tm.start("reducing A_f w/ SCC");
a = aut_scc = spot::scc_filter(a);
tm.stop("reducing A_f w/ SCC");
}
spot::tgba_tba_proxy* degeneralized = 0; spot::tgba_tba_proxy* degeneralized = 0;
spot::tgba_sgba_proxy* state_labeled = 0; spot::tgba_sgba_proxy* state_labeled = 0;
@ -819,17 +829,8 @@ main(int argc, char** argv)
} }
spot::tgba_reduc* aut_red = 0; spot::tgba_reduc* aut_red = 0;
spot::tgba* aut_scc = 0;
if (reduc_aut != spot::Reduce_None) if (reduc_aut != spot::Reduce_None)
{ {
if (reduc_aut & spot::Reduce_Scc)
{
tm.start("reducing A_f w/ SCC");
a = aut_scc = spot::scc_filter(a);
tm.stop("reducing A_f w/ SCC");
}
if (reduc_aut & ~spot::Reduce_Scc) if (reduc_aut & ~spot::Reduce_Scc)
{ {
tm.start("reducing A_f w/ sim."); tm.start("reducing A_f w/ sim.");
@ -1132,8 +1133,8 @@ main(int argc, char** argv)
delete system; delete system;
delete expl; delete expl;
delete aut_red; delete aut_red;
delete aut_scc;
delete degeneralized; delete degeneralized;
delete aut_scc;
delete state_labeled; delete state_labeled;
delete to_free; delete to_free;
delete echeck_inst; delete echeck_inst;