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 <