diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index 04a8d9a40..d8ac2977c 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -131,9 +131,8 @@ namespace spot if (child == constant::false_instance() || child == constant::true_instance()) return child; - // F([*0]) = G([*0]) = 1 - if (child == constant::empty_word_instance()) - return constant::true_instance(); + + assert(child != constant::empty_word_instance()); } break; @@ -185,9 +184,7 @@ namespace spot if (child == constant::true_instance() || child == constant::false_instance()) return child; - // X([*0]) = 1 - if (child == constant::empty_word_instance()) - return constant::true_instance(); + assert(child != constant::empty_word_instance()); break; case Finish: diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index 687ecf47b..a23e4ec45 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -60,10 +60,10 @@ namespace spot /// - GG(Exp) = G(Exp) /// - F(0) = 0 /// - G(0) = 0 + /// - X(0) = 0 /// - F(1) = 1 /// - G(1) = 1 - /// - F([*0]) = 1 - /// - G([*0]) = 1 + /// - X(1) = 1 /// - !1 = 0 /// - !0 = 1 /// - ![*0] = 1[+] (read below)