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

Revert everything related to Damien's work in 2008 (he will commit a new version soon).

Browse source 
Here are the reverted patches:
8c0d1003b0,
25a3114287,
9afbaf6342,
dc0005f4e1,
543190f2bc.
This commit is contained in:
Alexandre Duret-Lutz 2009-03-25 13:58:18 +01:00
parent 3d278663cd
commit b1bfdee870
130 changed files with 912 additions and 5104 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/ltlast/Makefile.am
View file

@ -1,4 +1,4 @@
## Copyright (C) 2003, 2008 Laboratoire d'Informatique de Paris 6 (LIP6),
## Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
## département Systèmes Répartis Coopératifs (SRC), Université Pierre
## et Marie Curie.
##
@ -19,6 +19,29 @@
## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
## 02111-1307, USA.
AM_CPPFLAGS = -I$(srcdir)/..
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
ltlastdir = $(pkgincludedir)/ltlast
ltlast_HEADERS = formula.hh
ltlast_HEADERS = \
allnodes.hh \
atomic_prop.hh \
binop.hh \
constant.hh \
formula.hh \
multop.hh \
predecl.hh \
refformula.hh \
unop.hh \
visitor.hh
noinst_LTLIBRARIES = libltlast.la
libltlast_la_SOURCES = \
atomic_prop.cc \
binop.cc \
constant.cc \
formula.cc \
multop.cc \
refformula.cc \
unop.cc

37
src/ltlast/allnodes.hh Normal file
View file

@ -0,0 +1,37 @@
// Copyright (C) 2003, 2004 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.
/// \file ltlast/allnodes.hh
/// \brief Define all LTL node types.
///
/// This file is usually needed when \b defining a visitor.
/// Prefer ltlast/predecl.hh when only \b declaring methods and functions
/// over LTL nodes.
#ifndef SPOT_LTLAST_ALLNODES_HH
# define SPOT_LTLAST_ALLNODES_HH
# include "binop.hh"
# include "unop.hh"
# include "multop.hh"
# include "atomic_prop.hh"
# include "constant.hh"
#endif // SPOT_LTLAST_ALLNODES_HH

108
src/ltlast/atomic_prop.cc Normal file
View file

@ -0,0 +1,108 @@
// Copyright (C) 2003, 2004, 2005 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 "atomic_prop.hh"
#include "visitor.hh"
#include <cassert>
#include <ostream>
namespace spot
{
namespace ltl
{
atomic_prop::atomic_prop(const std::string& name, environment& env)
: name_(name), env_(&env)
{
dump_ = "AP(" + name + ")";
set_key_();
}
atomic_prop::~atomic_prop()
{
// Get this instance out of the instance map.
pair p(name(), &env());
map::iterator i = instances.find(p);
assert (i != instances.end());
instances.erase(i);
}
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&
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());
}
unsigned
atomic_prop::instance_count()
{
return instances.size();
}
std::ostream&
atomic_prop::dump_instances(std::ostream& os)
{
for (map::iterator i = instances.begin(); i != instances.end(); ++i)
{
os << i->second << " = " << i->second->ref_count_()
<< " * atomic_prop(" << i->first.first << ", "
<< i->first.second->name() << ")" << std::endl;
}
return os;
}
}
}

76
src/ltlast/atomic_prop.hh Normal file
View file

@ -0,0 +1,76 @@
// Copyright (C) 2003, 2004 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.
/// \file ltlast/atomic_prop.hh
/// \brief LTL atomic propositions
#ifndef SPOT_LTLAST_ATOMIC_PROP_HH
# define SPOT_LTLAST_ATOMIC_PROP_HH
#include <string>
#include <iosfwd>
#include <map>
#include "refformula.hh"
#include "ltlenv/environment.hh"
namespace spot
{
namespace ltl
{
/// \brief Atomic propositions.
/// \ingroup ltl_ast
class atomic_prop : public ref_formula
{
public:
/// Build an atomic proposition with name \a name in
/// environment \a env.
static atomic_prop* instance(const std::string& name, environment& env);
virtual void accept(visitor& visitor);
virtual void accept(const_visitor& visitor) const;
/// Get the name of the atomic proposition.
const std::string& name() const;
/// Get the environment of the atomic proposition.
environment& env() const;
/// Number of instantiated atomic propositions. For debugging.
static unsigned instance_count();
/// List all instances of atomic propositions. For debugging.
static std::ostream& dump_instances(std::ostream& os);
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_;
};
}
}
#endif // SPOT_LTLAST_ATOMICPROP_HH

