From e6e85999de9647f3c58a13e27aa7af47931d0da6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 7 Feb 2012 15:36:18 +0100 Subject: [PATCH] Add new simplification rules like: "a | (Xa R b)" gives "b U a". * src/ltlvisit/simplify.cc: Add new rules. * doc/tl/tl.tex: Document them. * src/ltltest/reduccmp.test: Add test cases. --- doc/tl/tl.tex | 15 ++-- src/ltltest/reduccmp.test | 11 +++ src/ltlvisit/simplify.cc | 145 ++++++++++++++++++++++++++++++++++++-- 3 files changed, 159 insertions(+), 12 deletions(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index a53110e64..1f2a1526f 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -559,7 +559,7 @@ is usually used to simplify proofs. \G f &\equiv \NOT\F\NOT f \equiv \NOT((\NOT f)\M\1)\\ f\U g&\equiv ((\X g)\M f)\OR g \\ f \W g&\equiv (f\U g)\OR \G f \equiv ((\X g)\M f)\OR g\OR \NOT((\NOT f)\M\1)\\ - f \R g&\equiv (f \M g)\OR\G f \equiv (f \M g)\OR \NOT((\NOT f)\M\1) + f \R g&\equiv (f \M g)\OR\G g \equiv (f \M g)\OR \NOT((\NOT g)\M\1) \end{align*}} \ltltodo[noline]{Why do we have two ways to rewrite $f\W g$ with $\U$, and two ways to rewrite $f\M g$ with $\R$, but no similar rules for other operators? What are we missing?} @@ -571,10 +571,9 @@ successively rewrite $\U\to\M\to\R\to\U$ we get \begin{align*} f\U g &\equiv ((\X g)\M f)\OR g \\ &\equiv (((\X g) \R f)\AND\NOT (\0\R\NOT \X g))\OR g \\ - &\equiv (((f \U (\X g\AND f))\OR\NOT(\1\U\NOT f)) \AND\NOT (\underbrace{((\X g) \U -\0)}_{\text{trivially false}}\OR\NOT(\1\U\NOT\X g)))\OR g\\ - &\equiv (((f \U (\X g\AND f))\OR\NOT(\1\U\NOT f)) - \AND(\1\U\NOT\X g))\OR g\\ + &\equiv (((f \U (\X g\AND f))\OR\NOT(\1\U\NOT f)) \AND\NOT (\underbrace{((\NOT\X g) \U +(\0\AND \NOT\X g))}_{\text{trivially false}}\OR\NOT(\1\U\NOT\NOT\X g)))\OR g\\ + &\equiv (((f \U (\X g\AND f))\OR\NOT(\1\U\NOT f)) \AND(\1\U\X g))\OR g\\ \end{align*} @@ -1382,7 +1381,11 @@ $\OR$): (\F f)\AND (f \R g)&\equiv f\M g & (\G g)\OR (f \R g)&\equiv f\R g \\ (\F f)\AND (f \M g)&\equiv f\M g & - (\G g)\OR (f \M g)&\equiv f\R g + (\G g)\OR (f \M g)&\equiv f\R g \\ + f \AND ((\X f) \W g) &\equiv g \R f & + f \OR ((\X f) \R g) &\equiv g \W f \\ + f \AND ((\X f) \U g) &\equiv g \M f & + f \OR ((\X f) \M g) &\equiv g \U f \\ \end{align*} The above rules are applied even if more terms are presents in the operator's arguments. For instance $\F\G(a)\AND \G(b) \AND \F\G(c) \AND diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index 91b6f1656..75246b4a7 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -181,6 +181,17 @@ for x in ../reduccmp ../reductaustr; do run 0 $x 'a|b|c|X(F(a|b)|F(c)|Gd)' 'F(a|b|c)|XGd' run 0 $x 'b|c|X(F(a|b)|F(c)|Gd)' 'b|c|X(F(a|b|c)|Gd)' + run 0 $x 'a | (Xa R b) | c' '(b W a) | c' + run 0 $x 'a | (Xa M b) | c' '(b U a) | c' + run 0 $x 'a | (Xa M b) | (Xa R c)' '(b U a) | (c W a)' + run 0 $x 'a | (Xa M b) | XF(a)' 'Fa' + run 0 $x 'a | (Xa R b) | XF(a)' '(b W a) | Fa' # Gb | Fa ? + run 0 $x 'a & (Xa W b) & c' '(b R a) & c' + run 0 $x 'a & (Xa U b) & c' '(b M a) & c' + run 0 $x 'a & (Xa W b) & (Xa U c)' '(b R a) & (c M a)' + run 0 $x 'a & (Xa W b) & XGa' 'Ga' + run 0 $x 'a & (Xa U b) & XGa' '(b M a) & Ga' # Fb & Ga ? + # Syntactic implication run 0 $x '(a & b) R (a R c)' '(a & b)R c' run 0 $x 'a R ((a & b) R c)' '(a & b)R c' diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 80bcdf1b3..6fdbb0381 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -754,6 +754,40 @@ namespace spot return is_binop(f, binop::W); } + // X(a) R b or X(a) M b + // This returns a. + formula* + is_XRM(formula* f) + { + if (f->kind() != formula::BinOp) + return 0; + binop* bo = static_cast(f); + binop::type t = bo->op(); + if (t != binop::R && t != binop::M) + return 0; + unop* uo = is_X(bo->first()); + if (!uo) + return 0; + return uo->child(); + } + + // X(a) W b or X(a) U b + // This returns a. + formula* + is_XWU(formula* f) + { + if (f->kind() != formula::BinOp) + return 0; + binop* bo = static_cast(f); + binop::type t = bo->op(); + if (t != binop::W && t != binop::U) + return 0; + unop* uo = is_X(bo->first()); + if (!uo) + return 0; + return uo->child(); + } + multop* is_multop(formula* f, multop::type op) { @@ -1870,20 +1904,35 @@ namespace spot if (!mo->is_sere_formula()) { // a & X(G(a&b...) & c...) = Ga & X(G(b...) & c...) + // a & (Xa W b) = b R a + // a & (Xa U b) = b M a if (!mo->is_X_free()) { typedef Sgi::hash_set > fset_t; - fset_t xgset; - fset_t xset; + typedef Sgi::hash_map, + ptr_hash > fmap_t; + fset_t xgset; // XG(...) + fset_t xset; // X(...) + fmap_t wuset; // (X...)W(...) or (X...)U(...) unsigned s = res->size(); + std::vector tokill(s); + // Make a pass to search for subterms // of the form XGa or X(... & G(...&a&...) & ...) for (unsigned n = 0; n < s; ++n) { if (!(*res)[n]) continue; + + formula* xarg = is_XWU((*res)[n]); + if (xarg) + { + wuset[xarg].insert(n); + continue; + } + unop* uo = is_X((*res)[n]); if (!uo) continue; @@ -1930,7 +1979,38 @@ namespace spot (*res)[n]->destroy(); (*res)[n] = 0; } - // Make second pass to search for terms 'a' + // Make a second pass to check if the "a" + // terms can be used to simplify "Xa W b" or + // "Xa U b". + for (unsigned n = 0; n < s; ++n) + { + if (!(*res)[n]) + continue; + fmap_t::const_iterator gs = + wuset.find((*res)[n]); + if (gs == wuset.end()) + continue; + + const std::set& s = gs->second; + std::set::const_iterator g; + for (g = s.begin(); g != s.end(); ++g) + { + // a & (Xa W b) = b R a + // a & (Xa U b) = b M a + unsigned pos = *g; + binop* wu = down_cast((*res)[pos]); + binop::type t = (wu->op() == binop::U) + ? binop::M : binop::R; + unop* xa = down_cast(wu->first()); + formula* a = xa->child()->clone(); + formula* b = wu->second()->clone(); + wu->destroy(); + (*res)[pos] = binop::instance(t, b, a); + // Remember to kill "a". + tokill[n] = true; + } + } + // Make third pass to search for terms 'a' // that also appears as 'XGa'. Replace them // by 'Ga' and delete XGa. for (unsigned n = 0; n < s; ++n) @@ -1947,6 +2027,11 @@ namespace spot gf->destroy(); (*res)[n] = unop::instance(unop::G, x); } + else if (tokill[n]) + { + (*res)[n]->destroy(); + (*res)[n] = 0; + } } multop::vec* xv = new multop::vec; @@ -2471,21 +2556,36 @@ namespace spot } case multop::Or: { - // a | X(F(a|b...) | c...) = Fa | X(F(b...) | c...) + // a | X(F(a) | c...) = Fa | X(c...) + // a | (Xa R b) = b W a + // a | (Xa M b) = b U a if (!mo->is_X_free()) { typedef Sgi::hash_set > fset_t; - fset_t xfset; - fset_t xset; + typedef Sgi::hash_map, + ptr_hash > fmap_t; + fset_t xfset; // XF(...) + fset_t xset; // X(...) + fmap_t rmset; // (X...)R(...) or (X...)M(...) unsigned s = res->size(); + std::vector tokill(s); + // Make a pass to search for subterms // of the form XFa or X(... | F(...|a|...) | ...) for (unsigned n = 0; n < s; ++n) { if (!(*res)[n]) continue; + + formula* xarg = is_XRM((*res)[n]); + if (xarg) + { + rmset[xarg].insert(n); + continue; + } + unop* uo = is_X((*res)[n]); if (!uo) continue; @@ -2544,6 +2644,29 @@ namespace spot if (f != xfset.end()) --allofthem; assert(allofthem != -1U); + // At the same time, check if "a" can also + // be used to simplify "Xa R b" or "Xa M b". + fmap_t::const_iterator gs = rmset.find(x); + if (gs == rmset.end()) + continue; + const std::set& s = gs->second; + std::set::const_iterator g; + for (g = s.begin(); g != s.end(); ++g) + { + // a | (Xa R b) = b W a + // a | (Xa M b) = b U a + unsigned pos = *g; + binop* rm = down_cast((*res)[pos]); + binop::type t = + (rm->op() == binop::M) ? binop::U : binop::W; + unop* xa = down_cast(rm->first()); + formula* a = xa->child()->clone(); + formula* b = rm->second()->clone(); + rm->destroy(); + (*res)[pos] = binop::instance(t, b, a); + // Remember to kill "a". + tokill[n] = true; + } } // If we can remove all of them... if (allofthem == 0) @@ -2563,8 +2686,18 @@ namespace spot xfset.erase(f); ff->destroy(); (*res)[n] = unop::instance(unop::F, x); + // We don't need to kill "a" anymore. + tokill[n] = false; } } + // Kill any remaining "a", used to simplify Xa R b + // or Xa M b. + for (unsigned n = 0; n < s; ++n) + if (tokill[n] && (*res)[n]) + { + (*res)[n]->destroy(); + (*res)[n] = 0; + } // Now rebuild the formula that remains. multop::vec* xv = new multop::vec;