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

Typo from a previous patch.

Browse source 
* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Fix a typo
introduced three patches ago in the handling of unobserved events.
This commit is contained in:
Alexandre Duret-Lutz 2009-11-11 00:01:14 +01:00
parent 8c6a2b33d9
commit 7c946878e4
2 changed files with 8 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

7
ChangeLog
View file

@ -1,3 +1,10 @@
2009-11-10 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Typo from a previous patch.
* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Fix a typo
introduced three patches ago in the handling of unobserved events.
2009-11-10 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2009-11-10 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Do not comment states in the never claim by default. It takes too Do not comment states in the never claim by default. It takes too

2
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -924,7 +924,7 @@ namespace spot
// 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 all events, // unobservable events, the 1 state should accept all events,
// even unobservable events. // even unobservable events.
if (unobs && f == constant::true_instance()) if (unobs && now == constant::true_instance())
cond_for_true = all_events; cond_for_true = all_events;
else else
{ {