From 2fbcd7e52f5c0f40a1759a1666401cd487886f6a Mon Sep 17 00:00:00 2001 From: Damien Lefortier Date: Mon, 2 Mar 2009 17:31:12 +0100 Subject: [PATCH] Add support for ELTL (AST & parser), and an adaptation of LaCIM for ELTL. This is a new version of the work started in 2008 with LTL and ELTL formulae now sharing the same class hierarchy. * configure.ac: Adjust for src/eltlparse/ and src/eltltest/ directories, and call AX_BOOST_BASE. * m4/boost.m4: New file defining AX_BOOST_BASE([MINIMUM-VERSION]). * src/Makefile.am: Add eltlparse and eltltest. * src/eltlparse/: New directory. Contains the ELTL parser. * src/eltltest/: New directory. Contains tests related to ELTL (parser and AST). * src/ltlast/Makefile.am: Adjust for ELTL AST files. * src/ltlast/automatop.cc, src/ltlast/automatop.hh: New files. Represent automaton operators nodes used in ELTL ASTs. * src/ltlast/nfa.cc, src/ltlast/nfa.hh: New files. Represent simple NFAs used internally by automatop nodes. * src/ltlast/allnode.hh, src/ltlast/predecl.hh, src/ltlast/visitor.hh: Adjust for automatop. * src/ltlvisit/basicreduce.cc, src/ltlvisit/clone.cc, src/ltlvisit/clone.hh, src/ltlvisit/contain.cc, src/ltlvisit/dotty.cc, src/ltlvisit/nenoform.cc, src/ltlvisit/postfix.cc, src/ltlvisit/postfix.hh, src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc: Because LTL and ELTL formulae share the same class hierarchy, LTL visitors need to handle automatop nodes to compile. When it's meaningful the visitor applies on automatop nodes or simply assert(0) otherwise. * src/tgba/tgbabddconcretefactory.cc (create_anonymous_state), src/tgba/tgbabddconcretefactory.hh (create_anonymous_state): New function used by the LaCIM translation algorithm for ELTL. * src/tgbaalgos/Makefile.am: Adjust for eltl2tgba_lacim* files. * src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/eltl2tgba_lacim.hh: New files. Implementation of the LaCIM translation algorithm for ELTL. * src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc: Handle automatop nodes in the translation by an assert(0). * src/tgbatest/Makefile.am: Adjust for eltl2tgba.* files. * src/src/tgbatest/eltl2tgba.cc, src/tgbatest/eltl2tgba.test: New files --- ChangeLog | 41 ++++ configure.ac | 4 + m4/boost.m4 | 194 ++++++++++++++++++ src/Makefile.am | 5 +- src/eltlparse/Makefile.am | 62 ++++++ src/eltlparse/eltlparse.yy | 318 +++++++++++++++++++++++++++++ src/eltlparse/eltlscan.ll | 208 +++++++++++++++++++ src/eltlparse/fmterror.cc | 48 +++++ src/eltlparse/parsedecl.hh | 44 ++++ src/eltlparse/public.hh | 100 +++++++++ src/eltltest/Makefile.am | 44 ++++ src/eltltest/acc.cc | 42 ++++ src/eltltest/acc.test | 44 ++++ src/eltltest/defs.in | 75 +++++++ src/eltltest/nfa.cc | 57 ++++++ src/eltltest/nfa.test | 6 + src/ltlast/Makefile.am | 4 + src/ltlast/allnodes.hh | 1 + src/ltlast/automatop.cc | 108 ++++++++++ src/ltlast/automatop.hh | 98 +++++++++ src/ltlast/nfa.cc | 145 +++++++++++++ src/ltlast/nfa.hh | 148 ++++++++++++++ src/ltlast/predecl.hh | 1 + src/ltlast/visitor.hh | 2 + src/ltlvisit/basicreduce.cc | 6 + src/ltlvisit/clone.cc | 9 + src/ltlvisit/clone.hh | 1 + src/ltlvisit/contain.cc | 6 + src/ltlvisit/dotty.cc | 6 + src/ltlvisit/nenoform.cc | 15 ++ src/ltlvisit/postfix.cc | 15 ++ src/ltlvisit/postfix.hh | 2 + src/ltlvisit/reduce.cc | 6 + src/ltlvisit/syntimpl.cc | 18 ++ src/ltlvisit/tostring.cc | 42 ++++ src/tgba/formula2bdd.cc | 6 + src/tgba/tgbabddconcretefactory.cc | 12 ++ src/tgba/tgbabddconcretefactory.hh | 6 + src/tgbaalgos/Makefile.am | 2 + src/tgbaalgos/eltl2tgba_lacim.cc | 261 +++++++++++++++++++++++ src/tgbaalgos/eltl2tgba_lacim.hh | 55 +++++ src/tgbaalgos/ltl2tgba_fm.cc | 12 ++ src/tgbaalgos/ltl2tgba_lacim.cc | 6 + src/tgbatest/Makefile.am | 4 +- src/tgbatest/eltl2tgba.cc | 109 ++++++++++ src/tgbatest/eltl2tgba.test | 114 +++++++++++ 46 files changed, 2509 insertions(+), 3 deletions(-) create mode 100644 m4/boost.m4 create mode 100644 src/eltlparse/Makefile.am create mode 100644 src/eltlparse/eltlparse.yy create mode 100644 src/eltlparse/eltlscan.ll create mode 100644 src/eltlparse/fmterror.cc create mode 100644 src/eltlparse/parsedecl.hh create mode 100644 src/eltlparse/public.hh create mode 100644 src/eltltest/Makefile.am create mode 100644 src/eltltest/acc.cc create mode 100755 src/eltltest/acc.test create mode 100644 src/eltltest/defs.in create mode 100644 src/eltltest/nfa.cc create mode 100755 src/eltltest/nfa.test create mode 100644 src/ltlast/automatop.cc create mode 100644 src/ltlast/automatop.hh create mode 100644 src/ltlast/nfa.cc create mode 100644 src/ltlast/nfa.hh create mode 100644 src/tgbaalgos/eltl2tgba_lacim.cc create mode 100644 src/tgbaalgos/eltl2tgba_lacim.hh create mode 100644 src/tgbatest/eltl2tgba.cc create mode 100755 src/tgbatest/eltl2tgba.test diff --git a/ChangeLog b/ChangeLog index 40f9c9f54..368946824 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,44 @@ +2009-03-26 Damien Lefortier + + Add support for ELTL (AST & parser), and an adaptation of LaCIM + for ELTL. + + * configure.ac: Adjust for src/eltlparse/ and src/eltltest/ + directories, and call AX_BOOST_BASE. + * m4/boost.m4: New file defining AX_BOOST_BASE([MINIMUM-VERSION]). + * src/Makefile.am: Add eltlparse and eltltest. + * src/eltlparse/: New directory. Contains the ELTL parser. + * src/eltltest/: New directory. Contains tests related to + ELTL (parser and AST). + * src/ltlast/Makefile.am: Adjust for ELTL AST files. + * src/ltlast/automatop.cc, src/ltlast/automatop.hh: New files. + Represent automaton operators nodes used in ELTL ASTs. + * src/ltlast/nfa.cc, src/ltlast/nfa.hh: New files. Represent + simple NFAs used internally by automatop nodes. + * src/ltlast/allnode.hh, src/ltlast/predecl.hh, + src/ltlast/visitor.hh: Adjust for automatop. + * src/ltlvisit/basicreduce.cc, src/ltlvisit/clone.cc, + src/ltlvisit/clone.hh, src/ltlvisit/contain.cc, + src/ltlvisit/dotty.cc, src/ltlvisit/nenoform.cc, + src/ltlvisit/postfix.cc, src/ltlvisit/postfix.hh, + src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc, + src/ltlvisit/tostring.cc: Because LTL and ELTL formulae share the + same class hierarchy, LTL visitors need to handle automatop nodes + to compile. When it's meaningful the visitor applies on automatop + nodes or simply assert(0) otherwise. + * src/tgba/tgbabddconcretefactory.cc (create_anonymous_state), + src/tgba/tgbabddconcretefactory.hh (create_anonymous_state): New + function used by the LaCIM translation algorithm for ELTL. + * src/tgbaalgos/Makefile.am: Adjust for eltl2tgba_lacim* files. + * src/tgbaalgos/eltl2tgba_lacim.cc, + src/tgbaalgos/eltl2tgba_lacim.hh: New files. Implementation of + the LaCIM translation algorithm for ELTL. + * src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc: + Handle automatop nodes in the translation by an assert(0). + * src/tgbatest/Makefile.am: Adjust for eltl2tgba.* files. + * src/src/tgbatest/eltl2tgba.cc, src/tgbatest/eltl2tgba.test: New + files. + 2009-03-25 Alexandre Duret-Lutz * src/evtgbaparse/evtgbaparse.yy: Stay on 80 columns. diff --git a/configure.ac b/configure.ac index 8923f4eba..db8fe2478 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]) @@ -86,6 +87,9 @@ AC_CONFIG_FILES([ iface/nips/nipstest/Makefile iface/nips/nipstest/defs src/Makefile + src/eltlparse/Makefile + src/eltltest/Makefile + src/eltltest/defs 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..0586b3e8f --- /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 01e978131..4dda23ced 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -23,10 +23,10 @@ AUTOMAKE_OPTIONS = subdir-objects # List directories in the order they must be built. # Keep tests at the end. -SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse \ +SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse eltlparse \ tgba tgbaalgos tgbaparse \ evtgba evtgbaalgos evtgbaparse . \ - ltltest tgbatest evtgbatest sanity + ltltest eltltest tgbatest evtgbatest sanity lib_LTLIBRARIES = libspot.la libspot_la_SOURCES = @@ -37,6 +37,7 @@ libspot_la_LIBADD = \ ltlparse/libltlparse.la \ ltlvisit/libltlvisit.la \ ltlast/libltlast.la \ + eltlparse/libeltlparse.la \ tgba/libtgba.la \ tgbaalgos/libtgbaalgos.la \ tgbaparse/libtgbaparse.la \ diff --git a/src/eltlparse/Makefile.am b/src/eltlparse/Makefile.am new file mode 100644 index 000000000..713c02c78 --- /dev/null +++ b/src/eltlparse/Makefile.am @@ -0,0 +1,62 @@ +## Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +## département Systèmes Répartis Coopératifs (SRC), Université Pierre +## et Marie Curie. +## +## This file is part of Spot, a model checking library. +## +## Spot is free software; you can redistribute it and/or modify it +## under the terms of the GNU General Public License as published by +## the Free Software Foundation; either version 2 of the License, or +## (at your option) any later version. +## +## Spot is distributed in the hope that it will be useful, but WITHOUT +## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +## License for more details. +## +## You should have received a copy of the GNU General Public License +## along with Spot; see the file COPYING. If not, write to the Free +## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +## 02111-1307, USA. + +AM_CPPFLAGS = -I$(srcdir)/.. +AM_CXXFLAGS = #$(WARNING_CXXFLAGS) + +eltlparsedir = $(pkgincludedir)/eltlparse + +noinst_LTLIBRARIES = libeltlparse.la + +ELTLPARSE_YY = eltlparse.yy +FROM_ELTLPARSE_YY_MAIN = eltlparse.cc +FROM_ELTLPARSE_YY_OTHERS = \ + stack.hh \ + position.hh \ + location.hh \ + eltlparse.hh +FROM_ELTLPARSE_YY = $(FROM_ELTLPARSE_YY_MAIN) $(FROM_ELTLPARSE_YY_OTHERS) + +BUILT_SOURCES = $(FROM_ELTLPARSE_YY) +MAINTAINERCLEANFILES = $(FROM_ELTLPARSE_YY) + +$(FROM_ELTLPARSE_YY_MAIN): $(srcdir)/$(ELTLPARSE_YY) +## We must cd into $(srcdir) first because if we tell bison to read +## $(srcdir)/$(ELTLPARSE_YY), it will also use the value of $(srcdir)/ +## in the generated include statements. + cd $(srcdir) && \ + bison -Wall -Werror --report=all \ + $(ELTLPARSE_YY) -o $(FROM_ELTLPARSE_YY_MAIN) +$(FROM_ELTLPARSE_YY_OTHERS): $(ELTLPARSE_YY) + @test -f $@ || $(MAKE) $(AM_MAKEFLAGS) $(FROM_ELTLPARSE_YY_MAIN) + +EXTRA_DIST = $(ELTLPARSE_YY) + +libeltlparse_la_SOURCES = \ + fmterror.cc \ + $(FROM_ELTLPARSE_YY) \ + eltlscan.ll \ + parsedecl.hh + +eltlparse_HEADERS = \ + public.hh \ + location.hh \ + position.hh diff --git a/src/eltlparse/eltlparse.yy b/src/eltlparse/eltlparse.yy new file mode 100644 index 000000000..d3e1db6eb --- /dev/null +++ b/src/eltlparse/eltlparse.yy @@ -0,0 +1,318 @@ +/* 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. +*/ +%language "C++" +%locations +%defines +%name-prefix "eltlyy" +%debug +%error-verbose + +%code requires +{ +#include +#include +#include +#include +#include "public.hh" +#include "ltlast/allnodes.hh" +#include "ltlvisit/destroy.hh" + +// Implementation details 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))) +} + +%parse-param {spot::eltl::nfamap& nmap} +%parse-param {spot::eltl::parse_error_list_t &pe} +%parse-param {spot::ltl::environment &parse_environment} +%parse-param {spot::ltl::formula* &result} +%lex-param {spot::eltl::parse_error_list_t &pe} +%expect 0 +%pure-parser +%union +{ + int ival; + std::string* sval; + spot::ltl::nfa* nval; + spot::ltl::automatop::vec* aval; + spot::ltl::formula* fval; +} + +%code { +/* 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; +using namespace spot::ltl; +} + +/* All tokens. */ + +%token ATOMIC_PROP "atomic proposition" + IDENT "identifier" + +%token ARG "argument" + STATE "state" + OP_OR "or operator" + OP_XOR "xor operator" + OP_AND "and operator" + OP_IMPLIES "implication operator" + OP_EQUIV "equivalent operator" + OP_NOT "not 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" +%destructor { spot::ltl::destroy($$); } subformula + +%printer { debug_stream() << *$$; } "atomic proposition" + +%% + +result: nfa_list subformula + { + result = $2; + YYACCEPT; + } +; + +/* NFA definitions. */ + +nfa_list: /* empty. */ + | nfa_list nfa +; + +nfa: IDENT "=" "(" nfa_def ")" + { + $4->set_name(*$1); + nmap[*$1] = nfa::ptr($4); + delete $1; + } +; + +nfa_def: /* empty. */ + { + $$ = new nfa(); + } + | nfa_def STATE STATE ARG + { + if ($4 == -1 || $3 == -1 || $2 == -1) + { + std::string s = "out of range integer"; + PARSE_ERROR(@1, s); + YYERROR; + } + $1->add_transition($2, $3, $4); + $$ = $1; + } + | nfa_def STATE STATE CONST_TRUE + { + $1->add_transition($2, $3, -1); + $$ = $1; + } + | nfa_def ACC STATE + { + $1->set_final($3); + $$ = $1; + } +; + +/* 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; + delete $3; + YYERROR; + } + delete $1; + $$ = 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); } + | OP_NOT subformula + { $$ = unop::instance(unop::Not, $2); } +; + +arg_list: subformula + { + // TODO: delete it whenever a parse error occurs on a subformula. + $$ = new automatop::vec; + $$->push_back($1); + } + | arg_list "," subformula + { + $1->push_back($3); + $$ = $1; + } +; + +%% + +void +eltlyy::parser::error(const location_type& loc, const std::string& s) +{ + PARSE_ERROR(loc, s); +} + +namespace spot +{ + namespace eltl + { + formula* + parse_file(const std::string& name, + parse_error_list& error_list, + environment& env, + bool debug) + { + if (flex_open(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_; + flex_close(); + return result; + } + + formula* + parse_string(const std::string& eltl_string, + parse_error_list& error_list, + environment& env, + bool debug) + { + flex_scan_string(eltl_string.c_str()); + formula* result = 0; + nfamap nmap; + parse_error_list_t pe; + eltlyy::parser parser(nmap, pe, env, result); + parser.set_debug_level(debug); + parser.parse(); + error_list = pe.list_; + return result; + } + } +} + +// Local Variables: +// mode: c++ +// End: diff --git a/src/eltlparse/eltlscan.ll b/src/eltlparse/eltlscan.ll new file mode 100644 index 000000000..92ed586c6 --- /dev/null +++ b/src/eltlparse/eltlscan.ll @@ -0,0 +1,208 @@ +/* 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" + +static int _atoi (char* yytext, int base); + +#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]+ { + // Out of range is checked in the parser. + yylval->ival = _atoi(yytext, 10); + return token::STATE; + } + +$[0-9]+ { + // Out of range is checked in the parser. + yylval->ival = _atoi(++yytext, 10); + 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 + flex_open(const std::string &name) + { + if (name == "-") + yyin = stdin; + else + { + yyin = fopen(name.c_str(), "r"); + if (!yyin) + return 1; + } + return 0; + } + + void + flex_close() + { + fclose(yyin); + } + + void + flex_scan_string(const char* s) + { + yy_scan_string(s); + } + } +} + +static int +_atoi(char* yytext, int base) +{ + errno = 0; + long i = strtol(yytext, 0, base); + if (i > std::numeric_limits::max() || + i < std::numeric_limits::min() || errno == ERANGE) + return -1; + return i; +} diff --git a/src/eltlparse/fmterror.cc b/src/eltlparse/fmterror.cc new file mode 100644 index 000000000..b2e086f65 --- /dev/null +++ b/src/eltlparse/fmterror.cc @@ -0,0 +1,48 @@ +// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include "public.hh" + +namespace spot +{ + namespace eltl + { + bool + format_parse_errors(std::ostream& os, + parse_error_list& error_list) + { + bool printed = false; + spot::eltl::parse_error_list::iterator it; + for (it = error_list.begin(); it != error_list.end(); ++it) + { + if (it->second.first != "-") + { + os << it->second.first << ": "; + os << it->first << ": "; + } + os << it->second.second << std::endl; + printed = true; + } + return printed; + } + } +} diff --git a/src/eltlparse/parsedecl.hh b/src/eltlparse/parsedecl.hh new file mode 100644 index 000000000..ae3a6c8ee --- /dev/null +++ b/src/eltlparse/parsedecl.hh @@ -0,0 +1,44 @@ +// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_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 flex_open(const std::string& name); + void flex_close(); + void flex_scan_string(const char* s); + } +} + +#endif // SPOT_ELTLPARSE_PARSEDECL_HH diff --git a/src/eltlparse/public.hh b/src/eltlparse/public.hh new file mode 100644 index 000000000..f965ed64b --- /dev/null +++ b/src/eltlparse/public.hh @@ -0,0 +1,100 @@ +// 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 "ltlast/formula.hh" +// Unfortunately Bison 2.3 uses the same guards in all parsers :( +# undef BISON_LOCATION_HH +# undef BISON_POSITION_HH +# include "ltlenv/defaultenv.hh" +# include "ltlast/nfa.hh" +# include "eltlparse/location.hh" +# include +# include +# include +# include +# include + +namespace spot +{ + using namespace ltl; + + 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_file(const std::string& filename, + parse_error_list& error_list, + environment& env = default_environment::instance(), + bool debug = false); + + /// \brief Build a formula from an ELTL string. + /// \param eltl_string The string 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 formula built from \a eltl_string, or + /// 0 if the input was unparsable. + /// + /// \warning This function is not reentrant. + formula* parse_string(const std::string& eltl_string, + parse_error_list& error_list, + environment& env = default_environment::instance(), + bool debug = false); + + /// \brief Format diagnostics produced by spot::eltl::parse. + /// \param os Where diagnostics should be output. + /// \param eltl_string The string that were parsed. + /// \param error_list The error list filled by spot::eltl::parse while + /// parsing \a eltl_string. + /// \return \c true iff any diagnostic was output. + bool + format_parse_errors(std::ostream& os, + parse_error_list& error_list); + + /// @} + } +} + +#endif // SPOT_ELTLPARSE_PUBLIC_HH diff --git a/src/eltltest/Makefile.am b/src/eltltest/Makefile.am new file mode 100644 index 000000000..7f8a53ed6 --- /dev/null +++ b/src/eltltest/Makefile.am @@ -0,0 +1,44 @@ +## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de +## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +## Université Pierre et Marie Curie. +## +## This file is part of Spot, a model checking library. +## +## Spot is free software; you can redistribute it and/or modify it +## under the terms of the GNU General Public License as published by +## the Free Software Foundation; either version 2 of the License, or +## (at your option) any later version. +## +## Spot is distributed in the hope that it will be useful, but WITHOUT +## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +## License for more details. +## +## You should have received a copy of the GNU General Public License +## along with Spot; see the file COPYING. If not, write to the Free +## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +## 02111-1307, USA. + +AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) +LDADD = ../libspot.la + +check_SCRIPTS = defs +# Keep this sorted alphabetically. +check_PROGRAMS = \ + acc \ + nfa + +acc_SOURCES = acc.cc +nfa_SOURCES = nfa.cc + +EXTRA_DIST = $(TESTS) + +# Ordered by strength of the test. Test basic features first. +TESTS = \ + acc.test \ + nfa.test + +CLEANFILES = \ + input \ + prelude diff --git a/src/eltltest/acc.cc b/src/eltltest/acc.cc new file mode 100644 index 000000000..cf00a7833 --- /dev/null +++ b/src/eltltest/acc.cc @@ -0,0 +1,42 @@ +// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include +#include "eltlparse/public.hh" + +int +main(int argc, char** argv) +{ + spot::eltl::parse_error_list p; + const spot::ltl::formula* f = spot::eltl::parse_file( + argv[1], p, spot::ltl::default_environment::instance(), argc > 2); + + if (spot::eltl::format_parse_errors(std::cerr, p)) + { + if (f != 0) + std::cout << f->dump() << std::endl; + return 1; + } + + assert(f != 0); + std::cout << f->dump() << std::endl; +} diff --git a/src/eltltest/acc.test b/src/eltltest/acc.test new file mode 100755 index 000000000..b07f5bb2e --- /dev/null +++ b/src/eltltest/acc.test @@ -0,0 +1,44 @@ +#!/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 new file mode 100644 index 000000000..977e87b3a --- /dev/null +++ b/src/eltltest/nfa.cc @@ -0,0 +1,57 @@ +// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include +#include +#include "ltlast/nfa.hh" + +using namespace spot::ltl; + +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 << (*i)->label << std::endl; + dfs(a, (*i)->dst, m); + } +} + +int +main() +{ + nfa a; + + a.add_transition(0, 1, 1); + a.add_transition(1, 2, 2); + + std::cout << "init: " << a.format_state(a.get_init_state()) << std::endl; + + mset m; + dfs(a, a.get_init_state(), m); +} diff --git a/src/eltltest/nfa.test b/src/eltltest/nfa.test new file mode 100755 index 000000000..241c7f207 --- /dev/null +++ b/src/eltltest/nfa.test @@ -0,0 +1,6 @@ +#!/bin/sh + +. ./defs || exit 1 + +set -e +run 0 ./nfa || exit 1 diff --git a/src/ltlast/Makefile.am b/src/ltlast/Makefile.am index b7d3d6fa1..54014c57e 100644 --- a/src/ltlast/Makefile.am +++ b/src/ltlast/Makefile.am @@ -27,10 +27,12 @@ ltlastdir = $(pkgincludedir)/ltlast ltlast_HEADERS = \ allnodes.hh \ atomic_prop.hh \ + automatop.hh \ binop.hh \ constant.hh \ formula.hh \ multop.hh \ + nfa.hh \ predecl.hh \ refformula.hh \ unop.hh \ @@ -39,9 +41,11 @@ ltlast_HEADERS = \ noinst_LTLIBRARIES = libltlast.la libltlast_la_SOURCES = \ atomic_prop.cc \ + automatop.cc \ binop.cc \ constant.cc \ formula.cc \ multop.cc \ + nfa.cc \ refformula.cc \ unop.cc diff --git a/src/ltlast/allnodes.hh b/src/ltlast/allnodes.hh index 9b5664182..6797892f4 100644 --- a/src/ltlast/allnodes.hh +++ b/src/ltlast/allnodes.hh @@ -33,5 +33,6 @@ # include "multop.hh" # include "atomic_prop.hh" # include "constant.hh" +# include "automatop.hh" #endif // SPOT_LTLAST_ALLNODES_HH diff --git a/src/ltlast/automatop.cc b/src/ltlast/automatop.cc new file mode 100644 index 000000000..60193146c --- /dev/null +++ b/src/ltlast/automatop.cc @@ -0,0 +1,108 @@ +// 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 "automatop.hh" +#include "visitor.hh" + +namespace spot +{ + namespace ltl + { + automatop::automatop(const nfa::ptr nfa, vec* v) + : negated_(false), nfa_(nfa), children_(v) + { + dump_= nfa->get_name(); + dump_ += "("; + dump_ += (*v)[0]->dump(); + for (unsigned n = 1; n < v->size(); ++n) + dump_ += ", " + (*v)[n]->dump(); + dump_ += ")"; + set_key_(); + } + + automatop::~automatop() + { + // Get this instance out of the instance map. + pair p(nfa(), children_); + map::iterator i = instances.find(p); + assert (i != instances.end()); + instances.erase(i); + + delete children_; + } + + void + automatop::accept(visitor& v) + { + v.visit(this); + } + + void + automatop::accept(const_visitor& v) const + { + v.visit(this); + } + + automatop::map automatop::instances; + + automatop* + automatop::instance(const nfa::ptr nfa, vec* v) + { + assert(nfa != 0); + pair p(nfa, v); + map::iterator i = instances.find(p); + if (i != instances.end()) + { + delete v; + return static_cast(i->second->ref()); + } + automatop* res = new automatop(nfa, v); + instances[p] = res; + 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]; + } + + const nfa::ptr + automatop::nfa() const + { + assert(nfa_ != 0); + return nfa_; + } + } +} diff --git a/src/ltlast/automatop.hh b/src/ltlast/automatop.hh new file mode 100644 index 000000000..aea84bbeb --- /dev/null +++ b/src/ltlast/automatop.hh @@ -0,0 +1,98 @@ +// 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 ltlast/automatop.hh +/// \brief ELTL automaton operators +#ifndef SPOT_LTLAST_AUTOMATOP_HH +# define SPOT_LTLAST_AUTOMATOP_HH + +# include +# include +# include "nfa.hh" +# include "refformula.hh" + +namespace spot +{ + namespace ltl + { + /// \brief Automaton operators. + /// \ingroup eltl_ast + /// + class automatop : public ref_formula + { + public: + /// List of formulae. + typedef std::vector vec; + + /// \brief Build a spot::ltl::automatop with many children. + /// + /// This vector is acquired by the spot::ltl::automatop class, + /// the caller should allocate it with \c new, but not use it + /// (especially not destroy it) after it has been passed to + /// spot::ltl::automatop. + static automatop* + instance(const nfa::ptr nfa, 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); + + /// Get the NFA of this operator. + const nfa::ptr nfa() const; + + bool negated_; + protected: + typedef std::pair pair; + /// Comparison functor used internally by ltl::automatop. + struct paircmp + { + bool + operator () (const pair& p1, const pair& p2) const + { + if (p1.first != p2.first) + return p1.first < p2.first; + return *p1.second < *p2.second; + } + }; + typedef std::map map; + static map instances; + + automatop(const nfa::ptr nfa, vec* v); + virtual ~automatop(); + + private: + nfa::ptr nfa_; + vec* children_; + }; + } +} + +#endif // SPOT_LTLAST_AUTOMATOP_HH diff --git a/src/ltlast/nfa.cc b/src/ltlast/nfa.cc new file mode 100644 index 000000000..094225818 --- /dev/null +++ b/src/ltlast/nfa.cc @@ -0,0 +1,145 @@ +// 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 ltl + { + nfa::nfa() + : is_(), si_(), arity_(0), name_(), init_(0), finals_() + { + } + + nfa::~nfa() + { + is_map::iterator i; + for (i = is_.begin(); i != is_.end(); ++i) + { + state::iterator i2; + for (i2 = i->second->begin(); i2 != i->second->end(); ++i2) + delete *i2; + delete i->second; + } + } + + nfa::state* + nfa::add_state(int name) + { + is_map::iterator i = is_.find(name); + if (i == is_.end()) + { + state* s = new nfa::state; + is_[name] = s; + si_[s] = name; + + if (!init_) + init_ = s; + return s; + } + return i->second; + } + + void + nfa::add_transition(int src, int dst, int label) + { + state* s = add_state(src); + nfa::transition* t = new transition; + t->dst = add_state(dst); + t->label = label; + s->push_back(t); + if (label > arity_) + arity_ = label; + } + + void + nfa::set_init_state(int name) + { + init_ = add_state(name); + } + + void + nfa::set_final(int name) + { + finals_.insert(name); + } + + bool + nfa::is_final(const state* s) + { + return finals_.find(format_state(s)) != finals_.end(); + } + + bool + nfa::is_loop() + { + return finals_.empty(); + } + + int + nfa::arity() + { + return arity_ + 1; + } + + const nfa::state* + nfa::get_init_state() + { + if (!init_) + assert(0); + 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()); + } + + int + nfa::format_state(const state* s) const + { + si_map::const_iterator i = si_.find(s); + assert(i != si_.end()); + return i->second; + } + + const std::string& + nfa::get_name() const + { + return name_; + } + + void + nfa::set_name(const std::string& name) + { + name_ = name; + } + } +} diff --git a/src/ltlast/nfa.hh b/src/ltlast/nfa.hh new file mode 100644 index 000000000..7cca9907c --- /dev/null +++ b/src/ltlast/nfa.hh @@ -0,0 +1,148 @@ +// 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 ltlast/nfa.hh +/// \brief NFA interface used by automatop +#ifndef SPOT_LTLAST_NFA_HH +# define SPOT_LTLAST_NFA_HH + +# include "misc/hash.hh" +# include +# include +# include +# include + +namespace spot +{ + namespace ltl + { + /// Forward declaration. See below. + class succ_iterator; + + /// \brief Nondeterministic Finite Automata used by automata operators. + /// + /// States & labels are represented by integers. + /// Currently, only one initial state is possible. + 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 label; + const state* dst; + }; + + nfa(); + ~nfa(); + + void add_transition(int src, int dst, int label); + void set_init_state(int name); + void set_final(int name); + + /// \brief Get the initial state of the NFA. + const state* get_init_state(); + + /// \brief Tell whether the given state is final or not. + bool is_final(const state* s); + + /// \brief Tell whether the NFA is `loop', i.e. without any final state. + bool is_loop(); + + /// \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 loop. + /// \code + /// for (nfa::iterator i = a.begin(s); i != a.end(s); ++i); + /// \endcode + iterator begin(const state* s) const; + + /// \brief Return an iterator just past the last succesor of \a state. + iterator end(const state* s) const; + + int format_state(const state* s) const; + + const std::string& get_name() const; + void set_name(const std::string&); + + private: + state* add_state(int name); + + typedef Sgi::hash_map > is_map; + typedef Sgi::hash_map > si_map; + + is_map is_; + si_map si_; + + int arity_; + std::string name_; // FIXME. + + state* init_; + 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_LTLAST_NFA_HH_ diff --git a/src/ltlast/predecl.hh b/src/ltlast/predecl.hh index 121c9ef5d..90675757d 100644 --- a/src/ltlast/predecl.hh +++ b/src/ltlast/predecl.hh @@ -42,6 +42,7 @@ namespace spot struct binop; struct formula; struct multop; + struct automatop; } } diff --git a/src/ltlast/visitor.hh b/src/ltlast/visitor.hh index a6cfb933b..b6a7c6a6d 100644 --- a/src/ltlast/visitor.hh +++ b/src/ltlast/visitor.hh @@ -47,6 +47,7 @@ namespace spot 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. @@ -65,6 +66,7 @@ namespace spot 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; }; diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc index 9140ce506..261cd5473 100644 --- a/src/ltlvisit/basicreduce.cc +++ b/src/ltlvisit/basicreduce.cc @@ -285,6 +285,12 @@ namespace spot assert(0); } + void + visit(automatop*) + { + assert(0); + } + void visit(multop* mo) { diff --git a/src/ltlvisit/clone.cc b/src/ltlvisit/clone.cc index 6a0be0c62..b7cad0514 100644 --- a/src/ltlvisit/clone.cc +++ b/src/ltlvisit/clone.cc @@ -65,6 +65,15 @@ namespace spot recurse(bo->first()), recurse(bo->second())); } + 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(ao->nfa(), res); + } + void clone_visitor::visit(multop* mo) { diff --git a/src/ltlvisit/clone.hh b/src/ltlvisit/clone.hh index 604f8bf13..43cf4597b 100644 --- a/src/ltlvisit/clone.hh +++ b/src/ltlvisit/clone.hh @@ -47,6 +47,7 @@ namespace spot void visit(atomic_prop* ap); void visit(unop* uo); void visit(binop* bo); + void visit(automatop* mo); void visit(multop* mo); void visit(constant* c); diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc index dbb0ac3b8..13a39e4ec 100644 --- a/src/ltlvisit/contain.cc +++ b/src/ltlvisit/contain.cc @@ -231,6 +231,12 @@ namespace spot } } + void + visit(automatop*) + { + assert(0); + } + void visit(multop* mo) { diff --git a/src/ltlvisit/dotty.cc b/src/ltlvisit/dotty.cc index 67611b00c..e6928a8e7 100644 --- a/src/ltlvisit/dotty.cc +++ b/src/ltlvisit/dotty.cc @@ -75,6 +75,12 @@ namespace spot uo->child()->accept(*this); } + void + visit(const automatop*) + { + assert(0); + } + void visit(const multop* mo) { diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc index 208992461..1e4414c16 100644 --- a/src/ltlvisit/nenoform.cc +++ b/src/ltlvisit/nenoform.cc @@ -151,6 +151,21 @@ namespace spot assert(0); } + void + visit(automatop* ao) + { + if (negated_) + { + negated_ = false; + ao->negated_ = true; + } + automatop::vec* res = new automatop::vec; + unsigned aos = ao->size(); + for (unsigned i = 0; i < aos; ++i) + res->push_back(recurse(ao->nth(i))); + result_ = automatop::instance(ao->nfa(), res); + } + void visit(multop* mo) { diff --git a/src/ltlvisit/postfix.cc b/src/ltlvisit/postfix.cc index 8863e6a80..9b7fe1e2c 100644 --- a/src/ltlvisit/postfix.cc +++ b/src/ltlvisit/postfix.cc @@ -55,6 +55,15 @@ namespace spot doit(bo); } + 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::visit(multop* mo) { @@ -94,6 +103,12 @@ namespace spot doit_default(mo); } + void + postfix_visitor::doit(automatop* ao) + { + doit_default(ao); + } + void postfix_visitor::doit(constant* c) { diff --git a/src/ltlvisit/postfix.hh b/src/ltlvisit/postfix.hh index 4d341f59b..f467ed16c 100644 --- a/src/ltlvisit/postfix.hh +++ b/src/ltlvisit/postfix.hh @@ -45,12 +45,14 @@ namespace spot void visit(unop* uo); void visit(binop* bo); void visit(multop* mo); + void visit(automatop* c); void visit(constant* c); virtual void doit(atomic_prop* ap); virtual void doit(unop* uo); virtual void doit(binop* bo); virtual void doit(multop* mo); + virtual void doit(automatop* mo); virtual void doit(constant* c); virtual void doit_default(formula* f); }; diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index a34161043..96734a46a 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -188,6 +188,12 @@ namespace spot result_ = binop::instance(bo->op(), f1, f2); } + void + visit(automatop*) + { + assert(0); + } + void visit(multop* mo) { diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc index fffcfc136..ba3a6eb55 100644 --- a/src/ltlvisit/syntimpl.cc +++ b/src/ltlvisit/syntimpl.cc @@ -122,6 +122,12 @@ namespace spot assert(0); } + void + visit(const automatop*) + { + assert(0); + } + void visit(const multop* mo) { @@ -281,6 +287,12 @@ namespace spot assert(0); } + void + visit(const automatop*) + { + assert(0); + } + void visit(const multop* mo) { @@ -479,6 +491,12 @@ namespace spot assert(0); } + void + visit(const automatop*) + { + assert(0); + } + void visit(const multop* mo) { diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index 05b0a3827..4c27a153c 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -154,6 +154,27 @@ namespace spot os_ << ")"; } + void + visit(const automatop* ao) + { + // Warning: this string isn't parsable. + bool top_level = top_level_; + top_level_ = false; + if (!top_level) + os_ << "("; + os_ << ao->nfa()->get_name() << "("; + unsigned max = ao->size(); + ao->nth(0)->accept(*this); + for (unsigned n = 1; n < max; ++n) + { + os_ << ","; + ao->nth(n)->accept(*this); + } + os_ << ")"; + if (!top_level) + os_ << ")"; + } + void visit(const multop* mo) { @@ -284,6 +305,27 @@ namespace spot os_ << ")"; } + void + visit(const automatop* ao) + { + // Warning: this string isn't parsable. + bool top_level = top_level_; + top_level_ = false; + if (!top_level) + os_ << "("; + os_ << ao->nfa()->get_name() << "("; + unsigned max = ao->size(); + ao->nth(0)->accept(*this); + for (unsigned n = 1; n < max; ++n) + { + os_ << ","; + ao->nth(n)->accept(*this); + } + os_ << ")"; + if (!top_level) + os_ << ")"; + } + void visit(const multop* mo) { diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index edc42922e..ab7c9940d 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -111,6 +111,12 @@ namespace spot assert(0); } + virtual void + visit(const automatop*) + { + assert(!"unsupported operator"); + } + virtual void visit(const multop* node) { diff --git a/src/tgba/tgbabddconcretefactory.cc b/src/tgba/tgbabddconcretefactory.cc index 0d04023ae..8188cdf4b 100644 --- a/src/tgba/tgbabddconcretefactory.cc +++ b/src/tgba/tgbabddconcretefactory.cc @@ -47,6 +47,18 @@ namespace spot return num; } + int + tgba_bdd_concrete_factory::create_anonymous_state() + { + int num = get_dict()->register_anonymous_variables(2, this); + bdd_setpair(get_dict()->next_to_now, num + 1, num); + bdd_setpair(get_dict()->now_to_next, num, num + 1); + // Keep track of all "Now" variables for easy + // existential quantification. + data_.declare_now_next (bdd_ithvar(num), bdd_ithvar(num + 1)); + return num; + } + int tgba_bdd_concrete_factory::create_atomic_prop(const ltl::formula* f) { diff --git a/src/tgba/tgbabddconcretefactory.hh b/src/tgba/tgbabddconcretefactory.hh index a2c987e30..c31aa6a89 100644 --- a/src/tgba/tgbabddconcretefactory.hh +++ b/src/tgba/tgbabddconcretefactory.hh @@ -47,6 +47,12 @@ namespace spot /// Variable numbers can be turned into BDD using ithvar(). int create_state(const ltl::formula* f); + /// Create a anonymous Now/Next variables. + /// + /// \return The BDD variable number v for the Now state. The + /// Next BDD corresponds to v+1. + int create_anonymous_state(); + /// Create an atomic proposition variable for formula \a f. /// /// \param f The formula to create an aotmic proposition for. diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 56e7b7399..2acfba1e0 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 \ @@ -61,6 +62,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..910e3c06f --- /dev/null +++ b/src/tgbaalgos/eltl2tgba_lacim.cc @@ -0,0 +1,261 @@ +// 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 "ltlast/visitor.hh" +#include "ltlast/allnodes.hh" +#include "ltlvisit/lunabbrev.hh" +#include "ltlvisit/nenoform.hh" +#include "ltlvisit/destroy.hh" +#include "tgba/tgbabddconcretefactory.hh" +#include + +#include "eltl2tgba_lacim.hh" + +namespace spot +{ + namespace + { + using namespace ltl; + + /// \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; + } + case unop::X: + case unop::F: + case unop::G: + assert(!"unsupported operator"); + } + /* 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; + case binop::U: + case binop::R: + assert(!"unsupported operator"); + } + /* 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) + { + nmap m; + bdd acc = bddtrue; + std::pair vp = + recurse_state(node, node->nfa()->get_init_state(), m, acc); + + bdd tmp = bddtrue; + for (nmap::iterator it = m.begin(); it != m.end(); ++it) + tmp &= bdd_apply(bdd_ithvar(it->second.first + 1), + bdd_ithvar(it->second.second + 1), bddop_biimp); + fact_.constrain_relation(bdd_apply(acc, tmp, bddop_imp)); + + if (!node->nfa()->is_loop()) + fact_.declare_acceptance_condition(acc, node); + + bdd init = bdd_ithvar(vp.first); + res_ = node->negated_ ? bdd_not(init) : init; + } + + 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_; + + // Table containing the two now variables associated with each state. + // TODO: a little documentation about that. + typedef Sgi::hash_map< + const nfa::state*, std::pair, ptr_hash > nmap; + + std::pair& + recurse_state(const automatop* n, const nfa::state* s, nmap& m, bdd& acc) + { + const nfa::ptr nfa = n->nfa(); + nmap::iterator it; + it = m.find(s); + + int v1 = 0; + int v2 = 0; + if (it != m.end()) + return it->second; + else + { + v1 = fact_.create_anonymous_state(); + v2 = fact_.create_anonymous_state(); + m[s] = std::make_pair(v1, v2); + } + + bdd tmp1 = bddfalse; + bdd tmp2 = bddfalse; + bdd tmpacc = !bdd_ithvar(v2); + + for (nfa::iterator i = nfa->begin(s); i != nfa->end(s); ++i) + { + bdd f = (*i)->label == -1 ? bddtrue : recurse(n->nth((*i)->label)); + if (nfa->is_final((*i)->dst)) + { + tmp1 |= f; + tmp2 |= f; + tmpacc |= f; + } + else + { + std::pair vp = recurse_state(n, (*i)->dst, m, acc); + tmp1 |= (f & bdd_ithvar(vp.first + 1)); + tmp2 |= (f & bdd_ithvar(vp.second + 1)); + } + } + acc &= tmpacc; + fact_.constrain_relation(bdd_apply(bdd_ithvar(v1), tmp1, bddop_biimp)); + fact_.constrain_relation(bdd_apply(bdd_ithvar(v2), tmp2, bddop_imp)); + fact_.constrain_relation( + bdd_apply(bdd_ithvar(v2), bdd_ithvar(v1), bddop_imp)); + return m[s]; + } + }; + } // anonymous + + tgba_bdd_concrete* + eltl_to_tgba_lacim(const ltl::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 ltl::formula* f1 = ltl::unabbreviate_logic(f); + const ltl::formula* f2 = ltl::negative_normal_form(f1); + ltl::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); + ltl::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..053ea287a --- /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 "ltlast/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 ltl::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 cc6e3ab3d..b4b1652f7 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -401,6 +401,12 @@ namespace spot assert(0); } + void + visit(const automatop*) + { + assert(!"unsupported operator"); + } + void visit(const multop* node) { @@ -500,6 +506,12 @@ namespace spot assert(0); } + void + visit(const automatop*) + { + assert(!"unsupported operator"); + } + void visit(const multop* node) { diff --git a/src/tgbaalgos/ltl2tgba_lacim.cc b/src/tgbaalgos/ltl2tgba_lacim.cc index fe6ce96b7..f35ee65ad 100644 --- a/src/tgbaalgos/ltl2tgba_lacim.cc +++ b/src/tgbaalgos/ltl2tgba_lacim.cc @@ -210,6 +210,12 @@ namespace spot assert(0); } + void + visit(const automatop*) + { + assert(!"unsupported operator"); + } + void visit(const multop* node) { diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index b3ec54301..a413e6d79 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 = eltl2tgba ltl2tgba randtgba 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 @@ -65,6 +66,7 @@ tripprod_SOURCES = tripprod.cc # Keep this sorted by STRENGTH. Test basic things first, # because such failures will be easier to diagnose and fix. TESTS = \ + eltl2tgba.test \ explicit.test \ tgbaread.test \ readsave.test \ diff --git a/src/tgbatest/eltl2tgba.cc b/src/tgbatest/eltl2tgba.cc new file mode 100644 index 000000000..14eb276dd --- /dev/null +++ b/src/tgbatest/eltl2tgba.cc @@ -0,0 +1,109 @@ +// 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 "eltlparse/public.hh" +#include "tgbaalgos/eltl2tgba_lacim.hh" +#include "tgbaalgos/dotty.hh" +#include "tgbaalgos/save.hh" +#include "ltlvisit/destroy.hh" + +void +syntax(char* prog) +{ + std::cerr << "Usage: "<< prog << " [OPTIONS...] formula [file]" << std::endl + << " "<< prog << " -F [OPTIONS...] file [file]" << std::endl + << std::endl + << "Options:" << std::endl + << " -F read the formula from the file (extended input format)" + << std::endl; +} + +std::string +ltl_defs() +{ + std::string s = "\ +X=(0 1 true \ + 1 2 $0 \ + accept 2) \ +U=(0 0 $0 \ + 0 1 $1 \ + accept 1) \ +G=(0 0 $0)"; + return s; +} + +int +main(int argc, char** argv) +{ + if (argc < 2) + { + syntax(argv[0]); + return 1; + } + + spot::eltl::parse_error_list p; + spot::ltl::environment& env(spot::ltl::default_environment::instance()); + spot::ltl::formula* f = 0; + int formula_index = 0; + + if (strcmp(argv[1], "-F") == 0) + { + f = spot::eltl::parse_file(argv[2], p, env, false); + formula_index = 2; + } + else + { + std::stringstream oss; + oss << ltl_defs() << "%" << argv[1]; + f = spot::eltl::parse_string(oss.str(), p, env, false); + formula_index = 1; + } + + if (spot::eltl::format_parse_errors(std::cerr, p)) + { + if (f != 0) + std::cout << f->dump() << std::endl; + return 1; + } + + assert(f != 0); + std::cerr << 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); + if (argc >= formula_index + 1) + { + std::ofstream ofs(argv[formula_index + 1]); + spot::tgba_save_reachable(ofs, concrete); + ofs.close(); + } + + spot::ltl::destroy(f); + delete concrete; + delete dict; +} diff --git a/src/tgbatest/eltl2tgba.test b/src/tgbatest/eltl2tgba.test new file mode 100755 index 000000000..53c9dbcda --- /dev/null +++ b/src/tgbatest/eltl2tgba.test @@ -0,0 +1,114 @@ +#!/bin/sh + +. ./defs || exit -1 +set -e + +# Check if the TGBA was corretly constructed. +check_construct() +{ + run 0 ./eltl2tgba -F "$1" input +} + +# Check if the TGBA behaves correctly by doing an emptiness check on +# the product between the constructed TGBA and a given formula +# translated using FM. +check_true() +{ + run 0 ./ltl2tgba -e -Pinput -f "$1" +} +check_false() +{ + run 1 ./ltl2tgba -e -Pinput -f "$1" +} + +# Create the prelude file. +cat >input1 <input <input <input <input <input <input <input <