From a2893520caa8e3e677bff0282453b192dbc692ac Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 7 May 2012 14:30:43 +0200 Subject: [PATCH] Properly thank Christian and Felix. * THANKS, src/tgbaalgos/ltl2tgba_fm.cc: Here. --- THANKS | 2 ++ src/tgbaalgos/ltl2tgba_fm.cc | 4 ++++ 2 files changed, 6 insertions(+) diff --git a/THANKS b/THANKS index 856eac58b..e73f40175 100644 --- a/THANKS +++ b/THANKS @@ -1,7 +1,9 @@ We are grateful to these people for their comments, help, or suggestions. +Christian Dax Étienne Renault +Felix Klaedtke Gerard J. Holzmann Heikki Tauriainen Jean-Michel Couvreur diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index fc51ff2b5..a61f72547 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -1427,6 +1427,10 @@ namespace spot // Transitions going to destinations accepting the empty // word should recognize f2, and the automaton for f1 // 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 f1 = translate_ratexp(node->first(), dict_); res_ = bddtrue;