Commit 7602bd1a authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

automatop: remove this type of formula operator.

This was only used in ELTL stuff, which I just removed because it was
unused.

* src/ltlast/automatop.cc, src/ltlast/automatop.hh,
src/ltlast/formula_tree.cc, src/ltlast/formula_tree.hh,
src/ltlast/nfa.cc, src/ltlast/nfa.hh: Delete.
* src/ltlast/Makefile.am: Adjust.
* src/ltlast/allnodes.hh, src/ltlast/formula.hh, src/ltlast/predecl.hh,
src/ltlast/visitor.hh, src/ltltest/equals.cc, src/ltltest/ltlrel.cc,
src/ltltest/reduc.cc, src/ltlvisit/clone.cc, src/ltlvisit/clone.hh,
src/ltlvisit/dotty.cc, src/ltlvisit/lbt.cc, src/ltlvisit/mark.cc,
src/ltlvisit/postfix.cc, src/ltlvisit/postfix.hh,
src/ltlvisit/relabel.cc, src/ltlvisit/simplify.cc, src/ltlvisit/snf.cc,
src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbatest/ltl2tgba.cc,
iface/dve2/dve2check.cc: Remove all references to automatop.
parent af8ce5df
......@@ -379,12 +379,10 @@ main(int argc, char **argv)
spot::ltl::unop::dump_instances(std::cerr);
spot::ltl::binop::dump_instances(std::cerr);
spot::ltl::multop::dump_instances(std::cerr);
spot::ltl::automatop::dump_instances(std::cerr);
assert(spot::ltl::atomic_prop::instance_count() == 0);
assert(spot::ltl::unop::instance_count() == 0);
assert(spot::ltl::binop::instance_count() == 0);
assert(spot::ltl::multop::instance_count() == 0);
assert(spot::ltl::automatop::instance_count() == 0);
exit(exit_code);
}
## -*- coding: utf-8 -*-
## Copyright (C) 2009, 2010, 2011, 2013 Laboratoire de Recherche et
## Développement de l'Epita (LRDE).
## Copyright (C) 2009, 2010, 2011, 2013, 2014 Laboratoire de Recherche
## et Développement de l'Epita (LRDE).
## Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
## département Systèmes Répartis Coopératifs (SRC), Université Pierre
## et Marie Curie.
......@@ -29,13 +29,11 @@ ltlastdir = $(pkgincludedir)/ltlast
ltlast_HEADERS = \
allnodes.hh \
atomic_prop.hh \
automatop.hh \
binop.hh \
bunop.hh \
constant.hh \
formula.hh \
multop.hh \
nfa.hh \
predecl.hh \
refformula.hh \
unop.hh \
......@@ -44,14 +42,10 @@ ltlast_HEADERS = \
noinst_LTLIBRARIES = libltlast.la
libltlast_la_SOURCES = \
atomic_prop.cc \
automatop.cc \
binop.cc \
bunop.cc \
constant.cc \
formula.cc \
formula_tree.cc \
formula_tree.hh \
multop.cc \
nfa.cc \
refformula.cc \
unop.cc
// Copyright (C) 2003, 2004, 2010 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2014 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// 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.
......@@ -31,7 +34,6 @@
# include "multop.hh"
# include "atomic_prop.hh"
# include "constant.hh"
# include "automatop.hh"
# include "bunop.hh"
#endif // SPOT_LTLAST_ALLNODES_HH
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire
// de Recherche et Développement de l'Epita (LRDE)
//
// 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
#include "config.h"
#include <iostream>
#include <cstddef>
#include "automatop.hh"
#include "nfa.hh"
#include "visitor.hh"
namespace spot
{
namespace ltl
{
automatop::automatop(const nfa::ptr nfa, vec* v, bool negated)
: ref_formula(AutomatOp), nfa_(nfa), children_(v), negated_(negated)
{
assert(nfa);
is.boolean = false;
is.sugar_free_boolean = true;
is.in_nenoform = true;
is.X_free = true;
is.sugar_free_ltl = true;
is.ltl_formula = false;
is.eltl_formula = true;
is.psl_formula = false;
is.sere_formula = false;
is.finite = false;
is.eventual = false;
is.universal = false;
is.syntactic_safety = false;
is.syntactic_guarantee = false;
is.syntactic_obligation = false;
is.syntactic_recurrence = false;
is.syntactic_persistence = false;
is.not_marked = true;
is.accepting_eword = false;
unsigned s = v->size();
for (unsigned i = 0; i < s; ++i)
props &= (*v)[i]->get_props();
}
automatop::~automatop()
{
// Get this instance out of the instance map.
size_t c = instances.erase(key(get_nfa(), negated_, children_));
assert(c == 1);
(void) c; // For the NDEBUG case.
// Dereference children.
unsigned s = size();
for (unsigned n = 0; n < s; ++n)
nth(n)->destroy();
delete children_;
}
std::string
automatop::dump() const
{
std::string r = is_negated() ? "!" : "";
r += get_nfa()->get_name();
r += "(";
r += nth(0)->dump();
for (unsigned n = 1; n < size(); ++n)
r += ", " + nth(n)->dump();
r += ")";
return r;
}
void
automatop::accept(visitor& v) const
{
v.visit(this);
}
automatop::map automatop::instances;
const automatop*
automatop::instance(const nfa::ptr nfa, vec* v, bool negated)
{
assert(nfa);
const automatop* res;
auto ires = instances.insert(std::make_pair(key(nfa, negated, v),
nullptr));
if (!ires.second)
{
// The instance already exists.
for (vec::iterator vi = v->begin(); vi != v->end(); ++vi)
(*vi)->destroy();
delete v;
res = ires.first->second;
}
else
{
res = ires.first->second = new automatop(nfa, v, negated);
}
res->clone();
return res;
}
unsigned
automatop::instance_count()
{
return instances.size();
}
std::ostream&
automatop::dump_instances(std::ostream& os)
{
for (const auto& i: instances)
os << i.second << " = "
<< i.second->ref_count_() << " * "
<< i.second->dump()
<< std::endl;
return os;
}
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2012, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE)
//
// 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
/// \file ltlast/automatop.hh
/// \brief ELTL automaton operators
#ifndef SPOT_LTLAST_AUTOMATOP_HH
# define SPOT_LTLAST_AUTOMATOP_HH
# include "refformula.hh"
# include <vector>
# include <tuple>
# include <iosfwd>
# include <map>
# include "nfa.hh"
namespace spot
{
namespace ltl
{
/// \ingroup eltl_ast
/// \brief Automaton operators.
///
class SPOT_API automatop : public ref_formula
{
public:
/// List of formulae.
typedef std::vector<const formula*> vec;
/// \brief Build a spot::ltl::automatop with many children.
///
/// This vector is acquired by the spot::ltl::automatop 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::automatop.
static const automatop*
instance(const nfa::ptr nfa, vec* v, bool negated);
virtual void accept(visitor& v) const;
/// Get the number of arguments.
unsigned size() const
{
return children_->size();
}
/// \brief Get the nth argument.
///
/// Starting with \a n = 0.
const formula* nth(unsigned n) const
{
return (*children_)[n];
}
/// Get the NFA of this operator.
const spot::ltl::nfa::ptr get_nfa() const
{
return nfa_;
}
/// Whether the automaton is negated.
bool is_negated() const
{
return negated_;
}
/// Return a canonic representation of the atomic proposition
std::string dump() const;
/// Number of instantiated multop operators. For debugging.
static unsigned instance_count();
/// Dump all instances. For debugging.
static std::ostream& dump_instances(std::ostream& os);
protected:
typedef std::tuple<nfa::ptr, bool, vec*> key;
/// Comparison functor used internally by ltl::automatop.
struct tripletcmp
{
bool
operator()(const key& p1, const key& p2) const
{
if (std::get<0>(p1) != std::get<0>(p2))
return std::get<0>(p1) < std::get<0>(p2);
if (std::get<1>(p1) != std::get<1>(p2))
return std::get<1>(p1) < std::get<1>(p2);
return *std::get<2>(p1) < *std::get<2>(p2);
}
};
typedef std::map<key, const automatop*> map;
static map instances;
automatop(const nfa::ptr, vec* v, bool negated);
virtual ~automatop();
private:
const nfa::ptr nfa_;
vec* children_;
bool negated_;
};
}
}
#endif // SPOT_LTLAST_AUTOMATOP_HH
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire
// de Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
//
// This file is part of Spot, a model checking library.
......@@ -78,8 +78,7 @@ namespace spot
UnOp,
BinOp,
MultOp,
BUnOp,
AutomatOp };
BUnOp };
protected:
formula(opkind k) : count_(max_count++), kind_(k)
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2012, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
#include "config.h"
#include <cassert>
#include "formula_tree.hh"
#include "allnodes.hh"
namespace spot
{
namespace ltl
{
namespace formula_tree
{
const formula*
instanciate(const node_ptr np, const std::vector<const formula*>& v)
{
if (node_atomic* n = dynamic_cast<node_atomic*>(np.get()))
return n->i == True ? constant::true_instance() :
n->i == False ? constant::false_instance() : v.at(n->i)->clone();
if (node_unop* n = dynamic_cast<node_unop*>(np.get()))
return unop::instance(n->op, instanciate(n->child, v));
if (node_nfa* n = dynamic_cast<node_nfa*>(np.get()))
{
automatop::vec* va = new automatop::vec;
std::vector<node_ptr>::const_iterator i = n->children.begin();
while (i != n->children.end())
va->push_back(instanciate(*i++, v));
return automatop::instance(n->nfa, va, false);
}
if (node_binop* n = dynamic_cast<node_binop*>(np.get()))
return binop::instance(n->op,
instanciate(n->lhs, v),
instanciate(n->rhs, v));
if (node_multop* n = dynamic_cast<node_multop*>(np.get()))
return multop::instance(n->op,
instanciate(n->lhs, v),
instanciate(n->rhs, v));
SPOT_UNREACHABLE();
}
size_t
arity(const node_ptr np)
{
if (node_atomic* n = dynamic_cast<node_atomic*>(np.get()))
return std::max(n->i + 1, 0);
if (node_unop* n = dynamic_cast<node_unop*>(np.get()))
return arity(n->child);
if (node_nfa* n = dynamic_cast<node_nfa*>(np.get()))
{
size_t res = 0;
std::vector<node_ptr>::const_iterator i = n->children.begin();
while (i != n->children.end())
res = std::max(arity(*i++), res);
return res;
}
if (node_binop* n = dynamic_cast<node_binop*>(np.get()))
return std::max(arity(n->lhs), arity(n->rhs));
if (node_multop* n = dynamic_cast<node_multop*>(np.get()))
return std::max(arity(n->lhs), arity(n->rhs));
SPOT_UNREACHABLE();
}
}
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2012, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
/// \file ltlast/formula_tree.hh
/// \brief Trees representing formulae where atomic propositions are unknown
#ifndef SPOT_LTLAST_FORMULA_TREE_HH
# define SPOT_LTLAST_FORMULA_TREE_HH
# include "formula.hh"
# include <vector>
# include <memory>
# include "multop.hh"
# include "binop.hh"
# include "unop.hh"
# include "nfa.hh"
namespace spot
{
namespace ltl
{
/// Trees representing formulae where atomic propositions are unknown.
namespace formula_tree
{
// These struct should not need to be made public using
// SPOT_API, unfortunately dynamic_cast<> with g++-4.0.1 fails
// on Darwin if we do not.
struct SPOT_API node
{
virtual ~node() {};
};
typedef std::shared_ptr<node> node_ptr;
struct SPOT_API node_unop : node
{
unop::type op;
node_ptr child;
};
struct SPOT_API node_binop : node
{
binop::type op;
node_ptr lhs;
node_ptr rhs;
};
struct SPOT_API node_multop : node
{
multop::type op;
node_ptr lhs;
node_ptr rhs;
};
struct SPOT_API node_nfa : node
{
std::vector<node_ptr> children;
spot::ltl::nfa::ptr nfa;
};
/// Integer values for True and False used in node_atomic.
enum { True = -1, False = -2 };
struct SPOT_API node_atomic : node
{
int i;
};
/// Instanciate the formula corresponding to the node with
/// atomic propositions taken from \a v.
const formula* instanciate(const node_ptr np,
const std::vector<const formula*>& v);
/// Get the arity.
size_t arity(const node_ptr np);
}
}
}
#endif // SPOT_LTLAST_FORMULA_TREE_HH_
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
#include "config.h"
#include <cassert>
#include "nfa.hh"
#include "formula_tree.hh"
namespace spot
{
namespace ltl
{
nfa::nfa()
: is_(), si_(), arity_(0), name_(), init_(0), finals_()
{
}
nfa::~nfa()
{
is_map::iterator i;
for (i = is_.begin(); i != is_.end(); ++i)
{
state::iterator i2;
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
delete *i2;
delete i->second;
}
}
nfa::state*
nfa::add_state(int name)
{
is_map::iterator i = is_.find(name);
if (i == is_.end())
{
state* s = new nfa::state;
is_[name] = s;
si_[s] = name;
if (!init_)
init_ = s;
return s;
}
return i->second;
}
void
nfa::add_transition(int src, int dst, const label lbl)
{
state* s = add_state(src);
nfa::transition* t = new transition;
t->dst = add_state(dst);
t->lbl = lbl;
s->push_back(t);
size_t arity = formula_tree::arity(formula_tree::node_ptr(lbl));
if (arity >= arity_)
arity_ = arity;
}
void
nfa::set_init_state(int name)
{
init_ = add_state(name);
}
void
nfa::set_final(int name)
{
finals_.insert(name);
}
bool
nfa::is_final(const state* s)
{
return finals_.find(format_state(s)) != finals_.end();
}
bool
nfa::is_loop()
{
return finals_.empty();
}