153
src/ltlast/binop.cc Normal file
View file

@ -0,0 +1,153 @@
// Copyright (C) 2003, 2005 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 <cassert>
#include <utility>
#include "binop.hh"
#include "visitor.hh"
namespace spot
{
namespace ltl
{
binop::binop(type op, formula* first, formula* second)
: op_(op), first_(first), second_(second)
{
dump_ = "binop(";
dump_ += op_name();
dump_ += ", " + first->dump() + ", " + second->dump() + ")";
set_key_();
}
binop::~binop()
{
// Get this instance out of the instance map.
pairf pf(first(), second());
pair p(op(), pf);
map::iterator i = instances.find(p);
assert (i != instances.end());
instances.erase(i);
}
void
binop::accept(visitor& v)
{
v.visit(this);
}
void
binop::accept(const_visitor& v) const
{
v.visit(this);
}
const formula*
binop::first() const
{
return first_;
}
formula*
binop::first()
{
return first_;
}
const formula*
binop::second() const
{
return second_;
}
formula*
binop::second()
{
return second_;
}
binop::type
binop::op() const
{
return op_;
}
const char*
binop::op_name() const
{
switch (op_)
{
case Xor:
return "Xor";
case Implies:
return "Implies";
case Equiv:
return "Equiv";
case U:
return "U";
case R:
return "R";
}
// Unreachable code.
assert(0);
return 0;
}
binop::map binop::instances;
binop*
binop::instance(type op, formula* first, formula* second)
{
// Sort the operands of associative operators, so that for
// example the formula instance for 'a xor b' is the same as
// that for 'b xor a'.
switch (op)
{
case Xor:
case Equiv:
if (second < first)
std::swap(first, second);
break;
case Implies:
case U:
case R:
// Non associative operators.
break;
}
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());
}
unsigned
binop::instance_count()
{
return instances.size();
}
}
}

91
src/ltlast/binop.hh Normal file
View file

@ -0,0 +1,91 @@
// Copyright (C) 2003, 2004 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.
/// \file ltlast/binop.hh
/// \brief LTL binary operators
///
/// This does not include \c AND and \c OR operators. These are
/// considered to be multi-operand operators (see spot::ltl::multop).
#ifndef SPOT_LTLAST_BINOP_HH
# define SPOT_LTLAST_BINOP_HH
#include <map>
#include "refformula.hh"
namespace spot
{
namespace ltl
{
/// \brief Binary operator.
/// \ingroup ltl_ast
class binop : public ref_formula
{
public:
/// Different kinds of binary opertaors
///
/// And and Or are not here. Because they
/// are often nested we represent them as multops.
enum type { Xor, Implies, Equiv, U, R };
/// 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;
/// Get the first operand.
const formula* first() const;
/// Get the first operand.
formula* first();
/// Get the second operand.
const formula* second() const;
/// Get the second operand.
formula* second();
/// Get the type of this operator.
type op() const;
/// Get the type of this operator, as a string.
const char* op_name() const;
/// Number of instantiated binary operators. For debugging.
static unsigned instance_count();
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_;
formula* second_;
};
}
}
#endif // SPOT_LTLAST_BINOP_HH

99
src/ltlast/constant.cc Normal file
View file

@ -0,0 +1,99 @@
// Copyright (C) 2003, 2005 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 "constant.hh"
#include "visitor.hh"
#include <cassert>
namespace spot
{
namespace ltl
{
constant::constant(type val)
: val_(val)
{
switch (val)
{
case True:
dump_ = "constant(1)";
set_key_();
return;
case False:
dump_ = "constant(0)";
set_key_();
return;
}
// Unreachable code.
assert(0);
}
constant::~constant()
{
}
void
constant::accept(visitor& v)
{
v.visit(this);
}
void
constant::accept(const_visitor& v) const
{
v.visit(this);
}
constant::type
constant::val() const
{
return val_;
}
const char*
constant::val_name() const
{
switch (val_)
{
case True:
return "1";
case False:
return "0";
}
// Unreachable code.
assert(0);
return 0;
}
constant*
constant::false_instance()
{
static constant f(constant::False);
return &f;
}
constant*
constant::true_instance()
{
static constant t(constant::True);
return &t;
}
}
}

64
src/ltlast/constant.hh Normal file
View file

@ -0,0 +1,64 @@
// Copyright (C) 2003, 2004 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.
/// \file ltlast/constant.hh
/// \brief LTL constants
#ifndef SPOT_LTLAST_CONSTANT_HH
# define SPOT_LTLAST_CONSTANT_HH
#include "formula.hh"
namespace spot
{
namespace ltl
{
/// \brief A constant (True or False)
/// \ingroup ltl_ast
class constant : public formula
{
public:
enum type { False, True };
virtual void accept(visitor& v);
virtual void accept(const_visitor& v) const;
/// Return the value of the constant.
type val() const;
/// 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_;
};
}
}
#endif // SPOT_LTLAST_CONSTANT_HH

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

@ -0,0 +1,74 @@
// Copyright (C) 2003, 2005 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 "formula.hh"
#include "misc/hash.hh"
namespace spot
{
namespace ltl
{
formula*
formula::ref()
{
ref_();
return this;
}
formula::~formula()
{
}
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;
}
const std::string&
formula::dump() const
{
return dump_;
}
void
formula::set_key_()
{
string_hash sh;
hash_key_ = sh(dump_);
}
}
}

220
src/ltlast/formula.hh
View file

