From 3350ff71762105851431677aac97de9fbd9f4e4b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 19 Feb 2004 15:46:30 +0000 Subject: [PATCH] * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::current_state): Fix reference to Oddoux's thesis. --- ChangeLog | 5 +++++ src/tgba/tgbatba.cc | 20 ++++++++++---------- src/tgbaalgos/ltl2tgba_fm.cc | 10 ++-------- 3 files changed, 17 insertions(+), 18 deletions(-) diff --git a/ChangeLog b/ChangeLog index 891c0f383..ea5150977 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,8 @@ +2004-02-19 Alexandre Duret-Lutz + + * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::current_state): + Fix reference to Oddoux's thesis. + 2004-02-16 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add the diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 76a18a756..4043b5109 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -153,16 +153,16 @@ namespace spot // to the next acceptance set. If the current transition is also // in the next acceptance set, then go the one after, etc. // - // Jérôme Leroux's PhD thesis has a nice explanation of how it - // works, chapter 6. - // @PhDThesis{ leroux.03.phd, - // author = {J{\'e}r{\^o}me Leroux}, - // title = {Algorithmique de la v{\'e}rification des syst{\`e}mes - // {\`a} compteurs. Approximation et acc{\'e}l{\'e}ration. - // Impl{\'e}mentation de l'outil {\sc Fast}}, - // school = {{\'E}cole Normale Sup{\'e}rieure de Cachan}, - // year = {2003}, - // month = {December} + // See Denis Oddoux's PhD thesis for a nice explanation (in French). + // @PhDThesis{ oddoux.03.phd, + // author = {Denis Oddoux}, + // title = {Utilisation des automates alternants pour un + // model-checking efficace des logiques temporelles + // lin{\'e}aires.}, + // school = {Universit{\'e}e Paris 7}, + // year = {2003}, + // address = {Paris, France}, + // month = {December} // } // iterator next = expected_; diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 1a61985a4..66d95a5ab 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -570,10 +570,6 @@ namespace spot // way it will be explored before the other during the model // checking. dest_map::const_iterator i = dests.find(constant::true_instance()); - // conditions of the True arc, so when can remove them from - // all other arcs. This is not needed when exprop is used, - // but it does not hurt. - bdd cond_for_true = bddfalse; if (i != dests.end()) { // Transitions going to True are not expected to make any promises. @@ -581,10 +577,9 @@ namespace spot prom_map::const_iterator j = i->second.find(bddtrue); assert(j != i->second.end()); - cond_for_true = j->second; tgba_explicit::transition* t = a->create_transition(now, constant::true_instance()->val_name()); - a->add_condition(t, d.bdd_to_formula(cond_for_true)); + a->add_condition(t, d.bdd_to_formula(j->second)); } // Register other transitions. @@ -600,8 +595,7 @@ namespace spot { tgba_explicit::transition* t = a->create_transition(now, next); - a->add_condition(t, d.bdd_to_formula(j->second - - cond_for_true)); + a->add_condition(t, d.bdd_to_formula(j->second)); d.conj_bdd_to_acc(a, j->first, t); } }