From 7ea51cc65f35156f72bde510fad3b8661c5d8564 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 18 Nov 2009 15:40:37 +0100 Subject: [PATCH] Replace prune_scc() by scc_filter(). prune_scc() leaked memory and failed to remove chains of useless SCCs. * src/tgbaalgos/reductgba_sim.cc (reduc_tgba_sim): Call scc_filter() instead of prune_scc(), and do it before running any simulation-based reduction. * src/tgbaalgos/reductgba_sim.hh (reduc_tgba_sim): Return a const tgba*. * src/tgbatest/ltl2tgba.cc: Call scc_filter() instead of prune_scc(). * src/tgbatest/scc.test: Add two more tests that failed with prune_scc(). --- ChangeLog | 16 ++++++ src/tgbaalgos/reductgba_sim.cc | 27 ++++++---- src/tgbaalgos/reductgba_sim.hh | 4 +- src/tgbatest/ltl2tgba.cc | 99 ++++++++++++++++++---------------- src/tgbatest/reductgba.cc | 18 +++---- src/tgbatest/scc.test | 24 +++++++++ 6 files changed, 122 insertions(+), 66 deletions(-) diff --git a/ChangeLog b/ChangeLog index 20a630ab4..585852a13 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,19 @@ +2009-11-18 Alexandre Duret-Lutz + + Replace prune_scc() by scc_filter(). + + prune_scc() leaked memory and failed to remove chains of useless SCCs. + + * src/tgbaalgos/reductgba_sim.cc (reduc_tgba_sim): Call + scc_filter() instead of prune_scc(), and do it before running + any simulation-based reduction. + * src/tgbaalgos/reductgba_sim.hh (reduc_tgba_sim): Return a const + tgba*. + * src/tgbatest/ltl2tgba.cc, src/tgbatest/reductgba.cc: Call + scc_filter() instead of prune_scc(). + * src/tgbatest/scc.test: Add two more tests that failed with + prune_scc(). + 2009-11-18 Alexandre Duret-Lutz Quick implementation of a "useless SCC" filter using scc_map. diff --git a/src/tgbaalgos/reductgba_sim.cc b/src/tgbaalgos/reductgba_sim.cc index 8dee8c112..6f4d3a684 100644 --- a/src/tgbaalgos/reductgba_sim.cc +++ b/src/tgbaalgos/reductgba_sim.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2004, 2005, 2007 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2004, 2005, 2007, 2009 Laboratoire d'Informatique de +// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -21,6 +21,7 @@ #include "reductgba_sim.hh" #include "tgba/bddprint.hh" +#include "sccfilter.hh" namespace spot { @@ -663,11 +664,24 @@ namespace spot return false; } - tgba* + const tgba* reduc_tgba_sim(const tgba* f, int opt) { + if (opt & Reduce_Scc) + { + f = scc_filter(f); + + // No more reduction requested? Return the automaton as-is. + if (opt == Reduce_Scc) + return f; + } + spot::tgba_reduc* automatareduc = new spot::tgba_reduc(f); + // Destroy the automaton created by scc_filter. + if (opt & Reduce_Scc) + delete f; + if (opt & (Reduce_quotient_Dir_Sim | Reduce_transition_Dir_Sim)) { direct_simulation_relation* rel @@ -696,11 +710,6 @@ namespace spot free_relation_simulation(rel); } - if (opt & Reduce_Scc) - { - automatareduc->prune_scc(); - } - return automatareduc; } diff --git a/src/tgbaalgos/reductgba_sim.hh b/src/tgbaalgos/reductgba_sim.hh index bb33e70aa..0ae7af328 100644 --- a/src/tgbaalgos/reductgba_sim.hh +++ b/src/tgbaalgos/reductgba_sim.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -61,7 +61,7 @@ namespace spot /// \param opt a conjonction of spot::reduce_tgba_options specifying /// which optimizations to apply. /// \return the reduced automata. - tgba* reduc_tgba_sim(const tgba* a, int opt = Reduce_All); + const tgba* reduc_tgba_sim(const tgba* a, int opt = Reduce_All); /// \brief Compute a direct simulation relation on state of tgba \a f. direct_simulation_relation* get_direct_relation_simulation(const tgba* a, diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 994309f9b..7b7501898 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -48,6 +48,7 @@ #include "tgbaalgos/reductgba_sim.hh" #include "tgbaalgos/replayrun.hh" #include "tgbaalgos/rundotdec.hh" +#include "tgbaalgos/sccfilter.hh" #include "misc/timer.hh" #include "tgbaalgos/stats.hh" @@ -715,64 +716,71 @@ main(int argc, char** argv) } spot::tgba_reduc* aut_red = 0; + spot::tgba* aut_scc = 0; if (reduc_aut != spot::Reduce_None) { - tm.start("reducing formula automaton"); - a = aut_red = new spot::tgba_reduc(a); if (reduc_aut & spot::Reduce_Scc) - aut_red->prune_scc(); - - if (reduc_aut & (spot::Reduce_quotient_Dir_Sim | - spot::Reduce_transition_Dir_Sim | - spot::Reduce_quotient_Del_Sim | - spot::Reduce_transition_Del_Sim)) { - spot::direct_simulation_relation* rel_dir = 0; - spot::delayed_simulation_relation* rel_del = 0; + tm.start("reducing formula aut. w/ SCC"); + a = aut_scc = spot::scc_filter(a); + tm.start("reducing formula aut. w/ SCC"); + } + + if (reduc_aut & !spot::Reduce_Scc) + { + tm.start("reducing formula aut. w/ sim."); + a = aut_red = new spot::tgba_reduc(a); if (reduc_aut & (spot::Reduce_quotient_Dir_Sim | - spot::Reduce_transition_Dir_Sim)) + spot::Reduce_transition_Dir_Sim | + spot::Reduce_quotient_Del_Sim | + spot::Reduce_transition_Del_Sim)) { - rel_dir = - spot::get_direct_relation_simulation(a, - std::cout, - display_parity_game); - assert(rel_dir); - } - if (reduc_aut & (spot::Reduce_quotient_Del_Sim | - spot::Reduce_transition_Del_Sim)) - { - rel_del = - spot::get_delayed_relation_simulation(a, - std::cout, - display_parity_game); - assert(rel_del); - } + spot::direct_simulation_relation* rel_dir = 0; + spot::delayed_simulation_relation* rel_del = 0; + + if (reduc_aut & (spot::Reduce_quotient_Dir_Sim | + spot::Reduce_transition_Dir_Sim)) + { + rel_dir = + spot::get_direct_relation_simulation + (a, std::cout, display_parity_game); + assert(rel_dir); + } + if (reduc_aut & (spot::Reduce_quotient_Del_Sim | + spot::Reduce_transition_Del_Sim)) + { + rel_del = + spot::get_delayed_relation_simulation + (a, std::cout, display_parity_game); + assert(rel_del); + } + + if (display_rel_sim) + { + if (rel_dir) + aut_red->display_rel_sim(rel_dir, std::cout); + if (rel_del) + aut_red->display_rel_sim(rel_del, std::cout); + } + + if (reduc_aut & spot::Reduce_quotient_Dir_Sim) + aut_red->quotient_state(rel_dir); + if (reduc_aut & spot::Reduce_transition_Dir_Sim) + aut_red->delete_transitions(rel_dir); + if (reduc_aut & spot::Reduce_quotient_Del_Sim) + aut_red->quotient_state(rel_del); + if (reduc_aut & spot::Reduce_transition_Del_Sim) + aut_red->delete_transitions(rel_del); - if (display_rel_sim) - { if (rel_dir) - aut_red->display_rel_sim(rel_dir, std::cout); + spot::free_relation_simulation(rel_dir); if (rel_del) - aut_red->display_rel_sim(rel_del, std::cout); + spot::free_relation_simulation(rel_del); } - - if (reduc_aut & spot::Reduce_quotient_Dir_Sim) - aut_red->quotient_state(rel_dir); - if (reduc_aut & spot::Reduce_transition_Dir_Sim) - aut_red->delete_transitions(rel_dir); - if (reduc_aut & spot::Reduce_quotient_Del_Sim) - aut_red->quotient_state(rel_del); - if (reduc_aut & spot::Reduce_transition_Del_Sim) - aut_red->delete_transitions(rel_del); - - if (rel_dir) - spot::free_relation_simulation(rel_dir); - if (rel_del) - spot::free_relation_simulation(rel_del); + tm.stop("reducing formula aut. w/ sim."); } - tm.stop("reducing formula automaton"); } spot::tgba_explicit* expl = 0; @@ -1021,6 +1029,7 @@ main(int argc, char** argv) delete system; delete expl; delete aut_red; + delete aut_scc; delete degeneralized; delete state_labeled; delete to_free; diff --git a/src/tgbatest/reductgba.cc b/src/tgbatest/reductgba.cc index 9f6ffcf30..946611c77 100644 --- a/src/tgbatest/reductgba.cc +++ b/src/tgbatest/reductgba.cc @@ -40,6 +40,7 @@ #include "tgbaparse/public.hh" #include "tgbaalgos/dupexp.hh" #include "tgbaalgos/neverclaim.hh" +#include "tgbaalgos/sccfilter.hh" #include "misc/escape.hh" @@ -148,21 +149,18 @@ main(int argc, char** argv) spot::free_relation_simulation(rel_del); } + spot::tgba* res = automatareduc; + if (o & spot::Reduce_Scc) { - automatareduc->prune_scc(); - //automatareduc->display_scc(std::cout); + res = spot::scc_filter(automatareduc); + delete automatareduc; } - if (automatareduc != 0) - { - spot::dotty_reachable(std::cout, automatareduc); - } + spot::dotty_reachable(std::cout, res); - if (automata != 0) - delete automata; - if (automatareduc != 0) - delete automatareduc; + delete automata; + delete res; #ifndef REDUCCMP if (f != 0) f->destroy(); diff --git a/src/tgbatest/scc.test b/src/tgbatest/scc.test index 0fcda6007..9608d5f81 100755 --- a/src/tgbatest/scc.test +++ b/src/tgbatest/scc.test @@ -48,3 +48,27 @@ accepting paths: 2 dead paths: 1 EOF diff stdout expected + +run 0 ../ltl2tgba -f -R3 -k '(b U a) | (GFa & XG!a)' >stdout +cat >expected <stdout +cat >expected <