alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Massage the AST so that identical sub-formula share the same

Browse source 
reference-counted formula*.  One can't call constructors for AST
items anymore, everything need to be acquired through instance()
class methods.

* src/ltlast/formula.cc, src/ltlast/refformula.cc,
src/ltlast/refformula.hh: New files.
* src/ltlast/Makefile.am (libltlast_la_SOURCES): Add them.
* src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
src/ltlast/unop.cc, src/ltlast/unop.hh,
src/ltlast/binop.cc, src/ltlast/binop.hh: Make the constructor
and destructor protected.  Define a static function `instance()'
to get an instance with specific argument.  Use a map called
`instances' to store all known instances.  Inherit from
ref_formula.
* src/ltlast/constant.hh, src/ltlast/constant.cc: Protect
the constructor and destructor.  Provide the false_instance()
and true_instance() functions instead.
* src/formula.hh (ref, unref, ref_, unref_): New methods.
* src/ltlast/multop.cc, src/ltlast/multop.hh: Protect
the constructor, destructor, as well as the add() method.
Provides the instance(), and add() class methods instead.
Store children_ as a pointer.
* src/ltlenv/defaultenv.cc (require): Adjust to
call atomic_prop::instance.
* src/ltlparse/ltlparse.yy: Adjust to call instance() functions
instead of constructors.
* src/ltltest/Makefile.am (LDADD): Tweak library ordering.
* src/ltlvisit/clone.hh (clone_visitor): Inherit from visitor,
not const_visitor, and adjust all prototypes appropriately.
* src/ltlvisit/clone.cc (clone_visitor): Likewise.
Call ref() or instance() methods instead of copy constructors.
* src/ltlvisit/equals.cc: Simplify atomic_prop and constant
cases.
* src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc,
src/ltlvisit/tunabbrev.hh, src/ltlvisit/tunabbrev.cc,
src/ltlvisit/nenoform.hh, src/ltlvisit/nenoform.cc: Use instance()
methods instead of constructor.  Make these children of visitor, not
const_visitor.
* src/ltltest/readltl.c (main): Do not delete the formula.
This commit is contained in:
Alexandre Duret-Lutz 2003-05-15 13:39:39 +00:00
parent f1838ab8ef
commit 5f6d8b6234
29 changed files with 548 additions and 253 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ltlast/Makefile.am
View file

@ -11,10 +11,12 @@ libltlast_la_SOURCES = \
constant.cc \
constant.hh \
formula.hh \
formula.cc \
multop.cc \
multop.hh \
predecl.hh \
refformula.cc \
refformula.hh \
unop.cc \
unop.hh \
visitor.hh

28
src/ltlast/atomic_prop.cc
View file

@ -5,7 +5,7 @@ namespace spot
{
namespace ltl
{
atomic_prop::atomic_prop(const std::string& name, environment& env)
: name_(name), env_(&env)
{
@ -15,29 +15,45 @@ namespace spot
{
}
void
void
atomic_prop::accept(visitor& v)
{
v.visit(this);
}
void
atomic_prop::accept(const_visitor& v) const
{
v.visit(this);
}
}
const std::string&
atomic_prop::name() const
{
return name_;
}
environment&
environment&
atomic_prop::env() const
{
return *env_;
}
atomic_prop::map atomic_prop::instances;
atomic_prop*
atomic_prop::instance(const std::string& name, environment& env)
{
pair p(name, &env);
map::iterator i = instances.find(p);
if (i != instances.end())
{
return static_cast<atomic_prop*>(i->second->ref());
}
atomic_prop* ap = new atomic_prop(name, env);
instances[p] = ap;
return static_cast<atomic_prop*>(ap->ref());
}
}
}

18
src/ltlast/atomic_prop.hh
View file

