diff --git a/ChangeLog b/ChangeLog index ad5d22cf5..7a709f625 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,22 @@ +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, diff --git a/configure.ac b/configure.ac index 62427ec39..63ed67b65 100644 --- a/configure.ac +++ b/configure.ac @@ -44,6 +44,7 @@ AC_LANG(C++) AX_CHECK_BUDDY AX_CHECK_LBTT AX_CHECK_GSPNLIB +AX_BOOST_BASE([1.34]) AC_CHECK_FUNCS([srand48 drand48]) @@ -88,6 +89,7 @@ AC_CONFIG_FILES([ src/eltlparse/Makefile src/eltltest/Makefile src/eltltest/defs + src/eltlvisit/Makefile src/evtgba/Makefile src/evtgbaalgos/Makefile src/evtgbaparse/Makefile diff --git a/m4/boost.m4 b/m4/boost.m4 new file mode 100644 index 000000000..02534a30e --- /dev/null +++ b/m4/boost.m4 @@ -0,0 +1,194 @@ +##### 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 1a73b6d56..97e1ba8b7 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -24,7 +24,7 @@ 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 eltlparse \ + eltlenv eltlast eltlvisit eltlparse \ tgba tgbaalgos tgbaparse \ evtgba evtgbaalgos evtgbaparse . \ ltltest eltltest tgbatest evtgbatest sanity @@ -36,8 +36,10 @@ libspot_la_LIBADD = \ misc/libmisc.la \ ltlparse/libltlparse.la \ ltlvisit/libltlvisit.la \ + internal/libinternal.la \ eltlast/libeltlast.la \ eltlparse/libeltlparse.la \ + eltlvisit/libeltlvisit.la \ tgba/libtgba.la \ tgbaalgos/libtgbaalgos.la \ tgbaparse/libtgbaparse.la \ diff --git a/src/eltlast/Makefile.am b/src/eltlast/Makefile.am index 0b8fae81d..74d0a3f94 100644 --- a/src/eltlast/Makefile.am +++ b/src/eltlast/Makefile.am @@ -25,20 +25,11 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) eltlastdir = $(pkgincludedir)/eltlast eltlast_HEADERS = \ - allnodes.hh \ - atomic_prop.hh \ automatop.hh \ - binop.hh \ - constant.hh \ formula.hh \ - multop.hh \ - nfa.hh \ - refformula.hh \ - unop.hh \ - visitor.hh - + nfa.hh noinst_LTLIBRARIES = libeltlast.la libeltlast_la_SOURCES = \ automatop.cc \ - nfa.cc \ No newline at end of file + nfa.cc diff --git a/src/eltlast/allnodes.hh b/src/eltlast/allnodes.hh deleted file mode 100644 index d7ab24d39..000000000 --- a/src/eltlast/allnodes.hh +++ /dev/null @@ -1,36 +0,0 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 2 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -/// \file eltlast/allnodes.hh -/// \brief Define all ELTL node types. -/// -/// This file is usually needed when \b defining a visitor. -#ifndef SPOT_ELTLAST_ALLNODES_HH -# define SPOT_ELTLAST_ALLNODES_HH - -# include "binop.hh" -# include "unop.hh" -# include "multop.hh" -# include "atomic_prop.hh" -# include "constant.hh" -# include "automatop.hh" - -#endif // SPOT_ELTLAST_ALLNODES_HH diff --git a/src/eltlast/automatop.cc b/src/eltlast/automatop.cc index f3a7b1a69..5178f5d16 100644 --- a/src/eltlast/automatop.cc +++ b/src/eltlast/automatop.cc @@ -19,7 +19,6 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include "visitor.hh" #include "automatop.hh" namespace spot diff --git a/src/eltlast/automatop.hh b/src/eltlast/automatop.hh index 9b94521ea..0f8524cc8 100644 --- a/src/eltlast/automatop.hh +++ b/src/eltlast/automatop.hh @@ -24,14 +24,16 @@ #ifndef SPOT_ELTLAST_AUTOMATOP_HH # define SPOT_ELTLAST_AUTOMATOP_HH -# include "multop.hh" -# include "refformula.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 diff --git a/src/eltlast/formula.hh b/src/eltlast/formula.hh index e8d6c66b9..1e10f2722 100644 --- a/src/eltlast/formula.hh +++ b/src/eltlast/formula.hh @@ -25,6 +25,11 @@ # 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 { @@ -40,7 +45,21 @@ namespace spot /// \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; @@ -50,11 +69,33 @@ namespace spot /// /// 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 { @@ -86,10 +127,73 @@ namespace spot } }; - typedef spot::internal::formula formula; + typedef spot::internal::formula_ptr_less_than formula_ptr_less_than; + typedef spot::internal::formula_ptr_hash formula_ptr_hash; + + /// \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; + }; - typedef spot::internal::formula_ptr_less_than formula_ptr_less_than; - typedef spot::internal::formula_ptr_hash formula_ptr_hash; } } diff --git a/src/eltlast/nfa.cc b/src/eltlast/nfa.cc index a50abe036..2dc944f3f 100644 --- a/src/eltlast/nfa.cc +++ b/src/eltlast/nfa.cc @@ -61,7 +61,7 @@ namespace spot } void - nfa::add_transition(const std::string& s, const std::string& d, unsigned c) + nfa::add_transition(const std::string& s, const std::string& d, int c) { state* source = add_state(s); nfa::transition* t = new transition; @@ -90,7 +90,7 @@ namespace spot return finals_.find(state) != finals_.end(); } - unsigned + int nfa::arity() { return arity_ + 1; diff --git a/src/eltlast/nfa.hh b/src/eltlast/nfa.hh index 250ec7b11..c578ca5de 100644 --- a/src/eltlast/nfa.hh +++ b/src/eltlast/nfa.hh @@ -51,7 +51,7 @@ namespace spot /// Explicit transitions. struct transition { - unsigned cost; + int cost; const state* dest; }; @@ -59,7 +59,7 @@ namespace spot ~nfa(); void - add_transition(const std::string& s, const std::string& d, unsigned c); + add_transition(const std::string& s, const std::string& d, int c); void set_init_state(const std::string& state); @@ -72,7 +72,7 @@ namespace spot is_final(const std::string& state); /// \brief Get the `arity' i.e. max t.cost, for each transition t. - unsigned + int arity(); /// \brief Return an iterator on the first succesor (if any) of \a state. @@ -103,7 +103,7 @@ namespace spot sn_map sn_; state* init_; - unsigned arity_; + int arity_; std::set finals_; /// Explicitly disllow use of implicity generated member functions diff --git a/src/eltlast/visitor.hh b/src/eltlast/visitor.hh deleted file mode 100644 index 9426f8699..000000000 --- a/src/eltlast/visitor.hh +++ /dev/null @@ -1,82 +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/visitor.hh -/// \brief ELTL visitor interface -#ifndef SPOT_ELTLAST_VISITOR_HH -# define SPOT_ELTLAST_VISITOR_HH - -# include "binop.hh" -# include "unop.hh" -# include "multop.hh" -# include "atomic_prop.hh" -# include "constant.hh" - -namespace spot -{ - namespace eltl - { - // Forward declaration. - struct automatop; - - /// \brief Formula visitor that can modify the formula. - /// \ingroup eltl_essential - /// - /// Writing visitors is the prefered way - /// to traverse a formula, since it doesn't - /// involve any cast. - /// - /// If you do not need to modify the visited formula, inherit from - /// spot::eltl:const_visitor instead. - struct visitor - { - virtual ~visitor() {} - virtual void visit(atomic_prop* node) = 0; - virtual void visit(constant* node) = 0; - virtual void visit(binop* node) = 0; - virtual void visit(unop* node) = 0; - virtual void visit(multop* node) = 0; - virtual void visit(automatop* node) = 0; - }; - - /// \brief Formula visitor that cannot modify the formula. - /// - /// Writing visitors is the prefered way - /// to traverse a formula, since it doesn't - /// involve any cast. - /// - /// If you want to modify the visited formula, inherit from - /// spot::eltl:visitor instead. - struct const_visitor - { - virtual ~const_visitor() {} - virtual void visit(const atomic_prop* node) = 0; - virtual void visit(const constant* node) = 0; - virtual void visit(const binop* node) = 0; - virtual void visit(const unop* node) = 0; - virtual void visit(const multop* node) = 0; - virtual void visit(const automatop* node) = 0; - }; - - } -} - -#endif // SPOT_ELTLAST_VISITOR_HH diff --git a/src/eltlparse/eltlparse.yy b/src/eltlparse/eltlparse.yy index 9a0980722..bf00b4334 100644 --- a/src/eltlparse/eltlparse.yy +++ b/src/eltlparse/eltlparse.yy @@ -22,10 +22,11 @@ %{ #include #include +#include #include #include #include "public.hh" -#include "eltlast/allnodes.hh" +#include "eltlast/automatop.hh" // Implementation detail for error handling. namespace spot @@ -87,7 +88,8 @@ using namespace spot::eltl; OP_IMPLIES "implication operator" OP_EQUIV "equivalent operator" -%token EQ "=" +%token ACC "accept" + EQ "=" LPAREN "(" RPAREN ")" COMMA "," @@ -131,6 +133,7 @@ nfa_list: /* empty. */ nfa: IDENT "=" "(" nfa_def ")" { nmap[*$1] = nfa::ptr($4); + delete $1; } ; @@ -142,7 +145,8 @@ nfa_def: /* empty. */ { errno = 0; long i = strtol($4->c_str(), 0, 10); - if (i > INT_MAX || i < INT_MIN || errno == ERANGE) + if (i > std::numeric_limits::max() || + i < std::numeric_limits::min() || errno == ERANGE) { std::string s = "out of range integer `"; s += *$4; @@ -156,7 +160,12 @@ nfa_def: /* empty. */ $1->add_transition(*$2, *$3, i); $$ = $1; } - | nfa_def EQ STATE + | nfa_def STATE STATE CONST_TRUE + { + $1->add_transition(*$2, *$3, -1); + $$ = $1; + } + | nfa_def ACC STATE { $1->set_final(*$3); } diff --git a/src/eltlparse/eltlscan.ll b/src/eltlparse/eltlscan.ll index 767213c7d..a54f5491c 100644 --- a/src/eltlparse/eltlscan.ll +++ b/src/eltlparse/eltlscan.ll @@ -59,6 +59,10 @@ eol \n|\r|\n\r|\r\n /* 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); diff --git a/src/eltlparse/public.hh b/src/eltlparse/public.hh index 6813ce66c..19eafdb10 100644 --- a/src/eltlparse/public.hh +++ b/src/eltlparse/public.hh @@ -23,7 +23,6 @@ # define SPOT_ELTLPARSE_PUBLIC_HH # include "eltlast/formula.hh" -# include "eltlast/visitor.hh" // Unfortunately Bison 2.3 uses the same guards in all parsers :( # undef BISON_LOCATION_HH # undef BISON_POSITION_HH diff --git a/src/eltltest/acc.test b/src/eltltest/acc.test index fc9e5aaaf..6080022f0 100755 --- a/src/eltltest/acc.test +++ b/src/eltltest/acc.test @@ -4,9 +4,9 @@ set -e cat >prelude <input <input <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 new file mode 100644 index 000000000..4b73669e7 --- /dev/null +++ b/src/eltlvisit/clone.hh @@ -0,0 +1,64 @@ +// 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/eltlast/unop.hh b/src/eltlvisit/destroy.cc similarity index 76% rename from src/eltlast/unop.hh rename to src/eltlvisit/destroy.cc index 73ff7bf0e..b0c9706d0 100644 --- a/src/eltlast/unop.hh +++ b/src/eltlvisit/destroy.cc @@ -19,24 +19,24 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -/// \file eltlast/unop.hh -/// \brief ELTL unary operators -#ifndef SPOT_ELTLAST_UNOP_HH -# define SPOT_ELTLAST_UNOP_HH - -# include "formula.hh" -# include "internal/unop.hh" +#include "eltlvisit/destroy.hh" +#include "eltlvisit/clone.hh" namespace spot { namespace eltl { + void + destroy_visitor::doit_default(formula* c) + { + formula::unref(c); + } - /// \brief Unary operators. - /// \ingroup eltl_ast - typedef spot::internal::unop unop; - + void + destroy(const formula* f) + { + destroy_visitor v; + const_cast(f)->accept(v); + } } } - -#endif // SPOT_ELTLAST_UNOP_HH diff --git a/src/eltlast/constant.hh b/src/eltlvisit/destroy.hh similarity index 52% rename from src/eltlast/constant.hh rename to src/eltlvisit/destroy.hh index 17a04a97c..8f15bed71 100644 --- a/src/eltlast/constant.hh +++ b/src/eltlvisit/destroy.hh @@ -1,5 +1,5 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// 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. @@ -19,24 +19,32 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -/// \file eltlast/constant.hh -/// \brief ELTL constants -#ifndef SPOT_ELTLAST_CONSTANT_HH -# define SPOT_ELTLAST_CONSTANT_HH +#ifndef SPOT_ELTLVISIT_DESTROY_HH +# define SPOT_ELTLVISIT_DESTROY_HH -# include "formula.hh" -# include "internal/constant.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 A constant (True or False) - /// \ingroup eltl_ast - typedef spot::internal::constant constant; - + /// \brief Destroys a formula + /// \ingroup eltl_essential + void destroy(const formula *f); } } -#endif // SPOT_ELTLAST_CONSTANT_HH +#endif // SPOT_ELTLVISIT_DESTROY_HH diff --git a/src/eltlvisit/lunabbrev.cc b/src/eltlvisit/lunabbrev.cc new file mode 100644 index 000000000..ee317d3d3 --- /dev/null +++ b/src/eltlvisit/lunabbrev.cc @@ -0,0 +1,96 @@ +// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#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 new file mode 100644 index 000000000..954d22d1d --- /dev/null +++ b/src/eltlvisit/lunabbrev.hh @@ -0,0 +1,68 @@ +// 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 new file mode 100644 index 000000000..6df9f3982 --- /dev/null +++ b/src/eltlvisit/nenoform.cc @@ -0,0 +1,187 @@ +// 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 new file mode 100644 index 000000000..e516cf9f5 --- /dev/null +++ b/src/eltlvisit/nenoform.hh @@ -0,0 +1,51 @@ +// 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 new file mode 100644 index 000000000..030218c1b --- /dev/null +++ b/src/eltlvisit/postfix.cc @@ -0,0 +1,125 @@ +// 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/eltlast/refformula.hh b/src/eltlvisit/postfix.hh similarity index 50% rename from src/eltlast/refformula.hh rename to src/eltlvisit/postfix.hh index cd5d9db82..25b2925a7 100644 --- a/src/eltlast/refformula.hh +++ b/src/eltlvisit/postfix.hh @@ -19,24 +19,43 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -/// \file eltlast/refformula.hh -/// \brief Reference-counted ELTL formulae -#ifndef SPOT_ELTLAST_REFFORMULA_HH -# define SPOT_ELTLAST_REFFORMULA_HH +#ifndef SPOT_ELTLVISIT_POSTFIX_HH +# define SPOT_ELTLVISIT_POSTFIX_HH -# include "formula.hh" -# include "internal/refformula.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(); - /// \brief A reference-counted ELTL formula. - /// \ingroup eltl_ast - typedef spot::internal::ref_formula ref_formula; + 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_ELTLAST_REFFORMULA_HH +#endif // SPOT_ELTLVISIT_POSTFIX_HH diff --git a/src/eltlvisit/tostring.cc b/src/eltlvisit/tostring.cc new file mode 100644 index 000000000..8caf27b65 --- /dev/null +++ b/src/eltlvisit/tostring.cc @@ -0,0 +1,198 @@ +// 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/eltlast/binop.hh b/src/eltlvisit/tostring.hh similarity index 58% rename from src/eltlast/binop.hh rename to src/eltlvisit/tostring.hh index 8b78e3271..35dcb603f 100644 --- a/src/eltlast/binop.hh +++ b/src/eltlvisit/tostring.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -19,27 +19,30 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -/// \file eltlast/binop.hh -/// \brief ELTL binary operators -/// -/// This does not include \c AND and \c OR operators. These are -/// considered to be multi-operand operators (see spot::eltl::multop). -#ifndef SPOT_ELTLAST_BINOP_HH -# define SPOT_ELTLAST_BINOP_HH +#ifndef SPOT_ELTLVISIT_TOSTRING_HH +# define SPOT_ELTLVISIT_TOSTRING_HH -# include "formula.hh" -# include "internal/binop.hh" +#include +#include "eltlast/formula.hh" namespace spot { namespace eltl { + /// \addtogroup eltl_io + /// @{ - /// \brief Binary operator. - /// \ingroup eltl_ast - typedef spot::internal::binop binop; + /// \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_ELTLAST_BINOP_HH +#endif // SPOT_ELTLVISIT_TOSTRING_HH diff --git a/src/evtgbaalgos/tgba2evtgba.cc b/src/evtgbaalgos/tgba2evtgba.cc index 65789a99c..947f19daa 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 ltl::formula* v = + const internal::base_formula* v = automata_->get_dict()->var_formula_map[bdd_var(one)]; res->add_transition(name_[in], - to_string(v), + v->to_string(), ss, name_[out]); break; @@ -121,8 +121,8 @@ namespace spot bdd low = bdd_low(one); if (low == bddfalse) { - const ltl::formula* v = - automata_->get_dict()->acc_formula_map[bdd_var(one)]; + const ltl::formula* v = dynamic_cast( + 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 2777caf74..cdf7770de 100644 --- a/src/evtgbatest/ltl2evtgba.cc +++ b/src/evtgbatest/ltl2evtgba.cc @@ -24,7 +24,6 @@ #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 index 2b43a9062..3aa55fabe 100644 --- a/src/internal/Makefile.am +++ b/src/internal/Makefile.am @@ -19,9 +19,13 @@ ## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA ## 02111-1307, USA. -internaldir = $(pkgincludedir)/libinternal +AM_CPPFLAGS = -I$(srcdir)/.. +AM_CXXFLAGS = $(WARNING_CXXFLAGS) + +internaldir = $(pkgincludedir)/internal internal_HEADERS = \ + baseformula.hh \ refformula.hh \ refformula.hxx \ formula.hh \ @@ -42,3 +46,7 @@ internal_HEADERS = \ declenv.hh \ declenv.hxx \ environment.hh + +noinst_LTLIBRARIES = libinternal.la +libinternal_la_SOURCES = \ + baseformula.cc diff --git a/src/eltlast/multop.hh b/src/internal/baseformula.cc similarity index 57% rename from src/eltlast/multop.hh rename to src/internal/baseformula.cc index 70a1ac72c..0b27b261b 100644 --- a/src/eltlast/multop.hh +++ b/src/internal/baseformula.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) 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. @@ -19,26 +19,38 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -/// \file eltlast/multop.hh -/// \brief ELTL multi-operand operators -#ifndef SPOT_ELTLAST_MULTOP_HH -# define SPOT_ELTLAST_MULTOP_HH - -# include "formula.hh" -# include "internal/multop.hh" +#include +#include "baseformula.hh" namespace spot { - namespace eltl + namespace internal { + std::string + base_formula::to_string() const + { + std::ostringstream os; + to_string(os); + return os.str(); + } - /// \brief Multi-operand operators. - /// \ingroup eltl_ast - /// - /// These operators are considered commutative and associative. - typedef spot::internal::multop multop; + const std::string& + base_formula::dump() const + { + return dump_; + } + size_t + base_formula::hash() const + { + return hash_key_; + } + + void + base_formula::set_key_() + { + string_hash sh; + hash_key_ = sh(dump_); + } } } - -#endif // SPOT_ELTLAST_MULTOP_HH diff --git a/src/internal/baseformula.hh b/src/internal/baseformula.hh new file mode 100644 index 000000000..9cfe24dd0 --- /dev/null +++ b/src/internal/baseformula.hh @@ -0,0 +1,119 @@ +// 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/formula.hh b/src/internal/formula.hh index e0f3ca787..bd0a8d9ef 100644 --- a/src/internal/formula.hh +++ b/src/internal/formula.hh @@ -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, 2008 Laboratoire d'Informatique de +// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -24,10 +24,8 @@ #ifndef SPOT_INTERNAL_FORMULA_HH # define SPOT_INTERNAL_FORMULA_HH -# include -# include # include "predecl.hh" -# include "misc/hash.hh" +# include "baseformula.hh" namespace spot { @@ -40,12 +38,16 @@ namespace spot /// The only way you can work with a formula is to /// build a T::visitor or T::const_visitor. template - class formula : public T + 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. @@ -65,16 +67,6 @@ namespace spot /// this method directly as it doesn't touch the children. If you /// want to release a whole formula, use a destroy() visitor instead. static void unref(formula* f); - - /// Return a canonic representation of the formula - const std::string& dump() const; - - /// Return a hash_key for the formula. - size_t - hash() const - { - return hash_key_; - } protected: virtual ~formula(); @@ -83,77 +75,7 @@ namespace spot /// \brief decrement reference counter if any, return true when /// the instance must be deleted (usually when the counter hits 0). virtual bool unref_(); - - /// \brief Compute key_ from dump_. - /// - /// Should be called once in each object, after dump_ has been set. - void set_key_(); - /// The canonic representation of the formula - std::string dump_; - /// \brief The hash key of this formula. - /// - /// Initialized by set_key_(). - size_t hash_key_; }; - - /// \brief Strict Weak Ordering for const formula*. - /// \ingroup generic_essentials - /// - /// This is meant to be used as a comparison functor for - /// STL \c map whose key are of type const formula*. - /// - /// For instance here is how one could declare - /// a map of \c const::formula*. - /// \code - /// // Remember how many times each formula has been seen. - /// template - /// std::map*, int, - /// spot::internal::formula_ptr_less_than > seen; - /// \endcode - template - struct formula_ptr_less_than: - public std::binary_function*, const formula*, bool> - { - bool - operator()(const formula* left, const formula* right) const - { - assert(left); - assert(right); - size_t l = left->hash(); - size_t r = right->hash(); - if (1 != r) - return l < r; - return left->dump() < right->dump(); - } - }; - - /// \brief Hash Function for const formula*. - /// \ingroup generic_essentials - /// \ingroup hash_funcs - /// - /// This is meant to be used as a hash functor for - /// Sgi's \c hash_map whose key are of type const formula*. - /// - /// For instance here is how one could declare - /// a map of \c const::formula*. - /// \code - /// // Remember how many times each formula has been seen. - /// template - /// Sgi::hash_map*, int, - /// const spot::internal::formula_ptr_hash > seen; - /// \endcode - template - struct formula_ptr_hash: - public std::unary_function*, size_t> - { - size_t - operator()(const formula* that) const - { - assert(that); - return that->hash(); - } - }; - } } diff --git a/src/internal/formula.hxx b/src/internal/formula.hxx index 0634cba5e..c0fcf0def 100644 --- a/src/internal/formula.hxx +++ b/src/internal/formula.hxx @@ -67,18 +67,24 @@ namespace spot } template - const std::string& - formula::dump() const + base_formula* + formula::clone() const { - return dump_; + return T::clone_(this); + } + + template + std::ostream& + formula::to_string(std::ostream& os) const + { + return T::to_string_(this, os); } template void - formula::set_key_() + formula::destroy() const { - string_hash sh; - hash_key_ = sh(dump_); + T::destroy_(this); } } } diff --git a/src/internal/multop.hxx b/src/internal/multop.hxx index 72dac2bca..479e51dad 100644 --- a/src/internal/multop.hxx +++ b/src/internal/multop.hxx @@ -150,7 +150,7 @@ namespace spot v->insert(v->end(), inlined.begin(), inlined.end()); } - std::sort(v->begin(), v->end(), formula_ptr_less_than()); + std::sort(v->begin(), v->end(), formula_ptr_less_than()); // Remove duplicates. We can't use std::unique(), because we // must destroy() any formula we drop. diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index 8c40ad4ad..f631e9e31 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -64,14 +64,43 @@ 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 + /// \ingroup ltl_ast + /// + /// 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 { typedef spot::ltl::visitor visitor; typedef spot::ltl::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, U, R }; const char* binop_name(binop op) const { @@ -113,18 +142,8 @@ namespace spot } }; - /// \brief An LTL formula. - /// \ingroup ltl_essential - /// \ingroup ltl_ast - /// - /// 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; - - typedef spot::internal::formula_ptr_less_than formula_ptr_less_than; - typedef spot::internal::formula_ptr_hash formula_ptr_hash; - - + 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 diff --git a/src/ltlvisit/destroy.cc b/src/ltlvisit/destroy.cc index 131136d42..4a6210d3d 100644 --- a/src/ltlvisit/destroy.cc +++ b/src/ltlvisit/destroy.cc @@ -25,17 +25,10 @@ namespace spot { namespace ltl { - namespace + void + destroy_visitor::doit_default(formula* c) { - class destroy_visitor: public postfix_visitor - { - public: - virtual void - doit_default(formula* c) - { - formula::unref(c); - } - }; + formula::unref(c); } void diff --git a/src/ltlvisit/destroy.hh b/src/ltlvisit/destroy.hh index 7b076fc01..a0223bde9 100644 --- a/src/ltlvisit/destroy.hh +++ b/src/ltlvisit/destroy.hh @@ -28,6 +28,19 @@ 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/tgba/bdddict.cc b/src/tgba/bdddict.cc index a29c69fa0..5c1b0a23a 100644 --- a/src/tgba/bdddict.cc +++ b/src/tgba/bdddict.cc @@ -25,7 +25,6 @@ #include #include #include -#include #include #include "bdddict.hh" @@ -47,7 +46,8 @@ namespace spot } int - bdd_dict::register_proposition(const ltl::formula* f, const void* for_me) + bdd_dict::register_proposition(const internal::base_formula* f, + const void* for_me) { int num; // Do not build a variable that already exists. @@ -58,7 +58,7 @@ namespace spot } else { - f = clone(f); + f = f->clone(); num = allocate_variables(1); var_map[f] = num; var_formula_map[num] = f; @@ -82,7 +82,8 @@ namespace spot } int - bdd_dict::register_state(const ltl::formula* f, const void* for_me) + bdd_dict::register_state(const internal::base_formula* f, + const void* for_me) { int num; // Do not build a state that already exists. @@ -93,7 +94,7 @@ namespace spot } else { - f = ltl::clone(f); + f = f->clone(); num = allocate_variables(2); now_map[f] = num; now_formula_map[num] = f; @@ -107,8 +108,8 @@ namespace spot } int - bdd_dict::register_acceptance_variable(const ltl::formula* f, - const void* for_me) + bdd_dict::register_acceptance_variable(const internal::base_formula* f, + const void* for_me) { int num; // Do not build an acceptance variable that already exists. @@ -119,7 +120,7 @@ namespace spot } else { - f = clone(f); + f = f->clone(); num = allocate_variables(1); acc_map[f] = num; acc_formula_map[num] = f; @@ -150,13 +151,14 @@ namespace spot assert(i != acc_formula_map.end()); std::ostringstream s; // FIXME: We could be smarter and reuse unused "$n" numbers. - s << ltl::to_string(i->second) << "$" + s << i->second->to_string() + << "$" << ++clone_counts[var]; - ltl::formula* f = + internal::base_formula* f = ltl::atomic_prop::instance(s.str(), ltl::default_environment::instance()); int res = register_acceptance_variable(f, for_me); - ltl::destroy(f); + f->destroy(); return res; } @@ -233,7 +235,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 ltl::formula* f = 0; + const internal::base_formula* f = 0; vf_map::iterator vi = var_formula_map.find(var); if (vi != var_formula_map.end()) { @@ -278,7 +280,7 @@ namespace spot // formula itself. release_variables(var, n); if (f) - ltl::destroy(f); + f->destroy(); var_refs.erase(cur); } @@ -297,7 +299,8 @@ namespace spot } bool - bdd_dict::is_registered_proposition(const ltl::formula* f, const void* by_me) + bdd_dict::is_registered_proposition(const internal::base_formula* f, + const void* by_me) { fv_map::iterator fi = var_map.find(f); if (fi == var_map.end()) @@ -307,7 +310,8 @@ namespace spot } bool - bdd_dict::is_registered_state(const ltl::formula* f, const void* by_me) + bdd_dict::is_registered_state(const internal::base_formula* f, + const void* by_me) { fv_map::iterator fi = now_map.find(f); if (fi == now_map.end()) @@ -317,7 +321,7 @@ namespace spot } bool - bdd_dict::is_registered_acceptance_variable(const ltl::formula* f, + bdd_dict::is_registered_acceptance_variable(const internal::base_formula* f, const void* by_me) { fv_map::iterator fi = acc_map.find(f); @@ -336,23 +340,23 @@ namespace spot { os << " " << fi->second << " (x" << var_refs.find(fi->second)->second.size() << "): "; - to_string(fi->first, os) << std::endl; + fi->first->to_string(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["; - to_string(fi->first, os) << "]" << std::endl; + fi->first->to_string(os) << "]" << std::endl; os << " " << fi->second + 1 << " (x" << refs << "): Next["; - to_string(fi->first, os) << "]" << std::endl; + fi->first->to_string(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["; - to_string(fi->first, os) << "]" << std::endl; + fi->first->to_string(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 434d77703..0861a598b 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 "ltlast/formula.hh" +#include "internal/baseformula.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,7 +77,8 @@ namespace spot /// /// \return The variable number. Use bdd_ithvar() or bdd_nithvar() /// to convert this to a BDD. - int register_proposition(const ltl::formula* f, const void* for_me); + int + register_proposition(const internal::base_formula* f, const void* for_me); /// \brief Register BDD variables as atomic propositions. /// @@ -99,7 +100,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 ltl::formula* f, const void* for_me); + int register_state(const internal::base_formula* f, const void* for_me); /// \brief Register an atomic proposition. /// @@ -111,7 +112,8 @@ namespace spot /// /// \return The variable number. Use bdd_ithvar() or bdd_nithvar() /// to convert this to a BDD. - int register_acceptance_variable(const ltl::formula* f, const void* for_me); + int register_acceptance_variable(const internal::base_formula* f, + const void* for_me); /// \brief Clone an acceptance variable VAR for FOR_ME. /// @@ -156,9 +158,12 @@ namespace spot /// @{ /// Check whether formula \a f has already been registered by \a by_me. - 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, + 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, const void* by_me); /// @} diff --git a/src/tgba/bddprint.cc b/src/tgba/bddprint.cc index 4be59eb21..9b90fd4ff 100644 --- a/src/tgba/bddprint.cc +++ b/src/tgba/bddprint.cc @@ -23,9 +23,7 @@ #include #include #include "bddprint.hh" -#include "ltlvisit/tostring.hh" #include "formula2bdd.hh" -#include "ltlvisit/destroy.hh" namespace spot { @@ -42,7 +40,7 @@ namespace spot bdd_dict::vf_map::const_iterator isi = dict->var_formula_map.find(var); if (isi != dict->var_formula_map.end()) - to_string(isi->second, o); + isi->second->to_string(o); else { isi = dict->acc_formula_map.find(var); @@ -51,12 +49,12 @@ namespace spot if (want_acc) { o << "Acc["; - to_string(isi->second, o) << "]"; + isi->second->to_string(o) << "]"; } else { o << "\""; - to_string(isi->second, o) << "\""; + isi->second->to_string(o) << "\""; } } else @@ -64,14 +62,14 @@ namespace spot isi = dict->now_formula_map.find(var); if (isi != dict->now_formula_map.end()) { - o << "Now["; to_string(isi->second, o) << "]"; + o << "Now["; isi->second->to_string(o) << "]"; } else { isi = dict->now_formula_map.find(var - 1); if (isi != dict->now_formula_map.end()) { - o << "Next["; to_string(isi->second, o) << "]"; + o << "Next["; isi->second->to_string(o) << "]"; } else { diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index a7cd8f791..519e80b87 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -162,7 +162,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(isi->second); + formula* res = clone(dynamic_cast(isi->second)); bdd high = bdd_high(b); if (high == bddfalse) diff --git a/src/tgba/tgbabddconcretefactory.cc b/src/tgba/tgbabddconcretefactory.cc index 0d04023ae..acc5bc3c2 100644 --- a/src/tgba/tgbabddconcretefactory.cc +++ b/src/tgba/tgbabddconcretefactory.cc @@ -19,9 +19,8 @@ // 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) @@ -33,12 +32,12 @@ namespace spot { acc_map_::iterator ai; for (ai = acc_.begin(); ai != acc_.end(); ++ai) - destroy(ai->first); + ai->first->destroy(); get_dict()->unregister_all_my_variables(this); } int - tgba_bdd_concrete_factory::create_state(const ltl::formula* f) + tgba_bdd_concrete_factory::create_state(const internal::base_formula* f) { int num = get_dict()->register_state(f, this); // Keep track of all "Now" variables for easy @@ -48,7 +47,7 @@ namespace spot } int - tgba_bdd_concrete_factory::create_atomic_prop(const ltl::formula* f) + tgba_bdd_concrete_factory::create_atomic_prop(const internal::base_formula* f) { int num = get_dict()->register_proposition(f, this); // Keep track of all atomic proposition for easy @@ -58,8 +57,9 @@ namespace spot } void - tgba_bdd_concrete_factory::declare_acceptance_condition(bdd b, - const ltl::formula* a) + tgba_bdd_concrete_factory::declare_acceptance_condition( + bdd b, + const internal::base_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 = clone(a); + a = a->clone(); acc_[a] = b; } else diff --git a/src/tgba/tgbabddconcretefactory.hh b/src/tgba/tgbabddconcretefactory.hh index a2c987e30..c65a99584 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 "ltlast/formula.hh" +#include "internal/baseformula.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 ltl::formula* f); + int create_state(const internal::base_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 ltl::formula* f); + int create_atomic_prop(const internal::base_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 ltl::formula* a); + void declare_acceptance_condition(bdd b, const internal::base_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/tgbatba.cc b/src/tgba/tgbatba.cc index 938e34833..e07e96490 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, 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. // @@ -23,6 +23,7 @@ #include "tgbatba.hh" #include "bddprint.hh" #include "misc/hashfunc.hh" +#include "ltlast/formula.hh" namespace spot { diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 1b814093c..88a9e891c 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -31,6 +31,7 @@ tgbaalgos_HEADERS = \ dotty.hh \ dottydec.hh \ dupexp.hh \ + eltl2tgba_lacim.hh \ emptiness.hh \ emptiness_stats.hh \ gv04.hh \ @@ -60,6 +61,7 @@ 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 new file mode 100644 index 000000000..7ad6e4799 --- /dev/null +++ b/src/tgbaalgos/eltl2tgba_lacim.cc @@ -0,0 +1,188 @@ +// 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 new file mode 100644 index 000000000..732822cee --- /dev/null +++ b/src/tgbaalgos/eltl2tgba_lacim.hh @@ -0,0 +1,55 @@ +// 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 d73d48a34..7d9e5bd57 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -64,7 +64,7 @@ namespace spot { fv_map::iterator i; for (i = next_map.begin(); i != next_map.end(); ++i) - destroy(i->first); + destroy(dynamic_cast(i->first)); dict->unregister_all_my_variables(this); } @@ -125,7 +125,7 @@ namespace spot for (fi = next_map.begin(); fi != next_map.end(); ++fi) { os << " " << fi->second << ": Next["; - to_string(fi->first, os) << "]" << std::endl; + fi->first->to_string(os) << "]" << std::endl; } os << "Shared Dict:" << std::endl; dict->dump(os); @@ -137,13 +137,13 @@ namespace spot { vf_map::const_iterator isi = next_formula_map.find(var); if (isi != next_formula_map.end()) - return clone(isi->second); + return dynamic_cast(isi->second->clone()); isi = dict->acc_formula_map.find(var); if (isi != dict->acc_formula_map.end()) - return clone(isi->second); + return dynamic_cast(isi->second->clone()); isi = dict->var_formula_map.find(var); if (isi != dict->var_formula_map.end()) - return clone(isi->second); + return dynamic_cast(isi->second->clone()); assert(0); // Never reached, but some GCC versions complain about // a missing return otherwise. diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc index 13bc00763..5cb522415 100644 --- a/src/tgbaalgos/save.cc +++ b/src/tgbaalgos/save.cc @@ -84,7 +84,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 = ltl::to_string(vi->second); + std::string s = vi->second->to_string(); if (dynamic_cast(vi->second) && s[0] == '"') { diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index b3ec54301..8ae792cb3 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 +noinst_PROGRAMS = ltl2tgba randtgba eltl2tgba check_SCRIPTS = defs # Keep this sorted alphabetically. @@ -46,6 +46,7 @@ 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 @@ -85,7 +86,8 @@ TESTS = \ emptchke.test \ dfs.test \ emptchkr.test \ - spotlbtt.test + spotlbtt.test \ + eltl2tgba.test EXTRA_DIST = $(TESTS) diff --git a/src/eltlast/atomic_prop.hh b/src/tgbatest/eltl2tgba.cc similarity index 53% rename from src/eltlast/atomic_prop.hh rename to src/tgbatest/eltl2tgba.cc index 2e03cd0f3..ac4722250 100644 --- a/src/eltlast/atomic_prop.hh +++ b/src/tgbatest/eltl2tgba.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 +// 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,24 +19,32 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -/// \file eltlast/atomic_prop.hh -/// \brief ELTL atomic propositions -#ifndef SPOT_ELTLAST_ATOMIC_PROP_HH -# define SPOT_ELTLAST_ATOMIC_PROP_HH +#include +#include +#include "eltlparse/public.hh" +#include "tgbaalgos/eltl2tgba_lacim.hh" +#include "tgbaalgos/dotty.hh" -# include "formula.hh" -# include "internal/atomic_prop.hh" - -namespace spot +int +main(int argc, char** argv) { - namespace eltl + 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)) { - - /// \brief Atomic propositions. - /// \ingroup eltl_ast - typedef spot::internal::atomic_prop atomic_prop; - + if (f != 0) + std::cout << f->dump() << std::endl; + return 1; } -} -#endif // SPOT_ELTLAST_ATOMICPROP_HH + 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 new file mode 100755 index 000000000..ba1efa07d --- /dev/null +++ b/src/tgbatest/eltl2tgba.test @@ -0,0 +1,40 @@ +#!/bin/sh + +. ./defs || exit -1 +set -e + +check () +{ + run 0 ./eltl2tgba "$1" || exit 1 +} + +cat >input <input1 <input <