From 2140256004be7dae6bfabc343f0d669474da856f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 5 Mar 2010 23:16:01 +0100 Subject: [PATCH] Simplify F(a)|F(b) as F(a|b). Add similar rule for G(a)&G(b). * src/ltlvisit/basicreduce.cc (basic_reduce_visitor): Replace the FG(a)|FG(b) == FG(a|b) rule by the above more generic one. Add the dual rule for G(a)&G(b), as we had none (this one won't improve anything in the translation, but it is more symmetric this way). Also simplify some pointer checks. --- ChangeLog | 10 ++++++++ src/ltlvisit/basicreduce.cc | 46 +++++++++++++++++++++++++------------ 2 files changed, 41 insertions(+), 15 deletions(-) diff --git a/ChangeLog b/ChangeLog index 4c5c13af0..7b5112f4d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,13 @@ +2010-03-05 Alexandre Duret-Lutz + + Simplify F(a)|F(b) as F(a|b). Add similar rule for G(a)&G(b). + + * src/ltlvisit/basicreduce.cc (basic_reduce_visitor): Replace + the FG(a)|FG(b) == FG(a|b) rule by the above more generic one. + Add the dual rule for G(a)&G(b), as we had none (this one won't + improve anything in the translation, but it is more symmetric + this way). Also simplify some pointer checks. + 2010-03-05 Alexandre Duret-Lutz Better selection of the acceptance of the initial state in SBA. diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc index 22fae745c..d5175a7da 100644 --- a/src/ltlvisit/basicreduce.cc +++ b/src/ltlvisit/basicreduce.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004, 2007 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -305,7 +305,9 @@ namespace spot multop::vec* tmpU = new multop::vec; multop::vec* tmpR = new multop::vec; multop::vec* tmpFG = new multop::vec; + multop::vec* tmpF = new multop::vec; multop::vec* tmpGF = new multop::vec; + multop::vec* tmpG = new multop::vec; multop::vec* tmpOther = new multop::vec; @@ -326,7 +328,7 @@ namespace spot binop* bo = dynamic_cast(*i); if (uo) { - if (uo && uo->op() == unop::X) + if (uo->op() == unop::X) { // Xa & Xb = X(a & b) tmpX->push_back(uo->child()->clone()); @@ -337,6 +339,11 @@ namespace spot unop* uo2 = dynamic_cast(uo->child()); tmpFG->push_back(uo2->child()->clone()); } + else if (uo->op() == unop::G) + { + // G(a) | G(b) = G(a | b) + tmpG->push_back(uo->child()->clone()); + } else { tmpOther->push_back((*i)->clone()); @@ -416,10 +423,6 @@ namespace spot } (*i)->destroy(); } - - delete tmpGF; - tmpGF = 0; - break; case multop::Or: @@ -432,7 +435,7 @@ namespace spot binop* bo = dynamic_cast(*i); if (uo) { - if (uo && uo->op() == unop::X) + if (uo->op() == unop::X) { // Xa | Xb = X(a | b) tmpX->push_back(uo->child()->clone()); @@ -443,10 +446,10 @@ namespace spot unop* uo2 = dynamic_cast(uo->child()); tmpGF->push_back(uo2->child()->clone()); } - else if (is_FG(*i)) + else if (uo->op() == unop::F) { - // FG(a) | FG(b) = F(Ga | Gb) - tmpFG->push_back(uo->child()->clone()); + // F(a) | F(b) = F(a | b) + tmpF->push_back(uo->child()->clone()); } else { @@ -540,19 +543,32 @@ namespace spot else delete tmpX; + if (!tmpF->empty()) + tmpOther->push_back(unop::instance(unop::F, + multop::instance(mo->op(), + tmpF))); + else + delete tmpF; - if (tmpU && !tmpU->empty()) + if (!tmpG->empty()) + tmpOther->push_back(unop::instance(unop::G, + multop::instance(mo->op(), + tmpG))); + else + delete tmpG; + + if (!tmpU->empty()) tmpOther->push_back(multop::instance(mo->op(), tmpU)); else delete tmpU; - if (tmpR && !tmpR->empty()) + if (!tmpR->empty()) tmpOther->push_back(multop::instance(mo->op(), tmpR)); else delete tmpR; - if (tmpGF && !tmpGF->empty()) + if (!tmpGF->empty()) { formula* ftmp = unop::instance(unop::G, @@ -565,7 +581,7 @@ namespace spot delete tmpGF; - if (tmpFG && !tmpFG->empty()) + if (!tmpFG->empty()) { formula* ftmp = 0; if (mo->op() == multop::And)