diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 34ffcc683..a0a0e2aaa 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -271,6 +271,41 @@ namespace spot abs = constant::false_instance(); abs2 = constant::empty_word_instance(); weak_abs = 0; + + // Make a first pass to gather Boolean formulae. + // - Fusion(Exps1...,BoolExp1...BoolExpN,Exps2,Exps3...) = + // Fusion(Exps1...,AndNLM(And(BoolExp1...BoolExpN),Exps2),Exps3...) + { + vec* b = 0; + vec::iterator i = v->begin(); + while (i != v->end()) + { + if ((*i)->is_boolean()) + { + if (!b) + b = new vec; + b->push_back(*i); + i = v->erase(i); + } + else + { + if (b) + { + // We have found a non-Boolean Exp. "AndNLM" it + // with all the previous Boolean formulae. + *i = instance(AndNLM, instance(And, b), *i); + b = 0; + } + ++i; + } + } + if (b) + { + // Group all trailing Boolean formulae. + v->push_back(instance(And, b)); + } + } + break; default: diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index 5ceae9012..475d73f3b 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -101,6 +101,8 @@ namespace spot /// - Fusion(Exps1...,0,Exps2...) = 0 /// - Fusion(Exps1...,[*0],Exps2...) = 0 /// - Fusion(Exp) = Exp + /// - Fusion(Exps1...,BoolExp1...BoolExpN,Exps2,Exps3...) = + /// Fusion(Exps1...,AndNLM(And(BoolExp1...BoolExpN),Exps2),Exps3...) static formula* instance(type op, vec* v); virtual void accept(visitor& v); diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test index de06d1c03..5c02759c5 100755 --- a/src/ltltest/equals.test +++ b/src/ltltest/equals.test @@ -50,10 +50,6 @@ run 0 ../equals 'a & a & true' 'a' run 0 ../equals 'a & false & a' 'false' run 0 ../equals 'a | false | a' 'a' run 0 ../equals 'true | a | a' 'true' -run 0 ../equals '{a*}!' '{a*}<>->1' -run 0 ../equals '{a -> b} (c)' '(a->b)->c' -run 0 ../equals '{a & !b}!' 'a & !b' -run 0 ../equals '{a;[*0]}|->!Xb' 'a -> !Xb' # other formulae which are not run 1 ../equals 'a' 'b' @@ -144,6 +140,13 @@ run 0 ../equals '{x;x}[]->GX(1)' '1' run 0 ../equals '{x;x}[]->FF(0)' '{x;x}[]->0' run 0 ../equals '{x;x}[]->y' '{x;x}|->y' run 0 ../equals '{x;x}[]->y' '{x;x}(y)' +run 0 ../equals '{a*}!' '{a*}<>->1' +run 0 ../equals '{a -> b} (c)' '(a->b)->c' +run 0 ../equals '{a & !b}!' 'a & !b' +run 0 ../equals '{a;[*0]}|->!Xb' 'a -> !Xb' +run 0 ../equals '{{a;b}:b:c:d*:e:f}!' '{{a;b}:{{b && c } & d[*]}:{e && f}}!' +run 0 ../equals '{a:b:c}|->!Xb' '(a&b&c) -> !Xb' +run 0 ../equals '{a:b:c*}|->!Xb' '{(a&&b)&c*}|-> !Xb' run 0 ../equals '{a[*0]}' '{[*0]}' run 0 ../equals '{a[*..]}' '{a[*]}' diff --git a/src/ltltest/kind.test b/src/ltltest/kind.test index 9012efb25..85954c96d 100755 --- a/src/ltltest/kind.test +++ b/src/ltltest/kind.test @@ -53,6 +53,8 @@ check '{a;b}|->!Xb' '&fP' check '{a;b}|->X!b' '&!fP' check '{a;b}|->!Gb' '&xP' check '{a;b}|->F!b' '&!xP' +check '{a:b:c:d}!' 'B&!xfLEPS' # Equivalent to a&b&c&d +check 'a&b&c&d' 'B&!xfLEPS' run 0 ../consterm '1' run 0 ../consterm '0'