From 543190f2bcb67007ed2e1df0dbbc2d1435210418 Mon Sep 17 00:00:00 2001 From: Damien Lefortier Date: Tue, 25 Mar 2008 16:52:06 +0100 Subject: [PATCH] Template ltlast/ & ltlenv/ classes in internal/ & Add ELTL parser. --- ChangeLog | 24 +++ configure.ac | 6 + src/Makefile.am | 9 +- src/eltlast/Makefile.am | 44 ++++++ src/eltlast/allnodes.hh | 36 +++++ src/eltlast/atomic_prop.hh | 42 ++++++ src/eltlast/automatop.cc | 121 +++++++++++++++ src/eltlast/automatop.hh | 84 +++++++++++ src/eltlast/binop.hh | 45 ++++++ src/eltlast/constant.hh | 42 ++++++ src/eltlast/formula.hh | 96 ++++++++++++ src/eltlast/multop.hh | 44 ++++++ src/eltlast/nfa.cc | 127 ++++++++++++++++ src/eltlast/nfa.hh | 147 ++++++++++++++++++ src/eltlast/refformula.hh | 42 ++++++ src/eltlast/unop.hh | 42 ++++++ src/eltlast/visitor.hh | 82 ++++++++++ src/eltlenv/Makefile.am | 27 ++++ src/eltlenv/declenv.hh | 44 ++++++ src/eltlenv/defaultenv.hh | 45 ++++++ src/eltlenv/environment.hh | 39 +++++ src/eltlparse/Makefile.am | 62 ++++++++ src/eltlparse/eltlparse.yy | 279 +++++++++++++++++++++++++++++++++++ src/eltlparse/eltlscan.ll | 183 +++++++++++++++++++++++ src/eltlparse/fmterror.cc | 48 ++++++ src/eltlparse/parsedecl.hh | 43 ++++++ src/eltlparse/public.hh | 84 +++++++++++ src/eltltest/Makefile.am | 44 ++++++ src/eltltest/acc.cc | 42 ++++++ src/eltltest/acc.test | 31 ++++ src/eltltest/defs.in | 75 ++++++++++ src/eltltest/nfa.cc | 57 +++++++ src/eltltest/nfa.test | 6 + src/internal/Makefile.am | 44 ++++++ src/internal/atomic_prop.hh | 85 +++++++++++ src/internal/atomic_prop.hxx | 123 +++++++++++++++ src/internal/binop.hh | 99 +++++++++++++ src/internal/binop.hxx | 156 ++++++++++++++++++++ src/internal/constant.hh | 72 +++++++++ src/internal/constant.hxx | 112 ++++++++++++++ src/internal/declenv.hh | 69 +++++++++ src/internal/declenv.hxx | 83 +++++++++++ src/internal/defaultenv.hh | 59 ++++++++ src/internal/defaultenv.hxx | 68 +++++++++ src/internal/environment.hh | 72 +++++++++ src/internal/formula.hh | 162 ++++++++++++++++++++ src/internal/formula.hxx | 86 +++++++++++ src/internal/multop.hh | 138 +++++++++++++++++ src/internal/multop.hxx | 252 +++++++++++++++++++++++++++++++ src/internal/predecl.hh | 49 ++++++ src/internal/refformula.hh | 57 +++++++ src/internal/refformula.hxx | 69 +++++++++ src/internal/unop.hh | 85 +++++++++++ src/internal/unop.hxx | 122 +++++++++++++++ src/ltlast/Makefile.am | 14 -- src/ltlast/allnodes.hh | 2 - src/ltlast/atomic_prop.hh | 42 +----- src/ltlast/binop.hh | 54 +------ src/ltlast/constant.hh | 28 +--- src/ltlast/formula.hh | 162 +++++++------------- src/ltlast/multop.hh | 89 +---------- src/ltlast/refformula.hh | 18 +-- src/ltlast/unop.hh | 44 +----- src/ltlast/visitor.hh | 13 +- src/ltlenv/Makefile.am | 10 +- src/ltlenv/declenv.hh | 31 +--- src/ltlenv/defaultenv.hh | 16 +- src/ltlenv/environment.hh | 34 +---- src/ltlparse/public.hh | 1 + src/ltlvisit/randomltl.cc | 1 + src/tgba/tgbatba.cc | 1 + src/tgbaalgos/randomgraph.hh | 1 + src/tgbaparse/public.hh | 1 + src/tgbatest/explicit.cc | 1 + 74 files changed, 4299 insertions(+), 468 deletions(-) create mode 100644 src/eltlast/Makefile.am create mode 100644 src/eltlast/allnodes.hh create mode 100644 src/eltlast/atomic_prop.hh create mode 100644 src/eltlast/automatop.cc create mode 100644 src/eltlast/automatop.hh create mode 100644 src/eltlast/binop.hh create mode 100644 src/eltlast/constant.hh create mode 100644 src/eltlast/formula.hh create mode 100644 src/eltlast/multop.hh create mode 100644 src/eltlast/nfa.cc create mode 100644 src/eltlast/nfa.hh create mode 100644 src/eltlast/refformula.hh create mode 100644 src/eltlast/unop.hh create mode 100644 src/eltlast/visitor.hh create mode 100644 src/eltlenv/Makefile.am create mode 100644 src/eltlenv/declenv.hh create mode 100644 src/eltlenv/defaultenv.hh create mode 100644 src/eltlenv/environment.hh create mode 100644 src/eltlparse/Makefile.am create mode 100644 src/eltlparse/eltlparse.yy create mode 100644 src/eltlparse/eltlscan.ll create mode 100644 src/eltlparse/fmterror.cc create mode 100644 src/eltlparse/parsedecl.hh create mode 100644 src/eltlparse/public.hh create mode 100644 src/eltltest/Makefile.am create mode 100644 src/eltltest/acc.cc create mode 100755 src/eltltest/acc.test create mode 100644 src/eltltest/defs.in create mode 100644 src/eltltest/nfa.cc create mode 100755 src/eltltest/nfa.test create mode 100644 src/internal/Makefile.am create mode 100644 src/internal/atomic_prop.hh create mode 100644 src/internal/atomic_prop.hxx create mode 100644 src/internal/binop.hh create mode 100644 src/internal/binop.hxx create mode 100644 src/internal/constant.hh create mode 100644 src/internal/constant.hxx create mode 100644 src/internal/declenv.hh create mode 100644 src/internal/declenv.hxx create mode 100644 src/internal/defaultenv.hh create mode 100644 src/internal/defaultenv.hxx create mode 100644 src/internal/environment.hh create mode 100644 src/internal/formula.hh create mode 100644 src/internal/formula.hxx create mode 100644 src/internal/multop.hh create mode 100644 src/internal/multop.hxx create mode 100644 src/internal/predecl.hh create mode 100644 src/internal/refformula.hh create mode 100644 src/internal/refformula.hxx create mode 100644 src/internal/unop.hh create mode 100644 src/internal/unop.hxx diff --git a/ChangeLog b/ChangeLog index 12a5dbd30..62e3d9027 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,27 @@ +2008-04-16 Damien Lefortier + + * configure.ac, Makefile.am: Add src/eltltest/ support. + * src/eltlast/Makefile.am, src/eltlast/formula.hh, + src/eltlast/nfa.cc, src/eltlast/nfa.hh: Update nfa implementation. + * src/eltlparse/Makefile.am, src/eltlparse/eltlparse.yy, + src/eltlparse/eltlscan.ll, src/eltlparse/parsedecl.hh, + src/eltlparse/public.hh: Finish the parser for ELTL files. + * src/eltltest/Makefile.am, src/eltltest/acc.cc, + src/eltltest/acc.test: Add tests for the ELTL parser. + * src/internal/atomic_prop.hh, src/internal/atomic_prop.hxx, + src/internal/binop.hh, src/internal/binop.hxx, + src/internal/constant.hh, src/internal/constant.hxx, + src/internal/defaultenv.hh, src/internal/defaultenv.hxx, + src/internal/environment.hh, src/internal/formula.hh, + src/internal/formula.hxx, src/internal/multop.hh, + src/internal/multop.hxx, src/internal/predecl.hh, + src/internal/refformula.hh, src/internal/refformula.hxx, + src/internal/unop.hh src/internal/unop.hxx: Clean and update + documentation. + * src/ltlast/formula.hh, src/ltlenv/Makefile.am, + src/ltlenv/declenv.hh, src/tgbaalgos/randomgraph.hh: Fix make + check issues. + 2008-04-14 Alexandre Duret-Lutz Kill some FIXMEs. diff --git a/configure.ac b/configure.ac index 2067044a5..0b975314f 100644 --- a/configure.ac +++ b/configure.ac @@ -79,11 +79,17 @@ AC_CONFIG_FILES([ iface/gspn/Makefile iface/gspn/defs src/Makefile + src/eltlast/Makefile + src/eltlenv/Makefile + src/eltlparse/Makefile + src/eltltest/Makefile + src/eltltest/defs src/evtgba/Makefile src/evtgbaalgos/Makefile src/evtgbaparse/Makefile src/evtgbatest/Makefile src/evtgbatest/defs + src/internal/Makefile src/ltlast/Makefile src/ltlenv/Makefile src/ltlparse/Makefile diff --git a/src/Makefile.am b/src/Makefile.am index 8d7f096dd..b015b250f 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -23,20 +23,21 @@ AUTOMAKE_OPTIONS = subdir-objects # List directories in the order they must be built. # Keep tests at the end. -SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse \ +SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse internal \ + eltlenv eltlast eltlparse \ tgba tgbaalgos tgbaparse \ evtgba evtgbaalgos evtgbaparse . \ - ltltest tgbatest evtgbatest sanity + ltltest eltltest tgbatest evtgbatest sanity lib_LTLIBRARIES = libspot.la libspot_la_SOURCES = libspot_la_LDFLAGS = $(BUDDY_LDFLAGS) -no-undefined libspot_la_LIBADD = \ misc/libmisc.la \ - ltlenv/libltlenv.la \ ltlparse/libltlparse.la \ ltlvisit/libltlvisit.la \ - ltlast/libltlast.la \ + eltlast/libeltlast.la \ + eltlparse/libeltlparse.la \ tgba/libtgba.la \ tgbaalgos/libtgbaalgos.la \ tgbaparse/libtgbaparse.la \ diff --git a/src/eltlast/Makefile.am b/src/eltlast/Makefile.am new file mode 100644 index 000000000..0b8fae81d --- /dev/null +++ b/src/eltlast/Makefile.am @@ -0,0 +1,44 @@ +## Copyright (C) 2008 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. + +AM_CPPFLAGS = -I$(srcdir)/.. +AM_CXXFLAGS = $(WARNING_CXXFLAGS) + +eltlastdir = $(pkgincludedir)/eltlast + +eltlast_HEADERS = \ + allnodes.hh \ + atomic_prop.hh \ + automatop.hh \ + binop.hh \ + constant.hh \ + formula.hh \ + multop.hh \ + nfa.hh \ + refformula.hh \ + unop.hh \ + visitor.hh + + +noinst_LTLIBRARIES = libeltlast.la +libeltlast_la_SOURCES = \ + automatop.cc \ + nfa.cc \ No newline at end of file diff --git a/src/eltlast/allnodes.hh b/src/eltlast/allnodes.hh new file mode 100644 index 000000000..d7ab24d39 --- /dev/null +++ b/src/eltlast/allnodes.hh @@ -0,0 +1,36 @@ +// 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 eltlast/allnodes.hh +/// \brief Define all ELTL node types. +/// +/// This file is usually needed when \b defining a visitor. +#ifndef SPOT_ELTLAST_ALLNODES_HH +# define SPOT_ELTLAST_ALLNODES_HH + +# include "binop.hh" +# include "unop.hh" +# include "multop.hh" +# include "atomic_prop.hh" +# include "constant.hh" +# include "automatop.hh" + +#endif // SPOT_ELTLAST_ALLNODES_HH diff --git a/src/eltlast/atomic_prop.hh b/src/eltlast/atomic_prop.hh new file mode 100644 index 000000000..2e03cd0f3 --- /dev/null +++ b/src/eltlast/atomic_prop.hh @@ -0,0 +1,42 @@ +// Copyright (C) 2008 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 eltlast/atomic_prop.hh +/// \brief ELTL atomic propositions +#ifndef SPOT_ELTLAST_ATOMIC_PROP_HH +# define SPOT_ELTLAST_ATOMIC_PROP_HH + +# include "formula.hh" +# include "internal/atomic_prop.hh" + +namespace spot +{ + namespace eltl + { + + /// \brief Atomic propositions. + /// \ingroup eltl_ast + typedef spot::internal::atomic_prop atomic_prop; + + } +} + +#endif // SPOT_ELTLAST_ATOMICPROP_HH diff --git a/src/eltlast/automatop.cc b/src/eltlast/automatop.cc new file mode 100644 index 000000000..f3a7b1a69 --- /dev/null +++ b/src/eltlast/automatop.cc @@ -0,0 +1,121 @@ +// Copyright (C) 2008 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 "visitor.hh" +#include "automatop.hh" + +namespace spot +{ + namespace eltl + { + automatop::automatop(vec* v) + : nfa_(), children_(v) + { + dump_ = "automatop("; + dump_ += (*v)[0]->dump(); + for (unsigned n = 1; n < v->size(); ++n) + dump_ += ", " + (*v)[n]->dump(); + dump_ += ")"; + set_key_(); + } + + automatop::~automatop() + { + delete children_; + } + + void + automatop::accept(visitor& v) + { + v.visit(this); + } + + void + automatop::accept(const_visitor& v) const + { + v.visit(this); + } + + automatop* + automatop::instance(nfa::ptr nfa, formula* autop) + { + vec* v = new vec; + v->push_back(autop); + automatop* res = instance(v); + res->nfa_ = nfa; + return res; + } + + automatop* + automatop::instance(formula* first, formula* second) + { + vec* v = new vec; + v->push_back(first); + v->push_back(second); + return instance(v); + } + + automatop* + automatop::instance(vec* v) + { + // Inline children of same kind. + { + vec inlined; + vec::iterator i = v->begin(); + while (i != v->end()) + { + if (automatop* p = dynamic_cast(*i)) + { + unsigned ps = p->size(); + for (unsigned n = 0; n < ps; ++n) + inlined.push_back(p->nth(n)); + formula::unref(*i); + i = v->erase(i); + } + else + ++i; + } + v->insert(v->end(), inlined.begin(), inlined.end()); + } + + automatop* res = new automatop(v); + return static_cast(res->ref()); + } + + unsigned + automatop::size() const + { + return children_->size(); + } + + const formula* + automatop::nth(unsigned n) const + { + return (*children_)[n]; + } + + formula* + automatop::nth(unsigned n) + { + return (*children_)[n]; + } + } +} diff --git a/src/eltlast/automatop.hh b/src/eltlast/automatop.hh new file mode 100644 index 000000000..9b94521ea --- /dev/null +++ b/src/eltlast/automatop.hh @@ -0,0 +1,84 @@ +// Copyright (C) 2008 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 eltlast/automatop.hh +/// \brief ELTL automaton operators +#ifndef SPOT_ELTLAST_AUTOMATOP_HH +# define SPOT_ELTLAST_AUTOMATOP_HH + +# include "multop.hh" +# include "refformula.hh" +# include "nfa.hh" + +namespace spot +{ + namespace eltl + { + + /// \brief Automaton operators. + /// \ingroup eltl_ast + /// + class automatop : public ref_formula + { + public: + /// List of formulae. + typedef std::vector vec; + + /// \brief Build a spot::eltl::automatop with automaton \c nfa + /// and children of \c autop. + static automatop* instance(nfa::ptr nfa, formula* autop); + + /// \brief Build a spot::eltl::automatop with two children. + /// + /// If one of the children itself is a spot::eltl::automatop, + /// it will be merged. This allows incremental building of + /// n-ary eltl::automatop. + static automatop* instance(formula* first, formula* second); + + /// \brief Build a spot::eltl::automatop with many children. + static automatop* instance(vec* v); + + virtual void accept(visitor& v); + virtual void accept(const_visitor& v) const; + + /// Get the number of argument. + unsigned size() const; + /// \brief Get the nth argument. + /// + /// Starting with \a n = 0. + const formula* nth(unsigned n) const; + /// \brief Get the nth argument. + /// + /// Starting with \a n = 0. + formula* nth(unsigned n); + + protected: + automatop(vec* v); + virtual ~automatop(); + + private: + nfa::ptr nfa_; + vec* children_; + }; + } +} + +#endif // SPOT_ELTLAST_AUTOMATOP_HH diff --git a/src/eltlast/binop.hh b/src/eltlast/binop.hh new file mode 100644 index 000000000..8b78e3271 --- /dev/null +++ b/src/eltlast/binop.hh @@ -0,0 +1,45 @@ +// Copyright (C) 2008 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 eltlast/binop.hh +/// \brief ELTL binary operators +/// +/// This does not include \c AND and \c OR operators. These are +/// considered to be multi-operand operators (see spot::eltl::multop). +#ifndef SPOT_ELTLAST_BINOP_HH +# define SPOT_ELTLAST_BINOP_HH + +# include "formula.hh" +# include "internal/binop.hh" + +namespace spot +{ + namespace eltl + { + + /// \brief Binary operator. + /// \ingroup eltl_ast + typedef spot::internal::binop binop; + + } +} + +#endif // SPOT_ELTLAST_BINOP_HH diff --git a/src/eltlast/constant.hh b/src/eltlast/constant.hh new file mode 100644 index 000000000..17a04a97c --- /dev/null +++ b/src/eltlast/constant.hh @@ -0,0 +1,42 @@ +// 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 eltlast/constant.hh +/// \brief ELTL constants +#ifndef SPOT_ELTLAST_CONSTANT_HH +# define SPOT_ELTLAST_CONSTANT_HH + +# include "formula.hh" +# include "internal/constant.hh" + +namespace spot +{ + namespace eltl + { + + /// \brief A constant (True or False) + /// \ingroup eltl_ast + typedef spot::internal::constant constant; + + } +} + +#endif // SPOT_ELTLAST_CONSTANT_HH diff --git a/src/eltlast/formula.hh b/src/eltlast/formula.hh new file mode 100644 index 000000000..e8d6c66b9 --- /dev/null +++ b/src/eltlast/formula.hh @@ -0,0 +1,96 @@ +// Copyright (C) 2008 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 eltlast/formula.hh +/// \brief ELTL formula interface +#ifndef SPOT_ELTLAST_FORMULA_HH +# define SPOT_ELTLAST_FORMULA_HH + +# include "internal/formula.hh" + +namespace spot +{ + namespace eltl + { + /// \defgroup eltl ELTL formulae + /// + /// This module gathers types and definitions related to ELTL formulae. + + /// \addtogroup eltl_essential Essential ELTL types + /// \ingroup eltl + + /// \addtogroup eltl_ast ELTL Abstract Syntax Tree + /// \ingroup eltl + + /// Forward declarations + struct visitor; + struct const_visitor; + + /// \brief An ELTL formula. + /// \ingroup eltl_essential + /// \ingroup eltl_ast + /// + /// The only way you can work with a formula is to + /// build a spot::eltl::visitor or spot::eltl::const_visitor. + struct eltl_t + { + typedef spot::eltl::visitor visitor; + typedef spot::eltl::const_visitor const_visitor; + + enum binop { Xor, Implies, Equiv }; + const char* binop_name(binop op) const + { + switch (op) + { + case Xor: + return "Xor"; + case Implies: + return "Implies"; + case Equiv: + return "Equiv"; + } + // Unreachable code. + assert(0); + return 0; + } + + enum unop { Not }; + const char* unop_name(unop op) const + { + switch (op) + { + case Not: + return "Not"; + } + // Unreachable code. + assert(0); + return 0; + } + }; + + typedef spot::internal::formula formula; + + typedef spot::internal::formula_ptr_less_than formula_ptr_less_than; + typedef spot::internal::formula_ptr_hash formula_ptr_hash; + } +} + +#endif /* !SPOT_ELTLAST_FORMULA_HH_ */ diff --git a/src/eltlast/multop.hh b/src/eltlast/multop.hh new file mode 100644 index 000000000..70a1ac72c --- /dev/null +++ b/src/eltlast/multop.hh @@ -0,0 +1,44 @@ +// Copyright (C) 2008 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 eltlast/multop.hh +/// \brief ELTL multi-operand operators +#ifndef SPOT_ELTLAST_MULTOP_HH +# define SPOT_ELTLAST_MULTOP_HH + +# include "formula.hh" +# include "internal/multop.hh" + +namespace spot +{ + namespace eltl + { + + /// \brief Multi-operand operators. + /// \ingroup eltl_ast + /// + /// These operators are considered commutative and associative. + typedef spot::internal::multop multop; + + } +} + +#endif // SPOT_ELTLAST_MULTOP_HH diff --git a/src/eltlast/nfa.cc b/src/eltlast/nfa.cc new file mode 100644 index 000000000..a50abe036 --- /dev/null +++ b/src/eltlast/nfa.cc @@ -0,0 +1,127 @@ +// Copyright (C) 2008 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 +#include "nfa.hh" + +namespace spot +{ + namespace eltl + { + nfa::nfa() + : ns_(), sn_(), init_(0), arity_(0), finals_() + { + } + + nfa::~nfa() + { + ns_map::iterator i; + for (i = ns_.begin(); i != ns_.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(const std::string& name) + { + ns_map::iterator i = ns_.find(name); + if (i == ns_.end()) + { + state* s = new nfa::state; + ns_[name] = s; + sn_[s] = name; + + if (!init_) + init_ = s; + return s; + } + return i->second; + } + + void + nfa::add_transition(const std::string& s, const std::string& d, unsigned c) + { + state* source = add_state(s); + nfa::transition* t = new transition; + t->dest = add_state(d); + t->cost = c; + source->push_back(t); + if (c > arity_) + arity_ = c; + } + + void + nfa::set_init_state(const std::string& state) + { + init_ = add_state(state); + } + + void + nfa::set_final(const std::string& state) + { + finals_.insert(state); + } + + bool + nfa::is_final(const std::string& state) + { + return finals_.find(state) != finals_.end(); + } + + unsigned + nfa::arity() + { + return arity_ + 1; + } + + const nfa::state* + nfa::get_init_state() + { + if (!init_) + add_state("empty"); + return init_; + } + + nfa::iterator + nfa::begin(const state* s) const + { + return nfa::iterator(s->begin()); + } + + nfa::iterator + nfa::end(const state* s) const + { + return nfa::iterator(s->end()); + } + + std::string + nfa::format_state(const state* s) const + { + sn_map::const_iterator i = sn_.find(s); + assert(i != sn_.end()); + return i->second; + } + } +} diff --git a/src/eltlast/nfa.hh b/src/eltlast/nfa.hh new file mode 100644 index 000000000..250ec7b11 --- /dev/null +++ b/src/eltlast/nfa.hh @@ -0,0 +1,147 @@ +// Copyright (C) 2008 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 eltlast/nfa.hh +/// \brief NFA interface +#ifndef SPOT_ELTLAST_NFA_HH +# define SPOT_ELTLAST_NFA_HH + +# include "misc/hash.hh" +# include +# include +# include + +namespace spot +{ + namespace eltl + { + /// Forward declaration. See below. + class succ_iterator; + + /// \brief A Nondeterministic Finite Automaton used in ELTL + /// automata operators. + /// \ingroup eltl_essential + class nfa + { + public: + struct transition; + typedef std::list state; + /// Iterator over the successors of a state. + typedef succ_iterator iterator; + typedef boost::shared_ptr ptr; + + /// Explicit transitions. + struct transition + { + unsigned cost; + const state* dest; + }; + + nfa(); + ~nfa(); + + void + add_transition(const std::string& s, const std::string& d, unsigned c); + + void + set_init_state(const std::string& state); + const state* + get_init_state(); + + void + set_final(const std::string& state); + bool + is_final(const std::string& state); + + /// \brief Get the `arity' i.e. max t.cost, for each transition t. + unsigned + arity(); + + /// \brief Return an iterator on the first succesor (if any) of \a state. + /// + /// The usual way to do this with a \c for lopp. + /// \code + /// for (nfa::iterator i = a.begin(state); i != a.end(state); ++i) + /// ... + /// \endcode + iterator + begin(const state* state) const; + + /// \brief Return an iterator just past the last succesor of \a state. + iterator + end(const state* state) const; + + std::string + format_state(const state* state) const; + + private: + state* + add_state(const std::string& name); + + typedef Sgi::hash_map ns_map; + typedef Sgi::hash_map > sn_map; + + ns_map ns_; + sn_map sn_; + state* init_; + + unsigned arity_; + std::set finals_; + + /// Explicitly disllow use of implicity generated member functions + /// we don't want. + nfa(const nfa& other); + nfa& operator=(const nfa& other); + }; + + class succ_iterator + { + public: + succ_iterator(const nfa::state::const_iterator s) + : i_(s) + { + } + + void + operator++() + { + ++i_; + } + + bool + operator!=(const succ_iterator& rhs) const + { + return i_ != rhs.i_; + } + + const nfa::transition* operator*() const + { + return *i_; + } + + private: + nfa::state::const_iterator i_; + }; + + } +} + +#endif // SPOT_ELTLAST_NFA_HH_ diff --git a/src/eltlast/refformula.hh b/src/eltlast/refformula.hh new file mode 100644 index 000000000..cd5d9db82 --- /dev/null +++ b/src/eltlast/refformula.hh @@ -0,0 +1,42 @@ +// Copyright (C) 2008 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 eltlast/refformula.hh +/// \brief Reference-counted ELTL formulae +#ifndef SPOT_ELTLAST_REFFORMULA_HH +# define SPOT_ELTLAST_REFFORMULA_HH + +# include "formula.hh" +# include "internal/refformula.hh" + +namespace spot +{ + namespace eltl + { + + /// \brief A reference-counted ELTL formula. + /// \ingroup eltl_ast + typedef spot::internal::ref_formula ref_formula; + + } +} + +#endif // SPOT_ELTLAST_REFFORMULA_HH diff --git a/src/eltlast/unop.hh b/src/eltlast/unop.hh new file mode 100644 index 000000000..73ff7bf0e --- /dev/null +++ b/src/eltlast/unop.hh @@ -0,0 +1,42 @@ +// Copyright (C) 2008 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 eltlast/unop.hh +/// \brief ELTL unary operators +#ifndef SPOT_ELTLAST_UNOP_HH +# define SPOT_ELTLAST_UNOP_HH + +# include "formula.hh" +# include "internal/unop.hh" + +namespace spot +{ + namespace eltl + { + + /// \brief Unary operators. + /// \ingroup eltl_ast + typedef spot::internal::unop unop; + + } +} + +#endif // SPOT_ELTLAST_UNOP_HH diff --git a/src/eltlast/visitor.hh b/src/eltlast/visitor.hh new file mode 100644 index 000000000..9426f8699 --- /dev/null +++ b/src/eltlast/visitor.hh @@ -0,0 +1,82 @@ +// Copyright (C) 2008 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 eltlast/visitor.hh +/// \brief ELTL visitor interface +#ifndef SPOT_ELTLAST_VISITOR_HH +# define SPOT_ELTLAST_VISITOR_HH + +# include "binop.hh" +# include "unop.hh" +# include "multop.hh" +# include "atomic_prop.hh" +# include "constant.hh" + +namespace spot +{ + namespace eltl + { + // Forward declaration. + struct automatop; + + /// \brief Formula visitor that can modify the formula. + /// \ingroup eltl_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::eltl: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; + virtual void visit(automatop* 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::eltl: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; + virtual void visit(const automatop* node) = 0; + }; + + } +} + +#endif // SPOT_ELTLAST_VISITOR_HH diff --git a/src/eltlenv/Makefile.am b/src/eltlenv/Makefile.am new file mode 100644 index 000000000..aac06bcdb --- /dev/null +++ b/src/eltlenv/Makefile.am @@ -0,0 +1,27 @@ +## 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. + +eltlenvdir = $(pkgincludedir)/eltlenv + +eltlenv_HEADERS = \ + defaultenv.hh \ + declenv.hh \ + environment.hh diff --git a/src/eltlenv/declenv.hh b/src/eltlenv/declenv.hh new file mode 100644 index 000000000..ddb8ba633 --- /dev/null +++ b/src/eltlenv/declenv.hh @@ -0,0 +1,44 @@ +// Copyright (C) 2008 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. + +#ifndef SPOT_ELTLENV_DECLENV_HH +# define SPOT_ELTLENV_DECLENV_HH + +# include "environment.hh" +# include "internal/declenv.hh" + +namespace spot +{ + namespace eltl + { + + /// \brief A declarative environment. + /// \ingroup eltl_environment + /// + /// This environment recognizes all atomic propositions + /// that have been previously declared. It will reject other. + typedef spot::internal::declarative_environment + declarative_environment; + + } +} + +#endif // SPOT_ELTLENV_DECLENV_HH diff --git a/src/eltlenv/defaultenv.hh b/src/eltlenv/defaultenv.hh new file mode 100644 index 000000000..b251c27b5 --- /dev/null +++ b/src/eltlenv/defaultenv.hh @@ -0,0 +1,45 @@ +// Copyright (C) 2008 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. + +#ifndef SPOT_ELTLENV_DEFAULTENV_HH +# define SPOT_ELTLENV_DEFAULTENV_HH + +# include "environment.hh" +# include "internal/defaultenv.hh" + +namespace spot +{ + namespace eltl + { + + /// \brief A laxist environment. + /// \ingroup eltl_environment + /// + /// This environment recognizes all atomic propositions. + /// + /// This is a singleton. Use default_environment::instance() + /// to obtain the instance. + typedef spot::internal::default_environment default_environment; + + } +} + +#endif // SPOT_ELTLENV_DEFAULTENV_HH diff --git a/src/eltlenv/environment.hh b/src/eltlenv/environment.hh new file mode 100644 index 000000000..320af7d0a --- /dev/null +++ b/src/eltlenv/environment.hh @@ -0,0 +1,39 @@ +// Copyright (C) 2008 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. + +#ifndef SPOT_ELTLENV_ENVIRONMENT_HH +# define SPOT_ELTLENV_ENVIRONMENT_HH + +# include "eltlast/formula.hh" +# include "internal/environment.hh" + +namespace spot +{ + namespace eltl + { + /// \brief An environment that describes atomic propositions. + /// \ingroup eltl_essential + typedef spot::internal::environment environment; + + } +} + +#endif // SPOT_ELTLENV_ENVIRONMENT_HH diff --git a/src/eltlparse/Makefile.am b/src/eltlparse/Makefile.am new file mode 100644 index 000000000..026172405 --- /dev/null +++ b/src/eltlparse/Makefile.am @@ -0,0 +1,62 @@ +## Copyright (C) 2008 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. + +AM_CPPFLAGS = -I$(srcdir)/.. +AM_CXXFLAGS = #$(WARNING_CXXFLAGS) + +eltlparsedir = $(pkgincludedir)/eltlparse + +noinst_LTLIBRARIES = libeltlparse.la + +ELTLPARSE_YY = eltlparse.yy +FROM_ELTLPARSE_YY_MAIN = eltlparse.cc +FROM_ELTLPARSE_YY_OTHERS = \ + stack.hh \ + position.hh \ + location.hh \ + eltlparse.hh +FROM_ELTLPARSE_YY = $(FROM_ELTLPARSE_YY_MAIN) $(FROM_ELTLPARSE_YY_OTHERS) + +BUILT_SOURCES = $(FROM_ELTLPARSE_YY) +MAINTAINERCLEANFILES = $(FROM_ELTLPARSE_YY) + +$(FROM_ELTLPARSE_YY_MAIN): $(srcdir)/$(ELTLPARSE_YY) +## We must cd into $(srcdir) first because if we tell bison to read +## $(srcdir)/$(ELTLPARSE_YY), it will also use the value of $(srcdir)/ +## in the generated include statements. + cd $(srcdir) && \ + bison --defines --locations --skeleton=lalr1.cc --report=all \ + $(ELTLPARSE_YY) -o $(FROM_ELTLPARSE_YY_MAIN) +$(FROM_ELTLPARSE_YY_OTHERS): $(ELTLPARSE_YY) + @test -f $@ || $(MAKE) $(AM_MAKEFLAGS) $(FROM_ELTLPARSE_YY_MAIN) + +EXTRA_DIST = $(ELTLPARSE_YY) + +libeltlparse_la_SOURCES = \ + fmterror.cc \ + $(FROM_ELTLPARSE_YY) \ + eltlscan.ll \ + parsedecl.hh + +eltlparse_HEADERS = \ + public.hh \ + location.hh \ + position.hh diff --git a/src/eltlparse/eltlparse.yy b/src/eltlparse/eltlparse.yy new file mode 100644 index 000000000..433e599f2 --- /dev/null +++ b/src/eltlparse/eltlparse.yy @@ -0,0 +1,279 @@ +/* Copyright (C) 2008 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 +#include +#include +#include "public.hh" +#include "eltlast/allnodes.hh" + +// Implementation detail for error handling. +namespace spot +{ + namespace eltl + { + struct parse_error_list_t + { + parse_error_list list_; + std::string file_; + }; + } +} + +#define PARSE_ERROR(Loc, Msg) \ + pe.list_.push_back \ + (parse_error(Loc, spair(pe.file_, Msg))) + +%} + +%name-prefix="eltlyy" +%parse-param {spot::eltl::nfamap& nmap} +%parse-param {spot::eltl::parse_error_list_t &pe} +%parse-param {spot::eltl::environment &parse_environment} +%parse-param {spot::eltl::formula* &result} +%lex-param {spot::eltl::parse_error_list_t &pe} +%expect 0 +%debug +%error-verbose +%pure-parser +%union +{ + int ival; + std::string* sval; + spot::eltl::nfa* nval; + spot::eltl::formula* fval; +} + +%{ +/* ltlparse.hh and parsedecl.hh include each other recursively. + We mut ensure that YYSTYPE is declared (by the above %union) + before parsedecl.hh uses it. */ +#include "parsedecl.hh" +using namespace spot::eltl; + +%} + +/* All tokens. */ + +%token ARG "argument" + ATOMIC_PROP "atomic proposition" + IDENT "identifier" + OP_NOT "not operator" + STATE "state" + +%token OP_OR "or operator" + OP_XOR "xor operator" + OP_AND "and operator" + OP_IMPLIES "implication operator" + OP_EQUIV "equivalent operator" + +%token EQ "=" + LPAREN "(" + RPAREN ")" + COMMA "," + END_OF_FILE "end of file" + CONST_TRUE "constant true" + CONST_FALSE "constant false" + +/* Priorities. */ + +/* Logical operators. */ +%left OP_OR +%left OP_XOR +%left OP_AND +%left OP_IMPLIES OP_EQUIV + +%nonassoc OP_NOT + +%type nfa_def; +%type subformula; +%type arg_list; + +%destructor { delete $$; } "atomic proposition" + +%printer { debug_stream() << *$$; } "atomic proposition" + +%% + +result: nfa_list subformula + { + result = $2; + YYACCEPT; + } +; + +/* NFA definitions. */ + +nfa_list: /* empty. */ + | nfa_list nfa +; + +nfa: IDENT "=" "(" nfa_def ")" + { + nmap[*$1] = nfa::ptr($4); + } +; + +nfa_def: /* empty. */ + { + $$ = new nfa(); + } + | nfa_def STATE STATE ARG + { + errno = 0; + long i = strtol($4->c_str(), 0, 10); + if (i > INT_MAX || i < INT_MIN || errno == ERANGE) + { + std::string s = "out of range integer `"; + s += *$4; + s += "'"; + PARSE_ERROR(@1, s); + delete $2; + delete $3; + delete $4; + YYERROR; + } + $1->add_transition(*$2, *$3, i); + $$ = $1; + } + | nfa_def EQ STATE + { + $1->set_final(*$3); + } +; + +/* Formulae. */ + +subformula: ATOMIC_PROP + { + $$ = parse_environment.require(*$1); + if (!$$) + { + std::string s = "unknown atomic proposition `"; + s += *$1; + s += "' in environment `"; + s += parse_environment.name(); + s += "'"; + PARSE_ERROR(@1, s); + delete $1; + YYERROR; + } + else + delete $1; + } + | ATOMIC_PROP "(" arg_list ")" + { + nfamap::iterator i = nmap.find(*$1); + if (i == nmap.end()) + { + std::string s = "unknown automaton operator `"; + s += *$1; + s += "'"; + PARSE_ERROR(@1, s); + delete $1; + YYERROR; + } + + automatop* res = automatop::instance(i->second, $3); + if (res->size() != i->second->arity()) + { + std::ostringstream oss1; + oss1 << res->size(); + std::ostringstream oss2; + oss2 << i->second->arity(); + + std::string s(*$1); + s += " is used with "; + s += oss1.str(); + s += " arguments, but has an arity of "; + s += oss2.str(); + PARSE_ERROR(@1, s); + delete $1; + YYERROR; + } + $$ = res; + } + | CONST_TRUE + { $$ = constant::true_instance(); } + | CONST_FALSE + { $$ = constant::false_instance(); } + | "(" subformula ")" + { $$ = $2; } + | subformula OP_AND subformula + { $$ = multop::instance(multop::And, $1, $3); } + | subformula OP_OR subformula + { $$ = multop::instance(multop::Or, $1, $3); } + | subformula OP_XOR subformula + { $$ = binop::instance(binop::Xor, $1, $3); } + | subformula OP_IMPLIES subformula + { $$ = binop::instance(binop::Implies, $1, $3); } + | subformula OP_EQUIV subformula + { $$ = binop::instance(binop::Equiv, $1, $3); } +; + +arg_list: subformula + { $$ = $1; } + | subformula "," arg_list + { $$ = automatop::instance($1, $3); } +; + +%% + +void +eltlyy::parser::error(const location_type& loc, const std::string& s) +{ + PARSE_ERROR(loc, s); +} + +namespace spot +{ + namespace eltl + { + formula* + parse(const std::string& name, + parse_error_list& error_list, + environment& env, + bool debug) + { + if (eltlyyopen(name)) + { + error_list.push_back + (parse_error(eltlyy::location(), + spair("-", std::string("Cannot open file ") + name))); + return 0; + } + formula* result = 0; + nfamap nmap; + parse_error_list_t pe; + pe.file_ = name; + eltlyy::parser parser(nmap, pe, env, result); + parser.set_debug_level(debug); + parser.parse(); + error_list = pe.list_; + return result; + } + } +} + +// Local Variables: +// mode: c++ +// End: diff --git a/src/eltlparse/eltlscan.ll b/src/eltlparse/eltlscan.ll new file mode 100644 index 000000000..767213c7d --- /dev/null +++ b/src/eltlparse/eltlscan.ll @@ -0,0 +1,183 @@ +/* Copyright (C) 2008 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. +*/ +%option noyywrap +%option prefix="eltlyy" +%option outfile="lex.yy.c" + +%{ +#include +#include +#include "eltlparse/parsedecl.hh" + +#define YY_USER_ACTION \ + yylloc->columns(yyleng); + +// Flex uses `0' for end of file. 0 is not a token_type. +#define yyterminate() return token::END_OF_FILE + +// Stack for handling include files. +typedef std::pair state; +std::stack include; + +#define ERROR(Msg) \ + pe.list_.push_back \ + (spot::eltl::parse_error(*yylloc, spot::eltl::spair(pe.file_, Msg))) + +typedef eltlyy::parser::token token; + +%} + +eol \n|\r|\n\r|\r\n +%s formula +%x incl + +%% + +%{ + yylloc->step(); +%} + + /* Rules for the automaton definitions part. */ + +"=" return token::EQ; +"(" return token::LPAREN; +")" return token::RPAREN; +"%" BEGIN(formula); + +"include" BEGIN(incl); + +[a-zA-Z][a-zA-Z0-9_]* { + yylval->sval = new std::string(yytext, yyleng); + return token::IDENT; + } + +[0-9]+ { + yylval->sval = new std::string(yytext, yyleng); + return token::STATE; + } + +$[0-9]+ { + yylval->sval = new std::string(++yytext, --yyleng); + return token::ARG; + } + +<> { + if (include.empty()) + yyterminate(); + + state s = include.top(); + include.pop(); + pe.file_ = s.second; + yy_delete_buffer(YY_CURRENT_BUFFER); + yy_switch_to_buffer(s.first); + } + + /* Rules for the include part. */ + +[ \t]* +[^ \t\n]+ { + FILE* tmp = fopen(yytext, "r"); + if (!tmp) + ERROR(std::string("cannot open file ") + yytext); + else + { + include.push(make_pair(YY_CURRENT_BUFFER, pe.file_)); + pe.file_ = std::string(yytext); + yy_switch_to_buffer(yy_create_buffer(tmp, YY_BUF_SIZE)); + } + BEGIN(INITIAL); + } + + /* Rules for the formula part. */ + +"(" return token::LPAREN; +")" return token::RPAREN; +"!" return token::OP_NOT; +"," return token::COMMA; + + +"1"|[tT][rR][uU][eE] { + return token::CONST_TRUE; + } +"0"|[fF][aA][lL][sS][eE] { + return token::CONST_FALSE; + } + + /* & and | come from Spin. && and || from LTL2BA. + /\, \/, and xor are from LBTT. + */ +"||"|"|"|"+"|"\\/" { + return token::OP_OR; + } +"&&"|"&"|"."|"*"|"/\\" { + return token::OP_AND; + } +"^"|"xor" return token::OP_XOR; +"=>"|"->" return token::OP_IMPLIES; +"<=>"|"<->" return token::OP_EQUIV; + +[a-zA-Z][a-zA-Z0-9_]* { + yylval->sval = new std::string(yytext, yyleng); + return token::ATOMIC_PROP; + } + + /* Global rules. */ + + /* discard whitespace */ +{eol} yylloc->lines(yyleng); yylloc->step(); +[ \t]+ yylloc->step(); + +. return *yytext; + + +%{ + /* Dummy use of yyunput to shut up a gcc warning. */ + (void) &yyunput; +%} + +%% + +namespace spot +{ + namespace eltl + { + int + eltlyyopen(const std::string &name) + { + if (name == "-") + yyin = stdin; + else + { + yyin = fopen(name.c_str(), "r"); + if (!yyin) + return 1; + } + return 0; + } + + void + eltlyyclose() + { + fclose(yyin); + } + } +} diff --git a/src/eltlparse/fmterror.cc b/src/eltlparse/fmterror.cc new file mode 100644 index 000000000..b2e086f65 --- /dev/null +++ b/src/eltlparse/fmterror.cc @@ -0,0 +1,48 @@ +// Copyright (C) 2008 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 +#include "public.hh" + +namespace spot +{ + namespace eltl + { + bool + format_parse_errors(std::ostream& os, + parse_error_list& error_list) + { + bool printed = false; + spot::eltl::parse_error_list::iterator it; + for (it = error_list.begin(); it != error_list.end(); ++it) + { + if (it->second.first != "-") + { + os << it->second.first << ": "; + os << it->first << ": "; + } + os << it->second.second << std::endl; + printed = true; + } + return printed; + } + } +} diff --git a/src/eltlparse/parsedecl.hh b/src/eltlparse/parsedecl.hh new file mode 100644 index 000000000..9d9847edc --- /dev/null +++ b/src/eltlparse/parsedecl.hh @@ -0,0 +1,43 @@ +// Copyright (C) 2008 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. + +#ifndef SPOT_ELTLPARSE_PARSEDECL_HH +# define SPOT_ELTLPARSE_PARSEDECL_HH + +#include "eltlparse.hh" +#include "location.hh" + +# define YY_DECL \ + int eltlyylex (eltlyy::parser::semantic_type *yylval, \ + eltlyy::location *yylloc, \ + spot::eltl::parse_error_list_t &pe) +YY_DECL; + +namespace spot +{ + namespace eltl + { + int eltlyyopen(const std::string& name); + void eltlyyclose(); + } +} + +#endif // SPOT_ELTLPARSE_PARSEDECL_HH diff --git a/src/eltlparse/public.hh b/src/eltlparse/public.hh new file mode 100644 index 000000000..6813ce66c --- /dev/null +++ b/src/eltlparse/public.hh @@ -0,0 +1,84 @@ +// Copyright (C) 2003, 2004, 2005, 2006, 2008 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. + +#ifndef SPOT_ELTLPARSE_PUBLIC_HH +# define SPOT_ELTLPARSE_PUBLIC_HH + +# include "eltlast/formula.hh" +# include "eltlast/visitor.hh" +// Unfortunately Bison 2.3 uses the same guards in all parsers :( +# undef BISON_LOCATION_HH +# undef BISON_POSITION_HH +# include "eltlparse/location.hh" +# include "eltlenv/defaultenv.hh" +# include "eltlast/nfa.hh" +# include +# include +# include +# include +# include + +namespace spot +{ + namespace eltl + { + /// \addtogroup eltl_io + /// @{ + + typedef std::pair spair; + /// \brief A parse diagnostic >. + typedef std::pair parse_error; + /// \brief A list of parser diagnostics, as filled by parse. + typedef std::list parse_error_list; + + /// + typedef std::map nfamap; + + /// \brief Build a formula from a text file. + /// \param name The name of the file to parse. + /// \param error_list A list that will be filled with + /// parse errors that occured during parsing. + /// \param env The environment into which parsing should take place. + /// \param debug When true, causes the parser to trace its execution. + /// \return A pointer to the tgba built from \a filename, or + /// 0 if the file could not be opened. + /// + /// \warning This function is not reentrant. + formula* parse(const std::string& name, + parse_error_list& error_list, + environment& env = default_environment::instance(), + bool debug = false); + + /// \brief Format diagnostics produced by spot::eltl::parse. + /// \param os Where diagnostics should be output. + /// \param eltl_string The string that were parsed. + /// \param error_list The error list filled by spot::eltl::parse while + /// parsing \a eltl_string. + /// \return \c true iff any diagnostic was output. + bool + format_parse_errors(std::ostream& os, + parse_error_list& error_list); + + /// @} + } +} + +#endif // SPOT_ELTLPARSE_PUBLIC_HH diff --git a/src/eltltest/Makefile.am b/src/eltltest/Makefile.am new file mode 100644 index 000000000..7f8a53ed6 --- /dev/null +++ b/src/eltltest/Makefile.am @@ -0,0 +1,44 @@ +## Copyright (C) 2003, 2004, 2005, 2006 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. + +AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) +LDADD = ../libspot.la + +check_SCRIPTS = defs +# Keep this sorted alphabetically. +check_PROGRAMS = \ + acc \ + nfa + +acc_SOURCES = acc.cc +nfa_SOURCES = nfa.cc + +EXTRA_DIST = $(TESTS) + +# Ordered by strength of the test. Test basic features first. +TESTS = \ + acc.test \ + nfa.test + +CLEANFILES = \ + input \ + prelude diff --git a/src/eltltest/acc.cc b/src/eltltest/acc.cc new file mode 100644 index 000000000..289ff41d5 --- /dev/null +++ b/src/eltltest/acc.cc @@ -0,0 +1,42 @@ +// Copyright (C) 2008 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 +#include +#include "eltlparse/public.hh" + +int +main(int argc, char** argv) +{ + spot::eltl::parse_error_list p; + const spot::eltl::formula* f = spot::eltl::parse( + argv[1], p, spot::eltl::default_environment::instance(), argc > 2); + + if (spot::eltl::format_parse_errors(std::cerr, p)) + { + if (f != 0) + std::cout << f->dump() << std::endl; + return 1; + } + + assert(f != 0); + std::cout << f->dump() << std::endl; +} diff --git a/src/eltltest/acc.test b/src/eltltest/acc.test new file mode 100755 index 000000000..fc9e5aaaf --- /dev/null +++ b/src/eltltest/acc.test @@ -0,0 +1,31 @@ +#!/bin/sh + +. ./defs || exit 1 + +set -e +cat >prelude <input <input <&2 + exit 1 +} + +# If srcdir is not set, then we are not running from `make check', be verbose. +if test -z "$srcdir"; then + test -z "$VERBOSE" && VERBOSE=x + # compute $srcdir. + srcdir=`echo "$0" | sed -e 's,/[^\\/]*$,,'` + test $srcdir = $0 && srcdir=. +fi + +# Ensure $srcdir is set correctly. +test -f $srcdir/defs.in || { + echo "$srcdir/defs.in not found, check \$srcdir" 1>&2 + exit 1 +} + +# User can set VERBOSE to see all output. +test -z "$VERBOSE" && exec >/dev/null 2>&1 + +echo "== Running test $0" + +DOT='@DOT@' +VALGRIND='@VALGRIND@' + +run() +{ + expected_exitcode=$1 + shift + exitcode=0 + if test -n "$VALGRIND"; then + exec 6>valgrind.err + GLIBCPP_FORCE_NEW=1 \ + $VALGRIND --tool=memcheck --leak-check=yes --log-fd=6 -q "$@" || + exitcode=$? + cat valgrind.err 1>&2 + test -z "`sed 1q valgrind.err`" || exit 50 + rm -f valgrind.err + else + "$@" || exitcode=$? + fi + test $exitcode = $expected_exitcode || exit 1 +} + +# Turn on shell traces when VERBOSE=x. +if test "x$VERBOSE" = xx; then + set -x +else + : +fi diff --git a/src/eltltest/nfa.cc b/src/eltltest/nfa.cc new file mode 100644 index 000000000..59b181db4 --- /dev/null +++ b/src/eltltest/nfa.cc @@ -0,0 +1,57 @@ +// Copyright (C) 2008 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 +#include +#include +#include "eltlast/nfa.hh" + +using namespace spot::eltl; + +typedef std::set mset; + +void +dfs(nfa& a, const nfa::state* s, mset& m) +{ + if (m.find(s) != m.end()) + return; + m.insert(s); + + for (nfa::iterator i = a.begin(s); i != a.end(s); ++i) + { + std::cout << a.format_state((*i)->dest) << std::endl; + dfs(a, (*i)->dest, m); + } +} + +int +main() +{ + nfa a; + + a.add_transition("0", "1", 1); + a.add_transition("1", "2", 2); + + std::cout << "init: " << a.format_state(a.get_init_state()) << std::endl; + + mset m; + dfs(a, a.get_init_state(), m); +} diff --git a/src/eltltest/nfa.test b/src/eltltest/nfa.test new file mode 100755 index 000000000..241c7f207 --- /dev/null +++ b/src/eltltest/nfa.test @@ -0,0 +1,6 @@ +#!/bin/sh + +. ./defs || exit 1 + +set -e +run 0 ./nfa || exit 1 diff --git a/src/internal/Makefile.am b/src/internal/Makefile.am new file mode 100644 index 000000000..2b43a9062 --- /dev/null +++ b/src/internal/Makefile.am @@ -0,0 +1,44 @@ +## Copyright (C) 2003 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. + +internaldir = $(pkgincludedir)/libinternal + +internal_HEADERS = \ + refformula.hh \ + refformula.hxx \ + formula.hh \ + formula.hxx \ + atomic_prop.hh \ + atomic_prop.hxx \ + binop.hh \ + binop.hxx \ + constant.hh \ + constant.hxx \ + multop.hh \ + multop.hxx \ + predecl.hh \ + unop.hh \ + unop.hxx \ + defaultenv.hh \ + defaultenv.hxx \ + declenv.hh \ + declenv.hxx \ + environment.hh diff --git a/src/internal/atomic_prop.hh b/src/internal/atomic_prop.hh new file mode 100644 index 000000000..f4310f544 --- /dev/null +++ b/src/internal/atomic_prop.hh @@ -0,0 +1,85 @@ +// Copyright (C) 2003, 2004, 2008 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 internal/atomic_prop.hh +/// \brief Generic atomic propositions +#ifndef SPOT_INTERNAL_ATOMIC_PROP_HH +# define SPOT_INTERNAL_ATOMIC_PROP_HH + +#include +#include +#include +#include +#include +#include "refformula.hh" +#include "environment.hh" + +namespace spot +{ + namespace internal + { + + /// \brief Atomic propositions. + /// \ingroup generic_ast + template + 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); + + typedef typename T::visitor visitor; + typedef typename T::const_visitor const_visitor; + + 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*> pair; + typedef std::map*> map; + static map instances; + + private: + std::string name_; + environment* env_; + }; + + } +} + +# include "atomic_prop.hxx" + +#endif // SPOT_INTERNAL_ATOMICPROP_HH diff --git a/src/internal/atomic_prop.hxx b/src/internal/atomic_prop.hxx new file mode 100644 index 000000000..62cbd5aec --- /dev/null +++ b/src/internal/atomic_prop.hxx @@ -0,0 +1,123 @@ +// Copyright (C) 2003, 2004, 2005, 2008 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 internal/atomic_prop.hxx +/// \brief Generic atomic propositions implementation +#ifndef SPOT_INTERNAL_ATOMIC_PROP_HXX +# define SPOT_INTERNAL_ATOMIC_PROP_HXX + +#include "atomic_prop.hh" + +namespace spot +{ + namespace internal + { + + template + atomic_prop::atomic_prop(const std::string& name, environment& env) + : name_(name), env_(&env) + { + this->dump_ = "AP(" + name + ")"; + this->set_key_(); + } + + template + atomic_prop::~atomic_prop() + { + // Get this instance out of the instance map. + pair p(name(), &env()); + typename map::iterator i = instances.find(p); + assert (i != instances.end()); + instances.erase(i); + } + + template + void + atomic_prop::accept(visitor& v) + { + v.visit(this); + } + + template + void + atomic_prop::accept(const_visitor& v) const + { + v.visit(this); + } + + template + const std::string& + atomic_prop::name() const + { + return name_; + } + + template + environment& + atomic_prop::env() const + { + return *env_; + } + + template + typename atomic_prop::map atomic_prop::instances; + + template + atomic_prop* + atomic_prop::instance(const std::string& name, environment& env) + { + pair p(name, &env); + typename map::iterator i = instances.find(p); + if (i != instances.end()) + { + return static_cast*>(i->second->ref()); + } + atomic_prop* ap = new atomic_prop(name, env); + instances[p] = ap; + return static_cast*>(ap->ref()); + } + + template + unsigned + atomic_prop::instance_count() + { + return instances.size(); + } + + template + std::ostream& + atomic_prop::dump_instances(std::ostream& os) + { + + for (typename 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; + } + + } +} + +#endif // SPOT_INTERNAL_ATOMICPROP_HXX diff --git a/src/internal/binop.hh b/src/internal/binop.hh new file mode 100644 index 000000000..c13648c76 --- /dev/null +++ b/src/internal/binop.hh @@ -0,0 +1,99 @@ +// 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 internal/binop.hh +/// \brief Generic binary operators +/// +/// This does not include \c AND and \c OR operators. These are +/// considered to be multi-operand operators (see spot::internal::multop). +#ifndef SPOT_INTERNAL_BINOP_HH +# define SPOT_INTERNAL_BINOP_HH + +#include +#include "refformula.hh" +#include +#include + +namespace spot +{ + namespace internal + { + + /// \brief Generic binary operator. + /// \ingroup generic_ast + template + 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. + typedef typename T::binop type; + + /// Build an unary operator with operation \a op and + /// children \a first and \a second. + static binop* instance(type op, formula* first, formula* second); + + typedef typename T::visitor visitor; + typedef typename T::const_visitor const_visitor; + + 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*> pairf; + typedef std::pair pair; + typedef std::map*> map; + static map instances; + + binop(type op, formula* first, formula* second); + virtual ~binop(); + + private: + type op_; + formula* first_; + formula* second_; + }; + + } +} + +# include "binop.hxx" + +#endif // SPOT_INTERNAL_BINOP_HH diff --git a/src/internal/binop.hxx b/src/internal/binop.hxx new file mode 100644 index 000000000..1080218af --- /dev/null +++ b/src/internal/binop.hxx @@ -0,0 +1,156 @@ +// 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. + +/// \file internal/binop.hxx +/// \brief Generic binary operators implementation +#ifndef SPOT_INTERNAL_BINOP_HXX +# define SPOT_INTERNAL_BINOP_HXX + +#include "binop.hh" + +namespace spot +{ + namespace internal + { + template + binop::binop(type op, formula* first, formula* second) + : op_(op), first_(first), second_(second) + { + this->dump_ = "binop("; + this->dump_ += op_name(); + this->dump_ += ", " + first->dump() + ", " + second->dump() + ")"; + this->set_key_(); + } + + template + binop::~binop() + { + // Get this instance out of the instance map. + pairf pf(first(), second()); + pair p(op(), pf); + typename map::iterator i = instances.find(p); + assert (i != instances.end()); + instances.erase(i); + } + + template + void + binop::accept(visitor& v) + { + v.visit(this); + } + + template + void + binop::accept(const_visitor& v) const + { + v.visit(this); + } + + template + const formula* + binop::first() const + { + return first_; + } + + template + formula* + binop::first() + { + return first_; + } + + template + const formula* + binop::second() const + { + return second_; + } + + template + formula* + binop::second() + { + return second_; + } + + template + typename binop::type + binop::op() const + { + return op_; + } + + template + const char* + binop::op_name() const + { + return T::binop_name(op_); + } + + template + typename binop::map binop::instances; + + template + 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 T::Xor: + case T::Equiv: + if (second < first) + std::swap(first, second); + break; + case T::Implies: + // case U: + // case R: + // // Non associative operators. + default: + break; + } + + pairf pf(first, second); + pair p(op, pf); + typename map::iterator i = instances.find(p); + if (i != instances.end()) + { + return static_cast*>(i->second->ref()); + } + binop* ap = new binop(op, first, second); + instances[p] = ap; + return static_cast*>(ap->ref()); + } + + template + unsigned + binop::instance_count() + { + return instances.size(); + } + } +} + +#endif // SPOT_INTERNAL_BINOP_HXX diff --git a/src/internal/constant.hh b/src/internal/constant.hh new file mode 100644 index 000000000..e02458037 --- /dev/null +++ b/src/internal/constant.hh @@ -0,0 +1,72 @@ +// 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 internal/constant.hh +/// \brief Generic constants +#ifndef SPOT_INTERNAL_CONSTANT_HH +# define SPOT_INTERNAL_CONSTANT_HH + +#include +#include "formula.hh" + +namespace spot +{ + namespace internal + { + + /// \brief A constant (True or False) + /// \ingroup generic_ast + template + class constant : public formula + { + public: + enum type { False, True }; + + typedef typename T::visitor visitor; + typedef typename T::const_visitor const_visitor; + + 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::internal::constant::constant(1). + static constant* true_instance(); + /// Get the sole instance of spot::internal::constant::constant(0). + static constant* false_instance(); + + protected: + constant(type val); + virtual ~constant(); + + private: + type val_; + }; + + } +} + +# include "constant.hxx" + +#endif // SPOT_INTERNAL_CONSTANT_HH diff --git a/src/internal/constant.hxx b/src/internal/constant.hxx new file mode 100644 index 000000000..dec0fd430 --- /dev/null +++ b/src/internal/constant.hxx @@ -0,0 +1,112 @@ +// Copyright (C) 2003, 2005, 2008 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 internal/constant.hxx +/// \brief Generic constants implementation +#ifndef SPOT_INTERNAL_CONSTANT_HXX +# define SPOT_INTERNAL_CONSTANT_HXX + +#include "constant.hh" + +namespace spot +{ + namespace internal + { + template + constant::constant(type val) + : val_(val) + { + switch (val) + { + case True: + this->dump_ = "constant(1)"; + this->set_key_(); + return; + case False: + this->dump_ = "constant(0)"; + this->set_key_(); + return; + } + // Unreachable code. + assert(0); + } + + template + constant::~constant() + { + } + + template + void + constant::accept(visitor& v) + { + v.visit(this); + } + + template + void + constant::accept(const_visitor& v) const + { + v.visit(this); + } + + template + typename constant::type + constant::val() const + { + return val_; + } + + template + const char* + constant::val_name() const + { + switch (val_) + { + case True: + return "1"; + case False: + return "0"; + } + // Unreachable code. + assert(0); + return 0; + } + + template + constant* + constant::false_instance() + { + static constant f(constant::False); + return &f; + } + + template + constant* + constant::true_instance() + { + static constant t(constant::True); + return &t; + } + } +} + +#endif // SPOT_INTERNAL_CONSTANT_HXX diff --git a/src/internal/declenv.hh b/src/internal/declenv.hh new file mode 100644 index 000000000..c1c3adc12 --- /dev/null +++ b/src/internal/declenv.hh @@ -0,0 +1,69 @@ +// Copyright (C) 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. + +#ifndef SPOT_INTERNAL_DECLENV_HH +# define SPOT_INTERNAL_DECLENV_HH + +#include +#include +#include "atomic_prop.hh" +#include "environment.hh" + +namespace spot +{ + namespace internal + { + + /// \brief A declarative environment. + /// \ingroup generic_environment + /// + /// This environment recognizes all atomic propositions + /// that have been previously declared. It will reject other. + template + class declarative_environment : public environment + { + public: + declarative_environment(); + ~declarative_environment(); + + /// Declare an atomic proposition. Return false iff the + /// proposition was already declared. + bool declare(const std::string& prop_str); + + virtual formula* require(const std::string& prop_str); + + /// Get the name of the environment. + virtual const std::string& name(); + + typedef std::map*> prop_map; + + /// Get the map of atomic proposition known to this environment. + const prop_map& get_prop_map() const; + + private: + prop_map props_; + }; + } +} + +#include "declenv.hxx" + +#endif // SPOT_INTERNAL_DECLENV_HH diff --git a/src/internal/declenv.hxx b/src/internal/declenv.hxx new file mode 100644 index 000000000..5c96f90c3 --- /dev/null +++ b/src/internal/declenv.hxx @@ -0,0 +1,83 @@ +// Copyright (C) 2004, 2008 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. + +#ifndef SPOT_INTERNAL_DECLENV_HXX +# define SPOT_INTERNAL_DECLENV_HXX + +#include "declenv.hh" + +namespace spot +{ + namespace internal + { + + template + declarative_environment::declarative_environment() + { + } + + template + declarative_environment::~declarative_environment() + { + // FIXME !! + // for (prop_map::iterator i = props_.begin(); i != props_.end(); ++i) + // ltl::destroy(i->second); + } + + template + bool + declarative_environment::declare(const std::string& prop_str) + { + if (props_.find(prop_str) != props_.end()) + return false; + props_[prop_str] = internal::atomic_prop::instance(prop_str, *this); + return true; + } + + template + formula* + declarative_environment::require(const std::string& prop_str) + { + typename prop_map::iterator i = props_.find(prop_str); + if (i == props_.end()) + return 0; + // It's an atomic_prop, so we do not have to use the clone() visitor. + return i->second->ref(); + } + + template + const std::string& + declarative_environment::name() + { + static std::string name("declarative environment"); + return name; + } + + template + const typename declarative_environment::prop_map& + declarative_environment::get_prop_map() const + { + return props_; + } + } +} + +#endif // SPOT_INTERNAL_DECLENV_HXX diff --git a/src/internal/defaultenv.hh b/src/internal/defaultenv.hh new file mode 100644 index 000000000..f7382fbf8 --- /dev/null +++ b/src/internal/defaultenv.hh @@ -0,0 +1,59 @@ +// 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. + +#ifndef SPOT_INTERNAL_DEFAULTENV_HH +# define SPOT_INTERNAL_DEFAULTENV_HH + +#include "atomic_prop.hh" +#include "environment.hh" + +namespace spot +{ + namespace internal + { + + /// \brief A laxist environment. + /// \ingroup generic_environment + /// + /// This environment recognizes all atomic propositions. + /// + /// This is a singleton. Use default_environment::instance() + /// to obtain the instance. + template + class default_environment : public environment + { + public: + virtual ~default_environment(); + virtual formula* require(const std::string& prop_str); + virtual const std::string& name(); + + /// Get the sole instance of spot::internal::default_environment. + static default_environment& instance(); + protected: + default_environment(); + }; + + } +} + +#include "defaultenv.hxx" + +#endif // SPOT_INTERNAL_DEFAULTENV_HH diff --git a/src/internal/defaultenv.hxx b/src/internal/defaultenv.hxx new file mode 100644 index 000000000..06c8c436e --- /dev/null +++ b/src/internal/defaultenv.hxx @@ -0,0 +1,68 @@ +// Copyright (C) 2003 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. + +#ifndef SPOT_INTERNAL_DEFAULTENV_HXX +# define SPOT_INTERNAL_DEFAULTENV_HXX + +#include "defaultenv.hh" + +namespace spot +{ + namespace internal + { + + template + default_environment::~default_environment() + { + } + + template + formula* + default_environment::require(const std::string& s) + { + return atomic_prop::instance(s, *this); + } + + template + const std::string& + default_environment::name() + { + static std::string name("default environment"); + return name; + } + + template + default_environment::default_environment() + { + } + + template + default_environment& + default_environment::instance() + { + static default_environment* singleton = new default_environment(); + return *singleton; + } + + } +} + +#endif // SPOT_INTERNAL_DEFAULTENV_HXX diff --git a/src/internal/environment.hh b/src/internal/environment.hh new file mode 100644 index 000000000..df1af8492 --- /dev/null +++ b/src/internal/environment.hh @@ -0,0 +1,72 @@ +// 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. + +#ifndef SPOT_INTERNAL_ENVIRONMENT_HH +# define SPOT_INTERNAL_ENVIRONMENT_HH + +# include "formula.hh" +# include + +namespace spot +{ + namespace internal + { + /// \brief An environment that describes atomic propositions. + /// \ingroup generic_essential + template + class environment + { + public: + /// \brief Obtain the formula associated to \a prop_str + /// + /// Usually \a prop_str, is the name of an atomic proposition, + /// and spot::internal::require simply returns the associated + /// spot::internal::atomic_prop. + /// + /// Note this is not a \c const method. Some environments will + /// "create" the atomic proposition when requested. + /// + /// We return a spot::internal::formula instead of an + /// spot::internal::atomic_prop, because this + /// will allow nifty tricks (e.g., we could name formulae in an + /// environment, and let the parser build a larger tree from + /// these). + /// + /// \return 0 iff \a prop_str is not part of the environment, + /// or the associated spot::internal::formula otherwise. + virtual formula* require(const std::string& prop_str) = 0; + + /// Get the name of the environment. + virtual const std::string& name() = 0; + + virtual + ~environment() + { + } + + // FIXME: More functions will be needed later, but + // it's enough for now. + }; + + } +} + +#endif // SPOT_INTERNAL_ENVIRONMENT_HH diff --git a/src/internal/formula.hh b/src/internal/formula.hh new file mode 100644 index 000000000..ca9466dfc --- /dev/null +++ b/src/internal/formula.hh @@ -0,0 +1,162 @@ +// 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 internal/formula.hh +/// \brief Generic formula interface +#ifndef SPOT_INTERNAL_FORMULA_HH +# define SPOT_INTERNAL_FORMULA_HH + +# include +# include +# include "predecl.hh" +# include "misc/hash.hh" + +namespace spot +{ + namespace internal + { + /// \brief A Generic formula. + /// \ingroup generic_essential + /// \ingroup generic_ast + /// + /// The only way you can work with a formula is to + /// build a T::visitor or T::const_visitor. + template + class formula : public T + { + public: + typedef typename T::visitor visitor; + typedef typename T::const_visitor const_visitor; + + /// Entry point for T::visitor instances. + virtual void accept(visitor& v) = 0; + /// Entry point for T::const_visitor instances. + virtual void accept(const_visitor& v) const = 0; + + /// \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 a clone visitor 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 a destroy() visitor 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. + const size_t + hash() const + { + return hash_key_; + } + protected: + virtual ~formula(); + + /// \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_(); + + /// \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_; + }; + + /// \brief Strict Weak Ordering for const formula*. + /// \ingroup generic_essentials + /// + /// This is meant to be used as a comparison functor for + /// STL \c map whose key are of type const formula*. + /// + /// For instance here is how one could declare + /// a map of \c const::formula*. + /// \code + /// // Remember how many times each formula has been seen. + /// template + /// std::map*, int, + /// spot::internal::formula_ptr_less_than > seen; + /// \endcode + template + struct formula_ptr_less_than: + public std::binary_function*, const formula*, bool> + { + bool + operator()(const formula* left, const formula* right) const + { + 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(); + } + }; + + /// \brief Hash Function for const formula*. + /// \ingroup generic_essentials + /// \ingroup hash_funcs + /// + /// This is meant to be used as a hash functor for + /// Sgi's \c hash_map whose key are of type const formula*. + /// + /// For instance here is how one could declare + /// a map of \c const::formula*. + /// \code + /// // Remember how many times each formula has been seen. + /// template + /// Sgi::hash_map*, int, + /// const spot::internal::formula_ptr_hash > seen; + /// \endcode + template + struct formula_ptr_hash: + public std::unary_function*, size_t> + { + size_t + operator()(const formula* that) const + { + assert(that); + return that->hash(); + } + }; + + } +} + +# include "formula.hxx" + +#endif // SPOT_INTERNAL_FORMULA_HH diff --git a/src/internal/formula.hxx b/src/internal/formula.hxx new file mode 100644 index 000000000..0634cba5e --- /dev/null +++ b/src/internal/formula.hxx @@ -0,0 +1,86 @@ +// Copyright (C) 2003, 2005, 2008 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 internal/formula.hxx +/// \brief Generic formula implementation +#ifndef SPOT_INTERNAL_FORMULA_HXX +# define SPOT_INTERNAL_FORMULA_HXX + +#include "formula.hh" + +namespace spot +{ + namespace internal + { + template + formula* + formula::ref() + { + ref_(); + return this; + } + + template + formula::~formula() + { + } + + template + void + formula::unref(formula* f) + { + if (f->unref_()) + delete f; + } + + template + void + formula::ref_() + { + // Not reference counted by default. + } + + template + bool + formula::unref_() + { + // Not reference counted by default. + return false; + } + + template + const std::string& + formula::dump() const + { + return dump_; + } + + template + void + formula::set_key_() + { + string_hash sh; + hash_key_ = sh(dump_); + } + } +} + +#endif // SPOT_INTERNAL_FORMULA_HXX diff --git a/src/internal/multop.hh b/src/internal/multop.hh new file mode 100644 index 000000000..aa8a62961 --- /dev/null +++ b/src/internal/multop.hh @@ -0,0 +1,138 @@ +// 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 internal/multop.hh +/// \brief Generic multi-operand operators +#ifndef SPOT_INTERNAL_MULTOP_HH +# define SPOT_INTERNAL_MULTOP_HH + +#include +#include +#include +#include +#include +#include "refformula.hh" +#include "constant.hh" + +namespace spot +{ + namespace internal + { + + /// \brief Multi-operand operators. + /// \ingroup generic_ast + /// + /// These operators are considered commutative and associative. + template + class multop : public ref_formula + { + public: + enum type { Or, And }; + + /// List of formulae. + typedef std::vector*> vec; + + /// \brief Build a spot::internal::multop with two children. + /// + /// If one of the children itself is a spot::internal::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 internal::multop. + /// + /// This functions can perform slight optimizations and may not + /// return an internal::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::internal::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::internal::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::internal::multop. + /// + /// This functions can perform slight optimizations and may not + /// return an internal::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); + + typedef typename T::visitor visitor; + typedef typename T::const_visitor const_visitor; + + 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 pair; + /// Comparison functor used internally by internal::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*, paircmp> map; + static map instances; + + multop(type op, vec* v); + virtual ~multop(); + + private: + type op_; + vec* children_; + + static void destroy(formula* c); + }; + + } +} + +# include "multop.hxx" + +#endif // SPOT_INTERNAL_MULTOP_HH diff --git a/src/internal/multop.hxx b/src/internal/multop.hxx new file mode 100644 index 000000000..72dac2bca --- /dev/null +++ b/src/internal/multop.hxx @@ -0,0 +1,252 @@ +// Copyright (C) 2003, 2004, 2005, 2008 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 internal/multop.hxx +/// \brief Generic multi-operand operators implementation +#ifndef SPOT_INTERNAL_MULTOP_HXX +# define SPOT_INTERNAL_MULTOP_HXX + +#include "multop.hh" + +namespace spot +{ + namespace internal + { + template + multop::multop(type op, vec* v) + : op_(op), children_(v) + { + this->dump_ = "multop("; + this->dump_ += op_name(); + unsigned max = v->size(); + for (unsigned n = 0; n < max; ++n) + { + this->dump_ += ", " + (*v)[n]->dump(); + } + this->dump_ += ")"; + this->set_key_(); + } + + template + multop::~multop() + { + // Get this instance out of the instance map. + pair p(op(), children_); + typename map::iterator i = instances.find(p); + assert (i != instances.end()); + instances.erase(i); + + delete children_; + } + + template + void + multop::accept(visitor& v) + { + v.visit(this); + } + + template + void + multop::accept(const_visitor& v) const + { + v.visit(this); + } + + template + unsigned + multop::size() const + { + return children_->size(); + } + + template + const formula* + multop::nth(unsigned n) const + { + return (*children_)[n]; + } + + template + formula* + multop::nth(unsigned n) + { + return (*children_)[n]; + } + + template + typename multop::type + multop::op() const + { + return op_; + } + + template + const char* + multop::op_name() const + { + switch (op_) + { + case And: + return "And"; + case Or: + return "Or"; + } + // Unreachable code. + assert(0); + return 0; + } + + template + typename multop::map multop::instances; + + template + formula* + multop::instance(type op, vec* v) + { + pair p(op, v); + + // Inline children of same kind. + { + vec inlined; + typename vec::iterator i = v->begin(); + while (i != v->end()) + { + multop* p = dynamic_cast*>(*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; + typename vec::iterator i = v->begin(); + while (i != v->end()) + { + if (*i == last) + { + destroy(*i); + i = v->erase(i); + } + else + { + last = *i++; + } + } + } + + typename 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; + } + + typename map::iterator i = instances.find(p); + if (i != instances.end()) + { + delete v; + return static_cast*>(i->second->ref()); + } + multop* ap = new multop(op, v); + instances[p] = ap; + return static_cast*>(ap->ref()); + + } + + template + 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); + } + + template + unsigned + multop::instance_count() + { + return instances.size(); + } + + template + void + multop::destroy(formula* c) + { + if (unop* uo = dynamic_cast*>(c)) + { + destroy(uo->child()); + formula::unref(uo); + } + else if (binop* bo = dynamic_cast*>(c)) + { + destroy(bo->first()); + destroy(bo->second()); + formula::unref(bo); + } + else if (multop* mo = dynamic_cast*>(c)) + { + unsigned s = mo->size(); + for (unsigned i = 0; i < s; ++i) + destroy(mo->nth(i)); + formula::unref(mo); + } + else // constant* || atomic_prop* + formula::unref(c); + } + } +} + +#endif // SPOT_INTERNAL_MULTOP_HXX diff --git a/src/internal/predecl.hh b/src/internal/predecl.hh new file mode 100644 index 000000000..80a4817f7 --- /dev/null +++ b/src/internal/predecl.hh @@ -0,0 +1,49 @@ +// 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 internal/predecl.hh +/// \brief Predeclare all node types. +/// +/// This file is usually used when \b declaring methods and functions +/// over nodes. +#ifndef SPOT_INTERNAL_PREDECL_HH +# define SPOT_INTERNAL_PREDECL_HH + +namespace spot +{ + namespace internal + { + template + struct atomic_prop; + template + struct unop; + template + struct constant; + template + struct binop; + template + struct formula; + template + struct multop; + } +} + +#endif // SPOT_INTERNAL_PREDECL_HH diff --git a/src/internal/refformula.hh b/src/internal/refformula.hh new file mode 100644 index 000000000..3673b0b75 --- /dev/null +++ b/src/internal/refformula.hh @@ -0,0 +1,57 @@ +// 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 internal/refformula.hh +/// \brief Reference-counted generic formulae +#ifndef SPOT_INTERNAL_REFFORMULA_HH +# define SPOT_INTERNAL_REFFORMULA_HH + +#include "formula.hh" +#include + +namespace spot +{ + namespace internal + { + + /// \brief A reference-counted generic formula. + /// \ingroup generic_ast + template + 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_; + }; + + } +} + +# include "refformula.hxx" + +#endif // SPOT_INTERNAL_REFFORMULA_HH diff --git a/src/internal/refformula.hxx b/src/internal/refformula.hxx new file mode 100644 index 000000000..72cd269a0 --- /dev/null +++ b/src/internal/refformula.hxx @@ -0,0 +1,69 @@ +// 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 internal/refformula.hxx +/// \brief Reference-counted generic formulae implementation +#ifndef SPOT_INTERNAL_REFFORMULA_HXX +# define SPOT_INTERNAL_REFFORMULA_HXX + +#include "refformula.hh" + +namespace spot +{ + namespace internal + { + template + ref_formula::ref_formula() + : ref_counter_(0) + { + } + + template + ref_formula::~ref_formula() + { + } + + template + void + ref_formula::ref_() + { + ++ref_counter_; + } + + template + bool + ref_formula::unref_() + { + assert(ref_counter_ > 0); + return !--ref_counter_; + } + + template + unsigned + ref_formula::ref_count_() + { + return ref_counter_; + } + + } +} + +#endif // SPOT_INTERNAL_REFFORMULA_HXX diff --git a/src/internal/unop.hh b/src/internal/unop.hh new file mode 100644 index 000000000..46312b15a --- /dev/null +++ b/src/internal/unop.hh @@ -0,0 +1,85 @@ +// 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 internal/unop.hh +/// \brief Generic unary operators +#ifndef SPOT_INTERNAL_UNOP_HH +# define SPOT_INTERNAL_UNOP_HH + +#include +#include "refformula.hh" +#include + +namespace spot +{ + namespace internal + { + + /// \brief Generic unary operators. + /// \ingroup generic_ast + template + class unop : public ref_formula + { + public: + typedef typename T::unop type; + + /// Build an unary operator with operation \a op and + /// child \a child. + static unop* instance(type op, formula* child); + + typedef typename T::visitor visitor; + typedef typename T::const_visitor const_visitor; + + 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*> pair; + typedef std::map*> map; + static map instances; + + unop(type op, formula* child); + virtual ~unop(); + + private: + type op_; + formula* child_; + }; + + } +} + +# include "unop.hxx" + +#endif // SPOT_INTERNAL_UNOP_HH diff --git a/src/internal/unop.hxx b/src/internal/unop.hxx new file mode 100644 index 000000000..26a4178a3 --- /dev/null +++ b/src/internal/unop.hxx @@ -0,0 +1,122 @@ +// 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. + +/// \file internal/unop.hxx +/// \brief Generic unary operators implementation +#ifndef SPOT_INTERNAL_UNOP_HXX +# define SPOT_INTERNAL_UNOP_HXX + +#include "unop.hh" + +namespace spot +{ + namespace internal + { + template + unop::unop(type op, formula* child) + : op_(op), child_(child) + { + this->dump_ = "unop("; + this->dump_ += op_name(); + this->dump_ += ", " + child->dump() + ")"; + this->set_key_(); + } + + template + unop::~unop() + { + // Get this instance out of the instance map. + pair p(op(), child()); + typename map::iterator i = instances.find(p); + assert (i != instances.end()); + instances.erase(i); + } + + template + void + unop::accept(visitor& v) + { + v.visit(this); + } + + template + void + unop::accept(const_visitor& v) const + { + v.visit(this); + } + + template + const formula* + unop::child() const + { + return child_; + } + + template + formula* + unop::child() + { + return child_; + } + + template + typename unop::type + unop::op() const + { + return op_; + } + + template + const char* + unop::op_name() const + { + return T::unop_name(op_); + } + + template + typename unop::map unop::instances; + + template + unop* + unop::instance(type op, formula* child) + { + pair p(op, child); + typename map::iterator i = instances.find(p); + if (i != instances.end()) + { + return static_cast*>(i->second->ref()); + } + unop* ap = new unop(op, child); + instances[p] = ap; + return static_cast*>(ap->ref()); + } + + template + unsigned + unop::instance_count() + { + return instances.size(); + } + } +} + +#endif // SPOT_INTERNAL_UNOP_HXX diff --git a/src/ltlast/Makefile.am b/src/ltlast/Makefile.am index b7d3d6fa1..964d070a8 100644 --- a/src/ltlast/Makefile.am +++ b/src/ltlast/Makefile.am @@ -19,9 +19,6 @@ ## 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 = \ @@ -31,17 +28,6 @@ ltlast_HEADERS = \ 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 diff --git a/src/ltlast/allnodes.hh b/src/ltlast/allnodes.hh index 9b5664182..53d76103f 100644 --- a/src/ltlast/allnodes.hh +++ b/src/ltlast/allnodes.hh @@ -23,8 +23,6 @@ /// \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 diff --git a/src/ltlast/atomic_prop.hh b/src/ltlast/atomic_prop.hh index 984c37619..e42db59df 100644 --- a/src/ltlast/atomic_prop.hh +++ b/src/ltlast/atomic_prop.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -24,11 +24,8 @@ #ifndef SPOT_LTLAST_ATOMIC_PROP_HH # define SPOT_LTLAST_ATOMIC_PROP_HH -#include -#include -#include -#include "refformula.hh" -#include "ltlenv/environment.hh" +# include "formula.hh" +# include "internal/atomic_prop.hh" namespace spot { @@ -37,38 +34,7 @@ namespace spot /// \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 pair; - typedef std::map map; - static map instances; - - private: - std::string name_; - environment* env_; - }; + typedef spot::internal::atomic_prop atomic_prop; } } diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh index 6bf9fec5d..c44a5af73 100644 --- a/src/ltlast/binop.hh +++ b/src/ltlast/binop.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -27,8 +27,8 @@ #ifndef SPOT_LTLAST_BINOP_HH # define SPOT_LTLAST_BINOP_HH -#include -#include "refformula.hh" +# include "formula.hh" +# include "internal/binop.hh" namespace spot { @@ -37,53 +37,7 @@ namespace spot /// \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 pairf; - typedef std::pair pair; - typedef std::map map; - static map instances; - - binop(type op, formula* first, formula* second); - virtual ~binop(); - - private: - type op_; - formula* first_; - formula* second_; - }; + typedef spot::internal::binop binop; } } diff --git a/src/ltlast/constant.hh b/src/ltlast/constant.hh index 46b15e698..1c4dc6750 100644 --- a/src/ltlast/constant.hh +++ b/src/ltlast/constant.hh @@ -24,7 +24,8 @@ #ifndef SPOT_LTLAST_CONSTANT_HH # define SPOT_LTLAST_CONSTANT_HH -#include "formula.hh" +# include "formula.hh" +# include "internal/constant.hh" namespace spot { @@ -33,30 +34,7 @@ namespace spot /// \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_; - }; + typedef spot::internal::constant constant; } } diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index 749db27bc..7ef933c40 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -24,9 +24,7 @@ #ifndef SPOT_LTLAST_FORMULA_HH # define SPOT_LTLAST_FORMULA_HH -#include -#include -#include "predecl.hh" +# include "internal/formula.hh" namespace spot { @@ -61,6 +59,54 @@ namespace spot /// \addtogroup ltl_misc Miscellaneous algorithms for LTL formulae /// \ingroup ltl_algorithm + struct visitor; + struct const_visitor; + + struct ltl_t + { + typedef spot::ltl::visitor visitor; + typedef spot::ltl::const_visitor const_visitor; + + enum binop { Xor, Implies, Equiv, U, R }; + const char* binop_name(binop op) 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; + } + }; /// \brief An LTL formula. /// \ingroup ltl_essential @@ -68,114 +114,10 @@ namespace spot /// /// The only way you can work with a formula is to /// build a spot::ltl::visitor or spot::ltl::const_visitor. - class formula - { - 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; - - /// \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 hash_key_; - } - protected: - virtual ~formula(); - - /// \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_(); - - /// \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_; - }; - - /// \brief Strict Weak Ordering for const formula*. - /// \ingroup ltl_essentials - /// - /// This is meant to be used as a comparison functor for - /// STL \c map whose key are of type const formula*. - /// - /// 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 seen; - /// \endcode - struct formula_ptr_less_than: - public std::binary_function - { - bool - operator()(const formula* left, const formula* right) const - { - 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(); - } - }; - - /// \brief Hash Function for const formula*. - /// \ingroup ltl_essentials - /// \ingroup hash_funcs - /// - /// This is meant to be used as a hash functor for - /// Sgi's \c hash_map whose key are of type const formula*. - /// - /// 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 seen; - /// \endcode - struct formula_ptr_hash: - public std::unary_function - { - size_t - operator()(const formula* that) const - { - assert(that); - return that->hash(); - } - }; - + typedef spot::internal::formula formula; + typedef spot::internal::formula_ptr_less_than formula_ptr_less_than; + typedef spot::internal::formula_ptr_hash formula_ptr_hash; } } diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index 7157b503b..b662e00de 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -24,9 +24,8 @@ #ifndef SPOT_LTLAST_MULTOP_HH # define SPOT_LTLAST_MULTOP_HH -#include -#include -#include "refformula.hh" +# include "formula.hh" +# include "internal/multop.hh" namespace spot { @@ -37,87 +36,7 @@ namespace spot /// \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 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 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 map; - static map instances; - - multop(type op, vec* v); - virtual ~multop(); - - private: - type op_; - vec* children_; - }; + typedef spot::internal::multop multop; } } diff --git a/src/ltlast/refformula.hh b/src/ltlast/refformula.hh index b086fdd84..b9dedf9c8 100644 --- a/src/ltlast/refformula.hh +++ b/src/ltlast/refformula.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -24,7 +24,8 @@ #ifndef SPOT_LTLAST_REFFORMULA_HH # define SPOT_LTLAST_REFFORMULA_HH -#include "formula.hh" +# include "formula.hh" +# include "internal/refformula.hh" namespace spot { @@ -33,18 +34,7 @@ namespace spot /// \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_; - }; + typedef spot::internal::ref_formula ref_formula; } } diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index 487ecf034..4fe31a392 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -24,8 +24,8 @@ #ifndef SPOT_LTLAST_UNOP_HH # define SPOT_LTLAST_UNOP_HH -#include -#include "refformula.hh" +# include "formula.hh" +# include "internal/unop.hh" namespace spot { @@ -34,43 +34,7 @@ namespace spot /// \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 pair; - typedef std::map map; - static map instances; - - unop(type op, formula* child); - virtual ~unop(); - - private: - type op_; - formula* child_; - }; + typedef spot::internal::unop unop; } } diff --git a/src/ltlast/visitor.hh b/src/ltlast/visitor.hh index a6cfb933b..1a2785ab5 100644 --- a/src/ltlast/visitor.hh +++ b/src/ltlast/visitor.hh @@ -1,6 +1,6 @@ -// 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. +// Copyright (C) 2003, 2004, 2005, 2008 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. // @@ -24,7 +24,11 @@ #ifndef SPOT_LTLAST_VISITOR_HH # define SPOT_LTLAST_VISITOR_HH -#include "predecl.hh" +# include "binop.hh" +# include "unop.hh" +# include "multop.hh" +# include "atomic_prop.hh" +# include "constant.hh" namespace spot { @@ -67,7 +71,6 @@ namespace spot virtual void visit(const multop* node) = 0; }; - } } diff --git a/src/ltlenv/Makefile.am b/src/ltlenv/Makefile.am index c3dbf107f..9ab1e6926 100644 --- a/src/ltlenv/Makefile.am +++ b/src/ltlenv/Makefile.am @@ -19,17 +19,9 @@ ## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA ## 02111-1307, USA. -AM_CPPFLAGS = -I$(srcdir)/.. -AM_CXXFLAGS = $(WARNING_CXXFLAGS) - ltlenvdir = $(pkgincludedir)/ltlenv ltlenv_HEADERS = \ - declenv.hh \ defaultenv.hh \ + declenv.hh \ environment.hh - -noinst_LTLIBRARIES = libltlenv.la -libltlenv_la_SOURCES = \ - declenv.cc \ - defaultenv.cc diff --git a/src/ltlenv/declenv.hh b/src/ltlenv/declenv.hh index 27ff98e01..188d37c6c 100644 --- a/src/ltlenv/declenv.hh +++ b/src/ltlenv/declenv.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -23,10 +23,7 @@ # define SPOT_LTLENV_DECLENV_HH # include "environment.hh" -# include -# include -# include "ltlvisit/destroy.hh" -# include "ltlast/atomic_prop.hh" +# include "internal/declenv.hh" namespace spot { @@ -38,29 +35,9 @@ namespace spot /// /// This environment recognizes all atomic propositions /// that have been previously declared. It will reject other. - class declarative_environment : public environment - { - public: - declarative_environment(); - ~declarative_environment(); + typedef spot::internal::declarative_environment + declarative_environment; - /// Declare an atomic proposition. Return false iff the - /// proposition was already declared. - bool declare(const std::string& prop_str); - - virtual ltl::formula* require(const std::string& prop_str); - - /// Get the name of the environment. - virtual const std::string& name(); - - typedef std::map prop_map; - - /// Get the map of atomic proposition known to this environment. - const prop_map& get_prop_map() const; - - private: - prop_map props_; - }; } } diff --git a/src/ltlenv/defaultenv.hh b/src/ltlenv/defaultenv.hh index abd046270..74ede5cd3 100644 --- a/src/ltlenv/defaultenv.hh +++ b/src/ltlenv/defaultenv.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -23,6 +23,7 @@ # define SPOT_LTLENV_DEFAULTENV_HH # include "environment.hh" +# include "internal/defaultenv.hh" namespace spot { @@ -36,18 +37,7 @@ namespace spot /// /// This is a singleton. Use default_environment::instance() /// to obtain the instance. - class default_environment : public environment - { - public: - virtual ~default_environment(); - virtual formula* require(const std::string& prop_str); - virtual const std::string& name(); - - /// Get the sole instance of spot::ltl::default_environment. - static default_environment& instance(); - protected: - default_environment(); - }; + typedef spot::internal::default_environment default_environment; } } diff --git a/src/ltlenv/environment.hh b/src/ltlenv/environment.hh index 6dd6d8f32..02c8d9810 100644 --- a/src/ltlenv/environment.hh +++ b/src/ltlenv/environment.hh @@ -23,7 +23,7 @@ # define SPOT_LTLENV_ENVIRONMENT_HH # include "ltlast/formula.hh" -# include +# include "internal/environment.hh" namespace spot { @@ -31,37 +31,7 @@ namespace spot { /// \brief An environment that describes atomic propositions. /// \ingroup ltl_essential - class environment - { - public: - /// \brief Obtain the formula associated to \a prop_str - /// - /// Usually \a prop_str, is the name of an atomic proposition, - /// and spot::ltl::require simply returns the associated - /// spot::ltl::atomic_prop. - /// - /// Note this is not a \c const method. Some environments will - /// "create" the atomic proposition when requested. - /// - /// We return a spot::ltl::formula instead of an - /// spot::ltl::atomic_prop, because this - /// will allow nifty tricks (e.g., we could name formulae in an - /// environment, and let the parser build a larger tree from - /// these). - /// - /// \return 0 iff \a prop_str is not part of the environment, - /// or the associated spot::ltl::formula otherwise. - virtual formula* require(const std::string& prop_str) = 0; - - /// Get the name of the environment. - virtual const std::string& name() = 0; - - virtual - ~environment() - { - } - }; - + typedef spot::internal::environment environment; } } diff --git a/src/ltlparse/public.hh b/src/ltlparse/public.hh index 8e5daa819..929748e84 100644 --- a/src/ltlparse/public.hh +++ b/src/ltlparse/public.hh @@ -23,6 +23,7 @@ # define SPOT_LTLPARSE_PUBLIC_HH # include "ltlast/formula.hh" +# include "ltlast/visitor.hh" // Unfortunately Bison 2.3 uses the same guards in all parsers :( # undef BISON_LOCATION_HH # undef BISON_POSITION_HH diff --git a/src/ltlvisit/randomltl.cc b/src/ltlvisit/randomltl.cc index 73cf99493..9b739f429 100644 --- a/src/ltlvisit/randomltl.cc +++ b/src/ltlvisit/randomltl.cc @@ -23,6 +23,7 @@ #include #include "randomltl.hh" #include "ltlast/allnodes.hh" +#include "ltlast/visitor.hh" #include "misc/random.hh" #include #include diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 575b3731d..0dc957dc0 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -23,6 +23,7 @@ #include "tgbatba.hh" #include "bddprint.hh" #include "ltlast/constant.hh" +#include "ltlast/visitor.hh" #include "misc/hashfunc.hh" namespace spot diff --git a/src/tgbaalgos/randomgraph.hh b/src/tgbaalgos/randomgraph.hh index 7f776a61c..618c227c8 100644 --- a/src/tgbaalgos/randomgraph.hh +++ b/src/tgbaalgos/randomgraph.hh @@ -23,6 +23,7 @@ # define SPOT_TGBAALGOS_RANDOMGRAPH_HH #include "ltlvisit/apcollect.hh" +#include "ltlast/visitor.hh" #include "ltlenv/defaultenv.hh" namespace spot diff --git a/src/tgbaparse/public.hh b/src/tgbaparse/public.hh index 652ae6a28..e6103ea7e 100644 --- a/src/tgbaparse/public.hh +++ b/src/tgbaparse/public.hh @@ -27,6 +27,7 @@ # undef BISON_LOCATION_HH # undef BISON_POSITION_HH # include "tgbaparse/location.hh" +# include "ltlast/visitor.hh" # include "ltlenv/defaultenv.hh" # include # include diff --git a/src/tgbatest/explicit.cc b/src/tgbatest/explicit.cc index e917d5b6d..07340a710 100644 --- a/src/tgbatest/explicit.cc +++ b/src/tgbatest/explicit.cc @@ -25,6 +25,7 @@ #include "tgba/tgbaexplicit.hh" #include "tgbaalgos/dotty.hh" #include "ltlast/allnodes.hh" +#include "ltlast/visitor.hh" int main()