From 79bed65843e48398d0804e2b5533de71094421ab Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 9 Jul 2003 15:40:24 +0000 Subject: [PATCH] * lbtt/: New directory. Contains a patched version of lbtt 1.0.1. * Makefile.am (MAYBE_LBTT): New variables. (SUBDIRS): Add $(MAYBE_LBTT). (EXTRA_DIST): Add m4/lbtt.m4. * configure.ac: Call AX_CHECK_LBTT. * m4/lbtt.m4: New file. * src/tgbatest/Makefile.am (check_PROGRAMS): Add spotlbtt. (spotlbtt_SOURCES): New variables. (TESTS): Add spotlbtt.test. (CLEANFILE): Add config. * src/tgbatest/defs.in (top_builddir, LBTT, LBTT_TRANSLATE): New substitutions. * src/tgbatest/spotlbtt.cc, src/tgbatest/spotlbtt.test: New files. --- ChangeLog | 16 +++++++++- Makefile.am | 7 +++-- configure.ac | 1 + m4/lbtt.m4 | 26 ++++++++++++++++ src/tgbatest/.cvsignore | 1 + src/tgbatest/Makefile.am | 9 ++++-- src/tgbatest/defs.in | 3 ++ src/tgbatest/spotlbtt.cc | 63 ++++++++++++++++++++++++++++++++++++++ src/tgbatest/spotlbtt.test | 45 +++++++++++++++++++++++++++ 9 files changed, 165 insertions(+), 6 deletions(-) create mode 100644 m4/lbtt.m4 create mode 100644 src/tgbatest/spotlbtt.cc create mode 100755 src/tgbatest/spotlbtt.test diff --git a/ChangeLog b/ChangeLog index 1d63f95db..23aed1ab8 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,6 +1,20 @@ 2003-07-09 Alexandre Duret-Lutz - * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): + * lbtt/: New directory. Contains a patched version of lbtt 1.0.1. + * Makefile.am (MAYBE_LBTT): New variables. + (SUBDIRS): Add $(MAYBE_LBTT). + (EXTRA_DIST): Add m4/lbtt.m4. + * configure.ac: Call AX_CHECK_LBTT. + * m4/lbtt.m4: New file. + * src/tgbatest/Makefile.am (check_PROGRAMS): Add spotlbtt. + (spotlbtt_SOURCES): New variables. + (TESTS): Add spotlbtt.test. + (CLEANFILE): Add config. + * src/tgbatest/defs.in (top_builddir, LBTT, LBTT_TRANSLATE): New + substitutions. + * src/tgbatest/spotlbtt.cc, src/tgbatest/spotlbtt.test: New files. + + * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Fix computation of states sharing the same accepting set. Make sure we only output one initial state in LBTT's output. diff --git a/Makefile.am b/Makefile.am index a9a1e6eb1..168bbc1a1 100644 --- a/Makefile.am +++ b/Makefile.am @@ -1,8 +1,11 @@ if WITH_INCLUDED_BUDDY MAYBE_BUDDY = buddy endif WITH_INCLUDED_BUDDY +if WITH_INCLUDED_LBTT + MAYBE_LBTT = lbtt +endif WITH_INCLUDED_LBTT -SUBDIRS = $(MAYBE_BUDDY) doc src wrap iface +SUBDIRS = $(MAYBE_BUDDY) $(MAYBE_LBTT) doc src wrap iface ACLOCAL_AMFLAGS = -I m4 -EXTRA_DIST = m4/gccwarn.m4 m4/pypath.m4 m4/buddy.m4 HACKING +EXTRA_DIST = m4/gccwarn.m4 m4/pypath.m4 m4/buddy.m4 m4/lbtt.m4 HACKING diff --git a/configure.ac b/configure.ac index 463b43d19..19de148f7 100644 --- a/configure.ac +++ b/configure.ac @@ -13,6 +13,7 @@ AC_PROG_YACC AC_LANG(C++) AX_CHECK_BUDDY +AX_CHECK_LBTT AC_PROG_LIBTOOL diff --git a/m4/lbtt.m4 b/m4/lbtt.m4 new file mode 100644 index 000000000..bd33dc821 --- /dev/null +++ b/m4/lbtt.m4 @@ -0,0 +1,26 @@ +AC_DEFUN([AX_CHECK_LBTT], [ + AC_ARG_WITH([included-lbtt], + [AC_HELP_STRING([--with-included-lbtt], + [use the LBTT program inclued here])]) + AS_IF([AM_RUN_LOG([lbtt --help | grep spot])], + [need_included_lbtt=no], + [need_included_lbtt=yes]) + + if test "$need_included_lbtt" = yes; then + if test "$with_included_lbtt" = no; then + AC_MSG_ERROR([Cannot find lbtt. Please install lbtt first, + or configure with --with-included-lbtt]) + else + with_included_lbtt=yes + fi + fi + + if test "$with_included_lbtt" = yes; then + AC_CONFIG_SUBDIRS([lbtt]) + LBTT='${top_builddir}/lbtt/src/lbtt' + LBTT_TRANSLATE='${top_builddir}/lbtt/src/lbtt-translate' + fi + AM_CONDITIONAL([WITH_INCLUDED_LBTT], [test "$with_included_lbtt" = yes]) + AC_SUBST([LBTT]) + AC_SUBST([LBTT_TRANSLATE]) +]) diff --git a/src/tgbatest/.cvsignore b/src/tgbatest/.cvsignore index b74d25e91..1ae41702d 100644 --- a/src/tgbatest/.cvsignore +++ b/src/tgbatest/.cvsignore @@ -14,3 +14,4 @@ explprod *.dot tripprod mixprod +spotlbtt diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index cf55e370c..9d72aec5e 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -12,7 +12,8 @@ check_PROGRAMS = \ bddprod \ explprod \ tripprod \ - mixprod + mixprod \ + spotlbtt # Keep this sorted alphabetically. bddprod_SOURCES = ltlprod.cc @@ -25,6 +26,7 @@ mixprod_SOURCES = mixprod.cc readsave_SOURCES = readsave.cc tgbaread_SOURCES = tgbaread.cc tripprod_SOURCES = tripprod.cc +spotlbtt_SOURCES = spotlbtt.cc # Keep this sorted by STRENGTH. Test basic things first, # because such failures will be easier to diagnose and fix. @@ -37,8 +39,9 @@ TESTS = \ bddprod.test \ explprod.test \ tripprod.test \ - mixprod.test + mixprod.test \ + spotlbtt.test EXTRA_DIST = $(TESTS) -CLEANFILES = input input1 input2 input3 stdout expected +CLEANFILES = input input1 input2 input3 stdout expected config diff --git a/src/tgbatest/defs.in b/src/tgbatest/defs.in index 68de36ac3..b7db16a1a 100644 --- a/src/tgbatest/defs.in +++ b/src/tgbatest/defs.in @@ -26,6 +26,9 @@ test -z "$VERBOSE" && exec >/dev/null 2>&1 echo "== Running test $0" DOT='@DOT@' +top_builddir='@top_builddir@' +LBTT="@LBTT@" +LBTT_TRANSLATE="@LBTT_TRANSLATE@" # Turn on shell traces when VERBOSE=x. if test "x$VERBOSE" = xx; then diff --git a/src/tgbatest/spotlbtt.cc b/src/tgbatest/spotlbtt.cc new file mode 100644 index 000000000..7fe43233f --- /dev/null +++ b/src/tgbatest/spotlbtt.cc @@ -0,0 +1,63 @@ +#include +#include +#include +#include +#include "ltlvisit/destroy.hh" +#include "ltlast/allnodes.hh" +#include "ltlparse/public.hh" +#include "tgbaalgos/ltl2tgba.hh" +#include "tgbaalgos/lbtt.hh" + + +void +syntax(char* prog) +{ + std::cerr << "Usage: "<< prog << " file" << std::endl; + exit(2); +} + +int +main(int argc, char** argv) +{ + int exit_code = 0; + + if (argc != 2) + syntax(argv[0]); + + std::ifstream fin(argv[1]); + if (! fin) + { + std::cerr << "Cannot open " << argv[1] << std::endl; + exit(2); + } + + std::string input; + if (! std::getline(fin, input, '\0')) + { + std::cerr << "Cannot read " << argv[1] << std::endl; + exit(2); + } + + spot::ltl::environment& env(spot::ltl::default_environment::instance()); + spot::ltl::parse_error_list pel; + spot::ltl::formula* f = spot::ltl::parse(input, pel, env); + + exit_code = spot::ltl::format_parse_errors(std::cerr, input, pel); + + if (f) + { + spot::tgba_bdd_concrete a = spot::ltl_to_tgba(f); + spot::ltl::destroy(f); + spot::lbtt_reachable(std::cout, a); + } + else + { + exit_code = 1; + } + + assert(spot::ltl::atomic_prop::instance_count() == 0); + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); + return exit_code; +} diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test new file mode 100755 index 000000000..30beefbf6 --- /dev/null +++ b/src/tgbatest/spotlbtt.test @@ -0,0 +1,45 @@ +#!/bin/sh + +. ./defs + +set -e + +cat > config <