@ -20,16 +20,13 @@
// 02111-1307, USA.
/// \file ltlast/formula.hh
/// \brief LTL formula, AST and visitor interface
/// \brief LTL formula interface
#ifndef SPOT_LTLAST_FORMULA_HH
# define SPOT_LTLAST_FORMULA_HH
# include "internal/formula.hh"
# include "internal/atomic_prop.hh"
# include "internal/constant.hh"
# include "internal/unop.hh"
# include "internal/binop.hh"
# include "internal/multop.hh"
#include <string>
#include <cassert>
#include "predecl.hh"
namespace spot
{
@ -64,9 +61,6 @@ namespace spot
/// \addtogroup ltl_misc Miscellaneous algorithms for LTL formulae
/// \ingroup ltl_algorithm
struct ltl_t;
struct visitor;
struct const_visitor;
/// \brief An LTL formula.
/// \ingroup ltl_essential
@ -74,136 +68,114 @@ namespace spot
///
/// The only way you can work with a formula is to
/// build a spot::ltl::visitor or spot::ltl::const_visitor.
typedef spot::internal::formula<ltl_t> formula;
/// Forward declarations
formula* clone(const formula* f);
std::ostream& to_string(const formula* f, std::ostream& os);
void destroy(const formula* f);
struct ltl_t
class formula
{
typedef spot::ltl::visitor visitor;
typedef spot::ltl::const_visitor const_visitor;
public:
/// Entry point for vspot::ltl::visitor instances.
virtual void accept(visitor& v) = 0;
/// Entry point for vspot::ltl::const_visitor instances.
virtual void accept(const_visitor& v) const = 0;
static formula* clone_(const formula* f)
/// \brief clone this node
///
/// This increments the reference counter of this node (if one is
/// used). You should almost never use this method directly as
/// it doesn't touch the children. If you want to clone a
/// whole formula, use spot::ltl::clone() instead.
formula* ref();
/// \brief release this node
///
/// This decrements the reference counter of this node (if one is
/// used) and can free the object. You should almost never use
/// this method directly as it doesn't touch the children. If you
/// want to release a whole formula, use spot::ltl::destroy() instead.
static void unref(formula* f);
/// Return a canonic representation of the formula
const std::string& dump() const;
/// Return a hash_key for the formula.
size_t
hash() const
{
return clone(f);
return hash_key_;
}
protected:
virtual ~formula();
static std::ostream& to_string_(const formula* f, std::ostream& os)
{
return to_string(f, os);
}
/// \brief increment reference counter if any
virtual void ref_();
/// \brief decrement reference counter if any, return true when
/// the instance must be deleted (usually when the counter hits 0).
virtual bool unref_();
static void destroy_(const formula* f)
{
destroy(f);
}
/// \brief Compute key_ from dump_.
///
/// Should be called once in each object, after dump_ has been set.
void set_key_();
/// The canonic representation of the formula
std::string dump_;
/// \brief The hash key of this formula.
///
/// Initialized by set_key_().
size_t hash_key_;
};
enum binop { Xor, Implies, Equiv, U, R };
const char* binop_name(binop op) const
/// \brief Strict Weak Ordering for <code>const formula*</code>.
/// \ingroup ltl_essentials
///
/// This is meant to be used as a comparison functor for
/// STL \c map whose key are of type <code>const formula*</code>.
///
/// For instance here is how one could declare
/// a map of \c const::formula*.
/// \code
/// // Remember how many times each formula has been seen.
/// std::map<const spot::ltl::formula*, int,
/// spot::formula_ptr_less_than> seen;
/// \endcode
struct formula_ptr_less_than:
public std::binary_function<const formula*, const formula*, bool>
{
bool
operator()(const formula* left, const formula* right) const
{
switch (op)
{
case Xor:
return "Xor";
case Implies:
return "Implies";
case Equiv:
return "Equiv";
case U:
return "U";
case R:
return "R";
}
// Unreachable code.
assert(0);
return 0;
}
enum unop { Not, X, F, G };
const char* unop_name(unop op) const
{
switch (op)
{
case Not:
return "Not";
case X:
return "X";
case F:
return "F";
case G:
return "G";
}
// Unreachable code.
assert(0);
return 0;
assert(left);
assert(right);
size_t l = left->hash();
size_t r = right->hash();
if (1 != r)
return l < r;
return left->dump() < right->dump();
}
};
typedef spot::internal::formula_ptr_less_than formula_ptr_less_than;
typedef spot::internal::formula_ptr_hash formula_ptr_hash;
/// \brief Atomic propositions.
/// \ingroup ltl_ast
typedef spot::internal::atomic_prop<ltl_t> atomic_prop;
/// \brief A constant (True or False)
/// \ingroup ltl_ast
typedef spot::internal::constant<ltl_t> constant;
/// \brief Unary operators.
/// \ingroup ltl_ast
typedef spot::internal::unop<ltl_t> unop;
/// \brief Binary operator.
/// \ingroup ltl_ast
typedef spot::internal::binop<ltl_t> binop;
/// \brief Multi-operand operators.
/// \ingroup ltl_ast
/// \brief Hash Function for <code>const formula*</code>.
/// \ingroup ltl_essentials
/// \ingroup hash_funcs
///
/// These operators are considered commutative and associative.
typedef spot::internal::multop<ltl_t> multop;
/// \brief Formula visitor that can modify the formula.
/// \ingroup ltl_essential
/// This is meant to be used as a hash functor for
/// Sgi's \c hash_map whose key are of type <code>const formula*</code>.
///
/// Writing visitors is the prefered way
/// to traverse a formula, since it doesn't
/// involve any cast.
///
/// If you do not need to modify the visited formula, inherit from
/// spot::ltl:const_visitor instead.
struct visitor
/// For instance here is how one could declare
/// a map of \c const::formula*.
/// \code
/// // Remember how many times each formula has been seen.
/// Sgi::hash_map<const spot::ltl::formula*, int,
/// const spot::ltl::formula_ptr_hash> seen;
/// \endcode
struct formula_ptr_hash:
public std::unary_function<const formula*, size_t>
{
virtual ~visitor() {}
virtual void visit(atomic_prop* node) = 0;
virtual void visit(constant* node) = 0;
virtual void visit(binop* node) = 0;
virtual void visit(unop* node) = 0;
virtual void visit(multop* node) = 0;
size_t
operator()(const formula* that) const
{
assert(that);
return that->hash();
}
};
/// \brief Formula visitor that cannot modify the formula.
///
/// Writing visitors is the prefered way
/// to traverse a formula, since it doesn't
/// involve any cast.
///
/// If you want to modify the visited formula, inherit from
/// spot::ltl:visitor instead.
struct const_visitor
{
virtual ~const_visitor() {}
virtual void visit(const atomic_prop* node) = 0;
virtual void visit(const constant* node) = 0;
virtual void visit(const binop* node) = 0;
virtual void visit(const unop* node) = 0;
virtual void visit(const multop* node) = 0;
};
}
}

