From ab02ee60feab4c3bf53f9afa3a7e630a12a66282 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 23 Nov 2009 22:24:55 +0100 Subject: [PATCH] * src/tgbaalgos/sccfilter.cc (create_transition): Do not clone the same node twice when dealing with loops. --- ChangeLog | 5 +++++ src/tgbaalgos/sccfilter.cc | 2 +- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/ChangeLog b/ChangeLog index 9cc362f56..0ca000c5b 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,8 @@ +2009-11-23 Alexandre Duret-Lutz + + * src/tgbaalgos/sccfilter.cc (create_transition): Do not clone + the same node twice when dealing with loops. + 2009-11-23 Alexandre Duret-Lutz Use bdd_satprefix() to speedup minato on BDDs that are almost cubes. diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index a749da501..64930aa23 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -52,7 +52,7 @@ namespace spot const ltl::formula* out_f = a->get_label(out_s); if (!out_aut->has_state(in_f)) in_f->clone(); - if (!out_aut->has_state(out_f)) + if ((in_f != out_f) && !out_aut->has_state(out_f)) out_f->clone(); return out_aut->create_transition(in_f, out_f); }