@ -2,7 +2,8 @@
# define SPOT_LTLAST_ATOMIC_PROP_HH
#include <string>
#include "formula.hh"
#include <map>
#include "refformula.hh"
#include "ltlenv/environment.hh"
namespace spot
@ -11,13 +12,12 @@ namespace spot
{
/// Atomic propositions.
class atomic_prop : public formula
class atomic_prop : public ref_formula
{
public:
/// Build an atomic proposition with name \a name in
/// Build an atomic proposition with name \a name in
/// environment \a env.
atomic_prop(const std::string& name, environment& env);
virtual ~atomic_prop();
static atomic_prop* instance(const std::string& name, environment& env);
virtual void accept(visitor& visitor);
virtual void accept(const_visitor& visitor) const;
@ -26,6 +26,14 @@ namespace spot
const std::string& name() const;
/// Get the environment of the atomic proposition.
environment& env() const;
protected:
atomic_prop(const std::string& name, environment& env);
virtual ~atomic_prop();
typedef std::pair<std::string, environment*> pair;
typedef std::map<pair, atomic_prop*> map;
static map instances;
private:
std::string name_;
environment* env_;

25
src/ltlast/binop.cc
View file

@ -5,7 +5,7 @@
namespace spot
{
namespace ltl
{
{
binop::binop(type op, formula* first, formula* second)
: op_(op), first_(first), second_(second)
{
@ -45,19 +45,19 @@ namespace spot
return second_;
}
formula*
formula*
binop::second()
{
return second_;
}
binop::type
binop::type
binop::op() const
{
return op_;
}
const char*
const char*
binop::op_name() const
{
switch (op_)
@ -78,5 +78,22 @@ namespace spot
return 0;
}
binop::map binop::instances;
binop*
binop::instance(type op, formula* first, formula* second)
{
pairf pf(first, second);
pair p(op, pf);
map::iterator i = instances.find(p);
if (i != instances.end())
{
return static_cast<binop*>(i->second->ref());
}
binop* ap = new binop(op, first, second);
instances[p] = ap;
return static_cast<binop*>(ap->ref());
}
}
}

15
src/ltlast/binop.hh
View file

@ -1,6 +1,7 @@
#ifndef SPOT_LTLAST_BINOP_HH
# define SPOT_LTLAST_BINOP_HH
#include <map>
#include "formula.hh"
namespace spot
@ -18,8 +19,9 @@ namespace spot
/// are often nested we represent them as multops.
enum type { Xor, Implies, Equiv, U, R };
binop(type op, formula* first, formula* second);
virtual ~binop();
/// Build an unary operator with operation \a op and
/// children \a first and \a second.
static binop* instance(type op, formula* first, formula* second);
virtual void accept(visitor& v);
virtual void accept(const_visitor& v) const;
@ -38,6 +40,15 @@ namespace spot
/// Get the type of this operator, as a string.
const char* op_name() const;
protected:
typedef std::pair<formula*, formula*> pairf;
typedef std::pair<type, pairf> pair;
typedef std::map<pair, formula*> map;
static map instances;
binop(type op, formula* first, formula* second);
virtual ~binop();
private:
type op_;
formula* first_;

19
src/ltlast/constant.cc
View file

@ -5,7 +5,7 @@
namespace spot
{
namespace ltl
{
{
constant::constant(type val)
: val_(val)
{
@ -27,13 +27,13 @@ namespace spot
v.visit(this);
}
constant::type
constant::type
constant::val() const
{
return val_;
}
const char*
const char*
constant::val_name() const
{
switch (val_)
@ -48,5 +48,18 @@ namespace spot
return 0;
}
constant*
constant::false_instance()
{
static constant f(constant::False);
return &f;
}
constant*
constant::true_instance()
{
static constant t(constant::True);
return &t;
}
}
}

13
src/ltlast/constant.hh
View file

@ -13,10 +13,6 @@ namespace spot
{
public:
enum type { False, True };
constant(type val);
virtual ~constant();
virtual void accept(visitor& v);
virtual void accept(const_visitor& v) const;
@ -25,6 +21,15 @@ namespace spot
/// Return the value of the constant as a string.
const char* val_name() const;
/// Get the sole instance of spot::ltl::constant::constant(True).
static constant* true_instance();
/// Get the sole instance of spot::ltl::constant::constant(False).
static constant* false_instance();
protected:
constant(type val);
virtual ~constant();
private:
type val_;
};

34
src/ltlast/formula.cc Normal file
View file

@ -0,0 +1,34 @@
#include "formula.hh"
namespace spot
{
namespace ltl
{
formula*
formula::ref()
{
ref_();
return this;
}
void
formula::unref(formula* f)
{
if (f->unref_())
delete f;
}
void
formula::ref_()
{
// Not reference counted by default.
}
bool
formula::unref_()
{
// Not reference counted by default.
return false;
}
}
}

22
src/ltlast/formula.hh
View file

@ -3,20 +3,32 @@
#include "predecl.hh"
namespace spot
namespace spot
{
namespace ltl
namespace ltl
{
/// \brief An LTL formula.
///
/// The only way you can work with a formula is to
///
/// The only way you can work with a formula is to
/// build a spot::ltl::visitor or spot::ltl::const_visitor.
class formula
class formula
{
public:
virtual void accept(visitor& v) = 0;
virtual void accept(const_visitor& v) const = 0;
/// \brief clone this formula
formula* ref();
/// \brief release formula
static void unref(formula* f);
protected:
/// \brief increment reference counter if any
virtual void ref_();
/// \brief decrement reference counter if any, return true when
/// the instance must be delete (usually when the counter hits 0).
virtual bool unref_();
};
}

111
src/ltlast/multop.cc
View file

@ -6,42 +6,15 @@
namespace spot
{
namespace ltl
{
multop::multop(type op)
: op_(op)
{
multop::multop(type op, vec* v)
: op_(op), children_(v)
{
}
multop::multop(type op, formula* first, formula* second)
: op_(op)
{
children_.reserve(2);
add(first);
add(second);
}
void
multop::add(formula* f)
{
// If the formula we add is itself a multop for the same operator,
// merge its children with ours.
multop* p = dynamic_cast<multop*>(f);
if (p && p->op() == op())
{
unsigned ps = p->size();
for (unsigned i = 0; i < ps; ++i)
children_.push_back(p->nth(i));
// that sub-formula is now useless
delete f;
}
else
{
children_.push_back(f);
}
}
multop::~multop()
{
delete children_;
}
void
@ -59,28 +32,28 @@ namespace spot
unsigned
multop::size() const
{
return children_.size();
return children_->size();
}
const formula*
multop::nth(unsigned n) const
{
return children_[n];
return (*children_)[n];
}
formula*
formula*
multop::nth(unsigned n)
{
return children_[n];
return (*children_)[n];
}
multop::type
multop::type
multop::op() const
{
return op_;
}
const char*
const char*
multop::op_name() const
{
switch (op_)
@ -95,5 +68,69 @@ namespace spot
return 0;
}
multop::map multop::instances;
multop*
multop::instance(type op, vec* v)
{
pair p(op, v);
map::iterator i = instances.find(p);
if (i != instances.end())
{
delete v;
return static_cast<multop*>(i->second->ref());
}
multop* ap = new multop(op, v);
instances[p] = ap;
return static_cast<multop*>(ap->ref());
}
multop*
multop::instance(type op)
{
return instance(op, new vec);
}
multop*
multop::instance(type op, formula* first, formula* second)
{
vec* v = new vec;
multop::add(op, v, first);
multop::add(op, v, second);
return instance(op, v);
}
multop::vec*
multop::add(type op, vec* v, formula* f)
{
// If the formula we add is itself a multop for the same operator,
// merge its children.
multop* p = dynamic_cast<multop*>(f);
if (p && p->op() == op)
{
unsigned ps = p->size();
for (unsigned i = 0; i < ps; ++i)
v->push_back(p->nth(i));
// that sub-formula is now useless
formula::unref(f);
}
else
{
v->push_back(f);
}
return v;
}
void
multop::add(multop** m, formula* f)
{
vec* v = new vec(*(*m)->children_);
type op = (*m)->op();
multop::add(op, v, f);
formula::unref(*m);
*m = instance(op, v);
}
}
}

33
src/ltlast/multop.hh
View file

@ -2,13 +2,14 @@
# define SPOT_LTLAST_MULTOP_HH
#include <vector>
#include <map>
#include "formula.hh"
namespace spot
{
namespace ltl
{
/// \brief Multi-operand operators.
///
/// These operators are considered commutative and associative.
@ -17,25 +18,29 @@ namespace spot
public:
enum type { Or, And };
/// \brief Build a spot::ltl::multop with no child.
///
/// This has little value unless you call multop::add later.
multop(type op);
static multop* instance(type op);
/// \brief Build a spot::ltl::multop with two children.
///
///
/// If one of the children itself is a spot::ltl::multop
/// with the same type, it will be merged. I.e., children
/// if that child will be added, and that child itself will
/// be destroyed.
multop(type op, formula* first, formula* second);
static multop* instance(type op, formula* first, formula* second);
/// \brief Add another child to this operator.
///
/// If \a f itself is a spot::ltl::multop with the same type, it
/// will be merged. I.e., children of \a f will be added, and
/// that \a f will will be destroyed.
void add(formula* f);
virtual ~multop();
///
/// Note that this function overwrites the supplied ltl::multop pointer.
/// The old value is released and should not be used after this.
static void add(multop** m, formula* f);
virtual void accept(visitor& v);
virtual void accept(const_visitor& v) const;
@ -56,9 +61,21 @@ namespace spot
/// Get the type of this operator, as a string.
const char* op_name() const;
protected:
typedef std::vector<formula*> vec;
typedef std::pair<type, vec*> pair;
typedef std::map<pair, formula*> map;
static map instances;
multop(type op, vec* v);
static multop* instance(type op, vec* v);
static vec* multop::add(type op, vec* v, formula* f);
virtual ~multop();
private:
type op_;
std::vector<formula*> children_;
vec* children_;
};
}

27
src/ltlast/refformula.cc Normal file
View file

@ -0,0 +1,27 @@
#include "refformula.hh"
#include <cassert>
namespace spot
{
namespace ltl
{
ref_formula::ref_formula()
: ref_count_(0)
{
}
void
ref_formula::ref_()
{
++ref_count_;
}
bool
ref_formula::unref_()
{
assert(ref_count_ > 0);
return !--ref_count_;
}
}
}

25
src/ltlast/refformula.hh Normal file
View file

@ -0,0 +1,25 @@
#ifndef SPOT_LTLAST_REFFORMULAE_HH
# define SPOT_LTLAST_REFFORMULAE_HH
#include "formula.hh"
namespace spot
{
namespace ltl
{
/// \brief A reference-counted LTL formula.
class ref_formula : public formula
{
protected:
ref_formula();
void ref_();
bool unref_();
private:
unsigned ref_count_;
};
}
}
#endif // SPOT_LTLAST_REFFORMULAE_HH

22
src/ltlast/unop.cc
View file

@ -5,7 +5,7 @@
namespace spot
{
namespace ltl
{
{
unop::unop(type op, formula* child)
: op_(op), child_(child)
{
@ -39,13 +39,13 @@ namespace spot
return child_;
}
unop::type
unop::type
unop::op() const
{
return op_;
}
const char*
const char*
unop::op_name() const
{
switch (op_)
@ -64,5 +64,21 @@ namespace spot
return 0;
}
unop::map unop::instances;
unop*
unop::instance(type op, formula* child)
{
pair p(op, child);
map::iterator i = instances.find(p);
if (i != instances.end())
{
return static_cast<unop*>(i->second->ref());
}
unop* ap = new unop(op, child);
instances[p] = ap;
return static_cast<unop*>(ap->ref());
}
}
}

16
src/ltlast/unop.hh
View file

@ -1,21 +1,23 @@
#ifndef SPOT_LTLAST_UNOP_HH
# define SPOT_LTLAST_UNOP_HH
#include <map>
#include "formula.hh"
namespace spot
{
namespace ltl
{
/// Unary operator.
class unop : public formula
{
public:
enum type { Not, X, F, G };
unop(type op, formula* child);
virtual ~unop();
/// Build an unary operator with operation \a op and
/// child \a child.
static unop* instance(type op, formula* child);
virtual void accept(visitor& v);
virtual void accept(const_visitor& v) const;
@ -30,6 +32,14 @@ namespace spot
/// Get the type of this operator, as a string.
const char* op_name() const;
protected:
typedef std::pair<type, formula*> pair;
typedef std::map<pair, formula*> map;
static map instances;
unop(type op, formula* child);
virtual ~unop();
private:
type op_;
formula* child_;

4
src/ltlenv/defaultenv.cc
View file

@ -9,7 +9,7 @@ namespace spot
formula*
default_environment::require(const std::string& s)
{
return new atomic_prop(s, *this);
return atomic_prop::instance(s, *this);
}
const std::string&
@ -23,7 +23,7 @@ namespace spot
{
}
default_environment&
default_environment&
default_environment::instance()
{
static default_environment* singleton = new default_environment();

28
src/ltlparse/ltlparse.yy
View file

@ -101,15 +101,15 @@ subformula: ATOMIC_PROP
delete $1;
}
| CONST_TRUE
{ $$ = new constant(constant::True); }
{ $$ = constant::true_instance(); }
| CONST_FALSE
{ $$ = new constant(constant::False); }
{ $$ = constant::false_instance(); }
| PAR_OPEN subformula PAR_CLOSE
{ $$ = $2; }
| PAR_OPEN error PAR_CLOSE
{ error_list.push_back(parse_error(@$,
"treating this parenthetical block as false"));
$$ = new constant(constant::False);
$$ = constant::false_instance();
}
| PAR_OPEN subformula many_errors PAR_CLOSE
{ error_list.push_back(parse_error(@3,
@ -117,27 +117,27 @@ subformula: ATOMIC_PROP
$$ = $2;
}
| OP_NOT subformula
{ $$ = new unop(unop::Not, $2); }
{ $$ = unop::instance(unop::Not, $2); }
| subformula OP_AND subformula
{ $$ = new multop(multop::And, $1, $3); }
{ $$ = multop::instance(multop::And, $1, $3); }
| subformula OP_OR subformula
{ $$ = new multop(multop::Or, $1, $3); }
{ $$ = multop::instance(multop::Or, $1, $3); }
| subformula OP_XOR subformula
{ $$ = new binop(binop::Xor, $1, $3); }
{ $$ = binop::instance(binop::Xor, $1, $3); }
| subformula OP_IMPLIES subformula
{ $$ = new binop(binop::Implies, $1, $3); }
{ $$ = binop::instance(binop::Implies, $1, $3); }
| subformula OP_EQUIV subformula
{ $$ = new binop(binop::Equiv, $1, $3); }
{ $$ = binop::instance(binop::Equiv, $1, $3); }
| subformula OP_U subformula
{ $$ = new binop(binop::U, $1, $3); }
{ $$ = binop::instance(binop::U, $1, $3); }
| subformula OP_R subformula
{ $$ = new binop(binop::R, $1, $3); }
{ $$ = binop::instance(binop::R, $1, $3); }
| OP_F subformula
{ $$ = new unop(unop::F, $2); }
{ $$ = unop::instance(unop::F, $2); }
| OP_G subformula
{ $$ = new unop(unop::G, $2); }
{ $$ = unop::instance(unop::G, $2); }
| OP_X subformula
{ $$ = new unop(unop::X, $2); }
{ $$ = unop::instance(unop::X, $2); }
// | subformula many_errors
// { error_list->push_back(parse_error(@2,
// "ignoring these unexpected trailing tokens"));

4
src/ltltest/Makefile.am
View file

@ -1,8 +1,8 @@
AM_CPPFLAGS = -I$(srcdir)/..
LDADD = ../ltlparse/libltlparse.la \
../ltlvisit/libltlvisit.la \
../ltlast/libltlast.la \
../ltlenv/libltlenv.la
../ltlenv/libltlenv.la \
../ltlast/libltlast.la
check_SCRIPTS = defs
# Keep this sorted alphabetically.

1
src/ltltest/readltl.cc
View file

@ -46,7 +46,6 @@ main(int argc, char** argv)
spot::ltl::dump(*f, std::cout);
std::cout << std::endl;
#endif
delete f;
}
else
{

50
src/ltlvisit/clone.cc
View file

@ -1,7 +1,7 @@
#include "ltlast/allnodes.hh"
#include "clone.hh"
namespace spot
namespace spot
{
namespace ltl
{
@ -18,52 +18,52 @@ namespace spot
{
return result_;
}
void
clone_visitor::visit(const atomic_prop* ap)
void
clone_visitor::visit(atomic_prop* ap)
{
result_ = new atomic_prop(ap->name(), ap->env());
result_ = ap->ref();
}
void
clone_visitor::visit(const constant* c)
void
clone_visitor::visit(constant* c)
{
result_ = new constant(c->val());
result_ = c->ref();
}
void
clone_visitor::visit(const unop* uo)
void
clone_visitor::visit(unop* uo)
{
result_ = new unop(uo->op(), recurse(uo->child()));
result_ = unop::instance(uo->op(), recurse(uo->child()));
}
void
clone_visitor::visit(const binop* bo)
void
clone_visitor::visit(binop* bo)
{
result_ = new binop(bo->op(),
recurse(bo->first()), recurse(bo->second()));
result_ = binop::instance(bo->op(),
recurse(bo->first()), recurse(bo->second()));
}
void
clone_visitor::visit(const multop* mo)
void
clone_visitor::visit(multop* mo)
{
multop* res = new multop(mo->op());
multop* res = multop::instance(mo->op());
unsigned mos = mo->size();
for (unsigned i = 0; i < mos; ++i)
{
res->add(recurse(mo->nth(i)));
multop::add(&res, recurse(mo->nth(i)));
}
result_ = res;
}
formula*
clone_visitor::recurse(const formula* f)
formula*
clone_visitor::recurse(formula* f)
{
return clone(f);
}
formula*
clone(const formula* f)
formula*
clone(formula* f)
{
clone_visitor v;
f->accept(v);

24
src/ltlvisit/clone.hh
View file

@ -4,7 +4,7 @@
#include "ltlast/formula.hh"
#include "ltlast/visitor.hh"
namespace spot
namespace spot
{
namespace ltl
{
@ -14,28 +14,28 @@ namespace spot
/// to derive from it and override part of its methods.
/// But if you just want the functionality, consider using
/// spot::ltl::clone instead.
class clone_visitor : public const_visitor
class clone_visitor : public visitor
{
public:
clone_visitor();
virtual ~clone_visitor();
formula* result() const;
void visit(const atomic_prop* ap);
void visit(const unop* uo);
void visit(const binop* bo);
void visit(const multop* mo);
void visit(const constant* c);
virtual formula* recurse(const formula* f);
void visit(atomic_prop* ap);
void visit(unop* uo);
void visit(binop* bo);
void visit(multop* mo);
void visit(constant* c);
virtual formula* recurse(formula* f);
protected:
formula* result_;
};
/// \brief Clone a formula.
formula* clone(const formula* f);
formula* clone(formula* f);
}
}

40
src/ltlvisit/equals.cc
View file

@ -2,7 +2,7 @@
#include "equals.hh"
#include "ltlast/allnodes.hh"
namespace spot
namespace spot
{
namespace ltl
{
@ -15,26 +15,22 @@ namespace spot
{
}
bool
bool
equals_visitor::result() const
{
return result_;
}
void
equals_visitor::visit(const atomic_prop* ap)
{
const atomic_prop* p = dynamic_cast<const atomic_prop*>(f_);
if (p && p->name() == ap->name())
result_ = true;
result_ = f_ == ap;
}
void
equals_visitor::visit(const constant* c)
{
const constant* p = dynamic_cast<const constant*>(f_);
if (p && p->val() == c->val())
result_ = true;
result_ = f_ == c;
}
void
@ -53,34 +49,34 @@ namespace spot
const binop* p = dynamic_cast<const binop*>(f_);
if (!p || p->op() != bo->op())
return;
// The current visitor will descend the left branch.
// Build a second visitor for the right branch.
equals_visitor v2(p->second());
f_ = p->first();
bo->first()->accept(*this);
if (result_ == false)
return;
bo->second()->accept(v2);
result_ = v2.result();
}
void
equals_visitor::visit(const multop* m)
{
const multop* p = dynamic_cast<const multop*>(f_);
if (!p || p->op() != m->op())
return;
// This check is a bit more complicated than other checks
// because And(a, b, c) is equal to And(c, a, b, a).
unsigned m_size = m->size();
unsigned p_size = p->size();
std::vector<bool> p_seen(p_size, false);
for (unsigned nf = 0; nf < m_size; ++nf)
{
unsigned np;
@ -102,7 +98,7 @@ namespace spot
// of `p'. That doesn't means that both formula are equal.
// Condider m = And(a, b, c) against p = And(c, d, a, b).
// We should now check if any unmarked (accodring to p_seen)
// child of `p' has an counterpart in `m'. Because `m' might
// child of `p' has an counterpart in `m'. Because `m' might
// contain duplicate children, its faster to test that
// unmarked children of `p' have a counterpart in marked children
// of `p'.
@ -111,25 +107,25 @@ namespace spot
// Consider only unmarked children.
if (p_seen[np])
continue;
// Compare with marked children.
unsigned np2;
const formula *pnth = p->nth(np);
for (np2 = 0; np2 < p_size; ++np2)
if (p_seen[np2] && equals(p->nth(np2), pnth))
break;
// No match? Too bad.
if (np2 == p_size)
if (np2 == p_size)
return;
}
// The two formulas match.
result_ = true;
}
bool
bool
equals(const formula* f1, const formula* f2)
{
equals_visitor v(f1);

43
src/ltlvisit/lunabbrev.cc
View file

@ -1,7 +1,7 @@
#include "ltlast/allnodes.hh"
#include "lunabbrev.hh"
namespace spot
namespace spot
{
namespace ltl
{
@ -13,8 +13,8 @@ namespace spot
{
}
void
unabbreviate_logic_visitor::visit(const binop* bo)
void
unabbreviate_logic_visitor::visit(binop* bo)
{
formula* f1 = recurse(bo->first());
formula* f2 = recurse(bo->second());
@ -22,43 +22,48 @@ namespace spot
{
/* f1 ^ f2 == (f1 & !f2) | (f2 & !f1) */
case binop::Xor:
result_ = new multop(multop::Or,
new multop(multop::And, f1,
new unop(unop::Not, f2)),
new multop(multop::And, f2,
new unop(unop::Not, f1)));
result_ = multop::instance(multop::Or,
multop::instance(multop::And, f1,
unop::instance(unop::Not,
f2)),
multop::instance(multop::And, f2,
unop::instance(unop::Not,
f1)));
return;
/* f1 => f2 == !f1 | f2 */
case binop::Implies:
result_ = new multop(multop::Or, new unop(unop::Not, f1), f2);
result_ = multop::instance(multop::Or,
unop::instance(unop::Not, f1), f2);
return;
/* f1 <=> f2 == (f1 & f2) | (!f1 & !f2) */
case binop::Equiv:
result_ = new multop(multop::Or,
new multop(multop::And, f1, f2),
new multop(multop::And,
new unop(unop::Not, f1),
new unop(unop::Not, f2)));
result_ = multop::instance(multop::Or,
multop::instance(multop::And, f1, f2),
multop::instance(multop::And,
unop::instance(unop::Not,
f1),
unop::instance(unop::Not,
f2)));
return;
/* f1 U f2 == f1 U f2 */
/* f1 R f2 == f1 R f2 */
case binop::U:
case binop::R:
result_ = new binop(bo->op(), f1, f2);
result_ = binop::instance(bo->op(), f1, f2);
return;
}
/* Unreachable code. */
assert(0);
}
formula*
unabbreviate_logic_visitor::recurse(const formula* f)
formula*
unabbreviate_logic_visitor::recurse(formula* f)
{
return unabbreviate_logic(f);
}
formula*
unabbreviate_logic(const formula* f)
formula*
unabbreviate_logic(formula* f)
{
unabbreviate_logic_visitor v;
f->accept(v);

12
src/ltlvisit/lunabbrev.hh
View file

@ -3,11 +3,11 @@
#include "clone.hh"
namespace spot
namespace spot
{
namespace ltl
{
/// \brief Clone and rewrite a formula to remove most of the
/// \brief Clone and rewrite a formula to remove most of the
/// abbreviated logical operators.
///
/// This will rewrite binary operators such as binop::Implies,
@ -26,18 +26,18 @@ namespace spot
virtual ~unabbreviate_logic_visitor();
using super::visit;
void visit(const binop* bo);
void visit(binop* bo);
virtual formula* recurse(const formula* f);
virtual formula* recurse(formula* f);
};
/// \brief Clone rewrite a formula to remove most of the abbreviated
/// \brief Clone rewrite a formula to remove most of the abbreviated
/// logical operators.
///
/// This will rewrite binary operators such as binop::Implies,
/// binop::Equals, and binop::Xor, using only unop::Not, multop::Or,
/// and multop::And.
formula* unabbreviate_logic(const formula* f);
formula* unabbreviate_logic(formula* f);
}
}

94
src/ltlvisit/nenoform.cc
View file

@ -6,7 +6,7 @@ namespace spot
namespace ltl
{
class negative_normal_form_visitor : public const_visitor
class negative_normal_form_visitor : public visitor
{
public:
negative_normal_form_visitor(bool negated)
@ -14,7 +14,7 @@ namespace spot
{
}
virtual
virtual
~negative_normal_form_visitor()
{
}
@ -23,43 +23,43 @@ namespace spot
{
return result_;
}
void
visit(const atomic_prop* ap)
void
visit(atomic_prop* ap)
{
formula* f = new atomic_prop(ap->name(), ap->env());
formula* f = ap->ref();
if (negated_)
result_ = new unop(unop::Not, f);
result_ = unop::instance(unop::Not, f);
else
result_ = f;
}
void
visit(const constant* c)
void
visit(constant* c)
{
if (! negated_)
{
result_ = new constant(c->val());
result_ = c;
return;
}
switch (c->val())
{
case constant::True:
result_ = new constant(constant::False);
result_ = constant::false_instance();
return;
case constant::False:
result_ = new constant(constant::True);
result_ = constant::true_instance();
return;
}
/* Unreachable code. */
assert(0);
}
void
visit(const unop* uo)
void
visit(unop* uo)
{
const formula* f = uo->child();
formula* f = uo->child();
switch (uo->op())
{
case unop::Not:
@ -67,63 +67,67 @@ namespace spot
return;
case unop::X:
/* !Xa == X!a */
result_ = new unop(unop::X, recurse(f));
result_ = unop::instance(unop::X, recurse(f));
return;
case unop::F:
/* !Fa == G!a */
result_ = new unop(negated_ ? unop::G : unop::F, recurse(f));
result_ = unop::instance(negated_ ? unop::G : unop::F, recurse(f));
return;
case unop::G:
/* !Ga == F!a */
result_ = new unop(negated_ ? unop::F : unop::G, recurse(f));
result_ = unop::instance(negated_ ? unop::F : unop::G, recurse(f));
return;
}
/* Unreachable code. */
assert(0);
}
void
visit(const binop* bo)
void
visit(binop* bo)
{
const formula* f1 = bo->first();
const formula* f2 = bo->second();
formula* f1 = bo->first();
formula* f2 = bo->second();
switch (bo->op())
{
case binop::Xor:
/* !(a ^ b) == a <=> b */
result_ = new binop(negated_ ? binop::Equiv : binop::Xor,
recurse_(f1, false), recurse_(f2, false));
result_ = binop::instance(negated_ ? binop::Equiv : binop::Xor,
recurse_(f1, false),
recurse_(f2, false));
return;
case binop::Equiv:
/* !(a <=> b) == a ^ b */
result_ = new binop(negated_ ? binop::Xor : binop::Equiv,
recurse_(f1, false), recurse_(f2, false));
result_ = binop::instance(negated_ ? binop::Xor : binop::Equiv,
recurse_(f1, false),
recurse_(f2, false));
return;
case binop::Implies:
if (negated_)
/* !(a => b) == a & !b */
result_ = new multop(multop::And,
recurse_(f1, false), recurse_(f2, true));
result_ = multop::instance(multop::And,
recurse_(f1, false),
recurse_(f2, true));
else
result_ = new binop(binop::Implies, recurse(f1), recurse(f2));
result_ = binop::instance(binop::Implies,
recurse(f1), recurse(f2));
return;
case binop::U:
/* !(a U b) == !a R !b */
result_ = new binop(negated_ ? binop::R : binop::U,
recurse(f1), recurse(f2));
result_ = binop::instance(negated_ ? binop::R : binop::U,
recurse(f1), recurse(f2));
return;
case binop::R:
/* !(a R b) == !a U !b */
result_ = new binop(negated_ ? binop::U : binop::R,
recurse(f1), recurse(f2));
result_ = binop::instance(negated_ ? binop::U : binop::R,
recurse(f1), recurse(f2));
return;
}
/* Unreachable code. */
assert(0);
}
void
visit(const multop* mo)
void
visit(multop* mo)
{
/* !(a & b & c) == !a | !b | !c */
/* !(a | b | c) == !a & !b & !c */
@ -138,32 +142,32 @@ namespace spot
op = multop::And;
break;
}
multop* res = new multop(op);
multop* res = multop::instance(op);
unsigned mos = mo->size();
for (unsigned i = 0; i < mos; ++i)
res->add(recurse(mo->nth(i)));
multop::add(&res, recurse(mo->nth(i)));
result_ = res;
}
formula*
recurse_(const formula* f, bool negated)
formula*
recurse_(formula* f, bool negated)
{
return negative_normal_form(f, negated);
}
formula*
recurse(const formula* f)
formula*
recurse(formula* f)
{
return recurse_(f, negated_);
}
protected:
formula* result_;
bool negated_;
};
formula*
negative_normal_form(const formula* f, bool negated)
formula*
negative_normal_form(formula* f, bool negated)
{
negative_normal_form_visitor v(negated);
f->accept(v);

8
src/ltlvisit/nenoform.hh
View file

@ -4,13 +4,13 @@
#include "ltlast/formula.hh"
#include "ltlast/visitor.hh"
namespace spot
namespace spot
{
namespace ltl
{
/// \brief Build the negative normal form of \a f.
///
/// All negations of the formula are pushed in front of the
///
/// All negations of the formula are pushed in front of the
/// atomic propositions.
///
/// \param f The formula to normalize.
@ -22,7 +22,7 @@ namespace spot
/// or spot::ltl::unabbreviate_ltl first. (Calling these functions
/// after spot::ltl::negative_normal_form would likely produce a
/// formula which is not in negative normal form.)
formula* negative_normal_form(const formula* f, bool negated = false);
formula* negative_normal_form(formula* f, bool negated = false);
}
}

28
src/ltlvisit/tunabbrev.cc
View file

@ -1,7 +1,7 @@
#include "ltlast/allnodes.hh"
#include "tunabbrev.hh"
namespace spot
namespace spot
{
namespace ltl
{
@ -13,8 +13,8 @@ namespace spot
{
}
void
unabbreviate_ltl_visitor::visit(const unop* uo)
void
unabbreviate_ltl_visitor::visit(unop* uo)
{
switch (uo->op())
{
@ -23,26 +23,26 @@ namespace spot
this->super::visit(uo);
return;
case unop::F:
result_ = new binop(binop::U,
new constant(constant::True),
recurse(uo->child()));
result_ = binop::instance(binop::U,
constant::true_instance(),
recurse(uo->child()));
return;
case unop::G:
result_ = new binop(binop::R,
new constant(constant::False),
recurse(uo->child()));
result_ = binop::instance(binop::R,
constant::false_instance(),
recurse(uo->child()));
return;
}
}
formula*
unabbreviate_ltl_visitor::recurse(const formula* f)
formula*
unabbreviate_ltl_visitor::recurse(formula* f)
{
return unabbreviate_ltl(f);
}
formula*
unabbreviate_ltl(const formula* f)
formula*
unabbreviate_ltl(formula* f)
{
unabbreviate_ltl_visitor v;
f->accept(v);

12
src/ltlvisit/tunabbrev.hh
View file

@ -4,11 +4,11 @@
#include "ltlast/formula.hh"
#include "ltlvisit/lunabbrev.hh"
namespace spot
namespace spot
{
namespace ltl
{
/// \brief Clone and rewrite a formula to remove most of the
/// \brief Clone and rewrite a formula to remove most of the
/// abbreviated LTL and logical operators.
///
/// The rewriting performed on logical operator is
@ -28,12 +28,12 @@ namespace spot
unabbreviate_ltl_visitor();
virtual ~unabbreviate_ltl_visitor();
void visit(const unop* uo);
void visit(unop* uo);
formula* recurse(const formula* f);
formula* recurse(formula* f);
};
/// \brief Clone and rewrite a formula to remove most of the
/// \brief Clone and rewrite a formula to remove most of the
/// abbreviated LTL and logical operators.
///
/// The rewriting performed on logical operator is
@ -41,7 +41,7 @@ namespace spot
///
/// This will also rewrite unary operators such as unop::F,
/// and unop::G, using only binop::U, and binop::R.
formula* unabbreviate_ltl(const formula* f);
formula* unabbreviate_ltl(formula* f);
}
}