diff --git a/ChangeLog b/ChangeLog index 2b2d2c095..4539abd24 100644 --- a/ChangeLog +++ b/ChangeLog @@ -159,25 +159,6 @@ * iface/gspn/ssp.hh, iface/gspn/ssp.cc: Add the reversed_double_inclusion boolean for this. -2008-06-12 Damien Lefortier - - Add ELTL visitors in eltlvisit/ and start the ELTL translation (LACIM). - Merge all eltlast/ files into formula.hh (except automatop.hh). - - * src/eltlast/allnodes.hh, src/eltlast/atomic_prop.hh, - src/eltlast/binop.hh, src/eltlast/constant.hh, src/eltlast/multop.hh, - src/eltlast/refformula.hh, src/eltlast/unop.hh, - src/eltlast/visitor.hh: Delete and merge all these files into ... - * src/eltlast/formula.hh: ... this one. - * src/eltlvisit/: Add some visitors (clone, destroy, ...). - * src/internal/baseformula.hh, src/internal/baseformula.cc: - Add base_formula, a new base class of internal::formula. - * src/tgba/bdddict.cc src/tgba/bdddict.hh, src/tgba/bddprint.cc, - src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbabddconcretefactory.hh - Replace ltl::formula by internal::base_formula. - * src/tgbatest/eltl2tgba.cc: Beginning of the ELTL translation (LACIM). - * m4/boost.m4: Add AX_BOOST_BASE([MINIMUM-VERSION]). - 2008-06-12 Alexandre Duret-Lutz * iface/nips/nipstest/dotty.test, @@ -191,56 +172,15 @@ enough to make it pass "make check". Some major work is needed after the changes from 2008-04-16. -2008-06-12 Alexandre Duret-Lutz - - Merge all ltlast/ files into formula.hh. The forward declaration - of visitor was causing error messages too cryptic for users. - - * src/ltlast/allnodes.hh, src/ltlast/atomic_prop.hh, - src/ltlast/binop.hh, src/ltlast/constant.hh, src/ltlast/multop.hh, - src/ltlast/refformula.hh, src/ltlast/unop.hh, - src/ltlast/visitor.hh: Delete and merge all these files into ... - * src/ltlast/formula.hh: ... this one. - * src/ltlast/Makefile.am: Adjust. - * ltlparse/ltlparse.yy, ltlparse/public.hh, ltltest/equals.cc, - ltltest/randltl.cc, ltltest/readltl.cc, ltltest/reduc.cc, - ltltest/syntimpl.cc, ltltest/tostring.cc, ltlvisit/apcollect.hh, - ltlvisit/basicreduce.cc, ltlvisit/clone.cc, ltlvisit/clone.hh, - ltlvisit/contain.cc, ltlvisit/dotty.cc, ltlvisit/dump.cc, - ltlvisit/lunabbrev.cc, ltlvisit/nenoform.cc, ltlvisit/nenoform.hh, - ltlvisit/postfix.cc, ltlvisit/postfix.hh, ltlvisit/randomltl.cc, - ltlvisit/reduce.cc, ltlvisit/reduce.hh, ltlvisit/simpfg.cc, - ltlvisit/syntimpl.cc, ltlvisit/tostring.cc, ltlvisit/tunabbrev.cc, - tgba/bdddict.cc, tgba/formula2bdd.cc, tgba/tgbaexplicit.cc, - tgba/tgbatba.cc, tgbaalgos/ltl2tgba_fm.cc, - tgbaalgos/ltl2tgba_lacim.cc, tgbaalgos/randomgraph.cc, - tgbaalgos/randomgraph.hh, tgbaalgos/save.cc, tgbaparse/public.hh, - tgbaparse/tgbaparse.yy, tgbatest/explicit.cc, - tgbatest/explprod.cc, tgbatest/ltl2tgba.cc, tgbatest/ltlprod.cc, - tgbatest/mixprod.cc, tgbatest/powerset.cc, tgbatest/randtgba.cc, - tgbatest/readsave.cc, tgbatest/reductgba.cc, tgbatest/tgbaread.cc, - tgbatest/tripprod.cc: Adjust includes. - -2008-06-12 Alexandre Duret-Lutz - - * src/ltlast/atomic_prop.cc, src/ltlast/binop.cc, - src/ltlast/constant.cc, src/ltlast/formula.cc, - src/ltlast/multop.cc, src/ltlast/predecl.hh, - src/ltlast/refformula.cc, src/ltlast/unop.cc: Delete these files, - not used anymore since 2008-04-16. - 2008-06-11 Alexandre Duret-Lutz * iface/nips/dottynips.cc: Include ctsdlib for exit(). * iface/nips/emptiness_check.cc: Likewise. - * src/eltlparse/eltlparse.yy: Include limits.h for INT_MIN and - INT_MAX. - * src/sanity/includes.test: Remove empty line at beginning of file. * src/internal/formula.hh (formula::hash): Remove the const - qualifier from the return type, GCC 4.3.1 gicomplains. + qualifier from the return type, GCC 4.3.1 complains. 2008-06-02 Guillaume SADEGH @@ -317,30 +257,6 @@ * src/Makefile.am (_.cc): Fix for `make tags`. -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 5a1357901..8923f4eba 100644 --- a/configure.ac +++ b/configure.ac @@ -44,7 +44,6 @@ AC_LANG(C++) AX_CHECK_BUDDY AX_CHECK_LBTT AX_CHECK_GSPNLIB -AX_BOOST_BASE([1.34]) AC_CHECK_FUNCS([srand48 drand48]) @@ -87,18 +86,11 @@ AC_CONFIG_FILES([ iface/nips/nipstest/Makefile iface/nips/nipstest/defs src/Makefile - src/eltlast/Makefile - src/eltlenv/Makefile - src/eltlparse/Makefile - src/eltltest/Makefile - src/eltltest/defs - src/eltlvisit/Makefile 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/m4/boost.m4 b/m4/boost.m4 deleted file mode 100644 index 02534a30e..000000000 --- a/m4/boost.m4 +++ /dev/null @@ -1,194 +0,0 @@ -##### http://autoconf-archive.cryp.to/ax_boost_base.html -# -# SYNOPSIS -# -# AX_BOOST_BASE([MINIMUM-VERSION]) -# -# DESCRIPTION -# -# Test for the Boost C++ libraries of a particular version (or newer) -# -# If no path to the installed boost library is given the macro -# searchs under /usr, /usr/local, /opt and /opt/local and evaluates -# the $BOOST_ROOT environment variable. Further documentation is -# available at . -# -# This macro calls: -# -# AC_SUBST(BOOST_CPPFLAGS) / AC_SUBST(BOOST_LDFLAGS) -# -# And sets: -# -# HAVE_BOOST -# -# LAST MODIFICATION -# -# 2007-07-28 -# -# COPYLEFT -# -# Copyright (c) 2007 Thomas Porschberg -# -# Copying and distribution of this file, with or without -# modification, are permitted in any medium without royalty provided -# the copyright notice and this notice are preserved. - -AC_DEFUN([AX_BOOST_BASE], -[ -AC_ARG_WITH([boost], - AS_HELP_STRING([--with-boost@<:@=DIR@:>@], [use boost (default is yes) - it is possible to specify the root directory for boost (optional)]), - [ - if test "$withval" = "no"; then - want_boost="no" - elif test "$withval" = "yes"; then - want_boost="yes" - ac_boost_path="" - else - want_boost="yes" - ac_boost_path="$withval" - fi - ], - [want_boost="yes"]) - -if test "x$want_boost" = "xyes"; then - boost_lib_version_req=ifelse([$1], ,1.20.0,$1) - boost_lib_version_req_shorten=`expr $boost_lib_version_req : '\([[0-9]]*\.[[0-9]]*\)'` - boost_lib_version_req_major=`expr $boost_lib_version_req : '\([[0-9]]*\)'` - boost_lib_version_req_minor=`expr $boost_lib_version_req : '[[0-9]]*\.\([[0-9]]*\)'` - boost_lib_version_req_sub_minor=`expr $boost_lib_version_req : '[[0-9]]*\.[[0-9]]*\.\([[0-9]]*\)'` - if test "x$boost_lib_version_req_sub_minor" = "x" ; then - boost_lib_version_req_sub_minor="0" - fi - WANT_BOOST_VERSION=`expr $boost_lib_version_req_major \* 100000 \+ $boost_lib_version_req_minor \* 100 \+ $boost_lib_version_req_sub_minor` - AC_MSG_CHECKING(for boostlib >= $boost_lib_version_req) - succeeded=no - - dnl first we check the system location for boost libraries - dnl this location ist chosen if boost libraries are installed with the --layout=system option - dnl or if you install boost with RPM - if test "$ac_boost_path" != ""; then - BOOST_LDFLAGS="-L$ac_boost_path/lib" - BOOST_CPPFLAGS="-I$ac_boost_path/include" - else - for ac_boost_path_tmp in /usr /usr/local /opt /opt/local ; do - if test -d "$ac_boost_path_tmp/include/boost" && test -r "$ac_boost_path_tmp/include/boost"; then - BOOST_LDFLAGS="-L$ac_boost_path_tmp/lib" - BOOST_CPPFLAGS="-I$ac_boost_path_tmp/include" - break; - fi - done - fi - - CPPFLAGS_SAVED="$CPPFLAGS" - CPPFLAGS="$CPPFLAGS $BOOST_CPPFLAGS" - - LDFLAGS_SAVED="$LDFLAGS" - LDFLAGS="$LDFLAGS $BOOST_LDFLAGS" - - AC_LANG_PUSH(C++) - AC_COMPILE_IFELSE([AC_LANG_PROGRAM([[ - @%:@include - ]], [[ - #if BOOST_VERSION >= $WANT_BOOST_VERSION - // Everything is okay - #else - # error Boost version is too old - #endif - ]])],[ - AC_MSG_RESULT(yes) - succeeded=yes - found_system=yes - ],[ - ]) - AC_LANG_POP([C++]) - - - - dnl if we found no boost with system layout we search for boost libraries - dnl built and installed without the --layout=system option or for a staged(not installed) version - if test "x$succeeded" != "xyes"; then - _version=0 - if test "$ac_boost_path" != ""; then - BOOST_LDFLAGS="-L$ac_boost_path/lib" - if test -d "$ac_boost_path" && test -r "$ac_boost_path"; then - for i in `ls -d $ac_boost_path/include/boost-* 2>/dev/null`; do - _version_tmp=`echo $i | sed "s#$ac_boost_path##" | sed 's/\/include\/boost-//' | sed 's/_/./'` - V_CHECK=`expr $_version_tmp \> $_version` - if test "$V_CHECK" = "1" ; then - _version=$_version_tmp - fi - VERSION_UNDERSCORE=`echo $_version | sed 's/\./_/'` - BOOST_CPPFLAGS="-I$ac_boost_path/include/boost-$VERSION_UNDERSCORE" - done - fi - else - for ac_boost_path in /usr /usr/local /opt /opt/local ; do - if test -d "$ac_boost_path" && test -r "$ac_boost_path"; then - for i in `ls -d $ac_boost_path/include/boost-* 2>/dev/null`; do - _version_tmp=`echo $i | sed "s#$ac_boost_path##" | sed 's/\/include\/boost-//' | sed 's/_/./'` - V_CHECK=`expr $_version_tmp \> $_version` - if test "$V_CHECK" = "1" ; then - _version=$_version_tmp - best_path=$ac_boost_path - fi - done - fi - done - - VERSION_UNDERSCORE=`echo $_version | sed 's/\./_/'` - BOOST_CPPFLAGS="-I$best_path/include/boost-$VERSION_UNDERSCORE" - BOOST_LDFLAGS="-L$best_path/lib" - - if test "x$BOOST_ROOT" != "x"; then - if test -d "$BOOST_ROOT" && test -r "$BOOST_ROOT" && test -d "$BOOST_ROOT/stage/lib" && test -r "$BOOST_ROOT/stage/lib"; then - version_dir=`expr //$BOOST_ROOT : '.*/\(.*\)'` - stage_version=`echo $version_dir | sed 's/boost_//' | sed 's/_/./g'` - stage_version_shorten=`expr $stage_version : '\([[0-9]]*\.[[0-9]]*\)'` - V_CHECK=`expr $stage_version_shorten \>\= $_version` - if test "$V_CHECK" = "1" ; then - AC_MSG_NOTICE(We will use a staged boost library from $BOOST_ROOT) - BOOST_CPPFLAGS="-I$BOOST_ROOT" - BOOST_LDFLAGS="-L$BOOST_ROOT/stage/lib" - fi - fi - fi - fi - - CPPFLAGS="$CPPFLAGS $BOOST_CPPFLAGS" - LDFLAGS="$LDFLAGS $BOOST_LDFLAGS" - - AC_LANG_PUSH(C++) - AC_COMPILE_IFELSE([AC_LANG_PROGRAM([[ - @%:@include - ]], [[ - #if BOOST_VERSION >= $WANT_BOOST_VERSION - // Everything is okay - #else - # error Boost version is too old - #endif - ]])],[ - AC_MSG_RESULT(yes) - succeeded=yes - found_system=yes - ],[ - ]) - AC_LANG_POP([C++]) - fi - - if test "$succeeded" != "yes" ; then - CPPFLAGS="$CPPFLAGS_SAVED" - LDFLAGS="$LDFLAGS_SAVED" - - if test "$_version" = "0" ; then - AC_MSG_ERROR([[We could not detect the boost libraries (version $boost_lib_version_req_shorten or higher). If you have a staged boost library (still not installed) please specify \$BOOST_ROOT in your environment and do not give a PATH to --with-boost option. If you are sure you have boost installed, then check your version number looking in . See http://randspringer.de/boost for more documentation.]]) - else - AC_MSG_NOTICE([Your boost libraries seems to old (version $_version).]) - fi - else - AC_SUBST(BOOST_CPPFLAGS) - AC_SUBST(BOOST_LDFLAGS) - AC_DEFINE(HAVE_BOOST,,[define if the Boost library is available]) - fi -fi - -]) diff --git a/src/Makefile.am b/src/Makefile.am index 97e1ba8b7..01e978131 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -23,23 +23,20 @@ AUTOMAKE_OPTIONS = subdir-objects # List directories in the order they must be built. # Keep tests at the end. -SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse internal \ - eltlenv eltlast eltlvisit eltlparse \ +SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse \ tgba tgbaalgos tgbaparse \ evtgba evtgbaalgos evtgbaparse . \ - ltltest eltltest tgbatest evtgbatest sanity + ltltest 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 \ - internal/libinternal.la \ - eltlast/libeltlast.la \ - eltlparse/libeltlparse.la \ - eltlvisit/libeltlvisit.la \ + ltlast/libltlast.la \ tgba/libtgba.la \ tgbaalgos/libtgbaalgos.la \ tgbaparse/libtgbaparse.la \ diff --git a/src/eltlast/Makefile.am b/src/eltlast/Makefile.am deleted file mode 100644 index 74d0a3f94..000000000 --- a/src/eltlast/Makefile.am +++ /dev/null @@ -1,35 +0,0 @@ -## 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 = \ - automatop.hh \ - formula.hh \ - nfa.hh - -noinst_LTLIBRARIES = libeltlast.la -libeltlast_la_SOURCES = \ - automatop.cc \ - nfa.cc diff --git a/src/eltlast/automatop.cc b/src/eltlast/automatop.cc deleted file mode 100644 index 5178f5d16..000000000 --- a/src/eltlast/automatop.cc +++ /dev/null @@ -1,120 +0,0 @@ -// 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 "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 deleted file mode 100644 index 0f8524cc8..000000000 --- a/src/eltlast/automatop.hh +++ /dev/null @@ -1,86 +0,0 @@ -// 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 "formula.hh" -# include "nfa.hh" - -namespace spot -{ - namespace eltl - { - /// \brief Counted-reference formulae. - /// \ingroup eltl_ast - typedef spot::internal::ref_formula ref_formula; - - /// \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/formula.hh b/src/eltlast/formula.hh deleted file mode 100644 index 1e10f2722..000000000 --- a/src/eltlast/formula.hh +++ /dev/null @@ -1,200 +0,0 @@ -// 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" -# include "internal/atomic_prop.hh" -# include "internal/constant.hh" -# include "internal/unop.hh" -# include "internal/binop.hh" -# include "internal/multop.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 - - /// \addtogroup eltl_environment ELTL environments - /// \ingroup eltl - /// ELTL environment implementations. - - /// \addtogroup eltl_algorithm Algorithms for ELTL formulae - /// \ingroup eltl - - /// \addtogroup eltl_io Input/Output of ELTL formulae - /// \ingroup eltl_algorithm - - /// \addtogroup eltl_visitor Derivable visitors - /// \ingroup eltl_algorithm - - /// Forward declarations - struct eltl_t; - 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. - typedef spot::internal::formula formula; - - /// Forward declarations - formula* clone(const formula* f); - std::ostream& to_string(const formula* f, std::ostream& os); - void destroy(const formula* f); - - struct eltl_t - { - typedef spot::eltl::visitor visitor; - typedef spot::eltl::const_visitor const_visitor; - - static formula* clone_(const formula* f) - { - return clone(f); - } - - static std::ostream& to_string_(const formula* f, std::ostream& os) - { - return to_string(f, os); - } - - static void destroy_(const formula* f) - { - destroy(f); - } - - 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_ptr_less_than formula_ptr_less_than; - typedef spot::internal::formula_ptr_hash formula_ptr_hash; - - /// \brief Atomic propositions. - /// \ingroup eltl_ast - typedef spot::internal::atomic_prop atomic_prop; - - /// \brief A constant (True or False) - /// \ingroup eltl_ast - typedef spot::internal::constant constant; - - /// \brief Unary operators. - /// \ingroup eltl_ast - typedef spot::internal::unop unop; - - /// \brief Binary operator. - /// \ingroup eltl_ast - typedef spot::internal::binop binop; - - /// \brief Multi-operand operators. - /// \ingroup eltl_ast - /// - /// These operators are considered commutative and associative. - typedef spot::internal::multop multop; - - // 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_FORMULA_HH_ */ diff --git a/src/eltlast/nfa.cc b/src/eltlast/nfa.cc deleted file mode 100644 index 2dc944f3f..000000000 --- a/src/eltlast/nfa.cc +++ /dev/null @@ -1,127 +0,0 @@ -// 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, int 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(); - } - - int - 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 deleted file mode 100644 index c578ca5de..000000000 --- a/src/eltlast/nfa.hh +++ /dev/null @@ -1,147 +0,0 @@ -// 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 - { - int cost; - const state* dest; - }; - - nfa(); - ~nfa(); - - void - add_transition(const std::string& s, const std::string& d, int 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. - int - 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_; - - int 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/eltlenv/Makefile.am b/src/eltlenv/Makefile.am deleted file mode 100644 index aac06bcdb..000000000 --- a/src/eltlenv/Makefile.am +++ /dev/null @@ -1,27 +0,0 @@ -## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -## département Systèmes Répartis Coopératifs (SRC), Université Pierre -## et Marie Curie. -## -## This file is part of Spot, a model checking library. -## -## Spot is free software; you can redistribute it and/or modify it -## under the terms of the GNU General Public License as published by -## the Free Software Foundation; either version 2 of the License, or -## (at your option) any later version. -## -## Spot is distributed in the hope that it will be useful, but WITHOUT -## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -## License for more details. -## -## You should have received a copy of the GNU General Public License -## along with Spot; see the file COPYING. If not, write to the Free -## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -## 02111-1307, USA. - -eltlenvdir = $(pkgincludedir)/eltlenv - -eltlenv_HEADERS = \ - defaultenv.hh \ - declenv.hh \ - environment.hh diff --git a/src/eltlenv/declenv.hh b/src/eltlenv/declenv.hh deleted file mode 100644 index ddb8ba633..000000000 --- a/src/eltlenv/declenv.hh +++ /dev/null @@ -1,44 +0,0 @@ -// 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 deleted file mode 100644 index b251c27b5..000000000 --- a/src/eltlenv/defaultenv.hh +++ /dev/null @@ -1,45 +0,0 @@ -// 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 deleted file mode 100644 index 320af7d0a..000000000 --- a/src/eltlenv/environment.hh +++ /dev/null @@ -1,39 +0,0 @@ -// 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 deleted file mode 100644 index 026172405..000000000 --- a/src/eltlparse/Makefile.am +++ /dev/null @@ -1,62 +0,0 @@ -## 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 deleted file mode 100644 index bf00b4334..000000000 --- a/src/eltlparse/eltlparse.yy +++ /dev/null @@ -1,289 +0,0 @@ -/* 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 -#include -#include "public.hh" -#include "eltlast/automatop.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 ACC "accept" - 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); - delete $1; - } -; - -nfa_def: /* empty. */ - { - $$ = new nfa(); - } - | nfa_def STATE STATE ARG - { - errno = 0; - long i = strtol($4->c_str(), 0, 10); - if (i > std::numeric_limits::max() || - i < std::numeric_limits::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 STATE STATE CONST_TRUE - { - $1->add_transition(*$2, *$3, -1); - $$ = $1; - } - | nfa_def ACC 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 deleted file mode 100644 index a54f5491c..000000000 --- a/src/eltlparse/eltlscan.ll +++ /dev/null @@ -1,187 +0,0 @@ -/* 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; -"accept" return token::ACC; -[tT][rR][uU][eE] { - return token::CONST_TRUE; - } -"(" 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 deleted file mode 100644 index b2e086f65..000000000 --- a/src/eltlparse/fmterror.cc +++ /dev/null @@ -1,48 +0,0 @@ -// 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 deleted file mode 100644 index 9d9847edc..000000000 --- a/src/eltlparse/parsedecl.hh +++ /dev/null @@ -1,43 +0,0 @@ -// 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 deleted file mode 100644 index 19eafdb10..000000000 --- a/src/eltlparse/public.hh +++ /dev/null @@ -1,83 +0,0 @@ -// 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" -// 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 deleted file mode 100644 index 7f8a53ed6..000000000 --- a/src/eltltest/Makefile.am +++ /dev/null @@ -1,44 +0,0 @@ -## 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 deleted file mode 100644 index 289ff41d5..000000000 --- a/src/eltltest/acc.cc +++ /dev/null @@ -1,42 +0,0 @@ -// 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 deleted file mode 100755 index 6080022f0..000000000 --- a/src/eltltest/acc.test +++ /dev/null @@ -1,44 +0,0 @@ -#!/bin/sh - -. ./defs || exit 1 - -set -e -cat >prelude <input <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 deleted file mode 100644 index 59b181db4..000000000 --- a/src/eltltest/nfa.cc +++ /dev/null @@ -1,57 +0,0 @@ -// 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 deleted file mode 100755 index 241c7f207..000000000 --- a/src/eltltest/nfa.test +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh - -. ./defs || exit 1 - -set -e -run 0 ./nfa || exit 1 diff --git a/src/eltlvisit/Makefile.am b/src/eltlvisit/Makefile.am deleted file mode 100644 index 9877609ce..000000000 --- a/src/eltlvisit/Makefile.am +++ /dev/null @@ -1,42 +0,0 @@ -## 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)/.. $(BUDDY_CPPFLAGS) -AM_CXXFLAGS = $(WARNING_CXXFLAGS) - -eltlvisitdir = $(pkgincludedir)/eltlvisit - -eltlvisit_HEADERS = \ - clone.hh \ - destroy.hh \ - lunabbrev.hh \ - nenoform.hh \ - postfix.hh \ - tostring.hh - -noinst_LTLIBRARIES = libeltlvisit.la -libeltlvisit_la_SOURCES = \ - clone.cc \ - destroy.cc \ - lunabbrev.cc \ - nenoform.cc \ - postfix.cc \ - tostring.cc diff --git a/src/eltlvisit/clone.cc b/src/eltlvisit/clone.cc deleted file mode 100644 index e86de3a57..000000000 --- a/src/eltlvisit/clone.cc +++ /dev/null @@ -1,103 +0,0 @@ -// 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 "eltlast/automatop.hh" -#include "clone.hh" -#include "destroy.hh" - -namespace spot -{ - namespace eltl - { - clone_visitor::clone_visitor() - { - } - - clone_visitor::~clone_visitor() - { - } - - formula* - clone_visitor::result() const - { - return result_; - } - - void - clone_visitor::visit(atomic_prop* ap) - { - result_ = ap->ref(); - } - - void - clone_visitor::visit(constant* c) - { - result_ = c->ref(); - } - - void - clone_visitor::visit(unop* uo) - { - result_ = unop::instance(uo->op(), recurse(uo->child())); - } - - void - clone_visitor::visit(binop* bo) - { - result_ = binop::instance(bo->op(), - recurse(bo->first()), recurse(bo->second())); - } - - void - clone_visitor::visit(multop* mo) - { - multop::vec* res = new multop::vec; - unsigned mos = mo->size(); - for (unsigned i = 0; i < mos; ++i) - res->push_back(recurse(mo->nth(i))); - result_ = multop::instance(mo->op(), res); - } - - formula* - clone_visitor::recurse(formula* f) - { - return clone(f); - } - - void - clone_visitor::visit(automatop* ao) - { - automatop::vec* res = new automatop::vec; - for (unsigned i = 0; i < ao->size(); ++i) - res->push_back(recurse(ao->nth(i))); - result_ = automatop::instance(res); - // FIXME: nfa clone ! - } - - formula* - clone(const formula* f) - { - clone_visitor v; - const_cast(f)->accept(v); - return v.result(); - } - } -} diff --git a/src/eltlvisit/clone.hh b/src/eltlvisit/clone.hh deleted file mode 100644 index 4b73669e7..000000000 --- a/src/eltlvisit/clone.hh +++ /dev/null @@ -1,64 +0,0 @@ -// 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_ELTLVISIT_CLONE_HH -# define SPOT_ELTLVISIT_CLONE_HH - -#include "eltlast/formula.hh" - -namespace spot -{ - namespace eltl - { - /// \brief Clone a formula. - /// \ingroup eltl_visitor - /// - /// This visitor is public, because it's convenient to derive from - /// it and override part of its methods. But if you just want the - /// functionality, consider using spot::eltl::clone instead. - class clone_visitor : public visitor - { - public: - clone_visitor(); - virtual ~clone_visitor(); - - formula* result() const; - - void visit(atomic_prop* ap); - void visit(unop* uo); - void visit(binop* bo); - void visit(multop* mo); - void visit(constant* c); - void visit(automatop* ao); - - virtual formula* recurse(formula* f); - - protected: - formula* result_; - }; - - /// \brief Clone a formula. - /// \ingroup eltl_essential - formula* clone(const formula* f); - } -} - -#endif // SPOT_ELTLVISIT_LUNABBREV_HH diff --git a/src/eltlvisit/destroy.hh b/src/eltlvisit/destroy.hh deleted file mode 100644 index 8f15bed71..000000000 --- a/src/eltlvisit/destroy.hh +++ /dev/null @@ -1,50 +0,0 @@ -// 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_ELTLVISIT_DESTROY_HH -# define SPOT_ELTLVISIT_DESTROY_HH - -#include "eltlvisit/postfix.hh" - -namespace spot -{ - namespace eltl - { - /// \ingroup eltl_visitor - /// - /// This visitor is public, because it's convenient to write the - /// destroy method of the base_formula class. But if you just - /// want the functionality, consider using spot::eltl::destroy - /// instead. - class destroy_visitor: public postfix_visitor - { - public: - virtual void - doit_default(formula* c); - }; - - /// \brief Destroys a formula - /// \ingroup eltl_essential - void destroy(const formula *f); - } -} - -#endif // SPOT_ELTLVISIT_DESTROY_HH diff --git a/src/eltlvisit/lunabbrev.cc b/src/eltlvisit/lunabbrev.cc deleted file mode 100644 index ee317d3d3..000000000 --- a/src/eltlvisit/lunabbrev.cc +++ /dev/null @@ -1,96 +0,0 @@ -// 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 "clone.hh" -#include "destroy.hh" -#include "lunabbrev.hh" - -namespace spot -{ - namespace eltl - { - - unabbreviate_logic_visitor::unabbreviate_logic_visitor() - { - } - - unabbreviate_logic_visitor::~unabbreviate_logic_visitor() - { - } - - void - unabbreviate_logic_visitor::visit(binop* bo) - { - formula* f1 = recurse(bo->first()); - formula* f2 = recurse(bo->second()); - - switch (bo->op()) - { - /* f1 ^ f2 == (f1 & !f2) | (f2 & !f1) */ - case binop::Xor: - result_ = multop::instance(multop::Or, - multop::instance(multop::And, clone(f1), - unop::instance(unop::Not, - f2)), - multop::instance(multop::And, clone(f2), - unop::instance(unop::Not, - f1))); - return; - /* f1 => f2 == !f1 | f2 */ - case binop::Implies: - result_ = multop::instance(multop::Or, - unop::instance(unop::Not, f1), f2); - return; - /* f1 <=> f2 == (f1 & f2) | (!f1 & !f2) */ - case binop::Equiv: - result_ = multop::instance(multop::Or, - multop::instance(multop::And, - clone(f1), clone(f2)), - multop::instance(multop::And, - unop::instance(unop::Not, - f1), - unop::instance(unop::Not, - f2))); - return; - default: - result_ = binop::instance(bo->op(), f1, f2); - return; - } - /* Unreachable code. */ - assert(0); - } - - formula* - unabbreviate_logic_visitor::recurse(formula* f) - { - return unabbreviate_logic(f); - } - - formula* - unabbreviate_logic(const formula* f) - { - unabbreviate_logic_visitor v; - const_cast(f)->accept(v); - return v.result(); - } - } -} diff --git a/src/eltlvisit/lunabbrev.hh b/src/eltlvisit/lunabbrev.hh deleted file mode 100644 index 954d22d1d..000000000 --- a/src/eltlvisit/lunabbrev.hh +++ /dev/null @@ -1,68 +0,0 @@ -// 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_ELTLVISIT_LUNABBREV_HH -# define SPOT_ELTLVISIT_LUNABBREV_HH - -#include "clone.hh" - -namespace spot -{ - namespace eltl - { - /// \brief Clone and rewrite a formula to remove most of the - /// abbreviated logical operators. - /// \ingroup eltl_visitor - /// - /// This will rewrite binary operators such as binop::Implies, - /// binop::Equals, and binop::Xor, using only unop::Not, - /// multop::Or, and multop::And. - /// - /// This visitor is public, because it's convenient to derive from - /// it and override some of its methods. But if you just want the - /// functionality, consider using spot::ltl::unabbreviate_logic - /// instead. - class unabbreviate_logic_visitor : public clone_visitor - { - typedef clone_visitor super; - public: - unabbreviate_logic_visitor(); - virtual ~unabbreviate_logic_visitor(); - - using super::visit; - void visit(binop* bo); - - virtual formula* recurse(formula* f); - }; - - /// \brief Clone and rewrite a formula to remove most of the - /// abbreviated logical operators. - /// \ingroup eltl_rewriting - /// - /// This will rewrite binary operators such as binop::Implies, - /// binop::Equals, and binop::Xor, using only unop::Not, - /// multop::Or, and multop::And. - formula* unabbreviate_logic(const formula* f); - - } -} - -#endif // SPOT_ELTLVISIT_LUNABBREV_HH diff --git a/src/eltlvisit/nenoform.cc b/src/eltlvisit/nenoform.cc deleted file mode 100644 index 6df9f3982..000000000 --- a/src/eltlvisit/nenoform.cc +++ /dev/null @@ -1,187 +0,0 @@ -// 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 "nenoform.hh" -#include "clone.hh" -#include "destroy.hh" -#include - -namespace spot -{ - namespace eltl - { - namespace - { - class negative_normal_form_visitor: public visitor - { - public: - negative_normal_form_visitor(bool negated) - : negated_(negated) - { - } - - virtual - ~negative_normal_form_visitor() - { - } - - formula* result() const - { - return result_; - } - - void - visit(atomic_prop* ap) - { - formula* f = ap->ref(); - if (negated_) - result_ = unop::instance(unop::Not, f); - else - result_ = f; - } - - void - visit(constant* c) - { - if (!negated_) - { - result_ = c; - return; - } - - switch (c->val()) - { - case constant::True: - result_ = constant::false_instance(); - return; - case constant::False: - result_ = constant::true_instance(); - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(unop* uo) - { - formula* f = uo->child(); - switch (uo->op()) - { - case unop::Not: - result_ = recurse_(f, negated_ ^ true); - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(binop* bo) - { - formula* f1 = bo->first(); - formula* f2 = bo->second(); - switch (bo->op()) - { - case binop::Xor: - /* !(a ^ b) == a <=> b */ - result_ = binop::instance(negated_ ? binop::Equiv : binop::Xor, - recurse_(f1, false), - recurse_(f2, false)); - return; - case binop::Equiv: - /* !(a <=> b) == a ^ b */ - result_ = binop::instance(negated_ ? binop::Xor : binop::Equiv, - recurse_(f1, false), - recurse_(f2, false)); - return; - case binop::Implies: - if (negated_) - /* !(a => b) == a & !b */ - result_ = multop::instance(multop::And, - recurse_(f1, false), - recurse_(f2, true)); - else - result_ = binop::instance(binop::Implies, - recurse(f1), recurse(f2)); - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(multop* mo) - { - /* !(a & b & c) == !a | !b | !c */ - /* !(a | b | c) == !a & !b & !c */ - multop::type op = mo->op(); - if (negated_) - switch (op) - { - case multop::And: - op = multop::Or; - break; - case multop::Or: - op = multop::And; - break; - } - multop::vec* res = new multop::vec; - unsigned mos = mo->size(); - for (unsigned i = 0; i < mos; ++i) - res->push_back(recurse(mo->nth(i))); - result_ = multop::instance(op, res); - } - - void - visit(automatop* ao) - { - (void) ao; - } - - formula* - recurse_(formula* f, bool negated) - { - return negative_normal_form(f, negated); - } - - formula* - recurse(formula* f) - { - return recurse_(f, negated_); - } - - protected: - formula* result_; - bool negated_; - }; - } - - formula* - negative_normal_form(const formula* f, bool negated) - { - negative_normal_form_visitor v(negated); - const_cast(f)->accept(v); - return v.result(); - } - - } -} diff --git a/src/eltlvisit/nenoform.hh b/src/eltlvisit/nenoform.hh deleted file mode 100644 index e516cf9f5..000000000 --- a/src/eltlvisit/nenoform.hh +++ /dev/null @@ -1,51 +0,0 @@ -// 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_ELTLVISIT_NENOFORM_HH -# define SPOT_ELTLVISIT_NENOFORM_HH - -#include "eltlast/formula.hh" - -namespace spot -{ - namespace eltl - { - /// \brief Build the negative normal form of \a f. - /// \ingroup eltl_rewriting - /// - /// All negations of the formula are pushed in front of the - /// atomic propositions. - /// - /// \param f The formula to normalize. - /// \param negated If \c true, return the negative normal form of - /// \c !f - /// - /// Note that this will not remove abbreviated operators. If you - /// want to remove abbreviations, call - /// spot::eltl::unabbreviate_logic first. (Calling these - /// functions after spot::eltl::negative_normal_form would likely - /// produce a formula which is not in negative normal form.) - - formula* negative_normal_form(const formula* f, bool negated = false); - } -} - -#endif // SPOT_ELTLVISIT_NENOFORM_HH diff --git a/src/eltlvisit/postfix.cc b/src/eltlvisit/postfix.cc deleted file mode 100644 index 030218c1b..000000000 --- a/src/eltlvisit/postfix.cc +++ /dev/null @@ -1,125 +0,0 @@ -// 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 "eltlast/automatop.hh" -#include "postfix.hh" - -namespace spot -{ - namespace eltl - { - postfix_visitor::postfix_visitor() - { - } - - postfix_visitor::~postfix_visitor() - { - } - - void - postfix_visitor::visit(atomic_prop* ap) - { - doit(ap); - } - - void - postfix_visitor::visit(unop* uo) - { - uo->child()->accept(*this); - doit(uo); - } - - void - postfix_visitor::visit(binop* bo) - { - bo->first()->accept(*this); - bo->second()->accept(*this); - doit(bo); - } - - void - postfix_visitor::visit(multop* mo) - { - unsigned s = mo->size(); - for (unsigned i = 0; i < s; ++i) - mo->nth(i)->accept(*this); - doit(mo); - } - - void - postfix_visitor::visit(constant* c) - { - doit(c); - } - - void - postfix_visitor::visit(automatop* ao) - { - unsigned s = ao->size(); - for (unsigned i = 0; i < s; ++i) - ao->nth(i)->accept(*this); - doit(ao); - } - - void - postfix_visitor::doit(atomic_prop* ap) - { - doit_default(ap); - } - - void - postfix_visitor::doit(unop* uo) - { - doit_default(uo); - } - - void - postfix_visitor::doit(binop* bo) - { - doit_default(bo); - } - - void - postfix_visitor::doit(multop* mo) - { - doit_default(mo); - } - - void - postfix_visitor::doit(constant* c) - { - doit_default(c); - } - - void - postfix_visitor::doit(automatop* c) - { - doit_default(c); - } - - void - postfix_visitor::doit_default(formula* f) - { - (void)f; - // Dummy implementation that does nothing. - } - } -} diff --git a/src/eltlvisit/postfix.hh b/src/eltlvisit/postfix.hh deleted file mode 100644 index 25b2925a7..000000000 --- a/src/eltlvisit/postfix.hh +++ /dev/null @@ -1,61 +0,0 @@ -// 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_ELTLVISIT_POSTFIX_HH -# define SPOT_ELTLVISIT_POSTFIX_HH - -#include "eltlast/formula.hh" - -namespace spot -{ - namespace eltl - { - /// \brief Apply an algorithm on each node of an AST, - /// during a postfix traversal. - /// \ingroup eltl_visitor - /// - /// Override one or more of the postifix_visitor::doit methods - /// with the algorithm to apply. - class postfix_visitor : public visitor - { - public: - postfix_visitor(); - virtual ~postfix_visitor(); - - void visit(atomic_prop* ap); - void visit(unop* uo); - void visit(binop* bo); - void visit(multop* mo); - void visit(constant* c); - void visit(automatop* ao); - - virtual void doit(atomic_prop* ap); - virtual void doit(unop* uo); - virtual void doit(binop* bo); - virtual void doit(multop* mo); - virtual void doit(constant* c); - virtual void doit(automatop* ao); - virtual void doit_default(formula* f); - }; - } -} - -#endif // SPOT_ELTLVISIT_POSTFIX_HH diff --git a/src/eltlvisit/tostring.cc b/src/eltlvisit/tostring.cc deleted file mode 100644 index 8caf27b65..000000000 --- a/src/eltlvisit/tostring.cc +++ /dev/null @@ -1,198 +0,0 @@ -// 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. - -#include -#include -#include -#include -#include -#include "tostring.hh" - -namespace spot -{ - namespace eltl - { - namespace - { - static bool - is_bare_word(const char* str) - { - // Bare words cannot be empty, start with the letter of a unary - // operator, or be the name of an existing constant. Also they - // should start with an letter. - if (!*str - || *str == 'F' - || *str == 'G' - || *str == 'X' - || !(isalpha(*str) || *str == '_') - || !strcasecmp(str, "true") - || !strcasecmp(str, "false")) - return false; - // The remaining of the word must be alphanumeric. - while (*++str) - if (!(isalnum(*str) || *str == '_')) - return false; - return true; - } - - class to_string_visitor: public const_visitor - { - public: - to_string_visitor(std::ostream& os) - : os_(os), top_level_(true) - { - } - - virtual - ~to_string_visitor() - { - } - - void - visit(const atomic_prop* ap) - { - std::string str = ap->name(); - if (!is_bare_word(str.c_str())) - { - os_ << '"' << str << '"'; - } - else - { - os_ << str; - } - } - - void - visit(const constant* c) - { - os_ << c->val_name(); - } - - void - visit(const binop* bo) - { - bool top_level = top_level_; - top_level_ = false; - if (!top_level) - os_ << "("; - - bo->first()->accept(*this); - - switch (bo->op()) - { - case binop::Xor: - os_ << " ^ "; - break; - case binop::Implies: - os_ << " => "; - break; - case binop::Equiv: - os_ << " <=> "; - break; - } - - bo->second()->accept(*this); - if (!top_level) - os_ << ")"; - } - - void - visit(const unop* uo) - { - // The parser treats F0, F1, G0, G1, X0, and X1 as atomic - // propositions. So make sure we output F(0), G(1), etc. - bool need_parent = !!dynamic_cast(uo->child()); - switch (uo->op()) - { - case unop::Not: - os_ << "!"; - need_parent = false; - break; - } - - top_level_ = false; - if (need_parent) - os_ << "("; - uo->child()->accept(*this); - if (need_parent) - os_ << ")"; - } - - void - visit(const multop* mo) - { - bool top_level = top_level_; - top_level_ = false; - if (!top_level) - os_ << "("; - unsigned max = mo->size(); - mo->nth(0)->accept(*this); - const char* ch = " "; - switch (mo->op()) - { - case multop::Or: - ch = " | "; - break; - case multop::And: - ch = " & "; - break; - } - - for (unsigned n = 1; n < max; ++n) - { - os_ << ch; - mo->nth(n)->accept(*this); - } - if (!top_level) - os_ << ")"; - } - - void - visit(const automatop*) - { - // FIXME ! - os_ << "AP"; - } - - protected: - std::ostream& os_; - bool top_level_; - }; - - } // anonymous - - std::ostream& - to_string(const formula* f, std::ostream& os) - { - to_string_visitor v(os); - f->accept(v); - return os; - } - - std::string - to_string(const formula* f) - { - std::ostringstream os; - to_string(f, os); - return os.str(); - } - } -} diff --git a/src/eltlvisit/tostring.hh b/src/eltlvisit/tostring.hh deleted file mode 100644 index 35dcb603f..000000000 --- a/src/eltlvisit/tostring.hh +++ /dev/null @@ -1,48 +0,0 @@ -// 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. - -#ifndef SPOT_ELTLVISIT_TOSTRING_HH -# define SPOT_ELTLVISIT_TOSTRING_HH - -#include -#include "eltlast/formula.hh" - -namespace spot -{ - namespace eltl - { - /// \addtogroup eltl_io - /// @{ - - /// \brief Output a formula as a (parsable) string. - /// \param f The formula to translate. - /// \param os The stream where it should be output. - std::ostream& to_string(const formula* f, std::ostream& os); - - /// \brief Convert a formula into a (parsable) string. - /// \param f The formula to translate. - std::string to_string(const formula* f); - - /// @} - } -} - -#endif // SPOT_ELTLVISIT_TOSTRING_HH diff --git a/src/evtgbaalgos/tgba2evtgba.cc b/src/evtgbaalgos/tgba2evtgba.cc index 947f19daa..65789a99c 100644 --- a/src/evtgbaalgos/tgba2evtgba.cc +++ b/src/evtgbaalgos/tgba2evtgba.cc @@ -86,10 +86,10 @@ namespace spot bdd low = bdd_low(one); if (low == bddfalse) { - const internal::base_formula* v = + const ltl::formula* v = automata_->get_dict()->var_formula_map[bdd_var(one)]; res->add_transition(name_[in], - v->to_string(), + to_string(v), ss, name_[out]); break; @@ -121,8 +121,8 @@ namespace spot bdd low = bdd_low(one); if (low == bddfalse) { - const ltl::formula* v = dynamic_cast( - automata_->get_dict()->acc_formula_map[bdd_var(one)]); + const ltl::formula* v = + automata_->get_dict()->acc_formula_map[bdd_var(one)]; ss.insert(rsymbol(to_string(v))); break; } diff --git a/src/evtgbatest/ltl2evtgba.cc b/src/evtgbatest/ltl2evtgba.cc index cdf7770de..2777caf74 100644 --- a/src/evtgbatest/ltl2evtgba.cc +++ b/src/evtgbatest/ltl2evtgba.cc @@ -24,6 +24,7 @@ #include #include #include "ltlvisit/destroy.hh" +#include "ltlast/allnodes.hh" #include "ltlparse/public.hh" #include "evtgbaparse/public.hh" #include "evtgbaalgos/save.hh" diff --git a/src/internal/Makefile.am b/src/internal/Makefile.am deleted file mode 100644 index 3aa55fabe..000000000 --- a/src/internal/Makefile.am +++ /dev/null @@ -1,52 +0,0 @@ -## 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. - -AM_CPPFLAGS = -I$(srcdir)/.. -AM_CXXFLAGS = $(WARNING_CXXFLAGS) - -internaldir = $(pkgincludedir)/internal - -internal_HEADERS = \ - baseformula.hh \ - 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 - -noinst_LTLIBRARIES = libinternal.la -libinternal_la_SOURCES = \ - baseformula.cc diff --git a/src/internal/atomic_prop.hxx b/src/internal/atomic_prop.hxx deleted file mode 100644 index 62cbd5aec..000000000 --- a/src/internal/atomic_prop.hxx +++ /dev/null @@ -1,123 +0,0 @@ -// 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/baseformula.hh b/src/internal/baseformula.hh deleted file mode 100644 index 9cfe24dd0..000000000 --- a/src/internal/baseformula.hh +++ /dev/null @@ -1,119 +0,0 @@ -// 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_INTERNAL_BASEFORMULA_HH -# define SPOT_INTERNAL_BASEFORMULA_HH - -# include -# include "misc/hash.hh" - -namespace spot -{ - namespace internal - { - class base_formula - { - public: - /// \brief Output a formula as a (parsable) string. - std::string to_string() const; - - /// Some visitors virtual versions (LTL | ELTL). - virtual base_formula* clone() const = 0; - virtual std::ostream& to_string(std::ostream& os) const = 0; - virtual void destroy() const = 0; - - /// Return a canonic representation of the formula - const std::string& dump() const; - /// Return a hash_key for the formula. - size_t hash() const; - protected: - virtual ~base_formula() {}; - /// \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 base_formula*. - /// \ingroup generic_essentials - /// - /// This is meant to be used as a comparison functor for STL - /// \c map whose key are of type const base_formula*. - /// - /// For instance here is how one could declare - /// a map of \c const::base_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 base_formula* left, const base_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 base_formula*. - /// - /// For instance here is how one could declare - /// a map of \c const::base_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 base_formula* that) const - { - assert(that); - return that->hash(); - } - }; - - } -} - -#endif // SPOT_INTERNAL_BASEFORMULA_HH diff --git a/src/internal/declenv.hh b/src/internal/declenv.hh deleted file mode 100644 index c1c3adc12..000000000 --- a/src/internal/declenv.hh +++ /dev/null @@ -1,69 +0,0 @@ -// 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 deleted file mode 100644 index 5c96f90c3..000000000 --- a/src/internal/declenv.hxx +++ /dev/null @@ -1,83 +0,0 @@ -// 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 deleted file mode 100644 index f7382fbf8..000000000 --- a/src/internal/defaultenv.hh +++ /dev/null @@ -1,59 +0,0 @@ -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 2 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -#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 deleted file mode 100644 index 06c8c436e..000000000 --- a/src/internal/defaultenv.hxx +++ /dev/null @@ -1,68 +0,0 @@ -// 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 deleted file mode 100644 index df1af8492..000000000 --- a/src/internal/environment.hh +++ /dev/null @@ -1,72 +0,0 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 2 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -#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 deleted file mode 100644 index bd0a8d9ef..000000000 --- a/src/internal/formula.hh +++ /dev/null @@ -1,84 +0,0 @@ -// 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/formula.hh -/// \brief Generic formula interface -#ifndef SPOT_INTERNAL_FORMULA_HH -# define SPOT_INTERNAL_FORMULA_HH - -# include "predecl.hh" -# include "baseformula.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 base_formula - { - public: - typedef typename T::visitor visitor; - typedef typename T::const_visitor const_visitor; - - virtual base_formula* clone() const; - virtual std::ostream& to_string(std::ostream& os) const; - virtual void destroy() const; - - /// 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); - 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_(); - }; - } -} - -# include "formula.hxx" - -#endif // SPOT_INTERNAL_FORMULA_HH diff --git a/src/internal/formula.hxx b/src/internal/formula.hxx deleted file mode 100644 index c0fcf0def..000000000 --- a/src/internal/formula.hxx +++ /dev/null @@ -1,92 +0,0 @@ -// 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 - base_formula* - formula::clone() const - { - return T::clone_(this); - } - - template - std::ostream& - formula::to_string(std::ostream& os) const - { - return T::to_string_(this, os); - } - - template - void - formula::destroy() const - { - T::destroy_(this); - } - } -} - -#endif // SPOT_INTERNAL_FORMULA_HXX diff --git a/src/ltlast/Makefile.am b/src/ltlast/Makefile.am index 5e595a9ac..b7d3d6fa1 100644 --- a/src/ltlast/Makefile.am +++ b/src/ltlast/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2003, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +## Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. ## @@ -19,6 +19,29 @@ ## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA ## 02111-1307, USA. +AM_CPPFLAGS = -I$(srcdir)/.. +AM_CXXFLAGS = $(WARNING_CXXFLAGS) + ltlastdir = $(pkgincludedir)/ltlast -ltlast_HEADERS = formula.hh +ltlast_HEADERS = \ + allnodes.hh \ + atomic_prop.hh \ + binop.hh \ + constant.hh \ + formula.hh \ + multop.hh \ + predecl.hh \ + refformula.hh \ + unop.hh \ + visitor.hh + +noinst_LTLIBRARIES = libltlast.la +libltlast_la_SOURCES = \ + atomic_prop.cc \ + binop.cc \ + constant.cc \ + formula.cc \ + multop.cc \ + refformula.cc \ + unop.cc diff --git a/src/eltlvisit/destroy.cc b/src/ltlast/allnodes.hh similarity index 62% rename from src/eltlvisit/destroy.cc rename to src/ltlast/allnodes.hh index b0c9706d0..9b5664182 100644 --- a/src/eltlvisit/destroy.cc +++ b/src/ltlast/allnodes.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -19,24 +19,19 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include "eltlvisit/destroy.hh" -#include "eltlvisit/clone.hh" +/// \file ltlast/allnodes.hh +/// \brief Define all LTL node types. +/// +/// This file is usually needed when \b defining a visitor. +/// Prefer ltlast/predecl.hh when only \b declaring methods and functions +/// over LTL nodes. +#ifndef SPOT_LTLAST_ALLNODES_HH +# define SPOT_LTLAST_ALLNODES_HH -namespace spot -{ - namespace eltl - { - void - destroy_visitor::doit_default(formula* c) - { - formula::unref(c); - } +# include "binop.hh" +# include "unop.hh" +# include "multop.hh" +# include "atomic_prop.hh" +# include "constant.hh" - void - destroy(const formula* f) - { - destroy_visitor v; - const_cast(f)->accept(v); - } - } -} +#endif // SPOT_LTLAST_ALLNODES_HH diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc new file mode 100644 index 000000000..8fd0d2384 --- /dev/null +++ b/src/ltlast/atomic_prop.cc @@ -0,0 +1,108 @@ +// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "atomic_prop.hh" +#include "visitor.hh" +#include +#include + +namespace spot +{ + namespace ltl + { + + atomic_prop::atomic_prop(const std::string& name, environment& env) + : name_(name), env_(&env) + { + dump_ = "AP(" + name + ")"; + set_key_(); + } + + atomic_prop::~atomic_prop() + { + // Get this instance out of the instance map. + pair p(name(), &env()); + map::iterator i = instances.find(p); + assert (i != instances.end()); + instances.erase(i); + } + + void + atomic_prop::accept(visitor& v) + { + v.visit(this); + } + + void + atomic_prop::accept(const_visitor& v) const + { + v.visit(this); + } + + const std::string& + atomic_prop::name() const + { + return name_; + } + + environment& + atomic_prop::env() const + { + return *env_; + } + + atomic_prop::map atomic_prop::instances; + + atomic_prop* + atomic_prop::instance(const std::string& name, environment& env) + { + pair p(name, &env); + map::iterator i = instances.find(p); + if (i != instances.end()) + { + return static_cast(i->second->ref()); + } + atomic_prop* ap = new atomic_prop(name, env); + instances[p] = ap; + return static_cast(ap->ref()); + } + + unsigned + atomic_prop::instance_count() + { + return instances.size(); + } + + std::ostream& + atomic_prop::dump_instances(std::ostream& os) + { + + for (map::iterator i = instances.begin(); i != instances.end(); ++i) + { + os << i->second << " = " << i->second->ref_count_() + << " * atomic_prop(" << i->first.first << ", " + << i->first.second->name() << ")" << std::endl; + } + return os; + } + + } +} diff --git a/src/internal/atomic_prop.hh b/src/ltlast/atomic_prop.hh similarity index 62% rename from src/internal/atomic_prop.hh rename to src/ltlast/atomic_prop.hh index f4310f544..984c37619 100644 --- a/src/internal/atomic_prop.hh +++ b/src/ltlast/atomic_prop.hh @@ -1,6 +1,6 @@ -// 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. +// 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. // @@ -19,37 +19,30 @@ // 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 +/// \file ltlast/atomic_prop.hh +/// \brief LTL atomic propositions +#ifndef SPOT_LTLAST_ATOMIC_PROP_HH +# define SPOT_LTLAST_ATOMIC_PROP_HH #include #include #include -#include -#include #include "refformula.hh" -#include "environment.hh" +#include "ltlenv/environment.hh" namespace spot { - namespace internal + namespace ltl { /// \brief Atomic propositions. - /// \ingroup generic_ast - template - class atomic_prop : public ref_formula + /// \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); - - typedef typename T::visitor visitor; - typedef typename T::const_visitor const_visitor; + static atomic_prop* instance(const std::string& name, environment& env); virtual void accept(visitor& visitor); virtual void accept(const_visitor& visitor) const; @@ -57,7 +50,7 @@ namespace spot /// Get the name of the atomic proposition. const std::string& name() const; /// Get the environment of the atomic proposition. - environment& env() const; + environment& env() const; /// Number of instantiated atomic propositions. For debugging. static unsigned instance_count(); @@ -65,21 +58,19 @@ namespace spot static std::ostream& dump_instances(std::ostream& os); protected: - atomic_prop(const std::string& name, environment& env); + atomic_prop(const std::string& name, environment& env); virtual ~atomic_prop(); - typedef std::pair*> pair; - typedef std::map*> map; + typedef std::pair pair; + typedef std::map map; static map instances; private: std::string name_; - environment* env_; + environment* env_; }; } } -# include "atomic_prop.hxx" - -#endif // SPOT_INTERNAL_ATOMICPROP_HH +#endif // SPOT_LTLAST_ATOMICPROP_HH diff --git a/src/internal/binop.hxx b/src/ltlast/binop.cc similarity index 53% rename from src/internal/binop.hxx rename to src/ltlast/binop.cc index 1080218af..65dfad1e3 100644 --- a/src/internal/binop.hxx +++ b/src/ltlast/binop.cc @@ -19,138 +19,135 @@ // 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 +#include #include "binop.hh" +#include "visitor.hh" namespace spot { - namespace internal + namespace ltl { - template - binop::binop(type op, formula* first, formula* second) + 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_(); + dump_ = "binop("; + dump_ += op_name(); + dump_ += ", " + first->dump() + ", " + second->dump() + ")"; + set_key_(); } - template - binop::~binop() + 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); + map::iterator i = instances.find(p); assert (i != instances.end()); instances.erase(i); } - template void - binop::accept(visitor& v) + binop::accept(visitor& v) { v.visit(this); } - template void - binop::accept(const_visitor& v) const + binop::accept(const_visitor& v) const { v.visit(this); } - template - const formula* - binop::first() const + const formula* + binop::first() const { return first_; } - template - formula* - binop::first() + formula* + binop::first() { return first_; } - template - const formula* - binop::second() const + const formula* + binop::second() const { return second_; } - template - formula* - binop::second() + formula* + binop::second() { return second_; } - template - typename binop::type - binop::op() const + binop::type + binop::op() const { return op_; } - template const char* - binop::op_name() const + binop::op_name() const { - return T::binop_name(op_); + 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; } - template - typename binop::map binop::instances; + binop::map binop::instances; - template - binop* - binop::instance(type op, formula* first, formula* second) + 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: + { + case Xor: + case Equiv: if (second < first) std::swap(first, second); break; - case T::Implies: - // case U: - // case R: - // // Non associative operators. - default: + case Implies: + case U: + case R: + // Non associative operators. break; - } + } pairf pf(first, second); pair p(op, pf); - typename map::iterator i = instances.find(p); + map::iterator i = instances.find(p); if (i != instances.end()) { - return static_cast*>(i->second->ref()); + return static_cast(i->second->ref()); } - binop* ap = new binop(op, first, second); + binop* ap = new binop(op, first, second); instances[p] = ap; - return static_cast*>(ap->ref()); + return static_cast(ap->ref()); } - template unsigned - binop::instance_count() + binop::instance_count() { return instances.size(); } } } - -#endif // SPOT_INTERNAL_BINOP_HXX diff --git a/src/internal/binop.hh b/src/ltlast/binop.hh similarity index 66% rename from src/internal/binop.hh rename to src/ltlast/binop.hh index c13648c76..6bf9fec5d 100644 --- a/src/internal/binop.hh +++ b/src/ltlast/binop.hh @@ -19,54 +19,48 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -/// \file internal/binop.hh -/// \brief Generic binary operators +/// \file ltlast/binop.hh +/// \brief LTL binary operators /// /// This does not include \c AND and \c OR operators. These are -/// considered to be multi-operand operators (see spot::internal::multop). -#ifndef SPOT_INTERNAL_BINOP_HH -# define SPOT_INTERNAL_BINOP_HH +/// considered to be multi-operand operators (see spot::ltl::multop). +#ifndef SPOT_LTLAST_BINOP_HH +# define SPOT_LTLAST_BINOP_HH #include #include "refformula.hh" -#include -#include namespace spot { - namespace internal + namespace ltl { - /// \brief Generic binary operator. - /// \ingroup generic_ast - template - class binop : public ref_formula + /// \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. - typedef typename T::binop type; + 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); - - typedef typename T::visitor visitor; - typedef typename T::const_visitor const_visitor; + 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; + const formula* first() const; /// Get the first operand. - formula* first(); + formula* first(); /// Get the second operand. - const formula* second() const; + const formula* second() const; /// Get the second operand. - formula* second(); + formula* second(); /// Get the type of this operator. type op() const; @@ -77,23 +71,21 @@ namespace spot static unsigned instance_count(); protected: - typedef std::pair*, formula*> pairf; + typedef std::pair pairf; typedef std::pair pair; - typedef std::map*> map; + typedef std::map map; static map instances; - binop(type op, formula* first, formula* second); + binop(type op, formula* first, formula* second); virtual ~binop(); private: type op_; - formula* first_; - formula* second_; + formula* first_; + formula* second_; }; } } -# include "binop.hxx" - -#endif // SPOT_INTERNAL_BINOP_HH +#endif // SPOT_LTLAST_BINOP_HH diff --git a/src/internal/constant.hxx b/src/ltlast/constant.cc similarity index 54% rename from src/internal/constant.hxx rename to src/ltlast/constant.cc index dec0fd430..50573a3cd 100644 --- a/src/internal/constant.hxx +++ b/src/ltlast/constant.cc @@ -1,6 +1,6 @@ -// 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. +// 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. // @@ -19,65 +19,56 @@ // 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" +#include "visitor.hh" +#include namespace spot { - namespace internal + namespace ltl { - template - constant::constant(type val) + constant::constant(type val) : val_(val) { switch (val) { case True: - this->dump_ = "constant(1)"; - this->set_key_(); + dump_ = "constant(1)"; + set_key_(); return; case False: - this->dump_ = "constant(0)"; - this->set_key_(); + dump_ = "constant(0)"; + set_key_(); return; } // Unreachable code. assert(0); } - template - constant::~constant() + constant::~constant() { } - template void - constant::accept(visitor& v) + constant::accept(visitor& v) { v.visit(this); } - template void - constant::accept(const_visitor& v) const + constant::accept(const_visitor& v) const { v.visit(this); } - template - typename constant::type - constant::val() const + constant::type + constant::val() const { return val_; } - template const char* - constant::val_name() const + constant::val_name() const { switch (val_) { @@ -91,22 +82,18 @@ namespace spot return 0; } - template - constant* - constant::false_instance() + constant* + constant::false_instance() { - static constant f(constant::False); + static constant f(constant::False); return &f; } - template - constant* - constant::true_instance() + constant* + constant::true_instance() { - static constant t(constant::True); + static constant t(constant::True); return &t; } } } - -#endif // SPOT_INTERNAL_CONSTANT_HXX diff --git a/src/internal/constant.hh b/src/ltlast/constant.hh similarity index 72% rename from src/internal/constant.hh rename to src/ltlast/constant.hh index e02458037..46b15e698 100644 --- a/src/internal/constant.hh +++ b/src/ltlast/constant.hh @@ -19,30 +19,24 @@ // 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 +/// \file ltlast/constant.hh +/// \brief LTL constants +#ifndef SPOT_LTLAST_CONSTANT_HH +# define SPOT_LTLAST_CONSTANT_HH -#include #include "formula.hh" namespace spot { - namespace internal + namespace ltl { /// \brief A constant (True or False) - /// \ingroup generic_ast - template - class constant : public formula + /// \ingroup ltl_ast + 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; @@ -51,9 +45,9 @@ namespace spot /// Return the value of the constant as a string. const char* val_name() const; - /// Get the sole instance of spot::internal::constant::constant(1). + /// Get the sole instance of spot::ltl::constant::constant(True). static constant* true_instance(); - /// Get the sole instance of spot::internal::constant::constant(0). + /// Get the sole instance of spot::ltl::constant::constant(False). static constant* false_instance(); protected: @@ -67,6 +61,4 @@ namespace spot } } -# include "constant.hxx" - -#endif // SPOT_INTERNAL_CONSTANT_HH +#endif // SPOT_LTLAST_CONSTANT_HH diff --git a/src/internal/baseformula.cc b/src/ltlast/formula.cc similarity index 61% rename from src/internal/baseformula.cc rename to src/ltlast/formula.cc index 0b27b261b..e194c2c72 100644 --- a/src/internal/baseformula.cc +++ b/src/ltlast/formula.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// 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. @@ -19,38 +19,56 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include -#include "baseformula.hh" +#include "formula.hh" +#include "misc/hash.hh" namespace spot { - namespace internal + namespace ltl { - std::string - base_formula::to_string() const + formula* + formula::ref() { - std::ostringstream os; - to_string(os); - return os.str(); + ref_(); + return this; + } + + formula::~formula() + { + } + + void + formula::unref(formula* f) + { + if (f->unref_()) + delete f; + } + + void + formula::ref_() + { + // Not reference counted by default. + } + + bool + formula::unref_() + { + // Not reference counted by default. + return false; } const std::string& - base_formula::dump() const + formula::dump() const { return dump_; } - size_t - base_formula::hash() const - { - return hash_key_; - } - void - base_formula::set_key_() + formula::set_key_() { string_hash sh; hash_key_ = sh(dump_); } + } } diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index f631e9e31..749db27bc 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -20,16 +20,13 @@ // 02111-1307, USA. /// \file ltlast/formula.hh -/// \brief LTL formula, AST and visitor interface +/// \brief LTL formula interface #ifndef SPOT_LTLAST_FORMULA_HH # define SPOT_LTLAST_FORMULA_HH -# include "internal/formula.hh" -# include "internal/atomic_prop.hh" -# include "internal/constant.hh" -# include "internal/unop.hh" -# include "internal/binop.hh" -# include "internal/multop.hh" +#include +#include +#include "predecl.hh" namespace spot { @@ -64,9 +61,6 @@ namespace spot /// \addtogroup ltl_misc Miscellaneous algorithms for LTL formulae /// \ingroup ltl_algorithm - struct ltl_t; - struct visitor; - struct const_visitor; /// \brief An LTL formula. /// \ingroup ltl_essential @@ -74,136 +68,114 @@ namespace spot /// /// The only way you can work with a formula is to /// build a spot::ltl::visitor or spot::ltl::const_visitor. - typedef spot::internal::formula formula; - - /// Forward declarations - formula* clone(const formula* f); - std::ostream& to_string(const formula* f, std::ostream& os); - void destroy(const formula* f); - - struct ltl_t + class formula { - typedef spot::ltl::visitor visitor; - typedef spot::ltl::const_visitor const_visitor; + public: + /// Entry point for vspot::ltl::visitor instances. + virtual void accept(visitor& v) = 0; + /// Entry point for vspot::ltl::const_visitor instances. + virtual void accept(const_visitor& v) const = 0; - static formula* clone_(const formula* f) + /// \brief clone this node + /// + /// This increments the reference counter of this node (if one is + /// used). You should almost never use this method directly as + /// it doesn't touch the children. If you want to clone a + /// whole formula, use spot::ltl::clone() instead. + formula* ref(); + /// \brief release this node + /// + /// This decrements the reference counter of this node (if one is + /// used) and can free the object. You should almost never use + /// this method directly as it doesn't touch the children. If you + /// want to release a whole formula, use spot::ltl::destroy() instead. + static void unref(formula* f); + + /// Return a canonic representation of the formula + const std::string& dump() const; + + /// Return a hash_key for the formula. + size_t + hash() const { - return clone(f); + return hash_key_; } + protected: + virtual ~formula(); - static std::ostream& to_string_(const formula* f, std::ostream& os) - { - return to_string(f, os); - } + /// \brief increment reference counter if any + virtual void ref_(); + /// \brief decrement reference counter if any, return true when + /// the instance must be deleted (usually when the counter hits 0). + virtual bool unref_(); - static void destroy_(const formula* f) - { - destroy(f); - } + /// \brief Compute key_ from dump_. + /// + /// Should be called once in each object, after dump_ has been set. + void set_key_(); + /// The canonic representation of the formula + std::string dump_; + /// \brief The hash key of this formula. + /// + /// Initialized by set_key_(). + size_t hash_key_; + }; - enum binop { Xor, Implies, Equiv, U, R }; - const char* binop_name(binop op) const + /// \brief Strict Weak Ordering for 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 { - switch (op) - { - case Xor: - return "Xor"; - case Implies: - return "Implies"; - case Equiv: - return "Equiv"; - case U: - return "U"; - case R: - return "R"; - } - // Unreachable code. - assert(0); - return 0; - } - - enum unop { Not, X, F, G }; - const char* unop_name(unop op) const - { - switch (op) - { - case Not: - return "Not"; - case X: - return "X"; - case F: - return "F"; - case G: - return "G"; - } - // Unreachable code. - assert(0); - return 0; + assert(left); + assert(right); + size_t l = left->hash(); + size_t r = right->hash(); + if (1 != r) + return l < r; + return left->dump() < right->dump(); } }; - typedef spot::internal::formula_ptr_less_than formula_ptr_less_than; - typedef spot::internal::formula_ptr_hash formula_ptr_hash; - - /// \brief Atomic propositions. - /// \ingroup ltl_ast - typedef spot::internal::atomic_prop atomic_prop; - - /// \brief A constant (True or False) - /// \ingroup ltl_ast - typedef spot::internal::constant constant; - - /// \brief Unary operators. - /// \ingroup ltl_ast - typedef spot::internal::unop unop; - - /// \brief Binary operator. - /// \ingroup ltl_ast - typedef spot::internal::binop binop; - - /// \brief Multi-operand operators. - /// \ingroup ltl_ast + /// \brief Hash Function for const formula*. + /// \ingroup ltl_essentials + /// \ingroup hash_funcs /// - /// These operators are considered commutative and associative. - typedef spot::internal::multop multop; - - - /// \brief Formula visitor that can modify the formula. - /// \ingroup ltl_essential + /// This is meant to be used as a hash functor for + /// Sgi's \c hash_map whose key are of type const formula*. /// - /// Writing visitors is the prefered way - /// to traverse a formula, since it doesn't - /// involve any cast. - /// - /// If you do not need to modify the visited formula, inherit from - /// spot::ltl:const_visitor instead. - struct visitor + /// For instance here is how one could declare + /// a map of \c const::formula*. + /// \code + /// // Remember how many times each formula has been seen. + /// Sgi::hash_map seen; + /// \endcode + struct formula_ptr_hash: + public std::unary_function { - virtual ~visitor() {} - virtual void visit(atomic_prop* node) = 0; - virtual void visit(constant* node) = 0; - virtual void visit(binop* node) = 0; - virtual void visit(unop* node) = 0; - virtual void visit(multop* node) = 0; + size_t + operator()(const formula* that) const + { + assert(that); + return that->hash(); + } }; - /// \brief Formula visitor that cannot modify the formula. - /// - /// Writing visitors is the prefered way - /// to traverse a formula, since it doesn't - /// involve any cast. - /// - /// If you want to modify the visited formula, inherit from - /// spot::ltl:visitor instead. - struct const_visitor - { - virtual ~const_visitor() {} - virtual void visit(const atomic_prop* node) = 0; - virtual void visit(const constant* node) = 0; - virtual void visit(const binop* node) = 0; - virtual void visit(const unop* node) = 0; - virtual void visit(const multop* node) = 0; - }; + } } diff --git a/src/internal/multop.hxx b/src/ltlast/multop.cc similarity index 52% rename from src/internal/multop.hxx rename to src/ltlast/multop.cc index 479e51dad..1e00d07cb 100644 --- a/src/internal/multop.hxx +++ b/src/ltlast/multop.cc @@ -1,6 +1,6 @@ -// 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. +// 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. // @@ -19,89 +19,81 @@ // 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 +#include +#include #include "multop.hh" +#include "constant.hh" +#include "visitor.hh" +#include "ltlvisit/destroy.hh" namespace spot { - namespace internal + namespace ltl { - template - multop::multop(type op, vec* v) + multop::multop(type op, vec* v) : op_(op), children_(v) { - this->dump_ = "multop("; - this->dump_ += op_name(); + dump_ = "multop("; + dump_ += op_name(); unsigned max = v->size(); for (unsigned n = 0; n < max; ++n) { - this->dump_ += ", " + (*v)[n]->dump(); + dump_ += ", " + (*v)[n]->dump(); } - this->dump_ += ")"; - this->set_key_(); + dump_ += ")"; + set_key_(); } - template - multop::~multop() + multop::~multop() { // Get this instance out of the instance map. pair p(op(), children_); - typename map::iterator i = instances.find(p); + map::iterator i = instances.find(p); assert (i != instances.end()); instances.erase(i); delete children_; } - template void - multop::accept(visitor& v) + multop::accept(visitor& v) { v.visit(this); } - template void - multop::accept(const_visitor& v) const + multop::accept(const_visitor& v) const { v.visit(this); } - template unsigned - multop::size() const + multop::size() const { return children_->size(); } - template - const formula* - multop::nth(unsigned n) const + const formula* + multop::nth(unsigned n) const { return (*children_)[n]; } - template - formula* - multop::nth(unsigned n) + formula* + multop::nth(unsigned n) { return (*children_)[n]; } - template - typename multop::type - multop::op() const + multop::type + multop::op() const { return op_; } - template const char* - multop::op_name() const + multop::op_name() const { switch (op_) { @@ -115,22 +107,20 @@ namespace spot return 0; } - template - typename multop::map multop::instances; + multop::map multop::instances; - template - formula* - multop::instance(type op, vec* v) + formula* + multop::instance(type op, vec* v) { pair p(op, v); // Inline children of same kind. { vec inlined; - typename vec::iterator i = v->begin(); + vec::iterator i = v->begin(); while (i != v->end()) { - multop* p = dynamic_cast*>(*i); + multop* p = dynamic_cast(*i); if (p && p->op() == op) { unsigned ps = p->size(); @@ -139,7 +129,7 @@ namespace spot // 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); + formula::unref(*i); i = v->erase(i); } else @@ -155,8 +145,8 @@ namespace spot // 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(); + formula* last = 0; + vec::iterator i = v->begin(); while (i != v->end()) { if (*i == last) @@ -171,42 +161,41 @@ namespace spot } } - typename vec::size_type s = v->size(); + vec::size_type s = v->size(); if (s == 0) { delete v; switch (op) { case And: - return constant::true_instance(); + return constant::true_instance(); case Or: - return constant::false_instance(); + return constant::false_instance(); } /* Unreachable code. */ assert(0); } else if (s == 1) { - formula* res = (*v)[0]; + formula* res = (*v)[0]; delete v; return res; } - typename map::iterator i = instances.find(p); + map::iterator i = instances.find(p); if (i != instances.end()) { delete v; - return static_cast*>(i->second->ref()); + return static_cast(i->second->ref()); } - multop* ap = new multop(op, v); + multop* ap = new multop(op, v); instances[p] = ap; - return static_cast*>(ap->ref()); + return static_cast(ap->ref()); } - template - formula* - multop::instance(type op, formula* first, formula* second) + formula* + multop::instance(type op, formula* first, formula* second) { vec* v = new vec; v->push_back(first); @@ -214,39 +203,10 @@ namespace spot return instance(op, v); } - template unsigned - multop::instance_count() + 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/multop.hh b/src/ltlast/multop.hh similarity index 58% rename from src/internal/multop.hh rename to src/ltlast/multop.hh index aa8a62961..7157b503b 100644 --- a/src/internal/multop.hh +++ b/src/ltlast/multop.hh @@ -19,68 +19,59 @@ // 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 +/// \file ltlast/multop.hh +/// \brief LTL multi-operand operators +#ifndef SPOT_LTLAST_MULTOP_HH +# define SPOT_LTLAST_MULTOP_HH #include #include -#include -#include -#include #include "refformula.hh" -#include "constant.hh" namespace spot { - namespace internal + namespace ltl { /// \brief Multi-operand operators. - /// \ingroup generic_ast + /// \ingroup ltl_ast /// /// These operators are considered commutative and associative. - template - class multop : public ref_formula + class multop : public ref_formula { public: enum type { Or, And }; /// List of formulae. - typedef std::vector*> vec; + typedef std::vector vec; - /// \brief Build a spot::internal::multop with two children. + /// \brief Build a spot::ltl::multop with two children. /// - /// If one of the children itself is a spot::internal::multop + /// 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 internal::multop. + /// n-ary ltl::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); + /// 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::internal::multop with many children. + /// \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::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. + /// 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 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; + /// 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; @@ -90,11 +81,11 @@ namespace spot /// \brief Get the nth children. /// /// Starting with \a n = 0. - const formula* nth(unsigned n) const; + const formula* nth(unsigned n) const; /// \brief Get the nth children. /// /// Starting with \a n = 0. - formula* nth(unsigned n); + formula* nth(unsigned n); /// Get the type of this operator. type op() const; @@ -106,7 +97,7 @@ namespace spot protected: typedef std::pair pair; - /// Comparison functor used internally by internal::multop. + /// Comparison functor used internally by ltl::multop. struct paircmp { bool @@ -117,7 +108,7 @@ namespace spot return *p1.second < *p2.second; } }; - typedef std::map*, paircmp> map; + typedef std::map map; static map instances; multop(type op, vec* v); @@ -126,13 +117,9 @@ namespace spot private: type op_; vec* children_; - - static void destroy(formula* c); }; } } -# include "multop.hxx" - -#endif // SPOT_INTERNAL_MULTOP_HH +#endif // SPOT_LTLAST_MULTOP_HH diff --git a/src/internal/predecl.hh b/src/ltlast/predecl.hh similarity index 76% rename from src/internal/predecl.hh rename to src/ltlast/predecl.hh index 80a4817f7..121c9ef5d 100644 --- a/src/internal/predecl.hh +++ b/src/ltlast/predecl.hh @@ -19,31 +19,30 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -/// \file internal/predecl.hh -/// \brief Predeclare all node types. +/// \file ltlast/predecl.hh +/// \brief Predeclare all LTL 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 +/// over LTL nodes. +/// Use ltlast/allnodes.hh or an individual header when the definition of +/// the node is actually needed. +#ifndef SPOT_LTLAST_PREDECL_HH +# define SPOT_LTLAST_PREDECL_HH namespace spot { - namespace internal + namespace ltl { - template + struct visitor; + struct const_visitor; + struct atomic_prop; - template struct unop; - template struct constant; - template struct binop; - template struct formula; - template struct multop; } } -#endif // SPOT_INTERNAL_PREDECL_HH +#endif // SPOT_LTLAST_PREDECL_HH diff --git a/src/internal/refformula.hxx b/src/ltlast/refformula.cc similarity index 70% rename from src/internal/refformula.hxx rename to src/ltlast/refformula.cc index 72cd269a0..06ad2dad7 100644 --- a/src/internal/refformula.hxx +++ b/src/ltlast/refformula.cc @@ -19,51 +19,40 @@ // 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" +#include namespace spot { - namespace internal + namespace ltl { - template - ref_formula::ref_formula() + ref_formula::ref_formula() : ref_counter_(0) { } - template - ref_formula::~ref_formula() + ref_formula::~ref_formula() { } - template void - ref_formula::ref_() + ref_formula::ref_() { ++ref_counter_; } - template bool - ref_formula::unref_() + ref_formula::unref_() { assert(ref_counter_ > 0); return !--ref_counter_; } - template unsigned - ref_formula::ref_count_() + ref_formula::ref_count_() { return ref_counter_; } } } - -#endif // SPOT_INTERNAL_REFFORMULA_HXX diff --git a/src/internal/refformula.hh b/src/ltlast/refformula.hh similarity index 75% rename from src/internal/refformula.hh rename to src/ltlast/refformula.hh index 3673b0b75..b086fdd84 100644 --- a/src/internal/refformula.hh +++ b/src/ltlast/refformula.hh @@ -19,23 +19,21 @@ // 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 +/// \file ltlast/refformula.hh +/// \brief Reference-counted LTL formulae +#ifndef SPOT_LTLAST_REFFORMULA_HH +# define SPOT_LTLAST_REFFORMULA_HH #include "formula.hh" -#include namespace spot { - namespace internal + namespace ltl { - /// \brief A reference-counted generic formula. - /// \ingroup generic_ast - template - class ref_formula : public formula + /// \brief A reference-counted LTL formula. + /// \ingroup ltl_ast + class ref_formula : public formula { protected: virtual ~ref_formula(); @@ -44,7 +42,6 @@ namespace spot bool unref_(); /// Number of references to this formula. unsigned ref_count_(); - private: unsigned ref_counter_; }; @@ -52,6 +49,4 @@ namespace spot } } -# include "refformula.hxx" - -#endif // SPOT_INTERNAL_REFFORMULA_HH +#endif // SPOT_LTLAST_REFFORMULA_HH diff --git a/src/internal/unop.hxx b/src/ltlast/unop.cc similarity index 53% rename from src/internal/unop.hxx rename to src/ltlast/unop.cc index 26a4178a3..f4cd9f2a4 100644 --- a/src/internal/unop.hxx +++ b/src/ltlast/unop.cc @@ -19,104 +19,101 @@ // 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" +#include "visitor.hh" +#include namespace spot { - namespace internal + namespace ltl { - template - unop::unop(type op, formula* child) + unop::unop(type op, formula* child) : op_(op), child_(child) { - this->dump_ = "unop("; - this->dump_ += op_name(); - this->dump_ += ", " + child->dump() + ")"; - this->set_key_(); + dump_ = "unop("; + dump_ += op_name(); + dump_ += ", " + child->dump() + ")"; + set_key_(); } - template - unop::~unop() + unop::~unop() { // Get this instance out of the instance map. pair p(op(), child()); - typename map::iterator i = instances.find(p); + map::iterator i = instances.find(p); assert (i != instances.end()); instances.erase(i); } - template void - unop::accept(visitor& v) + unop::accept(visitor& v) { v.visit(this); } - template void - unop::accept(const_visitor& v) const + unop::accept(const_visitor& v) const { v.visit(this); } - template - const formula* - unop::child() const + const formula* + unop::child() const { return child_; } - template - formula* - unop::child() + formula* + unop::child() { return child_; } - template - typename unop::type - unop::op() const + unop::type + unop::op() const { return op_; } - template const char* - unop::op_name() const + unop::op_name() const { - return T::unop_name(op_); + switch (op_) + { + case Not: + return "Not"; + case X: + return "X"; + case F: + return "F"; + case G: + return "G"; + } + // Unreachable code. + assert(0); + return 0; } - template - typename unop::map unop::instances; + unop::map unop::instances; - template - unop* - unop::instance(type op, formula* child) + unop* + unop::instance(type op, formula* child) { pair p(op, child); - typename map::iterator i = instances.find(p); + map::iterator i = instances.find(p); if (i != instances.end()) { - return static_cast*>(i->second->ref()); + return static_cast(i->second->ref()); } - unop* ap = new unop(op, child); + unop* ap = new unop(op, child); instances[p] = ap; - return static_cast*>(ap->ref()); + return static_cast(ap->ref()); } - template unsigned - unop::instance_count() + unop::instance_count() { return instances.size(); } } } - -#endif // SPOT_INTERNAL_UNOP_HXX diff --git a/src/internal/unop.hh b/src/ltlast/unop.hh similarity index 68% rename from src/internal/unop.hh rename to src/ltlast/unop.hh index 46312b15a..487ecf034 100644 --- a/src/internal/unop.hh +++ b/src/ltlast/unop.hh @@ -19,42 +19,37 @@ // 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 +/// \file ltlast/unop.hh +/// \brief LTL unary operators +#ifndef SPOT_LTLAST_UNOP_HH +# define SPOT_LTLAST_UNOP_HH #include #include "refformula.hh" -#include namespace spot { - namespace internal + namespace ltl { - /// \brief Generic unary operators. - /// \ingroup generic_ast - template - class unop : public ref_formula + /// \brief Unary operators. + /// \ingroup ltl_ast + class unop : public ref_formula { public: - typedef typename T::unop type; + 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); - - typedef typename T::visitor visitor; - typedef typename T::const_visitor const_visitor; + 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; + const formula* child() const; /// Get the sole operand of this operator. - formula* child(); + formula* child(); /// Get the type of this operator. type op() const; @@ -65,21 +60,19 @@ namespace spot static unsigned instance_count(); protected: - typedef std::pair*> pair; - typedef std::map*> map; + typedef std::pair pair; + typedef std::map map; static map instances; - unop(type op, formula* child); + unop(type op, formula* child); virtual ~unop(); private: type op_; - formula* child_; + formula* child_; }; } } -# include "unop.hxx" - -#endif // SPOT_INTERNAL_UNOP_HH +#endif // SPOT_LTLAST_UNOP_HH diff --git a/src/ltlast/visitor.hh b/src/ltlast/visitor.hh new file mode 100644 index 000000000..a6cfb933b --- /dev/null +++ b/src/ltlast/visitor.hh @@ -0,0 +1,74 @@ +// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +/// \file ltlast/visitor.hh +/// \brief LTL visitor interface +#ifndef SPOT_LTLAST_VISITOR_HH +# define SPOT_LTLAST_VISITOR_HH + +#include "predecl.hh" + +namespace spot +{ + namespace ltl + { + /// \brief Formula visitor that can modify the formula. + /// \ingroup ltl_essential + /// + /// Writing visitors is the prefered way + /// to traverse a formula, since it doesn't + /// involve any cast. + /// + /// If you do not need to modify the visited formula, inherit from + /// spot::ltl:const_visitor instead. + struct visitor + { + virtual ~visitor() {} + virtual void visit(atomic_prop* node) = 0; + virtual void visit(constant* node) = 0; + virtual void visit(binop* node) = 0; + virtual void visit(unop* node) = 0; + virtual void visit(multop* node) = 0; + }; + + /// \brief Formula visitor that cannot modify the formula. + /// + /// Writing visitors is the prefered way + /// to traverse a formula, since it doesn't + /// involve any cast. + /// + /// If you want to modify the visited formula, inherit from + /// spot::ltl:visitor instead. + struct const_visitor + { + virtual ~const_visitor() {} + virtual void visit(const atomic_prop* node) = 0; + virtual void visit(const constant* node) = 0; + virtual void visit(const binop* node) = 0; + virtual void visit(const unop* node) = 0; + virtual void visit(const multop* node) = 0; + }; + + + } +} + +#endif // SPOT_LTLAST_VISITOR_HH diff --git a/src/ltlenv/Makefile.am b/src/ltlenv/Makefile.am index 9ab1e6926..c3dbf107f 100644 --- a/src/ltlenv/Makefile.am +++ b/src/ltlenv/Makefile.am @@ -19,9 +19,17 @@ ## 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 = \ - defaultenv.hh \ declenv.hh \ + defaultenv.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 188d37c6c..27ff98e01 100644 --- a/src/ltlenv/declenv.hh +++ b/src/ltlenv/declenv.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -23,7 +23,10 @@ # define SPOT_LTLENV_DECLENV_HH # include "environment.hh" -# include "internal/declenv.hh" +# include +# include +# include "ltlvisit/destroy.hh" +# include "ltlast/atomic_prop.hh" namespace spot { @@ -35,9 +38,29 @@ namespace spot /// /// This environment recognizes all atomic propositions /// that have been previously declared. It will reject other. - typedef spot::internal::declarative_environment - declarative_environment; + 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 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 74ede5cd3..abd046270 100644 --- a/src/ltlenv/defaultenv.hh +++ b/src/ltlenv/defaultenv.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -23,7 +23,6 @@ # define SPOT_LTLENV_DEFAULTENV_HH # include "environment.hh" -# include "internal/defaultenv.hh" namespace spot { @@ -37,7 +36,18 @@ namespace spot /// /// This is a singleton. Use default_environment::instance() /// to obtain the instance. - typedef spot::internal::default_environment default_environment; + 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(); + }; } } diff --git a/src/ltlenv/environment.hh b/src/ltlenv/environment.hh index 02c8d9810..6dd6d8f32 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 "internal/environment.hh" +# include namespace spot { @@ -31,7 +31,37 @@ namespace spot { /// \brief An environment that describes atomic propositions. /// \ingroup ltl_essential - typedef spot::internal::environment environment; + 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() + { + } + }; + } } diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 98e7abbcf..ce74666d0 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -1,4 +1,4 @@ -/* Copyright (C) 2003, 2004, 2005, 2006, 2008 Laboratoire d'Informatique de +/* 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. ** @@ -22,6 +22,7 @@ %{ #include #include "public.hh" +#include "ltlast/allnodes.hh" #include "ltlvisit/destroy.hh" %} diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc index f3bb024cd..32cb4d5fd 100644 --- a/src/ltltest/equals.cc +++ b/src/ltltest/equals.cc @@ -30,6 +30,7 @@ #include "ltlvisit/nenoform.hh" #include "ltlvisit/destroy.hh" #include "ltlvisit/contain.hh" +#include "ltlast/allnodes.hh" #include "ltlvisit/reduce.hh" #include "ltlvisit/tostring.hh" diff --git a/src/ltltest/randltl.cc b/src/ltltest/randltl.cc index acf86ce3e..c0f6109da 100644 --- a/src/ltltest/randltl.cc +++ b/src/ltltest/randltl.cc @@ -25,6 +25,7 @@ #include #include #include +#include "ltlast/atomic_prop.hh" #include "ltlvisit/randomltl.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/destroy.hh" diff --git a/src/ltltest/readltl.cc b/src/ltltest/readltl.cc index d72c2b83d..b32e6b1d6 100644 --- a/src/ltltest/readltl.cc +++ b/src/ltltest/readltl.cc @@ -27,6 +27,7 @@ #include "ltlvisit/dump.hh" #include "ltlvisit/dotty.hh" #include "ltlvisit/destroy.hh" +#include "ltlast/allnodes.hh" void syntax(char* prog) diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc index 242c51fef..75ee28ab8 100644 --- a/src/ltltest/reduc.cc +++ b/src/ltltest/reduc.cc @@ -32,6 +32,7 @@ #include "ltlvisit/reduce.hh" #include "ltlvisit/length.hh" #include "ltlvisit/contain.hh" +#include "ltlast/allnodes.hh" void syntax(char* prog) diff --git a/src/ltltest/syntimpl.cc b/src/ltltest/syntimpl.cc index 77c60969a..4e0dcf474 100644 --- a/src/ltltest/syntimpl.cc +++ b/src/ltltest/syntimpl.cc @@ -29,6 +29,7 @@ #include "ltlvisit/destroy.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/syntimpl.hh" +#include "ltlast/allnodes.hh" #include "ltlvisit/nenoform.hh" void diff --git a/src/ltltest/tostring.cc b/src/ltltest/tostring.cc index df0995fa1..43cf021d7 100644 --- a/src/ltltest/tostring.cc +++ b/src/ltltest/tostring.cc @@ -25,6 +25,7 @@ #include "ltlparse/public.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/destroy.hh" +#include "ltlast/allnodes.hh" void syntax(char *prog) diff --git a/src/ltlvisit/apcollect.hh b/src/ltlvisit/apcollect.hh index 756273977..069afa0e9 100644 --- a/src/ltlvisit/apcollect.hh +++ b/src/ltlvisit/apcollect.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2005, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -23,7 +23,7 @@ # define SPOT_LTLVISIT_APCOLLECT_HH #include -#include "ltlast/formula.hh" +#include "ltlast/atomic_prop.hh" namespace spot { diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc index c47955b0b..9140ce506 100644 --- a/src/ltlvisit/basicreduce.cc +++ b/src/ltlvisit/basicreduce.cc @@ -20,6 +20,8 @@ // 02111-1307, USA. #include "basicreduce.hh" +#include "ltlast/visitor.hh" +#include "ltlast/allnodes.hh" #include #include "clone.hh" diff --git a/src/ltlvisit/clone.cc b/src/ltlvisit/clone.cc index ac2cebc33..6a0be0c62 100644 --- a/src/ltlvisit/clone.cc +++ b/src/ltlvisit/clone.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -19,6 +19,7 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +#include "ltlast/allnodes.hh" #include "clone.hh" namespace spot diff --git a/src/ltlvisit/clone.hh b/src/ltlvisit/clone.hh index 7aeafb6b5..604f8bf13 100644 --- a/src/ltlvisit/clone.hh +++ b/src/ltlvisit/clone.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -23,6 +23,7 @@ # define SPOT_LTLVISIT_CLONE_HH #include "ltlast/formula.hh" +#include "ltlast/visitor.hh" namespace spot { diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc index 866297177..dbb0ac3b8 100644 --- a/src/ltlvisit/contain.cc +++ b/src/ltlvisit/contain.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2006, 2007, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2006, 2007 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -23,6 +23,10 @@ #include "destroy.hh" #include "clone.hh" #include "tunabbrev.hh" +#include "ltlast/unop.hh" +#include "ltlast/binop.hh" +#include "ltlast/multop.hh" +#include "ltlast/constant.hh" #include "tgba/tgbaproduct.hh" #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/save.hh" diff --git a/src/ltlvisit/destroy.cc b/src/ltlvisit/destroy.cc index 4a6210d3d..131136d42 100644 --- a/src/ltlvisit/destroy.cc +++ b/src/ltlvisit/destroy.cc @@ -25,10 +25,17 @@ namespace spot { namespace ltl { - void - destroy_visitor::doit_default(formula* c) + namespace { - formula::unref(c); + class destroy_visitor: public postfix_visitor + { + public: + virtual void + doit_default(formula* c) + { + formula::unref(c); + } + }; } void diff --git a/src/ltlvisit/destroy.hh b/src/ltlvisit/destroy.hh index a0223bde9..7b076fc01 100644 --- a/src/ltlvisit/destroy.hh +++ b/src/ltlvisit/destroy.hh @@ -28,19 +28,6 @@ namespace spot { namespace ltl { - /// \ingroup ltl_visitor - /// - /// This visitor is public, because it's convenient to write the - /// destroy method of the base_formula class. But if you just - /// want the functionality, consider using spot::ltl::destroy - /// instead. - class destroy_visitor: public postfix_visitor - { - public: - virtual void - doit_default(formula* c); - }; - /// \brief Destroys a formula /// \ingroup ltl_essential void destroy(const formula *f); diff --git a/src/ltlvisit/dotty.cc b/src/ltlvisit/dotty.cc index 12de237b1..67611b00c 100644 --- a/src/ltlvisit/dotty.cc +++ b/src/ltlvisit/dotty.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -21,6 +21,8 @@ #include "misc/hash.hh" #include "dotty.hh" +#include "ltlast/visitor.hh" +#include "ltlast/allnodes.hh" #include namespace spot diff --git a/src/ltlvisit/dump.cc b/src/ltlvisit/dump.cc index 7823d16f1..3d94732cf 100644 --- a/src/ltlvisit/dump.cc +++ b/src/ltlvisit/dump.cc @@ -1,6 +1,6 @@ -// 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. +// 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. // @@ -20,6 +20,8 @@ // 02111-1307, USA. #include "dump.hh" +#include "ltlast/visitor.hh" +#include "ltlast/allnodes.hh" #include namespace spot diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc index 0e49410cb..7c006a1e5 100644 --- a/src/ltlvisit/lunabbrev.cc +++ b/src/ltlvisit/lunabbrev.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -19,6 +19,7 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +#include "ltlast/allnodes.hh" #include "ltlvisit/clone.hh" #include "lunabbrev.hh" #include diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc index 26334c6e6..208992461 100644 --- a/src/ltlvisit/nenoform.cc +++ b/src/ltlvisit/nenoform.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -19,8 +19,9 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include #include "nenoform.hh" +#include "ltlast/allnodes.hh" +#include namespace spot { diff --git a/src/ltlvisit/nenoform.hh b/src/ltlvisit/nenoform.hh index 336064a32..3569c1359 100644 --- a/src/ltlvisit/nenoform.hh +++ b/src/ltlvisit/nenoform.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -23,6 +23,7 @@ # define SPOT_LTLVISIT_NENOFORM_HH #include "ltlast/formula.hh" +#include "ltlast/visitor.hh" namespace spot { diff --git a/src/ltlvisit/postfix.cc b/src/ltlvisit/postfix.cc index 37f27db06..8863e6a80 100644 --- a/src/ltlvisit/postfix.cc +++ b/src/ltlvisit/postfix.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -20,6 +20,7 @@ // 02111-1307, USA. #include "ltlvisit/postfix.hh" +#include "ltlast/allnodes.hh" namespace spot { diff --git a/src/ltlvisit/postfix.hh b/src/ltlvisit/postfix.hh index c275ebea0..4d341f59b 100644 --- a/src/ltlvisit/postfix.hh +++ b/src/ltlvisit/postfix.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -23,6 +23,7 @@ # define SPOT_LTLVISIT_POSTFIX_HH #include "ltlast/formula.hh" +#include "ltlast/visitor.hh" namespace spot { diff --git a/src/ltlvisit/randomltl.cc b/src/ltlvisit/randomltl.cc index 303d18b23..73cf99493 100644 --- a/src/ltlvisit/randomltl.cc +++ b/src/ltlvisit/randomltl.cc @@ -22,6 +22,7 @@ #include #include #include "randomltl.hh" +#include "ltlast/allnodes.hh" #include "misc/random.hh" #include #include diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index 3b4db1886..a34161043 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -22,6 +22,7 @@ #include "reduce.hh" #include "basicreduce.hh" #include "syntimpl.hh" +#include "ltlast/allnodes.hh" #include #include "lunabbrev.hh" diff --git a/src/ltlvisit/reduce.hh b/src/ltlvisit/reduce.hh index aae9d15b9..3c6fcf850 100644 --- a/src/ltlvisit/reduce.hh +++ b/src/ltlvisit/reduce.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2006, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2006 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_LTLVISIT_REDUCE_HH #include "ltlast/formula.hh" +#include "ltlast/visitor.hh" namespace spot { diff --git a/src/ltlvisit/simpfg.cc b/src/ltlvisit/simpfg.cc index 928671505..fa143cfd9 100644 --- a/src/ltlvisit/simpfg.cc +++ b/src/ltlvisit/simpfg.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -19,6 +19,8 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +#include "ltlast/allnodes.hh" +#include "ltlvisit/clone.hh" #include "simpfg.hh" #include diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc index 295647cd4..fffcfc136 100644 --- a/src/ltlvisit/syntimpl.cc +++ b/src/ltlvisit/syntimpl.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2005, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -20,6 +20,7 @@ // 02111-1307, USA. #include "syntimpl.hh" +#include "ltlast/allnodes.hh" #include #include "lunabbrev.hh" diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index 2aee59a05..05b0a3827 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -25,6 +25,9 @@ #include #include #include "tostring.hh" +#include "ltlast/visitor.hh" +#include "ltlast/allnodes.hh" + namespace spot { diff --git a/src/ltlvisit/tunabbrev.cc b/src/ltlvisit/tunabbrev.cc index 477e80e9c..7d372148e 100644 --- a/src/ltlvisit/tunabbrev.cc +++ b/src/ltlvisit/tunabbrev.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -19,6 +19,7 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +#include "ltlast/allnodes.hh" #include "tunabbrev.hh" namespace spot diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc index 5c1b0a23a..e4ff5a61b 100644 --- a/src/tgba/bdddict.cc +++ b/src/tgba/bdddict.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2005, 2006, 2008 Laboratoire d'Informatique de +// 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. // @@ -25,6 +25,8 @@ #include #include #include +#include +#include #include #include "bdddict.hh" @@ -46,8 +48,7 @@ namespace spot } int - bdd_dict::register_proposition(const internal::base_formula* f, - const void* for_me) + bdd_dict::register_proposition(const ltl::formula* f, const void* for_me) { int num; // Do not build a variable that already exists. @@ -58,7 +59,7 @@ namespace spot } else { - f = f->clone(); + f = clone(f); num = allocate_variables(1); var_map[f] = num; var_formula_map[num] = f; @@ -82,8 +83,7 @@ namespace spot } int - bdd_dict::register_state(const internal::base_formula* f, - const void* for_me) + bdd_dict::register_state(const ltl::formula* f, const void* for_me) { int num; // Do not build a state that already exists. @@ -94,7 +94,7 @@ namespace spot } else { - f = f->clone(); + f = ltl::clone(f); num = allocate_variables(2); now_map[f] = num; now_formula_map[num] = f; @@ -108,8 +108,8 @@ namespace spot } int - bdd_dict::register_acceptance_variable(const internal::base_formula* f, - const void* for_me) + bdd_dict::register_acceptance_variable(const ltl::formula* f, + const void* for_me) { int num; // Do not build an acceptance variable that already exists. @@ -120,7 +120,7 @@ namespace spot } else { - f = f->clone(); + f = clone(f); num = allocate_variables(1); acc_map[f] = num; acc_formula_map[num] = f; @@ -151,14 +151,13 @@ namespace spot assert(i != acc_formula_map.end()); std::ostringstream s; // FIXME: We could be smarter and reuse unused "$n" numbers. - s << i->second->to_string() - << "$" + s << ltl::to_string(i->second) << "$" << ++clone_counts[var]; - internal::base_formula* f = + ltl::formula* f = ltl::atomic_prop::instance(s.str(), ltl::default_environment::instance()); int res = register_acceptance_variable(f, for_me); - f->destroy(); + ltl::destroy(f); return res; } @@ -235,7 +234,7 @@ namespace spot // Let's free it. First, we need to find // if this is a Now, a Var, or an Acc variable. int n = 1; - const internal::base_formula* f = 0; + const ltl::formula* f = 0; vf_map::iterator vi = var_formula_map.find(var); if (vi != var_formula_map.end()) { @@ -280,7 +279,7 @@ namespace spot // formula itself. release_variables(var, n); if (f) - f->destroy(); + ltl::destroy(f); var_refs.erase(cur); } @@ -299,8 +298,7 @@ namespace spot } bool - bdd_dict::is_registered_proposition(const internal::base_formula* f, - const void* by_me) + bdd_dict::is_registered_proposition(const ltl::formula* f, const void* by_me) { fv_map::iterator fi = var_map.find(f); if (fi == var_map.end()) @@ -310,8 +308,7 @@ namespace spot } bool - bdd_dict::is_registered_state(const internal::base_formula* f, - const void* by_me) + bdd_dict::is_registered_state(const ltl::formula* f, const void* by_me) { fv_map::iterator fi = now_map.find(f); if (fi == now_map.end()) @@ -321,7 +318,7 @@ namespace spot } bool - bdd_dict::is_registered_acceptance_variable(const internal::base_formula* f, + bdd_dict::is_registered_acceptance_variable(const ltl::formula* f, const void* by_me) { fv_map::iterator fi = acc_map.find(f); @@ -340,23 +337,23 @@ namespace spot { os << " " << fi->second << " (x" << var_refs.find(fi->second)->second.size() << "): "; - fi->first->to_string(os) << std::endl; + to_string(fi->first, os) << std::endl; } os << "States:" << std::endl; for (fi = now_map.begin(); fi != now_map.end(); ++fi) { int refs = var_refs.find(fi->second)->second.size(); os << " " << fi->second << " (x" << refs << "): Now["; - fi->first->to_string(os) << "]" << std::endl; + to_string(fi->first, os) << "]" << std::endl; os << " " << fi->second + 1 << " (x" << refs << "): Next["; - fi->first->to_string(os) << "]" << std::endl; + to_string(fi->first, os) << "]" << std::endl; } os << "Acceptance Conditions:" << std::endl; for (fi = acc_map.begin(); fi != acc_map.end(); ++fi) { os << " " << fi->second << " (x" << var_refs.find(fi->second)->second.size() << "): Acc["; - fi->first->to_string(os) << "]" << std::endl; + to_string(fi->first, os) << "]" << std::endl; } os << "Ref counts:" << std::endl; vr_map::const_iterator ri; diff --git a/src/tgba/bdddict.hh b/src/tgba/bdddict.hh index 0861a598b..434d77703 100644 --- a/src/tgba/bdddict.hh +++ b/src/tgba/bdddict.hh @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2004, 2006 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, 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. // @@ -27,7 +27,7 @@ #include #include #include -#include "internal/baseformula.hh" +#include "ltlast/formula.hh" #include "misc/bddalloc.hh" namespace spot @@ -43,9 +43,9 @@ namespace spot ~bdd_dict(); /// Formula-to-BDD-variable maps. - typedef std::map fv_map; + typedef std::map fv_map; /// BDD-variable-to-formula maps. - typedef std::map vf_map; + typedef std::map vf_map; fv_map now_map; ///< Maps formulae to "Now" BDD variables vf_map now_formula_map; ///< Maps "Now" BDD variables to formulae @@ -77,8 +77,7 @@ namespace spot /// /// \return The variable number. Use bdd_ithvar() or bdd_nithvar() /// to convert this to a BDD. - int - register_proposition(const internal::base_formula* f, const void* for_me); + int register_proposition(const ltl::formula* f, const void* for_me); /// \brief Register BDD variables as atomic propositions. /// @@ -100,7 +99,7 @@ namespace spot /// \return The first variable number. Add one to get the second /// variable. Use bdd_ithvar() or bdd_nithvar() to convert this /// to a BDD. - int register_state(const internal::base_formula* f, const void* for_me); + int register_state(const ltl::formula* f, const void* for_me); /// \brief Register an atomic proposition. /// @@ -112,8 +111,7 @@ namespace spot /// /// \return The variable number. Use bdd_ithvar() or bdd_nithvar() /// to convert this to a BDD. - int register_acceptance_variable(const internal::base_formula* f, - const void* for_me); + int register_acceptance_variable(const ltl::formula* f, const void* for_me); /// \brief Clone an acceptance variable VAR for FOR_ME. /// @@ -158,12 +156,9 @@ namespace spot /// @{ /// Check whether formula \a f has already been registered by \a by_me. - bool is_registered_proposition(const internal::base_formula* f, - const void* by_me); - - bool is_registered_state(const internal::base_formula* f, - const void* by_me); - bool is_registered_acceptance_variable(const internal::base_formula* f, + bool is_registered_proposition(const ltl::formula* f, const void* by_me); + bool is_registered_state(const ltl::formula* f, const void* by_me); + bool is_registered_acceptance_variable(const ltl::formula* f, const void* by_me); /// @} diff --git a/src/tgba/bddprint.cc b/src/tgba/bddprint.cc index 9b90fd4ff..4be59eb21 100644 --- a/src/tgba/bddprint.cc +++ b/src/tgba/bddprint.cc @@ -23,7 +23,9 @@ #include #include #include "bddprint.hh" +#include "ltlvisit/tostring.hh" #include "formula2bdd.hh" +#include "ltlvisit/destroy.hh" namespace spot { @@ -40,7 +42,7 @@ namespace spot bdd_dict::vf_map::const_iterator isi = dict->var_formula_map.find(var); if (isi != dict->var_formula_map.end()) - isi->second->to_string(o); + to_string(isi->second, o); else { isi = dict->acc_formula_map.find(var); @@ -49,12 +51,12 @@ namespace spot if (want_acc) { o << "Acc["; - isi->second->to_string(o) << "]"; + to_string(isi->second, o) << "]"; } else { o << "\""; - isi->second->to_string(o) << "\""; + to_string(isi->second, o) << "\""; } } else @@ -62,14 +64,14 @@ namespace spot isi = dict->now_formula_map.find(var); if (isi != dict->now_formula_map.end()) { - o << "Now["; isi->second->to_string(o) << "]"; + o << "Now["; to_string(isi->second, o) << "]"; } else { isi = dict->now_formula_map.find(var - 1); if (isi != dict->now_formula_map.end()) { - o << "Next["; isi->second->to_string(o) << "]"; + o << "Next["; to_string(isi->second, o) << "]"; } else { diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index 519e80b87..edc42922e 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -21,6 +21,8 @@ #include #include "formula2bdd.hh" +#include "ltlast/allnodes.hh" +#include "ltlast/visitor.hh" #include "misc/minato.hh" #include "ltlvisit/clone.hh" @@ -162,7 +164,7 @@ namespace spot int var = bdd_var(b); bdd_dict::vf_map::const_iterator isi = d->var_formula_map.find(var); assert(isi != d->var_formula_map.end()); - formula* res = clone(dynamic_cast(isi->second)); + formula* res = clone(isi->second); bdd high = bdd_high(b); if (high == bddfalse) diff --git a/src/tgba/tgbabddconcretefactory.cc b/src/tgba/tgbabddconcretefactory.cc index acc5bc3c2..0d04023ae 100644 --- a/src/tgba/tgbabddconcretefactory.cc +++ b/src/tgba/tgbabddconcretefactory.cc @@ -19,8 +19,9 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +#include "ltlvisit/clone.hh" +#include "ltlvisit/destroy.hh" #include "tgbabddconcretefactory.hh" - namespace spot { tgba_bdd_concrete_factory::tgba_bdd_concrete_factory(bdd_dict* dict) @@ -32,12 +33,12 @@ namespace spot { acc_map_::iterator ai; for (ai = acc_.begin(); ai != acc_.end(); ++ai) - ai->first->destroy(); + destroy(ai->first); get_dict()->unregister_all_my_variables(this); } int - tgba_bdd_concrete_factory::create_state(const internal::base_formula* f) + tgba_bdd_concrete_factory::create_state(const ltl::formula* f) { int num = get_dict()->register_state(f, this); // Keep track of all "Now" variables for easy @@ -47,7 +48,7 @@ namespace spot } int - tgba_bdd_concrete_factory::create_atomic_prop(const internal::base_formula* f) + tgba_bdd_concrete_factory::create_atomic_prop(const ltl::formula* f) { int num = get_dict()->register_proposition(f, this); // Keep track of all atomic proposition for easy @@ -57,9 +58,8 @@ namespace spot } void - tgba_bdd_concrete_factory::declare_acceptance_condition( - bdd b, - const internal::base_formula* a) + tgba_bdd_concrete_factory::declare_acceptance_condition(bdd b, + const ltl::formula* a) { // Maintain a conjunction of BDDs associated to A. We will latter // (in tgba_bdd_concrete_factory::finish()) associate this @@ -67,7 +67,7 @@ namespace spot acc_map_::iterator ai = acc_.find(a); if (ai == acc_.end()) { - a = a->clone(); + a = clone(a); acc_[a] = b; } else diff --git a/src/tgba/tgbabddconcretefactory.hh b/src/tgba/tgbabddconcretefactory.hh index c65a99584..a2c987e30 100644 --- a/src/tgba/tgbabddconcretefactory.hh +++ b/src/tgba/tgbabddconcretefactory.hh @@ -23,7 +23,7 @@ # define SPOT_TGBA_TGBABDDCONCRETEFACTORY_HH #include "misc/hash.hh" -#include "internal/baseformula.hh" +#include "ltlast/formula.hh" #include "tgbabddfactory.hh" namespace spot @@ -45,7 +45,7 @@ namespace spot /// The state variables are not created if they already exist. /// Instead their existing variable numbers are returned. /// Variable numbers can be turned into BDD using ithvar(). - int create_state(const internal::base_formula* f); + int create_state(const ltl::formula* f); /// Create an atomic proposition variable for formula \a f. /// @@ -55,7 +55,7 @@ namespace spot /// The atomic proposition is not created if it already exists. /// Instead its existing variable number is returned. Variable numbers /// can be turned into BDD using ithvar(). - int create_atomic_prop(const internal::base_formula* f); + int create_atomic_prop(const ltl::formula* f); /// Declare an acceptance condition. /// @@ -68,7 +68,7 @@ namespace spot /// \param b a BDD indicating which variables are in the /// acceptance set /// \param a the formula associated - void declare_acceptance_condition(bdd b, const internal::base_formula* a); + void declare_acceptance_condition(bdd b, const ltl::formula* a); const tgba_bdd_core_data& get_core_data() const; bdd_dict* get_dict() const; @@ -86,8 +86,8 @@ namespace spot private: tgba_bdd_core_data data_; ///< Core data for the new automata. - typedef Sgi::hash_map acc_map_; + typedef Sgi::hash_map acc_map_; acc_map_ acc_; ///< BDD associated to each acceptance condition }; diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index fff7ea89e..0880cacdd 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -19,6 +19,8 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +#include "ltlast/atomic_prop.hh" +#include "ltlast/constant.hh" #include "ltlvisit/destroy.hh" #include "tgbaexplicit.hh" #include "tgba/formula2bdd.hh" diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index e07e96490..575b3731d 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -1,6 +1,6 @@ -// 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. +// 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. // @@ -22,8 +22,8 @@ #include #include "tgbatba.hh" #include "bddprint.hh" +#include "ltlast/constant.hh" #include "misc/hashfunc.hh" -#include "ltlast/formula.hh" namespace spot { diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 2acfba1e0..56e7b7399 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -31,7 +31,6 @@ tgbaalgos_HEADERS = \ dotty.hh \ dottydec.hh \ dupexp.hh \ - eltl2tgba_lacim.hh \ emptiness.hh \ emptiness_stats.hh \ gv04.hh \ @@ -62,7 +61,6 @@ libtgbaalgos_la_SOURCES = \ dotty.cc \ dottydec.cc \ dupexp.cc \ - eltl2tgba_lacim.cc \ emptiness.cc \ gv04.cc \ lbtt.cc \ diff --git a/src/tgbaalgos/eltl2tgba_lacim.cc b/src/tgbaalgos/eltl2tgba_lacim.cc deleted file mode 100644 index 7ad6e4799..000000000 --- a/src/tgbaalgos/eltl2tgba_lacim.cc +++ /dev/null @@ -1,188 +0,0 @@ -// 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 "eltlast/formula.hh" -#include "eltlvisit/lunabbrev.hh" -#include "eltlvisit/nenoform.hh" -#include "eltlvisit/destroy.hh" -#include "tgba/tgbabddconcretefactory.hh" -#include - -#include "eltl2tgba_lacim.hh" - -namespace spot -{ - namespace - { - using namespace eltl; - - /// \brief Recursively translate a formula into a BDD. - class eltl_trad_visitor: public const_visitor - { - public: - eltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false) - : fact_(fact), root_(root) - { - } - - virtual - ~eltl_trad_visitor() - { - } - - bdd - result() - { - return res_; - } - - void - visit(const atomic_prop* node) - { - res_ = bdd_ithvar(fact_.create_atomic_prop(node)); - } - - void - visit(const constant* node) - { - switch (node->val()) - { - case constant::True: - res_ = bddtrue; - return; - case constant::False: - res_ = bddfalse; - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(const unop* node) - { - switch (node->op()) - { - case unop::Not: - { - res_ = bdd_not(recurse(node->child())); - return; - } - } - /* Unreachable code. */ - assert(0); - } - - void - visit(const binop* node) - { - bdd f1 = recurse(node->first()); - bdd f2 = recurse(node->second()); - - switch (node->op()) - { - case binop::Xor: - res_ = bdd_apply(f1, f2, bddop_xor); - return; - case binop::Implies: - res_ = bdd_apply(f1, f2, bddop_imp); - return; - case binop::Equiv: - res_ = bdd_apply(f1, f2, bddop_biimp); - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(const multop* node) - { - int op = -1; - bool root = false; - switch (node->op()) - { - case multop::And: - op = bddop_and; - res_ = bddtrue; - // When the root formula is a conjunction it's ok to - // consider all children as root formulae. This allows the - // root-G trick to save many more variable. (See the - // translation of G.) - root = root_; - break; - case multop::Or: - op = bddop_or; - res_ = bddfalse; - break; - } - assert(op != -1); - unsigned s = node->size(); - for (unsigned n = 0; n < s; ++n) - { - res_ = bdd_apply(res_, recurse(node->nth(n), root), op); - } - } - - void - visit (const automatop* node) - { - // FIXME. - (void) node; - } - - bdd - recurse(const formula* f, bool root = false) - { - eltl_trad_visitor v(fact_, root); - f->accept(v); - return v.result(); - } - - private: - bdd res_; - tgba_bdd_concrete_factory& fact_; - bool root_; - }; - } // anonymous - - tgba_bdd_concrete* - eltl_to_tgba_lacim(const eltl::formula* f, bdd_dict* dict) - { - // Normalize the formula. We want all the negations on - // the atomic propositions. We also suppress logic - // abbreviations such as <=>, =>, or XOR, since they - // would involve negations at the BDD level. - const eltl::formula* f1 = eltl::unabbreviate_logic(f); - const eltl::formula* f2 = eltl::negative_normal_form(f1); - eltl::destroy(f1); - - // Traverse the formula and draft the automaton in a factory. - tgba_bdd_concrete_factory fact(dict); - eltl_trad_visitor v(fact, true); - f2->accept(v); - eltl::destroy(f2); - fact.finish(); - - // Finally setup the resulting automaton. - return new tgba_bdd_concrete(fact, v.result()); - } -} diff --git a/src/tgbaalgos/eltl2tgba_lacim.hh b/src/tgbaalgos/eltl2tgba_lacim.hh deleted file mode 100644 index 732822cee..000000000 --- a/src/tgbaalgos/eltl2tgba_lacim.hh +++ /dev/null @@ -1,55 +0,0 @@ -// 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_TGBAALGOS_ELTL2TGBA_LACIM_HH -# define SPOT_TGBAALGOS_ELTL2TGBA_LACIM_HH - -#include "eltlast/formula.hh" -#include "tgba/tgbabddconcrete.hh" - -namespace spot -{ - /// \brief Build a spot::tgba_bdd_concrete from an ELTL formula. - /// \ingroup tgba_eltl - /// - /// This is based on the following paper. - /// \verbatim - /// @InProceedings{ couvreur.00.lacim, - /// author = {Jean-Michel Couvreur}, - /// title = {Un point de vue symbolique sur la logique temporelle - /// lin{\'e}aire}, - /// booktitle = {Actes du Colloque LaCIM 2000}, - /// month = {August}, - /// year = {2000}, - /// pages = {131--140}, - /// volume = {27}, - /// series = {Publications du LaCIM}, - /// publisher = {Universit{\'e} du Qu{\'e}bec {\`a} Montr{\'e}al}, - /// editor = {Pierre Leroux} - /// } - /// \endverbatim - /// \param f The formula to translate into an automaton. - /// \param dict The spot::bdd_dict the constructed automata should use. - /// \return A spot::tgba_bdd_concrete that recognizes the language of \a f. - tgba_bdd_concrete* eltl_to_tgba_lacim(const eltl::formula* f, bdd_dict* dict); -} - -#endif // SPOT_TGBAALGOS_LTL2TGBA_LACIM_HH diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 9e4943361..cc6e3ab3d 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -23,6 +23,8 @@ #include "misc/bddalloc.hh" #include "misc/bddlt.hh" #include "misc/minato.hh" +#include "ltlast/visitor.hh" +#include "ltlast/allnodes.hh" #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/nenoform.hh" #include "ltlvisit/destroy.hh" @@ -64,7 +66,7 @@ namespace spot { fv_map::iterator i; for (i = next_map.begin(); i != next_map.end(); ++i) - destroy(dynamic_cast(i->first)); + destroy(i->first); dict->unregister_all_my_variables(this); } @@ -117,18 +119,33 @@ namespace spot return num; } + std::ostream& + dump(std::ostream& os) const + { + fv_map::const_iterator fi; + os << "Next Variables:" << std::endl; + for (fi = next_map.begin(); fi != next_map.end(); ++fi) + { + os << " " << fi->second << ": Next["; + to_string(fi->first, os) << "]" << std::endl; + } + os << "Shared Dict:" << std::endl; + dict->dump(os); + return os; + } + formula* var_to_formula(int var) const { vf_map::const_iterator isi = next_formula_map.find(var); if (isi != next_formula_map.end()) - return dynamic_cast(isi->second->clone()); + return clone(isi->second); isi = dict->acc_formula_map.find(var); if (isi != dict->acc_formula_map.end()) - return dynamic_cast(isi->second->clone()); + return clone(isi->second); isi = dict->var_formula_map.find(var); if (isi != dict->var_formula_map.end()) - return dynamic_cast(isi->second->clone()); + return clone(isi->second); assert(0); // Never reached, but some GCC versions complain about // a missing return otherwise. diff --git a/src/tgbaalgos/ltl2tgba_lacim.cc b/src/tgbaalgos/ltl2tgba_lacim.cc index a00f81d23..fe6ce96b7 100644 --- a/src/tgbaalgos/ltl2tgba_lacim.cc +++ b/src/tgbaalgos/ltl2tgba_lacim.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -19,6 +19,8 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +#include "ltlast/visitor.hh" +#include "ltlast/allnodes.hh" #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/nenoform.hh" #include "ltlvisit/destroy.hh" diff --git a/src/tgbaalgos/randomgraph.cc b/src/tgbaalgos/randomgraph.cc index 365f0f6c4..f85e5e5b8 100644 --- a/src/tgbaalgos/randomgraph.cc +++ b/src/tgbaalgos/randomgraph.cc @@ -22,6 +22,7 @@ #include "randomgraph.hh" #include "tgba/tgbaexplicit.hh" #include "misc/random.hh" +#include "ltlast/atomic_prop.hh" #include "ltlvisit/destroy.hh" #include #include diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc index 5cb522415..b87a36eff 100644 --- a/src/tgbaalgos/save.cc +++ b/src/tgbaalgos/save.cc @@ -1,6 +1,6 @@ -// 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. +// 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. // @@ -23,6 +23,7 @@ #include "save.hh" #include "tgba/bddprint.hh" #include "ltlvisit/tostring.hh" +#include "ltlast/atomic_prop.hh" #include "reachiter.hh" #include "misc/escape.hh" @@ -84,7 +85,7 @@ namespace spot bdd_dict::vf_map::const_iterator vi = d->acc_formula_map.find(v); assert(vi != d->acc_formula_map.end()); - std::string s = vi->second->to_string(); + std::string s = ltl::to_string(vi->second); if (dynamic_cast(vi->second) && s[0] == '"') { diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy index 8b9a8da5e..7fe3b4252 100644 --- a/src/tgbaparse/tgbaparse.yy +++ b/src/tgbaparse/tgbaparse.yy @@ -1,4 +1,4 @@ -/* Copyright (C) 2003, 2004, 2005, 2006, 2008 Laboratoire d'Informatique de +/* 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. ** @@ -47,6 +47,7 @@ typedef std::map formula_cache; } %{ +#include "ltlast/constant.hh" #include "ltlvisit/destroy.hh" /* Unfortunately Bison 2.3 uses the same guards in all parsers :( */ #undef BISON_POSITION_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 8ae792cb3..b3ec54301 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -25,7 +25,7 @@ LDADD = ../libspot.la # These are the most used test programs, and they are also useful # to run manually outside the test suite. Always build them. -noinst_PROGRAMS = ltl2tgba randtgba eltl2tgba +noinst_PROGRAMS = ltl2tgba randtgba check_SCRIPTS = defs # Keep this sorted alphabetically. @@ -46,7 +46,6 @@ check_PROGRAMS = \ # Keep this sorted alphabetically. bddprod_SOURCES = ltlprod.cc bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT -eltl2tgba_SOURCES = eltl2tgba.cc explicit_SOURCES = explicit.cc expldot_SOURCES = powerset.cc expldot_CXXFLAGS = -DDOTTY @@ -86,8 +85,7 @@ TESTS = \ emptchke.test \ dfs.test \ emptchkr.test \ - spotlbtt.test \ - eltl2tgba.test + spotlbtt.test EXTRA_DIST = $(TESTS) diff --git a/src/tgbatest/eltl2tgba.cc b/src/tgbatest/eltl2tgba.cc deleted file mode 100644 index ac4722250..000000000 --- a/src/tgbatest/eltl2tgba.cc +++ /dev/null @@ -1,50 +0,0 @@ -// 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" -#include "tgbaalgos/eltl2tgba_lacim.hh" -#include "tgbaalgos/dotty.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; - - spot::bdd_dict* dict = new spot::bdd_dict(); - spot::tgba_bdd_concrete* concrete = spot::eltl_to_tgba_lacim(f, dict); - - spot::dotty_reachable(std::cout, concrete); - delete concrete; -} diff --git a/src/tgbatest/eltl2tgba.test b/src/tgbatest/eltl2tgba.test deleted file mode 100755 index ba1efa07d..000000000 --- a/src/tgbatest/eltl2tgba.test +++ /dev/null @@ -1,40 +0,0 @@ -#!/bin/sh - -. ./defs || exit -1 -set -e - -check () -{ - run 0 ./eltl2tgba "$1" || exit 1 -} - -cat >input <input1 <input < #include #include "ltlvisit/destroy.hh" +#include "ltlast/allnodes.hh" #include "ltlparse/public.hh" #include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgba/tgbaproduct.hh" diff --git a/src/tgbatest/mixprod.cc b/src/tgbatest/mixprod.cc index dcce01fcf..dc246c2e2 100644 --- a/src/tgbatest/mixprod.cc +++ b/src/tgbatest/mixprod.cc @@ -23,6 +23,7 @@ #include #include #include "ltlvisit/destroy.hh" +#include "ltlast/allnodes.hh" #include "ltlparse/public.hh" #include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgba/tgbaproduct.hh" diff --git a/src/tgbatest/powerset.cc b/src/tgbatest/powerset.cc index 7780b82be..6bfebd85e 100644 --- a/src/tgbatest/powerset.cc +++ b/src/tgbatest/powerset.cc @@ -26,6 +26,7 @@ #include "tgbaalgos/powerset.hh" #include "tgbaparse/public.hh" #include "tgbaalgos/save.hh" +#include "ltlast/allnodes.hh" #include "tgbaalgos/dotty.hh" void diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 48e59499b..5204484af 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -41,6 +41,7 @@ #include "tgbaalgos/save.hh" #include "tgbaalgos/stats.hh" #include "ltlenv/defaultenv.hh" +#include "ltlast/atomic_prop.hh" #include "tgbaalgos/dotty.hh" #include "tgbaparse/public.hh" #include "misc/random.hh" diff --git a/src/tgbatest/readsave.cc b/src/tgbatest/readsave.cc index 4d998b08f..6783ed265 100644 --- a/src/tgbatest/readsave.cc +++ b/src/tgbatest/readsave.cc @@ -26,6 +26,7 @@ #include "tgbaparse/public.hh" #include "tgba/tgbaexplicit.hh" #include "tgbaalgos/save.hh" +#include "ltlast/allnodes.hh" void syntax(char* prog) diff --git a/src/tgbatest/reductgba.cc b/src/tgbatest/reductgba.cc index 0d0c7ac24..26e92266f 100644 --- a/src/tgbatest/reductgba.cc +++ b/src/tgbatest/reductgba.cc @@ -27,6 +27,7 @@ #include "ltlvisit/destroy.hh" #include "ltlvisit/reduce.hh" +#include "ltlast/allnodes.hh" #include "ltlparse/public.hh" #include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgbaalgos/ltl2tgba_fm.hh" diff --git a/src/tgbatest/tgbaread.cc b/src/tgbatest/tgbaread.cc index 50a375462..d05e6cf78 100644 --- a/src/tgbatest/tgbaread.cc +++ b/src/tgbatest/tgbaread.cc @@ -26,6 +26,7 @@ #include "tgbaparse/public.hh" #include "tgba/tgbaexplicit.hh" #include "tgbaalgos/dotty.hh" +#include "ltlast/allnodes.hh" void syntax(char* prog) diff --git a/src/tgbatest/tripprod.cc b/src/tgbatest/tripprod.cc index 84e849fe1..0a33f2e6b 100644 --- a/src/tgbatest/tripprod.cc +++ b/src/tgbatest/tripprod.cc @@ -26,6 +26,7 @@ #include "tgba/tgbaproduct.hh" #include "tgbaparse/public.hh" #include "tgbaalgos/save.hh" +#include "ltlast/allnodes.hh" void syntax(char* prog)