From 5bea6e4950af06f10368f26fff11acd8be0674aa Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 19 Apr 2012 18:09:20 +0200 Subject: [PATCH] Fix handling of 1 in trivial identities for rational operators. Especially, 1&f and 1:f were mistakenly always reduced to f, which is incorrect when f accept the empty word. * src/ltlast/multop.cc: Here. * src/ltlast/multop.hh, doc/tl/tl.tex: Adjust documentation. * src/ltltest/equals.test: Add more tests. --- doc/tl/tl.tex | 14 +++++--- src/ltlast/multop.cc | 79 +++++++++++++++++++++++++++++------------ src/ltlast/multop.hh | 24 +++++++------ src/ltltest/equals.test | 11 ++++++ 4 files changed, 91 insertions(+), 37 deletions(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 7cbb653ef..b7403ce4a 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -692,7 +692,7 @@ $b_1$, $b_2$ are assumed to be Boolean formul\ae. \end{align*} \noindent -The following rules are all valid with the two arguments swapped. +The following rules are all valid with the two arguments swapped (on input). %(Even for the non-commutative operators \samp{$\CONCAT$} and %\samp{$\FUSION$}.) @@ -705,10 +705,14 @@ The following rules are all valid with the two arguments swapped. \0\OR f &\equiv f & \0 \FUSION f &\equiv \0 & \0 \CONCAT f &\equiv \0 \\ - \1\AND f &\equiv f& - \1\ANDALT f &\equiv f & - \1\OR f &\equiv \1 & - \1 \FUSION f & \equiv f\\ + \1\AND f&\equiv + \begin{cases} + 1 &\mathrlap{\text{if~} \varepsilon\VDash f} \\ + f &\mathrlap{\text{if~} \varepsilon\nVDash f} \\ + \end{cases} & + \1\ANDALT b &\equiv b & + \1\OR b &\equiv \1 & + \1 \FUSION f & \equiv f\mathrlap{\text{~if~}\varepsilon\nVDash f}\\ \eword\AND f &\equiv f & \eword\ANDALT f &\equiv \begin{cases} diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 17ec4ab52..3c34eef94 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -283,6 +283,8 @@ namespace spot if (op != Concat && op != Fusion) std::sort(v->begin(), v->end(), formula_ptr_less_than()); + unsigned orig_size = v->size(); + formula* neutral; formula* neutral2; formula* abs; @@ -306,11 +308,11 @@ namespace spot gather_bool(v, And); break; case AndNLM: - neutral = constant::true_instance(); - neutral2 = constant::empty_word_instance(); + neutral = constant::empty_word_instance(); + neutral2 = 0; abs = constant::false_instance(); abs2 = 0; - weak_abs = 0; + weak_abs = constant::true_instance(); gather_bool(v, And); break; case Or: @@ -388,7 +390,7 @@ namespace spot break; } - // Remove duplicates (except for Concat). We can't use + // Remove duplicates (except for Concat and Fusion). We can't use // std::unique(), because we must destroy() any formula we drop. // Also ignore neutral elements and handle absorbent elements. { @@ -411,31 +413,54 @@ namespace spot } else { - if (*i == weak_abs) - weak_abs_seen = true; - if (op != Concat) // Don't remove duplicates for Concat. + weak_abs_seen |= (*i == weak_abs); + if (op != Concat && op != Fusion) // Don't remove duplicates last = *i; ++i; } } - // We have a* && [*0] && c = 0 - // and a* && [*0] && c* = [*0] - // So if [*0] has been seen, check if alls term recognize the - // empty word. if (weak_abs_seen) { - bool acc_eword = true; - for (i = v->begin(); i != v->end(); ++i) + if (op == AndRat) { - acc_eword &= (*i)->accepts_eword(); - (*i)->destroy(); + // We have a* && [*0] && c = 0 + // and a* && [*0] && c* = [*0] + // So if [*0] has been seen, check if alls term + // recognize the empty word. + bool acc_eword = true; + for (i = v->begin(); i != v->end(); ++i) + { + acc_eword &= (*i)->accepts_eword(); + (*i)->destroy(); + } + delete v; + if (acc_eword) + return weak_abs; + else + return abs; } - delete v; - if (acc_eword) - return weak_abs; else - return constant::false_instance(); + { + // Similarly, a* & 1 & (c;d) = c;d + // a* & 1 & c* = 1 + assert(op == AndNLM); + multop::vec tmp; + for (i = v->begin(); i != v->end(); ++i) + { + if (*i == weak_abs) + continue; + if ((*i)->accepts_eword()) + { + (*i)->destroy(); + continue; + } + tmp.push_back(*i); + } + if (tmp.empty()) + tmp.push_back(weak_abs); + v->swap(tmp); + } } } @@ -449,11 +474,21 @@ namespace spot else if (s == 1) { // Simply replace Multop(Op,X) by X. + // Except we should never reduce the + // arguments of a Fusion operator to + // a list with a single formula that + // accepts [*0]. formula* res = (*v)[0]; - delete v; - return res; + if (op != Fusion || orig_size == 1 + || !res->accepts_eword()) + { + delete v; + return res; + } + // If Fusion(f, ...) reduce to Fusion(f), emit Fusion(1,f). + // to ensure that [*0] is not accepted. + v->insert(v->begin(), constant::true_instance()); } - // The hash key. pair p(op, v); diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index f0f7b886e..291f72bed 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -84,27 +84,31 @@ namespace spot /// - And(Exps1...,1,Exps2...) = And(Exps1...,Exps2...) /// - And(Exps1...,0,Exps2...) = 0 /// - And(Exp) = Exp - /// - AndRat(Exps1...,0,Exps2...) = 0 - /// - AndRat(Exps1...,BoolExp1,Exps2...,BoolExps2...) = - /// AndRat(Exps1...,Exps2...,And(BoolExp1,BoolExps2...)) - /// - AndRat(Exps1...,[*0],Exps2...) = [*0] if all Expi accept [*0] - /// - AndRat(Exps1...,[*0],Exps2...) = 0 if some Expi reject [*0] - /// - AndNLM(Exps1...,1,Exps2...) = AndNLM(Exps1...,Exps2...) + /// - Or(Exps1...,1,Exps2...) = 1 + /// - Or(Exps1...,0,Exps2...) = Or(Exps1...,Exps2...) + /// - Or(Exp) = Exp + /// - AndNLM(FExps1...,1,Exps2...) = AndNLM(Exps2...) + /// if Fexps1... accept [*0], and Exps2... don't. + /// - AndNLM(FExps1...,1,FExps2...) = 1 + /// if Fexps1...,FExps2... all accept[*0]. /// - AndNLM(Exps1...,0,Exps2...) = 0 /// - AndNLM(Exps1...,[*0],Exps2...) = AndNLM(Exps1...,Exps2...) /// - AndNLM(Exp) = Exp /// - AndNLM(Exps1...,BoolExp1,Exps2...,BoolExp2,Exps3...) = /// AndNLM(Exps1...,Exps2...,Exps3...,And(BoolExp1,BoolExp2)) - /// - Or(Exps1...,1,Exps2...) = 1 - /// - Or(Exps1...,0,Exps2...) = Or(Exps1...,Exps2...) - /// - Or(Exp) = Exp + /// - AndRat(Exps1...,0,Exps2...) = 0 + /// - AndRat(Exps1...,BoolExp1,Exps2...,BoolExps2...) = + /// AndRat(Exps1...,Exps2...,And(BoolExp1,BoolExps2...)) + /// - AndRat(Exps1...,[*0],Exps2...) = [*0] if all Expi accept [*0] + /// - AndRat(Exps1...,[*0],Exps2...) = 0 if some Expi reject [*0] /// - OrRat(Exps1...,0,Exps2...) = OrRat(Exps1...,Exps2...) /// - OrRat(Exps1...,BoolExp1,Exps2...,BoolExps2...) = /// OrRat(Exps1...,Exps2...,Or(BoolExp1,BoolExps2...)) /// - Concat(Exps1...,0,Exps2...) = 0 /// - Concat(Exps1...,[*0],Exps2...) = Concat(Exps1...,Exps2...) /// - Concat(Exp) = Exp - /// - Fusion(Exps1...,1,Exps2...) = Concat(Exps1...,Exps2...) + /// - Fusion(Exps1...1,Exps2...) = Fusion(Exps1...,Exps2...) + /// if at least one exp reject [*0] /// - Fusion(Exps1...,0,Exps2...) = 0 /// - Fusion(Exps1...,[*0],Exps2...) = 0 /// - Fusion(Exp) = Exp diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test index ad4c86be3..7e696b142 100755 --- a/src/ltltest/equals.test +++ b/src/ltltest/equals.test @@ -149,6 +149,17 @@ 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&b&c*}|->!Xb' '{(a&&b)&c*}|-> !Xb' +run 0 ../equals '{0&{f;g*}}!' '0' +run 0 ../equals '{1&{f;g*}}!' '{f;g*}!' +# 1 should not be removed in the following two formulae +run 1 ../equals '{1&{g*}}!' '{g*}!' +run 1 ../equals '{1|{b;c}}<>->a' '{b;c}<>->a' +run 0 ../equals '{1:{a;b}:1:c*}!' '{{a;b}:c*}!' +run 0 ../equals '{c*:1:{a;b}:1}!' '{c*:{a;b}}!' +# make sure twin arguments are not reduced in Fusion. +run 1 ../equals '{(a;!a)*:(a;!a)*:b}!' '{(a;!a)*:b}!' +# make sure 1:a* is not reduced to a*. +run 1 ../equals '{(1:a*);b}!' '{a*;b}!' run 0 ../equals '{a[*0]}' '{[*0]}' run 0 ../equals '{a[*..]}' '{a[*]}'