212
src/ltlast/multop.cc Normal file
View file

@ -0,0 +1,212 @@
// Copyright (C) 2003, 2004, 2005 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 <cassert>
#include <utility>
#include <algorithm>
#include "multop.hh"
#include "constant.hh"
#include "visitor.hh"
#include "ltlvisit/destroy.hh"
namespace spot
{
namespace ltl
{
multop::multop(type op, vec* v)
: op_(op), children_(v)
{
dump_ = "multop(";
dump_ += op_name();
unsigned max = v->size();
for (unsigned n = 0; n < max; ++n)
{
dump_ += ", " + (*v)[n]->dump();
}
dump_ += ")";
set_key_();
}
multop::~multop()
{
// Get this instance out of the instance map.
pair p(op(), children_);
map::iterator i = instances.find(p);
assert (i != instances.end());
instances.erase(i);
delete children_;
}
void
multop::accept(visitor& v)
{
v.visit(this);
}
void
multop::accept(const_visitor& v) const
{
v.visit(this);
}
unsigned
multop::size() const
{
return children_->size();
}
const formula*
multop::nth(unsigned n) const
{
return (*children_)[n];
}
formula*
multop::nth(unsigned n)
{
return (*children_)[n];
}
multop::type
multop::op() const
{
return op_;
}
const char*
multop::op_name() const
{
switch (op_)
{
case And:
return "And";
case Or:
return "Or";
}
// Unreachable code.
assert(0);
return 0;
}
multop::map multop::instances;
formula*
multop::instance(type op, vec* v)
{
pair p(op, v);
// Inline children of same kind.
{
vec inlined;
vec::iterator i = v->begin();
while (i != v->end())
{
multop* p = dynamic_cast<multop*>(*i);
if (p && p->op() == op)
{
unsigned ps = p->size();
for (unsigned n = 0; n < ps; ++n)
inlined.push_back(p->nth(n));
// That sub-formula is now useless, drop it.
// Note that we use unref(), not destroy(), because we've
// adopted its children and don't want to destroy these.
formula::unref(*i);
i = v->erase(i);
}
else
{
++i;
}
}
v->insert(v->end(), inlined.begin(), inlined.end());
}
std::sort(v->begin(), v->end(), formula_ptr_less_than());
// Remove duplicates. We can't use std::unique(), because we
// must destroy() any formula we drop.
{
formula* last = 0;
vec::iterator i = v->begin();
while (i != v->end())
{
if (*i == last)
{
destroy(*i);
i = v->erase(i);
}
else
{
last = *i++;
}
}
}
vec::size_type s = v->size();
if (s == 0)
{
delete v;
switch (op)
{
case And:
return constant::true_instance();
case Or:
return constant::false_instance();
}
/* Unreachable code. */
assert(0);
}
else if (s == 1)
{
formula* res = (*v)[0];
delete v;
return res;
}
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());
}
formula*
multop::instance(type op, formula* first, formula* second)
{
vec* v = new vec;
v->push_back(first);
v->push_back(second);
return instance(op, v);
}
unsigned
multop::instance_count()
{
return instances.size();
}
}
}

125
src/ltlast/multop.hh Normal file
View file

