From 0b74f549125e291804b1e496883b64a6dfd2032c Mon Sep 17 00:00:00 2001 From: Thomas Badie Date: Mon, 20 Aug 2012 17:01:47 +0200 Subject: [PATCH] * src/tgbaalgos/simulation.cc: Fix a bug in the simulation. --- src/tgbaalgos/simulation.cc | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index 4131c2c67..1e772063b 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -298,11 +298,12 @@ namespace spot // transition which has as a destination a state with // no outgoing transition. if (it->first == bddfalse) - previous_class_[*it_s] = bddfalse; + previous_class_[*it_s] = bddfalse; else previous_class_[*it_s] = *it_bdd; } - ++it_bdd; + if (it->first != bddfalse) + ++it_bdd; } } @@ -415,10 +416,16 @@ namespace spot // by removing a transition which has as a destination a // state with no outgoing transition. if (it->first == bddfalse) - now_to_next[it->first] = bddfalse; + { + now_to_next[it->first] = bddfalse; + free_var_.push(bdd_var(*it_bdd)); + it_bdd = used_var_.erase(it_bdd); + } else - now_to_next[it->first] = *it_bdd; - ++it_bdd; + { + now_to_next[it->first] = *it_bdd; + ++it_bdd; + } } update_po(now_to_next);