diff --git a/lbtt/ChangeLog b/lbtt/ChangeLog index f0b8db9e4..56664b92f 100644 --- a/lbtt/ChangeLog +++ b/lbtt/ChangeLog @@ -1,3 +1,25 @@ +2004-07-30 Heikki Tauriainen + + * Version 1.1.1 released. + +2004-07-30 Heikki Tauriainen + + * src/TestOperations.cc (generateBuchiAutomaton): Protect + against referencing a null pointer returned by strsignal on + some platforms. + (performBuchiIntersectionCheck): Handle product size + exceptions gracefully. Skip redundant writes to an unopened + transcript file. + + * configure.ac: Update version. + * NEWS: Update. + * README: Update. + +2004-07-16 Alexandre Duret-Lutz + + * configure.ac: Call AC_GNU_SOURCE to make glibc's strsignal + definition visible even to non-GNU compilers. + 2004-07-07 Heikki Tauriainen * Version 1.1.0 released. diff --git a/lbtt/NEWS b/lbtt/NEWS index 4abdfd71b..0621efd5a 100644 --- a/lbtt/NEWS +++ b/lbtt/NEWS @@ -1,4 +1,4 @@ -lbtt NEWS -- history of user-visible changes. 7 Jul 2004 +lbtt NEWS -- history of user-visible changes. 30 Jul 2004 Copyright (C) 2004 Heikki Tauriainen Permission is granted to anyone to make or distribute verbatim copies @@ -12,6 +12,11 @@ Copyright (C) 2004 Heikki Tauriainen Please send bug reports to . +Version 1.1.1 + +* This release includes fixes to build problems with non-GNU + compilers on GNU libc systems and a few minor bug fixes. + Version 1.1.0 * File formats diff --git a/lbtt/README b/lbtt/README index c400bf804..41506e366 100644 --- a/lbtt/README +++ b/lbtt/README @@ -1,11 +1,11 @@ -lbtt version 1.1.0 +lbtt version 1.1.1 ------------------ lbtt is a tool for testing programs that translate formulas expressed in propositional linear temporal logic (LTL) into Büchi automata. The goal of the tool is to assist implementing LTL-to-Büchi translation algorithms correctly by providing an -automated testing environment for LTL-to-B@"uchi translators. +automated testing environment for LTL-to-Büchi translators. Additionally, the testing environment can be used for very basic profiling of different LTL-to-Büchi translators to evaluate their performance. @@ -18,7 +18,7 @@ the terms of the GNU General Public License. lbtt comes with NO WARRANTY. See the file COPYING for details. -Quick installation instructions: +Brief installation instructions: -------------------------------- The basic procedure to build lbtt, the associated tools diff --git a/lbtt/configure.ac b/lbtt/configure.ac index 52119c3b4..5c9df77bc 100644 --- a/lbtt/configure.ac +++ b/lbtt/configure.ac @@ -1,8 +1,8 @@ # Process this file with autoconf to produce a configure script. AC_PREREQ([2.59]) -AC_INIT([lbtt], [1.1.0], [heikki.tauriainen@hut.fi]) -AC_REVISION([Revision: 1.4]) +AC_INIT([lbtt], [1.1.1], [heikki.tauriainen@hut.fi]) +AC_REVISION([Revision: 1.5]) AC_CONFIG_SRCDIR([src/main.cc]) AC_CONFIG_HEADERS([config.h]) AM_INIT_AUTOMAKE @@ -70,6 +70,7 @@ fi # Check for the availability of headers. +AC_GNU_SOURCE AC_HEADER_STDC AC_CHECK_HEADERS([libintl.h fcntl.h sys/times.h]) AC_HEADER_SYS_WAIT @@ -148,7 +149,7 @@ if test "${slist_header}" != no; then [[${slist_namespace}::slist s;]])], [break]) fi - done + done if test "${slist_namespace}" != error; then AC_MSG_RESULT([header <${slist_header}>, typename ${slist_namespace}::slist]) AC_DEFINE( @@ -167,7 +168,6 @@ fi if test "${slist_header}" = no; then AC_MSG_RESULT([no]) - fi AC_LANG(C) diff --git a/lbtt/src/TestOperations.cc b/lbtt/src/TestOperations.cc index 5e3b3ed64..5389cdbef 100644 --- a/lbtt/src/TestOperations.cc +++ b/lbtt/src/TestOperations.cc @@ -1114,11 +1114,14 @@ void generateBuchiAutomaton if (WIFSIGNALED(exitcode)) { failure_reason += "aborted by signal " - + toString(WTERMSIG(exitcode)) + + toString(WTERMSIG(exitcode)); + #ifdef HAVE_STRSIGNAL - + " (" + strsignal(WTERMSIG(exitcode)) + ")" + const char* signame = strsignal(WTERMSIG(exitcode)); + if (signame != 0) + failure_reason += " (" + string(signame) + ")"; #endif /* HAVE_STRSIGNAL */ - ; + if (WTERMSIG(exitcode) == SIGINT || WTERMSIG(exitcode) == SIGQUIT) raise(WTERMSIG(exitcode)); } @@ -1776,6 +1779,7 @@ void performBuchiIntersectionCheck() printText("\n\n", 2); if (round_info.transcript_file.is_open()) + { writeToTranscript("User break during Büchi automata intersection " "emptiness check"); round_info.transcript_file << string(8, ' ') + "(+) " @@ -1783,9 +1787,33 @@ void performBuchiIntersectionCheck() + ", (-) " + configuration.algorithmString(alg_2) + "\n\n"; + } throw; } + catch (const ::Graph::Product< ::Graph::BuchiProduct>::SizeException&) + { + if (!printText(": aborted (product may be too large)", 4)) + printText(" [Product may be too large: (+) " + + configuration.algorithmString(alg_1) + + ", (-) " + + configuration.algorithmString(alg_2) + + "]", + 2, + 6); + printText("\n", 2); + + if (round_info.transcript_file.is_open()) + { + writeToTranscript("Automata intersection emptiness check aborted " + "(product may be too large)"); + round_info.transcript_file << string(8, ' ') + "(+) " + + configuration.algorithmString(alg_1) + + ", (-) " + + configuration.algorithmString(alg_2) + + "\n\n"; + } + } catch (const bad_alloc&) { if (!printText(": aborted (out of memory)", 4)) @@ -1799,6 +1827,7 @@ void performBuchiIntersectionCheck() printText("\n", 2); if (round_info.transcript_file.is_open()) + { writeToTranscript("Out of memory during Büchi automata " "intersection emptiness check"); round_info.transcript_file << string(8, ' ') + "(+) " @@ -1806,6 +1835,7 @@ void performBuchiIntersectionCheck() + ", (-) " + configuration.algorithmString(alg_2) + "\n\n"; + } } } }