From b89f1e252eb1bef6a1cbb5416783662b27205128 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 27 Oct 2004 11:13:52 +0000 Subject: [PATCH] * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Do not assert that the true state has only one link when unobs is used. --- ChangeLog | 5 +++++ src/tgbaalgos/ltl2tgba_fm.cc | 20 +++++++++++--------- 2 files changed, 16 insertions(+), 9 deletions(-) diff --git a/ChangeLog b/ChangeLog index b651f9e4f..54f64dcb4 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,8 @@ +2004-10-27 Alexandre Duret-Lutz + + * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Do not assert + that the true state has only one link when unobs is used. + 2004-10-23 Alexandre Duret-Lutz * src/evtgbatest/Makefile.am (CLEANFILES): New variable. diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 20b1becbc..a5fcf95f3 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -854,18 +854,20 @@ namespace spot bdd cond_for_true = bddfalse; if (i != dests.end()) { - // There should be only one transition going to 1 (true) ... - assert(i->second.size() == 1); - prom_map::const_iterator j = i->second.begin(); - // ... and it is not expected to make any promises. - assert(j->first == bddtrue); - - cond_for_true = j->second; // When translating LTL for an event-based logic with - // unobservable events, the 1 state should accept even - // unobservable events. + // unobservable events, the 1 state should accept all events, + // even unobservable events. if (unobs && f == constant::true_instance()) cond_for_true = all_events; + else + { + // There should be only one transition going to 1 (true) ... + assert(i->second.size() == 1); + prom_map::const_iterator j = i->second.begin(); + // ... and it is not expected to make any promises. + assert(j->first == bddtrue); + 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));