Delete useless *.cc files in ltlast/
This commit is contained in:
Alexandre Duret-Lutz
parent
994482ed2c
commit
9afbaf6342
9 changed files with 8 additions and 871 deletions
|
|
@ -1,3 +1,11 @@
|
||||||
|
2008-06-12 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||||
|
|
||||||
|
* src/ltlast/atomic_prop.cc, src/ltlast/binop.cc,
|
||||||
|
src/ltlast/constant.cc, src/ltlast/formula.cc,
|
||||||
|
src/ltlast/multop.cc, src/ltlast/predecl.hh,
|
||||||
|
src/ltlast/refformula.cc, src/ltlast/unop.cc: Delete these files,
|
||||||
|
not used anymore since 2008-04-16.
|
||||||
|
|
||||||
2008-06-11 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
2008-06-11 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||||
|
|
||||||
* iface/nips/dottynips.cc: Include ctsdlib for exit().
|
* iface/nips/dottynips.cc: Include ctsdlib for exit().
|
||||||
|
|
|
||||||
|
|
@ -1,108 +0,0 @@
|
||||||
// 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;
|
|
||||||
}
|
|
||||||
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,153 +0,0 @@
|
||||||
// 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();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,99 +0,0 @@
|
||||||
// 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;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,74 +0,0 @@
|
||||||
// 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_);
|
|
||||||
}
|
|
||||||
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,212 +0,0 @@
|
||||||
// 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();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,48 +0,0 @@
|
||||||
// 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
|
|
||||||
|
|
@ -1,58 +0,0 @@
|
||||||
// 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_;
|
|
||||||
}
|
|
||||||
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,119 +0,0 @@
|
||||||
// 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();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue