alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Import of lbtt 1.1.1

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2004-07-30 11:37:46 +00:00
parent d7b3d97422
commit 894050ed90
5 changed files with 68 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

22
lbtt/ChangeLog
View file

@ -1,3 +1,25 @@
2004-07-30 Heikki Tauriainen <heikki.tauriainen@hut.fi>
* Version 1.1.1 released.
2004-07-30 Heikki Tauriainen <heikki.tauriainen@hut.fi>
* 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 <adl@src.lip6.fr>
* configure.ac: Call AC_GNU_SOURCE to make glibc's strsignal
definition visible even to non-GNU compilers.
2004-07-07 Heikki Tauriainen <heikki.tauriainen@hut.fi>
* Version 1.1.0 released.

7
lbtt/NEWS
View file

@ -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 <heikki.tauriainen@hut.fi>.
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

6
lbtt/README
View file

@ -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

8
lbtt/configure.ac
View file

@ -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<int> 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)

36
lbtt/src/TestOperations.cc
View file

@ -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";
}
}
}
}