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

Do not simplify F([*0]) and G([*0]). Make sure it does not happen.

Browse source 
* src/ltlast/unop.hh, src/ltlast/unop.cc: Replace the
simplification by an assert.
This commit is contained in:
Alexandre Duret-Lutz 2010-10-25 17:00:53 +02:00
parent 473cf77144
commit 5bb171c8f6
2 changed files with 5 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ltlast/unop.cc
View file

@ -131,9 +131,8 @@ namespace spot
if (child == constant::false_instance() if (child == constant::false_instance()
|| child == constant::true_instance()) || child == constant::true_instance())
return child; return child;
// F([*0]) = G([*0]) = 1
if (child == constant::empty_word_instance()) assert(child != constant::empty_word_instance());
return constant::true_instance();
} }
break; break;
@ -185,9 +184,7 @@ namespace spot
if (child == constant::true_instance() if (child == constant::true_instance()
|| child == constant::false_instance()) || child == constant::false_instance())
return child; return child;
// X([*0]) = 1 assert(child != constant::empty_word_instance());
if (child == constant::empty_word_instance())
return constant::true_instance();
break; break;
case Finish: case Finish:

4
src/ltlast/unop.hh
View file

@ -60,10 +60,10 @@ namespace spot
/// - GG(Exp) = G(Exp) /// - GG(Exp) = G(Exp)
/// - F(0) = 0 /// - F(0) = 0
/// - G(0) = 0 /// - G(0) = 0
/// - X(0) = 0
/// - F(1) = 1 /// - F(1) = 1
/// - G(1) = 1 /// - G(1) = 1
/// - F([*0]) = 1 /// - X(1) = 1
/// - G([*0]) = 1
/// - !1 = 0 /// - !1 = 0
/// - !0 = 1 /// - !0 = 1
/// - ![*0] = 1[+] (read below) /// - ![*0] = 1[+] (read below)