From 866384b4239b0d26ee962c929c6f1815ee8fc562 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 17 Apr 2012 18:33:39 +0200 Subject: [PATCH] =?UTF-8?q?Fix=20trivial=20rules=20for=20b=E2=82=81:b?= =?UTF-8?q?=E2=82=82=20and=20b&f.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * src/ltlast/multop.cc (instance): Here. * src/ltlast/multop.hh, doc/tl/tl.tex: Adjust documentation. * src/ltltest/equals.test: Adjust test cases. --- doc/tl/tl.tex | 4 +-- src/ltlast/multop.cc | 54 ++++++++++++++++++++++------------------- src/ltlast/multop.hh | 6 ++--- src/ltltest/equals.test | 7 +++--- 4 files changed, 38 insertions(+), 33 deletions(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 8da743d3e..41ffe2c4e 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, except the one marked with $\equivM$. +The following rules are all valid with the two arguments swapped. %(Even for the non-commutative operators \samp{$\CONCAT$} and %\samp{$\FUSION$}.) @@ -721,7 +721,7 @@ The following rules are all valid with the two arguments swapped, except the one b_1 \AND b_2 &\equiv b_1\ANDALT b_2 & && && - b:f &\equivM b\AND f\\ + b_1:b_2 &\equiv b_1\ANDALT b_2\\ \end{align*} \section{SERE-LTL Binding Operators} diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 23a81dc75..a1ac89d4c 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -196,9 +196,9 @@ namespace spot // pointers that we must ignore. if ((*i) == 0) { - // FIXME: We should replace the pointer by the - // first non-null value at the end of the array - // instead of calling erase. + // FIXME: For commutative operators we should replace + // the pointer by the first non-null value at the end + // of the array instead of calling erase. i = v->erase(i); continue; } @@ -271,9 +271,12 @@ namespace spot ++i; } } - // - AndNLM(Exps1...,Bool1,Exps2...,Bool2,Exp3...) = - // AndNLM(Exps1...,Exps2...,Exp3...,And(Bool1,Bool2)) - v->push_back(instance(And, b)); + // - AndNLM(Exps1...,Bool1,Exps2...,Bool2,Exps3...) = + // AndNLM(Exps1...,Exps2...,Exps3...,And(Bool1,Bool2)) + if (!b->empty()) + v->push_back(instance(And, b)); + else + delete b; } break; case Or: @@ -297,38 +300,39 @@ namespace spot abs2 = constant::empty_word_instance(); weak_abs = 0; - // Make a first pass to gather Boolean formulae. + // Make a first pass to group adjacent Boolean formulae. // - Fusion(Exps1...,BoolExp1...BoolExpN,Exps2,Exps3...) = - // Fusion(Exps1...,AndNLM(And(BoolExp1...BoolExpN),Exps2),Exps3...) + // Fusion(Exps1...,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); + vec::iterator first = i; + ++i; + if (i == v->end()) + break; + if (!(*i)->is_boolean()) + { + ++i; + continue; + } + do + ++i; + while (i != v->end() && (*i)->is_boolean()); + // We have at least two adjacent Boolean formulae. + // Replace the first one by the conjunction of all. + vec* b = new vec; + b->insert(b->begin(), first, i); + i = v->erase(first + 1, i); + *first = instance(And, b); } 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; diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index 29414afed..9b229a97d 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -90,8 +90,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)) + /// - AndNLM(Exps1...,BoolExp1,Exps2...,BoolExp2,Exps3...) = + /// AndNLM(Exps1...,Exps2...,Exps3...,And(BoolExp1,BoolExp2)) /// - Or(Exps1...,1,Exps2...) = 1 /// - Or(Exps1...,0,Exps2...) = And(Exps1...,Exps2...) /// - Or(Exp) = Exp @@ -103,7 +103,7 @@ namespace spot /// - Fusion(Exps1...,[*0],Exps2...) = 0 /// - Fusion(Exp) = Exp /// - Fusion(Exps1...,BoolExp1...BoolExpN,Exps2,Exps3...) = - /// Fusion(Exps1...,AndNLM(And(BoolExp1...BoolExpN),Exps2),Exps3...) + /// Fusion(Exps1...,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 f0090e257..ad4c86be3 100755 --- a/src/ltltest/equals.test +++ b/src/ltltest/equals.test @@ -145,9 +145,10 @@ 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;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 '{a[*0]}' '{[*0]}' run 0 ../equals '{a[*..]}' '{a[*]}'