Commit 0f11e5fe authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Speedup mark_concat_ops() and simplify_mark() with a cache.

* src/ltlvisit/mark.hh, src/ltlvisit/mark.cc (mark_concat_ops,
simplify_mark): Rewrite these two functions as methods of
(mark_tools): this new class.
* src/ltlast/binop.cc, src/ltlast/unop.cc: Adjust computation
of not_marked to ignore marked operators that are not at
the top-level.  I.e., something like X(!{a}) is not marked.
* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::mt): New
instance of mark_tools.
(formula_canonizer::translate) Adjust calls to
mark_concat_ops() and simplify_mark().
parent f68f639e
......@@ -106,9 +106,8 @@ namespace spot
is.accepting_eword = false;
break;
case EConcatMarked:
is.not_marked = false;
// fall through
case EConcat:
is.not_marked = (op != EConcatMarked);
is.ltl_formula = false;
is.boolean = false;
is.eltl_formula = false;
......@@ -130,11 +129,11 @@ namespace spot
is.syntactic_obligation = second->is_syntactic_guarantee();
is.syntactic_recurrence = second->is_syntactic_guarantee();
}
assert(first->is_sere_formula());
assert(second->is_psl_formula());
break;
case UConcat:
is.not_marked = true;
is.ltl_formula = false;
is.boolean = false;
is.eltl_formula = false;
......@@ -156,11 +155,11 @@ namespace spot
is.syntactic_obligation = second->is_syntactic_safety();
is.syntactic_persistence = second->is_syntactic_safety();
}
assert(first->is_sere_formula());
assert(second->is_psl_formula());
break;
case U:
is.not_marked = true;
// f U g is universal if g is eventual, or if f == 1.
is.eventual = second->is_eventual();
is.eventual |= (first == constant::true_instance());
......@@ -181,6 +180,7 @@ namespace spot
// is.syntactic_persistence = Persistence U Persistance
break;
case W:
is.not_marked = true;
// f W g is universal if f and g are, or if g == 0.
is.universal |= (second == constant::false_instance());
is.boolean = false;
......@@ -200,6 +200,7 @@ namespace spot
break;
case R:
is.not_marked = true;
// g R f is universal if f is universal, or if g == 0.
is.universal = second->is_universal();
is.universal |= (first == constant::false_instance());
......@@ -220,6 +221,7 @@ namespace spot
break;
case M:
is.not_marked = true;
// g M f is eventual if both g and f are eventual, or if f == 1.
is.eventual |= (second == constant::true_instance());
is.boolean = false;
......
......@@ -39,6 +39,7 @@ namespace spot
switch (op)
{
case Not:
is.not_marked = true;
is.eventual = child->is_universal();
is.universal = child->is_eventual();
is.in_nenoform = (child->kind() == AtomicProp);
......@@ -53,6 +54,7 @@ namespace spot
is.accepting_eword = false;
break;
case X:
is.not_marked = true;
is.boolean = false;
is.X_free = false;
is.eltl_formula = false;
......@@ -65,6 +67,7 @@ namespace spot
is.accepting_eword = false;
break;
case F:
is.not_marked = true;
is.boolean = false;
is.eltl_formula = false;
is.sere_formula = false;
......@@ -79,6 +82,7 @@ namespace spot
is.accepting_eword = false;
break;
case G:
is.not_marked = true;
is.boolean = false;
is.eltl_formula = false;
is.sere_formula = false;
......@@ -93,6 +97,7 @@ namespace spot
is.accepting_eword = false;
break;
case Finish:
is.not_marked = true;
is.boolean = false;
is.ltl_formula = false;
is.psl_formula = false;
......@@ -120,6 +125,7 @@ namespace spot
is.accepting_eword = false;
break;
case Closure:
is.not_marked = true;
is.boolean = false;
is.ltl_formula = false;
is.eltl_formula = false;
......
......@@ -22,6 +22,8 @@
#include "ltlast/allnodes.hh"
#include <cassert>
#include <algorithm>
#include "ltlvisit/tostring.hh"
#include "misc/casts.hh"
namespace spot
{
......@@ -32,11 +34,11 @@ namespace spot
class simplify_mark_visitor : public visitor
{
formula* result_;
bool has_mark_;
mark_tools* tools_;
public:
simplify_mark_visitor()
: has_mark_(false)
simplify_mark_visitor(mark_tools* t)
: tools_(t)
{
}
......@@ -50,12 +52,6 @@ namespace spot
return result_;
}
bool
has_mark()
{
return has_mark_;
}
void
visit(atomic_prop* ao)
{
......@@ -77,22 +73,7 @@ namespace spot
void
visit(unop* uo)
{
switch (uo->op())
{
case unop::NegClosure:
has_mark_ = true;
/* fall through */
case unop::Finish:
case unop::Closure:
case unop::Not:
case unop::X:
case unop::F:
case unop::G:
result_ = uo->clone();
return;
}
/* Unreachable code. */
assert(0);
result_ = uo->clone();
}
void
......@@ -150,7 +131,6 @@ namespace spot
case binop::EConcatMarked:
EMpairs.insert(std::make_pair(bo->first(),
bo->second()));
has_mark_ = true;
break;
}
}
......@@ -174,33 +154,13 @@ namespace spot
void
visit(binop* bo)
{
switch (bo->op())
{
case binop::EConcatMarked:
has_mark_ = true;
/* fall through */
case binop::Xor:
case binop::Implies:
case binop::Equiv:
case binop::U:
case binop::W:
case binop::M:
case binop::R:
case binop::EConcat:
case binop::UConcat:
result_ = bo->clone();
return;
}
/* Unreachable code. */
assert(0);
result_ = bo->clone();
}
formula*
recurse(const formula* f)
recurse(formula* f)
{
formula* g = f->clone();
has_mark_ |= simplify_mark(g);
return g;
return tools_->simplify_mark(f);
}
};
......@@ -208,8 +168,11 @@ namespace spot
class mark_visitor : public visitor
{
formula* result_;
mark_tools* tools_;
public:
mark_visitor()
mark_visitor(mark_tools* t)
: tools_(t)
{
}
~mark_visitor()
......@@ -294,28 +257,74 @@ namespace spot
formula*
recurse(formula* f)
{
return mark_concat_ops(f);
return tools_->mark_concat_ops(f);
}
};
}
mark_tools::mark_tools()
: simpvisitor_(new simplify_mark_visitor(this)),
markvisitor_(new mark_visitor(this))
{
}
mark_tools::~mark_tools()
{
delete simpvisitor_;
delete markvisitor_;
{
f2f_map::iterator i = simpmark_.begin();
f2f_map::iterator end = simpmark_.end();
while (i != end)
{
f2f_map::iterator old = i++;
old->second->destroy();
old->first->destroy();
}
}
{
f2f_map::iterator i = markops_.begin();
f2f_map::iterator end = markops_.end();
while (i != end)
{
f2f_map::iterator old = i++;
old->second->destroy();
old->first->destroy();
}
}
}
formula*
mark_concat_ops(const formula* f)
mark_tools::mark_concat_ops(const formula* f)
{
mark_visitor v;
const_cast<formula*>(f)->accept(v);
return v.result();
f2f_map::iterator i = markops_.find(f);
if (i != markops_.end())
return i->second->clone();
const_cast<formula*>(f)->accept(*markvisitor_);
formula* r = down_cast<mark_visitor*>(markvisitor_)->result();
markops_[f->clone()] = r->clone();
return r;
}
bool
simplify_mark(formula*& f)
formula*
mark_tools::simplify_mark(const formula* f)
{
simplify_mark_visitor v;
const_cast<formula*>(f)->accept(v);
f->destroy();
f = v.result();
return v.has_mark();
if (!f->is_marked())
return f->clone();
f2f_map::iterator i = simpmark_.find(f);
if (i != simpmark_.end())
return i->second->clone();
const_cast<formula*>(f)->accept(*simpvisitor_);
formula* r = down_cast<simplify_mark_visitor*>(simpvisitor_)->result();
simpmark_[f->clone()] = r->clone();
return r;
}
}
......
// Copyright (C) 2010 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -23,18 +23,35 @@
#include "ltlast/formula.hh"
#include "ltlast/visitor.hh"
#include "misc/hash.hh"
namespace spot
{
namespace ltl
{
/// \brief Mark operators UConcat and EConcat.
/// \ingroup ltl_rewriting
///
/// \param f The formula to rewrite.
formula* mark_concat_ops(const formula* f);
class mark_tools
{
public:
/// \brief Mark operators UConcat and EConcat.
/// \ingroup ltl_rewriting
///
/// \param f The formula to rewrite.
formula* mark_concat_ops(const formula* f);
formula* simplify_mark(const formula* f);
mark_tools();
~mark_tools();
private:
typedef Sgi::hash_map<const formula*, const formula*,
ptr_hash<formula> > f2f_map;
f2f_map simpmark_;
f2f_map markops_;
visitor* simpvisitor_;
visitor* markvisitor_;
};
bool simplify_mark(formula*& f);
}
}
......
......@@ -108,6 +108,7 @@ namespace spot
bdd_dict* dict;
ltl_simplifier* ls;
mark_tools mt;
typedef bdd_dict::fv_map fv_map;
typedef bdd_dict::vf_map vf_map;
......@@ -1760,7 +1761,11 @@ namespace spot
// Handle a Miyano-Hayashi style unrolling for
// rational operators. Marked nodes correspond to
// subformulae in the Miyano-Hayashi set.
if (simplify_mark(dest))
formula* tmp = d_.mt.simplify_mark(dest);
dest->destroy();
dest = tmp;
if (dest->is_marked())
{
// Make the promise that we will exit marked sets.
int a =
......@@ -1772,7 +1777,7 @@ namespace spot
// We have no marked operators, but still
// have other rational operator to check.
// Start a new marked cycle.
formula* dest2 = mark_concat_ops(dest);
formula* dest2 = d_.mt.mark_concat_ops(dest);
dest->destroy();
dest = dest2;
}
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment