From e06b3b7974ffe03fd18b5e5aebd1e68987dd21f3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 24 Apr 2012 17:22:23 +0200 Subject: [PATCH] Trivially reduce 1[*]&&f = f and 1[*]|f = 1[*]. * src/ltlast/bunop.hh (one_star): New static method building 1[*]. * src/ltlast/bunop.cc (bunop::~bunop, bunop::instance_count): Adjust. * src/ltlast/multop.cc: Implement the trivial rewriting. * src/ltlast/multop.hh, doc/tl/tl.tex: Document it. * src/ltltest/equals.test: Test it. --- doc/tl/tl.tex | 7 ++++++- src/ltlast/bunop.cc | 11 ++++++++++- src/ltlast/bunop.hh | 14 ++++++++++++++ src/ltlast/multop.cc | 9 +++++---- src/ltlast/multop.hh | 2 ++ src/ltltest/equals.test | 2 ++ 6 files changed, 39 insertions(+), 6 deletions(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index b7403ce4a..fa195cea8 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 (on input). +The following rules are all valid with the two arguments swapped. %(Even for the non-commutative operators \samp{$\CONCAT$} and %\samp{$\FUSION$}.) @@ -713,6 +713,11 @@ The following rules are all valid with the two arguments swapped (on input). \1\ANDALT b &\equiv b & \1\OR b &\equiv \1 & \1 \FUSION f & \equiv f\mathrlap{\text{~if~}\varepsilon\nVDash f}\\ + && + \1\STAR{} \AND f &\equiv f & + \1\STAR{} \OR f &\equiv \1\STAR{} & + && + && \\ \eword\AND f &\equiv f & \eword\ANDALT f &\equiv \begin{cases} diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc index d28a5be29..9b2950db8 100644 --- a/src/ltlast/bunop.cc +++ b/src/ltlast/bunop.cc @@ -31,6 +31,10 @@ namespace spot { namespace ltl { + // Can't build it on startup, because it uses + // constant::true_instance that may not have been built yet... + formula* bunop::one_star_ = 0; + bunop::bunop(type op, formula* child, unsigned min, unsigned max) : ref_formula(BUnOp), op_(op), child_(child), min_(min), max_(max) { @@ -62,6 +66,10 @@ namespace spot bunop::~bunop() { + // one_star_ should never get delete. Otherwise, that means + // is has been destroyed too much, or not cloned enough. + assert(this != one_star_); + // Get this instance out of the instance map. pair p(pairo(op(), child()), pairu(min_, max_)); map::iterator i = instances.find(p); @@ -316,7 +324,8 @@ namespace spot unsigned bunop::instance_count() { - return instances.size(); + // Don't count one_star_ since it should not be destroyed. + return instances.size() - !!one_star_; } std::ostream& diff --git a/src/ltlast/bunop.hh b/src/ltlast/bunop.hh index e89ea1c03..98066564c 100644 --- a/src/ltlast/bunop.hh +++ b/src/ltlast/bunop.hh @@ -26,6 +26,7 @@ #include #include #include "refformula.hh" +#include "constant.hh" namespace spot { @@ -116,6 +117,18 @@ namespace spot /// Dump all instances. For debugging. static std::ostream& dump_instances(std::ostream& os); + /// \brief Return a formula for 1[*]. + /// + /// A global instance is returned, and it should not be + /// destroyed. Remember to clone it if you use it to build a + /// formula. + static formula* one_star() + { + if (!one_star_) + one_star_ = instance(Star, constant::true_instance()); + return one_star_; + } + protected: typedef std::pair pairu; typedef std::pair pairo; @@ -131,6 +144,7 @@ namespace spot formula* child_; unsigned min_; unsigned max_; + static formula* one_star_; }; /// \brief Cast \a f into a bunop. diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 3c34eef94..8a9d35bd3 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -27,6 +27,7 @@ #include #include "multop.hh" #include "constant.hh" +#include "bunop.hh" #include "visitor.hh" namespace spot @@ -300,7 +301,7 @@ namespace spot weak_abs = 0; break; case AndRat: - neutral = 0; /* FIXME: we should use 1[*] as neutral */ + neutral = bunop::one_star(); neutral2 = 0; abs = constant::false_instance(); abs2 = 0; @@ -325,7 +326,7 @@ namespace spot case OrRat: neutral = constant::false_instance(); neutral2 = 0; - abs = 0; // FIXME: should be 1[*]. + abs = bunop::one_star(); abs2 = 0; weak_abs = 0; gather_bool(v, Or); @@ -409,7 +410,7 @@ namespace spot for (i = v->begin(); i != v->end(); ++i) (*i)->destroy(); delete v; - return abs; + return abs->clone(); } else { @@ -469,7 +470,7 @@ namespace spot { delete v; assert(neutral != 0); - return neutral; + return neutral->clone(); } else if (s == 1) { diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index 291f72bed..11dc11219 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -101,9 +101,11 @@ namespace spot /// 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] + /// - AndRat(Exps1...,1[*],Exps2...) = AndRat(Exps1...,Exps2...) /// - OrRat(Exps1...,0,Exps2...) = OrRat(Exps1...,Exps2...) /// - OrRat(Exps1...,BoolExp1,Exps2...,BoolExps2...) = /// OrRat(Exps1...,Exps2...,Or(BoolExp1,BoolExps2...)) + /// - OrRat(Exps1...,1[*],Exps2...) = 1[*] /// - Concat(Exps1...,0,Exps2...) = 0 /// - Concat(Exps1...,[*0],Exps2...) = Concat(Exps1...,Exps2...) /// - Concat(Exp) = Exp diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test index 7e696b142..db079eb61 100755 --- a/src/ltltest/equals.test +++ b/src/ltltest/equals.test @@ -149,6 +149,8 @@ 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&&[*]}!' 'a' +run 0 ../equals '{[*]||a||[*]}!' '{[*]}!' 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