diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index 7cf62be89..fe89c9ea2 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -258,17 +258,24 @@ namespace spot case EConcat: // - 0 <>-> Exp = 0 // - 1 <>-> Exp = Exp - if (first == constant::false_instance()) - return second; + // - Exp <>-> 0 = 0 if (first == constant::true_instance()) + return second; + if (first == constant::false_instance()) { second->destroy(); return first; } + if (second == constant::false_instance()) + { + first->destroy(); + return second; + } break; case UConcat: // - 0 []-> Exp = 1 // - 1 []-> Exp = Exp + // - Exp []-> 1 = 1 if (first == constant::false_instance()) return constant::true_instance(); if (first == constant::true_instance()) @@ -276,6 +283,11 @@ namespace spot second->destroy(); return first; } + if (second == constant::true_instance()) + { + first->destroy(); + return second; + } break; } diff --git a/src/ltltest/consterm.cc b/src/ltltest/consterm.cc index ddf0b2e8d..94531c5c6 100644 --- a/src/ltltest/consterm.cc +++ b/src/ltltest/consterm.cc @@ -39,7 +39,7 @@ main(int argc, char **argv) syntax(argv[0]); spot::ltl::parse_error_list p1; - spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1); + spot::ltl::formula* f1 = spot::ltl::parse_ratexp(argv[1], p1); if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1)) return 2; diff --git a/src/ltltest/consterm.test b/src/ltltest/consterm.test index 864b489b4..9bab7b9b0 100755 --- a/src/ltltest/consterm.test +++ b/src/ltltest/consterm.test @@ -32,9 +32,8 @@ run 0 ../consterm '0' run 1 ../consterm '#e' run 1 ../consterm 'a*' run 1 ../consterm '0*' -run 0 ../consterm '!#e' -run 0 ../consterm '((a U b) + c)' -run 1 ../consterm '((a U b) + #e)' -run 0 ../consterm '((a U b) + #e) & e' -run 1 ../consterm '((a U b) + #e) & #e' -run 1 ../consterm '((a U b) + #e) & (a* + b)' +run 0 ../consterm '((a ; b) + c)' +run 1 ../consterm '((a ; b) + #e)' +run 0 ../consterm '((a ; b) + #e) & e' +run 1 ../consterm '((a ; b) + #e) & #e' +run 1 ../consterm '((a ; b) + #e) & (a* + b)' diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test index 15221b653..ea6983db2 100755 --- a/src/ltltest/equals.test +++ b/src/ltltest/equals.test @@ -70,17 +70,19 @@ run 0 ../equals 'a & b ^ c | d' 'd | c ^ b & a' run 0 ../equals 'FFG__GFF' 'F(F(G("__GFF")))' # Trivial simplifications -run 0 ../equals '0*' '#e' -run 0 ../equals '#e*' '#e' -run 0 ../equals 'Exp**' 'Exp*' +run 0 ../equals '{0*}<>->a' '{#e}<>->a' +run 0 ../equals '{#e*}<>->a' '{#e}<>->a' +run 0 ../equals '{Exp**}<>->a' '{Exp*}<>->a' run 0 ../equals 'FF(Exp)' 'F(Exp)' run 0 ../equals 'GG(Exp)' 'G(Exp)' run 0 ../equals 'F(0)' '0' run 0 ../equals 'G(0)' '0' run 0 ../equals 'F(1)' '1' run 0 ../equals 'G(1)' '1' -run 0 ../equals 'F(#e)' '1' -run 0 ../equals 'G(#e)' '1' +run 0 ../equals 'F({#e}<>->1)' 'F({#e}<>->1)' +run 0 ../equals 'G({#e}<>->1)' 'G({#e}<>->1)' +run 0 ../equals 'F({1}<>->1)' '1' +run 0 ../equals 'G({1}<>->1)' '1' run 0 ../equals '!1' '0' run 0 ../equals '!0' '1' run 0 ../equals '!!Exp' 'Exp' @@ -105,12 +107,16 @@ run 0 ../equals GGx Gx run 0 ../equals GGGGGx Gx run 0 ../equals '!!x' x run 0 ../equals '!!!!!x' '!x' -run 0 ../equals '#e;x' x -run 0 ../equals 'x;#e' x -run 0 ../equals '#e;x;#e;#e' x -run 0 ../equals '#e;x;#e;x;#e' 'x;x' -run 0 ../equals 'x;x;x;#e;x;x' 'x;x;x;x;x' -run 0 ../equals 'x;0;x;x;x' '0' -run 0 ../equals '0*' '#e' -run 0 ../equals '#e*' '#e' -run 0 ../equals 'x;x;FF(0)' '0' +run 0 ../equals '{#e;x}<>->1' '{x}<>->1' +run 0 ../equals '{x;#e}<>->1' '{x}<>-> 1' +run 0 ../equals '{#e;x;#e;#e}<>->1' '{x}<>->1' +run 0 ../equals '{#e;x;#e;x;#e}<>->1' '{x;x}<>->1' +run 0 ../equals '{x;x;x;#e;x;x}<>->1' '{x;x;x;x;x}<>->1' +run 0 ../equals '{x;0;x;x;x}<>->1' '0' +run 0 ../equals '{x;0;x;x;x}[]->1' '1' +run 0 ../equals '{0*;1}<>->x' 'x' +run 0 ../equals '{#e*;1}<>->x' 'x' +run 0 ../equals '{x;x}<>->FF(0)' '0' +run 0 ../equals '{x;x}<>->GX(1)' '{x;x}<>->1' +run 0 ../equals '{x;x}[]->GX(1)' '1' +run 0 ../equals '{x;x}[]->FF(0)' '{x;x}[]->0' diff --git a/src/ltltest/nenoform.test b/src/ltltest/nenoform.test index f46682de8..0f6d1595c 100755 --- a/src/ltltest/nenoform.test +++ b/src/ltltest/nenoform.test @@ -68,6 +68,5 @@ run 0 ../nenoform '!(a U (!b U ((a & b & c) R d)))' \ run 0 ../nenoform '!(GF a => FG b)' 'GFa & GF!b' # Rational operators -run 0 ../nenoform '!(X((!Xa)*))' 'X!((X!a)*)' -run 0 ../nenoform 'X((Xa)*)' 'X((Xa)*)' -run 0 ../nenoform '!F!X!(GF(a);!FG(a);x)' 'GX!(GFa;GF!a;x)' +run 0 ../nenoform '!X{a;b}<>->Fx' 'X{a;b}[]->G!x' +run 0 ../nenoform '!F({a*}<>->{b*}<>->c)' 'G({a*}[]->{b*}[]->!c)'