alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Do not assert

Browse source 
that the true state has only one link when unobs is used.
This commit is contained in:
Alexandre Duret-Lutz 2004-10-27 11:13:52 +00:00
parent 0864d1ca1e
commit b89f1e252e
2 changed files with 16 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ChangeLog
View file

@ -1,3 +1,8 @@
2004-10-27 Alexandre Duret-Lutz <adl@src.lip6.fr>
* 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 <adl@src.lip6.fr> 2004-10-23 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/evtgbatest/Makefile.am (CLEANFILES): New variable. * src/evtgbatest/Makefile.am (CLEANFILES): New variable.

20
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -854,18 +854,20 @@ namespace spot
bdd cond_for_true = bddfalse; bdd cond_for_true = bddfalse;
if (i != dests.end()) 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 // When translating LTL for an event-based logic with
// unobservable events, the 1 state should accept even // unobservable events, the 1 state should accept all events,
// unobservable events. // even unobservable events.
if (unobs && f == constant::true_instance()) if (unobs && f == constant::true_instance())
cond_for_true = all_events; 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 = tgba_explicit::transition* t =
a->create_transition(now, constant::true_instance()->val_name()); 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(cond_for_true));