@ -0,0 +1,125 @@
// Copyright (C) 2003, 2004 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.
/// \file ltlast/multop.hh
/// \brief LTL multi-operand operators
#ifndef SPOT_LTLAST_MULTOP_HH
# define SPOT_LTLAST_MULTOP_HH
#include <vector>
#include <map>
#include "refformula.hh"
namespace spot
{
namespace ltl
{
/// \brief Multi-operand operators.
/// \ingroup ltl_ast
///
/// These operators are considered commutative and associative.
class multop : public ref_formula
{
public:
enum type { Or, And };
/// List of formulae.
typedef std::vector<formula*> vec;
/// \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. This allows incremental building of
/// n-ary ltl::multop.
///
/// This functions can perform slight optimizations and
/// may not return an ltl::multop objects. For instance
/// if \c first and \c second are equal, that formula is
/// returned as-is.
static formula* instance(type op, formula* first, formula* second);
/// \brief Build a spot::ltl::multop with many children.
///
/// Same as the other instance() function, but take a vector of
/// formula in argument. This vector is acquired by the
/// spot::ltl::multop class, the caller should allocate it with
/// \c new, but not use it (especially not destroy it) after it
/// has been passed to spot::ltl::multop.
///
/// This functions can perform slight optimizations and
/// may not return an ltl::multop objects. For instance
/// if the vector contain only one unique element, this
/// this formula will be returned as-is.
static formula* instance(type op, vec* v);
virtual void accept(visitor& v);
virtual void accept(const_visitor& v) const;
/// Get the number of children.
unsigned size() const;
/// \brief Get the nth children.
///
/// Starting with \a n = 0.
const formula* nth(unsigned n) const;
/// \brief Get the nth children.
///
/// Starting with \a n = 0.
formula* nth(unsigned n);
/// Get the type of this operator.
type op() const;
/// Get the type of this operator, as a string.
const char* op_name() const;
/// Number of instantiated multi-operand operators. For debugging.
static unsigned instance_count();
protected:
typedef std::pair<type, vec*> pair;
/// Comparison functor used internally by ltl::multop.
struct paircmp
{
bool
operator () (const pair& p1, const pair& p2) const
{
if (p1.first != p2.first)
return p1.first < p2.first;
return *p1.second < *p2.second;
}
};
typedef std::map<pair, formula*, paircmp> map;
static map instances;
multop(type op, vec* v);
virtual ~multop();
private:
type op_;
vec* children_;
};
}
}
#endif // SPOT_LTLAST_MULTOP_HH

48
src/ltlast/predecl.hh Normal file
View file

@ -0,0 +1,48 @@
// Copyright (C) 2003, 2004 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.
/// \file ltlast/predecl.hh
/// \brief Predeclare all LTL node types.
///
/// This file is usually used when \b declaring methods and functions
/// over LTL nodes.
/// Use ltlast/allnodes.hh or an individual header when the definition of
/// the node is actually needed.
#ifndef SPOT_LTLAST_PREDECL_HH
# define SPOT_LTLAST_PREDECL_HH
namespace spot
{
namespace ltl
{
struct visitor;
struct const_visitor;
struct atomic_prop;
struct unop;
struct constant;
struct binop;
struct formula;
struct multop;
}
}
#endif // SPOT_LTLAST_PREDECL_HH

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

@ -0,0 +1,58 @@
// Copyright (C) 2003, 2004 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 "refformula.hh"
#include <cassert>
namespace spot
{
namespace ltl
{
ref_formula::ref_formula()
: ref_counter_(0)
{
}
ref_formula::~ref_formula()
{
}
void
ref_formula::ref_()
{
++ref_counter_;
}
bool
ref_formula::unref_()
{
assert(ref_counter_ > 0);
return !--ref_counter_;
}
unsigned
ref_formula::ref_count_()
{
return ref_counter_;
}
}
}

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

@ -0,0 +1,52 @@
// Copyright (C) 2003, 2004, 2005 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.
/// \file ltlast/refformula.hh
/// \brief Reference-counted LTL formulae
#ifndef SPOT_LTLAST_REFFORMULA_HH
# define SPOT_LTLAST_REFFORMULA_HH
#include "formula.hh"
namespace spot
{
namespace ltl
{
/// \brief A reference-counted LTL formula.
/// \ingroup ltl_ast
class ref_formula : public formula
{
protected:
virtual ~ref_formula();
ref_formula();
void ref_();
bool unref_();
/// Number of references to this formula.
unsigned ref_count_();
private:
unsigned ref_counter_;
};
}
}
#endif // SPOT_LTLAST_REFFORMULA_HH

