diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index 020e33139..bc9cf56e8 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -25,6 +25,7 @@ #include #include "binop.hh" #include "unop.hh" +#include "multop.hh" #include "constant.hh" #include "visitor.hh" #include @@ -365,6 +366,7 @@ namespace spot // - 1 <>-> Exp = Exp // - [*0] <>-> Exp = 0 // - Exp <>-> 0 = 0 + // - boolExp <>-> Exp = boolExp & Exp if (first == constant::true_instance()) return second; if (first == constant::false_instance() @@ -378,12 +380,15 @@ namespace spot first->destroy(); return second; } + if (first->is_boolean()) + return multop::instance(multop::And, first, second); break; case UConcat: // - 0 []-> Exp = 1 // - 1 []-> Exp = Exp // - [*0] []-> Exp = 1 // - Exp []-> 1 = 1 + // - boolExp []-> Exp = boolExp -> Exp if (first == constant::true_instance()) return second; if (first == constant::false_instance() @@ -397,6 +402,8 @@ namespace spot first->destroy(); return second; } + if (first->is_boolean()) + return binop::instance(binop::Implies, first, second); break; } diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh index 12b36cabc..9b340cf9b 100644 --- a/src/ltlast/binop.hh +++ b/src/ltlast/binop.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -96,6 +96,16 @@ namespace spot /// - (1 M Exp) = Exp /// - (0 M Exp) = 0 /// - (Exp M Exp) = Exp + /// - 0 <>-> Exp = 0 + /// - 1 <>-> Exp = Exp + /// - [*0] <>-> Exp = 0 + /// - Exp <>-> 0 = 0 + /// - boolExp <>-> Exp = boolExp & Exp + /// - 0 []-> Exp = 1 + /// - 1 []-> Exp = Exp + /// - [*0] []-> Exp = 1 + /// - Exp []-> 1 = 1 + /// - boolExp <>-> Exp = boolExp -> Exp static formula* instance(type op, formula* first, formula* second); virtual void accept(visitor& v); diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 1cd452592..34ffcc683 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -45,18 +45,18 @@ namespace spot { case Concat: case Fusion: + case AndNLM: + // Note: AndNLM(p1,p2) is a Boolean formula, but it is + // actually rewritten as And(p1,p2) by trivial identities + // before this constructor is called. So at this point, + // AndNLM is always used with at most one Boolean argument, + // and the result is therefore NOT Boolean. is.boolean = false; is.ltl_formula = false; is.eltl_formula = false; is.psl_formula = false; is.eventual = false; is.universal = false; - // fall through - case AndNLM: - // The non-matching-length-And (&) can only appear in the - // rational parts of PSL formula. We don't remove the - // Boolean flag, because applied to atomic propositions a&b - // has the same effect as a&&b. case And: for (unsigned i = 1; i < s; ++i) props &= (*v)[i]->get_props(); @@ -229,6 +229,27 @@ namespace spot abs = constant::false_instance(); abs2 = 0; weak_abs = 0; + + // Make a first pass to gather all boolean terms. + { + vec* b = new vec; + vec::iterator i = v->begin(); + while (i != v->end()) + { + if ((*i)->is_boolean()) + { + b->push_back(*i); + i = v->erase(i); + } + else + { + ++i; + } + } + // - AndNLM(Exps1...,Bool1,Exps2...,Bool2,Exp3...) = + // AndNLM(Exps1...,Exps2...,Exp3...,And(Bool1,Bool2)) + v->push_back(instance(And, b)); + } break; case Or: neutral = constant::false_instance(); @@ -291,6 +312,7 @@ namespace spot ++i; } } + // We have a* & [*0] & c = 0 // and a* & [*0] & c* = [*0] // So if [*0] has been seen, check if alls term recognize the diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index bea72d54e..5ceae9012 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -89,6 +89,8 @@ namespace spot /// - AndNLM(Exps1...,0,Exps2...) = 0 /// - AndNLM(Exps1...,[*0],Exps2...) = AndNLM(Exps1...,Exps2...) /// - AndNLM(Exp) = Exp + /// - AndNLM(Exps1...,BoolExp1,Exps2...,BoolExp2,Exp3...) = + /// AndNLM(Exps1...,Exps2...,Exp3...,And(BoolExp1,BoolExp2)) /// - Or(Exps1...,1,Exps2...) = 1 /// - Or(Exps1...,0,Exps2...) = And(Exps1...,Exps2...) /// - Or(Exp) = Exp diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc index c230ef979..987e525d6 100644 --- a/src/ltltest/equals.cc +++ b/src/ltltest/equals.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -120,6 +120,12 @@ main(int argc, char** argv) int exit_code = f1 != f2; + if (exit_code) + { + spot::ltl::dump(std::cerr, f1) << std::endl; + spot::ltl::dump(std::cerr, f2) << std::endl; + } + f1->destroy(); f2->destroy(); diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test index 25a740257..de06d1c03 100755 --- a/src/ltltest/equals.test +++ b/src/ltltest/equals.test @@ -51,6 +51,9 @@ 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' diff --git a/src/ltltest/kind.test b/src/ltltest/kind.test index 738379378..9012efb25 100755 --- a/src/ltltest/kind.test +++ b/src/ltltest/kind.test @@ -49,10 +49,10 @@ check 'a M b' '&!xfLP' check 'a M 1' '&!xfLPe' check 'a R b' '&!xfLP' check '0 R b' '&!xfLPu' -check '{a}|->!Xb' '&fP' -check '{a}|->X!b' '&!fP' -check '{a}|->!Gb' '&xP' -check '{a}|->F!b' '&!xP' +check '{a;b}|->!Xb' '&fP' +check '{a;b}|->X!b' '&!fP' +check '{a;b}|->!Gb' '&xP' +check '{a;b}|->F!b' '&!xP' run 0 ../consterm '1' run 0 ../consterm '0'