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

Properly thank Christian and Felix.

Browse source 
* THANKS, src/tgbaalgos/ltl2tgba_fm.cc: Here.
This commit is contained in:
Alexandre Duret-Lutz 2012-05-07 14:30:43 +02:00
parent 7438fa3c65
commit a2893520ca
2 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
THANKS
View file

@ -1,7 +1,9 @@
We are grateful to these people for their comments, help, or We are grateful to these people for their comments, help, or
suggestions. suggestions.
Christian Dax
Étienne Renault Étienne Renault
Felix Klaedtke
Gerard J. Holzmann Gerard J. Holzmann
Heikki Tauriainen Heikki Tauriainen
Jean-Michel Couvreur Jean-Michel Couvreur

4
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -1427,6 +1427,10 @@ namespace spot
// Transitions going to destinations accepting the empty // Transitions going to destinations accepting the empty
// word should recognize f2, and the automaton for f1 // word should recognize f2, and the automaton for f1
// should be understood as universal. // should be understood as universal.
//
// The crux of this translation (the use of implication,
// and the interpretation as a universal automaton) was
// explained to me (adl) by Felix Klaedtke.
bdd f2 = recurse(node->second()); bdd f2 = recurse(node->second());
bdd f1 = translate_ratexp(node->first(), dict_); bdd f1 = translate_ratexp(node->first(), dict_);
res_ = bddtrue; res_ = bddtrue;