alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/src/ltlvisit/reduce.cc
Alexandre Duret-Lutz 957ba664b7 Get rid of all dynamic_cast<>s while working on LTL formulae. 
They are too slow.

* src/ltlast/formula.hh (opkind, kind, kind_): Use an enum
to indicate the actual kind of the formula.  This way we can
check the kind of a formula without relying on dynamic_cast.
* src/ltlast/atomic_prop.cc, src/ltlast/automatop.cc,
src/ltlast/binop.cc, src/ltlast/bunop.cc, src/ltlast/constant.cc,
src/ltlast/multop.cc, src/ltlast/refformula.cc,
src/ltlast/refformula.hh, src/ltlast/unop.cc: Adjust constructors.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/mark.cc,
src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc,
src/ltlvisit/tostring.cc: Replace all dynamic_cast by a
call to kind() followed by a static_cast.
2012-04-28 09:30:36 +02:00

487 lines
10 KiB
C++
Raw Blame History

// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include "reduce.hh"
#include "basicreduce.hh"
#include "syntimpl.hh"
#include "ltlast/allnodes.hh"
#include <cassert>
#include "lunabbrev.hh"
#include "simpfg.hh"
#include "nenoform.hh"
#include "contain.hh"
namespace spot
{
namespace ltl
{
namespace
{
/////////////////////////////////////////////////////////////////////////
class reduce_visitor: public visitor
{
public:
reduce_visitor(int opt)
: opt_(opt)
{
}
virtual ~reduce_visitor()
{
}
formula*
result() const
{
return result_;
}
void
visit(atomic_prop* ap)
{
formula* f = ap->clone();
result_ = f;
}
void
visit(constant* c)
{
result_ = c;
}
void
visit(bunop* bo)
{
result_ = bunop::instance(bo->op(), recurse(bo->child()),
bo->min(), bo->max());
}
void
visit(unop* uo)
{
result_ = recurse(uo->child());
switch (uo->op())
{
case unop::F:
/* If f is a pure eventuality formula then F(f)=f. */
if (!(opt_ & Reduce_Eventuality_And_Universality)
|| !result_->is_eventual())
result_ = unop::instance(unop::F, result_);
return;
case unop::G:
/* If f is a pure universality formula then G(f)=f. */
if (!(opt_ & Reduce_Eventuality_And_Universality)
|| !result_->is_universal())
result_ = unop::instance(unop::G, result_);
return;
case unop::Not:
case unop::X:
case unop::Finish:
case unop::Closure:
case unop::NegClosure:
result_ = unop::instance(uo->op(), result_);
return;
}
/* Unreachable code. */
assert(0);
}
void
visit(binop* bo)
{
binop::type op = bo->op();
formula* f2 = recurse(bo->second());
if (opt_ & Reduce_Eventuality_And_Universality)
{
/* If b is a pure eventuality formula then a U b = b.
If b is a pure universality formula a R b = b. */
if ((f2->is_eventual() && (op == binop::U))
|| (f2->is_universal() && (op == binop::R)))
{
result_ = f2;
return;
}
}
formula* f1 = recurse(bo->first());
if (opt_ & Reduce_Eventuality_And_Universality)
{
/* If a is a pure eventuality formula then a M b = a & b.
If a is a pure universality formula a W b = a|b. */
if (f1->is_eventual() && (op == binop::M))
{
result_ = multop::instance(multop::And, f1, f2);
return;
}
if (f1->is_universal() && (op == binop::W))
{
result_ = multop::instance(multop::Or, f1, f2);
return;
}
}
/* case of implies */
if (opt_ & Reduce_Syntactic_Implications)
{
switch (op)
{
case binop::Xor:
case binop::Equiv:
case binop::Implies:
case binop::UConcat:
case binop::EConcat:
case binop::EConcatMarked:
return;
case binop::U:
/* a < b => a U b = b */
if (syntactic_implication(f1, f2))
{
result_ = f2;
f1->destroy();
return;
}
/* !b < a => a U b = Fb */
if (syntactic_implication_neg(f2, f1, false))
{
result_ = unop::instance(unop::F, f2);
f1->destroy();
return;
}
/* a < b => a U (b U c) = (b U c) */
/* a < b => a U (b W c) = (b W c) */
if (f2->kind() == formula::BinOp)
{
binop* bo = static_cast<binop*>(f2);
if ((bo->op() == binop::U || bo->op() == binop::W)
&& syntactic_implication(f1, bo->first()))
{
result_ = f2;
f1->destroy();
return;
}
}
break;
case binop::R:
/* b < a => a R b = b */
if (syntactic_implication(f2, f1))
{
result_ = f2;
f1->destroy();
return;
}
/* b < !a => a R b = Gb */
if (syntactic_implication_neg(f2, f1, true))
{
result_ = unop::instance(unop::G, f2);
f1->destroy();
return;
}
if (f2->kind() == formula::BinOp)
{
/* b < a => a R (b R c) = b R c */
/* b < a => a R (b M c) = b M c */
binop* bo = static_cast<binop*>(f2);
if ((bo->op() == binop::R || bo->op() == binop::M)
&& syntactic_implication(bo->first(), f1))
{
result_ = f2;
f1->destroy();
return;
}
/* a < b => a R (b R c) = a R c */
if (bo->op() == binop::R
&& syntactic_implication(f1, bo->first()))
{
result_ = binop::instance(binop::R, f1,
bo->second()->clone());
f2->destroy();
return;
}
}
break;
case binop::W:
/* a < b => a W b = b */
if (syntactic_implication(f1, f2))
{
result_ = f2;
f1->destroy();
return;
}
/* !b < a => a W b = 1 */
if (syntactic_implication_neg(f2, f1, false))
{
result_ = constant::true_instance();
f1->destroy();
f2->destroy();
return;
}
/* a < b => a W (b W c) = (b W c) */
if (f2->kind() == formula::BinOp)
{
binop* bo = static_cast<binop*>(f2);
if (bo->op() == binop::W
&& syntactic_implication(f1, bo->first()))
{
result_ = f2;
f1->destroy();
return;
}
}
break;
case binop::M:
/* b < a => a M b = b */
if (syntactic_implication(f2, f1))
{
result_ = f2;
f1->destroy();
return;
}
/* b < !a => a M b = 0 */
if (syntactic_implication_neg(f2, f1, true))
{
result_ = constant::false_instance();
f1->destroy();
f2->destroy();
return;
}
if (f2->kind() == formula::BinOp)
{
/* b < a => a M (b M c) = b M c */
binop* bo = static_cast<binop*>(f2);
if (bo->op() == binop::M
&& syntactic_implication(bo->first(), f1))
{
result_ = f2;
f1->destroy();
return;
}
/* a < b => a M (b M c) = a M c */
/* a < b => a M (b R c) = a M c */
if ((bo->op() == binop::M || bo->op() == binop::R)
&& syntactic_implication(f1, bo->first()))
{
result_ = binop::instance(binop::M, f1,
bo->second()->clone());
f2->destroy();
return;
}
}
break;
}
}
result_ = binop::instance(op, f1, f2);
}
void
visit(automatop*)
{
assert(0);
}
void
visit(multop* mo)
{
unsigned mos = mo->size();
multop::vec* res = new multop::vec;
for (unsigned i = 0; i < mos; ++i)
res->push_back(recurse(mo->nth(i)));
if ((opt_ & Reduce_Syntactic_Implications)
&& (mo->op() != multop::Concat))
{
bool removed = true;
multop::vec::iterator f1;
multop::vec::iterator f2;
while (removed)
{
removed = false;
f2 = f1 = res->begin();
++f1;
while (f1 != res->end())
{
assert(f1 != f2);
// a < b => a + b = b
// a < b => a & b = a
if ((syntactic_implication(*f1, *f2) && // f1 < f2
(mo->op() == multop::Or)) ||
((syntactic_implication(*f2, *f1)) && // f2 < f1
(mo->op() == multop::And)))
{
// We keep f2
(*f1)->destroy();
res->erase(f1);
removed = true;
break;
}
else if ((syntactic_implication(*f2, *f1) && // f2 < f1
(mo->op() == multop::Or)) ||
((syntactic_implication(*f1, *f2)) && // f1 < f2
(mo->op() == multop::And)))
{
// We keep f1
(*f2)->destroy();
res->erase(f2);
removed = true;
break;
}
else
++f1;
}
}
/* f1 < !f2 => f1 & f2 = false
!f1 < f2 => f1 | f2 = true */
for (f1 = res->begin(); f1 != res->end(); f1++)
for (f2 = res->begin(); f2 != res->end(); f2++)
if (f1 != f2 &&
syntactic_implication_neg(*f1, *f2,
mo->op() != multop::Or))
{
for (multop::vec::iterator j = res->begin();
j != res->end(); j++)
(*j)->destroy();
res->clear();
delete res;
if (mo->op() == multop::Or)
result_ = constant::true_instance();
else
result_ = constant::false_instance();
return;
}
}
if (!res->empty())
{
result_ = multop::instance(mo->op(), res);
return;
}
assert(0);
}
formula*
recurse(formula* f)
{
return reduce(f, opt_);
}
protected:
formula* result_;
int opt_;
};
} // anonymous
formula*
reduce(const formula* f, int opt)
{
formula* f1;
formula* f2;
formula* prev = 0;
int n = 0;
while (f != prev)
{
++n;
assert(n < 100);
if (prev)
{
prev->destroy();
prev = const_cast<formula*>(f);
}
else
{
prev = f->clone();
}
f1 = unabbreviate_logic(f);
f2 = simplify_f_g(f1);
f1->destroy();
f1 = negative_normal_form(f2);
f2->destroy();
f2 = f1;
if (opt & Reduce_Basics)
{
f1 = basic_reduce(f2);
f2->destroy();
f2 = f1;
}
if (opt & (Reduce_Syntactic_Implications
| Reduce_Eventuality_And_Universality))
{
reduce_visitor v(opt);
f2->accept(v);
f1 = v.result();
f2->destroy();
f2 = f1;
}
if (opt & (Reduce_Containment_Checks
| Reduce_Containment_Checks_Stronger))
{
formula* f1 =
reduce_tau03(f2,
opt & Reduce_Containment_Checks_Stronger);
f2->destroy();
f2 = f1;
}
f = f2;
}
prev->destroy();
return const_cast<formula*>(f);
}
bool
is_eventual(const formula* f)
{
return f->is_eventual();
}
bool
is_universal(const formula* f)
{
return f->is_universal();
}
}
}
Reference in a new issue View git blame Copy permalink