119
src/ltlast/unop.cc Normal file
View file

@ -0,0 +1,119 @@
// Copyright (C) 2003, 2005 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 "unop.hh"
#include "visitor.hh"
#include <cassert>
namespace spot
{
namespace ltl
{
unop::unop(type op, formula* child)
: op_(op), child_(child)
{
dump_ = "unop(";
dump_ += op_name();
dump_ += ", " + child->dump() + ")";
set_key_();
}
unop::~unop()
{
// Get this instance out of the instance map.
pair p(op(), child());
map::iterator i = instances.find(p);
assert (i != instances.end());
instances.erase(i);
}
void
unop::accept(visitor& v)
{
v.visit(this);
}
void
unop::accept(const_visitor& v) const
{
v.visit(this);
}
const formula*
unop::child() const
{
return child_;
}
formula*
unop::child()
{
return child_;
}
unop::type
unop::op() const
{
return op_;
}
const char*
unop::op_name() const
{
switch (op_)
{
case Not:
return "Not";
case X:
return "X";
case F:
return "F";
case G:
return "G";
}
// Unreachable code.
assert(0);
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());
}
unsigned
unop::instance_count()
{
return instances.size();
}
}
}

78
src/ltlast/unop.hh Normal file
View file

@ -0,0 +1,78 @@
// Copyright (C) 2003, 2004 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.
/// \file ltlast/unop.hh
/// \brief LTL unary operators
#ifndef SPOT_LTLAST_UNOP_HH
# define SPOT_LTLAST_UNOP_HH
#include <map>
#include "refformula.hh"
namespace spot
{
namespace ltl
{
/// \brief Unary operators.
/// \ingroup ltl_ast
class unop : public ref_formula
{
public:
enum type { Not, X, F, G };
/// 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;
/// Get the sole operand of this operator.
const formula* child() const;
/// Get the sole operand of this operator.
formula* child();
/// Get the type of this operator.
type op() const;
/// Get the type of this operator, as a string.
const char* op_name() const;
/// Number of instantiated unary operators. For debugging.
static unsigned instance_count();
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_;
};
}
}
#endif // SPOT_LTLAST_UNOP_HH

74
src/ltlast/visitor.hh Normal file
View file

@ -0,0 +1,74 @@
// Copyright (C) 2003, 2004, 2005 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.
/// \file ltlast/visitor.hh
/// \brief LTL visitor interface
#ifndef SPOT_LTLAST_VISITOR_HH
# define SPOT_LTLAST_VISITOR_HH
#include "predecl.hh"
namespace spot
{
namespace ltl
{
/// \brief Formula visitor that can modify the formula.
/// \ingroup ltl_essential
///
/// Writing visitors is the prefered way
/// to traverse a formula, since it doesn't
/// involve any cast.
///
/// If you do not need to modify the visited formula, inherit from
/// spot::ltl:const_visitor instead.
struct visitor
{
virtual ~visitor() {}
virtual void visit(atomic_prop* node) = 0;
virtual void visit(constant* node) = 0;
virtual void visit(binop* node) = 0;
virtual void visit(unop* node) = 0;
virtual void visit(multop* node) = 0;
};
/// \brief Formula visitor that cannot modify the formula.
///
/// Writing visitors is the prefered way
/// to traverse a formula, since it doesn't
/// involve any cast.
///
/// If you want to modify the visited formula, inherit from
/// spot::ltl:visitor instead.
struct const_visitor
{
virtual ~const_visitor() {}
virtual void visit(const atomic_prop* node) = 0;
virtual void visit(const constant* node) = 0;
virtual void visit(const binop* node) = 0;
virtual void visit(const unop* node) = 0;
virtual void visit(const multop* node) = 0;
};
}
}
#endif // SPOT_LTLAST_VISITOR_HH