Commit 7ea51cc6 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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().
parent 74f620d1
2009-11-18 Alexandre Duret-Lutz <adl@lrde.epita.fr>
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 <adl@lrde.epita.fr>
Quick implementation of a "useless SCC" filter using scc_map.
......
// Copyright (C) 2004, 2005, 2007 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// et Marie Curie.
// Copyright (C) 2004, 2005, 2007, 2009 Laboratoire d'Informatique de
// Paris 6 (LIP6), dpartement Systmes Rpartis Coopratifs (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;
}
......
// 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,
......
......@@ -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();
{
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_quotient_Dir_Sim |
spot::Reduce_transition_Dir_Sim |
spot::Reduce_quotient_Del_Sim |
spot::Reduce_transition_Del_Sim))
if (reduc_aut & !spot::Reduce_Scc)
{
spot::direct_simulation_relation* rel_dir = 0;
spot::delayed_simulation_relation* rel_del = 0;
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))
{
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))
spot::Reduce_transition_Dir_Sim |
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;
......
......@@ -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();
......
......@@ -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 <<EOF
transitions: 5
states: 3
total SCCs: 3
accepting SCCs: 1
dead SCCs: 0
accepting paths: 2
dead paths: 0
EOF
diff stdout expected
run 0 ../ltl2tgba -f -R3 -k 'XXXX(0)' >stdout
cat >expected <<EOF
transitions: 0
states: 1
total SCCs: 1
accepting SCCs: 0
dead SCCs: 1
accepting paths: 0
dead paths: 1
EOF
diff stdout expected
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment