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

Import of lbtt 1.2.0

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2005-08-31 15:14:51 +00:00
parent e4befcecc7
commit 0a12b942a4
75 changed files with 1069 additions and 769 deletions
Download patch file Download diff file Expand all files Collapse all files

2
lbtt/AUTHORS
View file

@ -1 +1 @@
Heikki Tauriainen <heikki.tauriainen@hut.fi> Heikki Tauriainen <heikki.tauriainen@tkk.fi>

113
lbtt/ChangeLog
View file

@ -1,3 +1,116 @@
2005-08-30 Heikki Tauriainen <heikki.tauriainen@tkk.fi>
* src/main.cc: [HAVE_ISATTY && HAVE_UNISTD_H]: Include the
unistd.h header.
(testLoop): Add support for reading LTL formulas from standard
input using the new variable `round_info.formula_input_stream'.
(main) [HAVE_ISATTY]: If formulas are to be read from the
standard input which is not a terminal, force lbtt to work in
non-interactive mode.
* src/TestOperations.cc (generateFormula):
Use `round_info.formula_input_stream' instead of
`round_info.formula_input_file'.
* src/TestRoundInfo.h (TestRoundInfo::formula_input_stream): New
variable.
* src/Configuration.cc (Configuration::showCommandLineHelp):
Update description of the --formulafile command line option.
(Configuration::print): Do not display a file name when reading
formulas from standard input.
* src/SpotWrapper.h, src/SpotWrapper.cc: Merge files from
Spot 0.2 (contributed by Alexandre Duret-Lutz); remove #pragma
definitions.
* src/ExternalTranslator.h, src/Makefile.in, src/translate.cc:
Merge changes from Spot 0.2 (contributed by Alexandre Duret-Lutz).
* doc/lbtt.texi: Fix typo in URL of the FormulaOptions block
generator. Update version, add documentation and references about
support for Spot. Describe the new semantics of the --formulafile
command line option.
* NEWS, README, configure.ac: Update.
* Version 1.2.0 released.
2005-08-18 Heikki Tauriainen <heikki.tauriainen@tkk.fi>
* NEWS, README: Update to next version.
* Version 1.1.3 released.
2005-08-18 Heikki Tauriainen <heikki.tauriainen@tkk.fi>
* src/TestOperations.cc (generateBuchiAutomaton): Do not
block interrupt signals while running a child process; if lbtt
is currently in the foreground, transfer the controlling terminal
to the child instead.
* configure.ac: Add tests for the getpgrp, tcgetpgrp and
tcsetpgrp functions.
2005-08-17 Heikki Tauriainen <heikki.tauriainen@tkk.fi>
* src/BitArray.h (BitArray::set, BitArray::clear): Do not
set/clear more bits than specified.
* src/main.cc (main): Add a space before error message.
2005-08-16 Heikki Tauriainen <heikki.tauriainen@tkk.fi>
* src/main.cc: Include the sys/types.h header.
(translator_process): New global variable.
(abortHandler): If a translator process is still active when
aborting, terminate it.
* src/TestOperations.cc: Declare the external translator_process
variable.
(generateBuchiAutomaton): Replace the pid variable with the
translator_process variable.
Use setpgid instead of setsid. Always try to terminate the
subprocess if waitpid fails (not only in case of timeouts).
* configure.ac: Replace test for setsid with test for
setpgid.
2005-08-15 Heikki Tauriainen <heikki.tauriainen@tkk.fi>
* configure.ac: Update version and e-mail address.
Remove test for the slist header.
* AUTHORS, doc/lbtt.texi: Update e-mail address.
* src/LbttAlloc.h: Remove definition for the ALLOC macro.
Update copyright information.
* src/BuchiAutomaton.cc, src/BuchiProduct.cc, src/BuchiProduct.h,
src/Configuration.cc, src/Configuration.h, src/DispUtil.cc,
src/ExternalTranslator.h, src/FormulaRandomizer.cc,
src/FormulaRandomizer.h, src/Graph.h.in, src/IntervalList.cc,
src/IntervalList.h, src/Ltl-parse.yy, src/LtlFormula.cc,
src/LtlFormula.h, src/main.cc, src/NeverClaimAutomaton.cc,
src/NeverClaimAutomaton.h, src/PathEvaluator.cc,
src/PathEvaluator.h, src/Product.h, src/SccCollection.h,
src/SharedTestData.h, src/StatDisplay.cc, src/StatDisplay.h,
src/StateSpace.cc, src/StateSpaceRandomizer.cc,
src/StringUtil.cc, src/StringUtil.h, src/TestOperations.cc,
src/TestOperations.h, src/TestRoundInfo.h, src/TestStatistics.cc,
src/TestStatistics.h, src/UserCommandReader.cc,
src/UserCommandReader.h, src/UserCommands.cc,
src/UserCommands.h:
Remove uses of the ALLOC macro.
Update copyright information.
* src/BitArray.cc, src/BitArray.h, src/Bitset.h,
src/BuchiAutomaton.h, src/Config-lex.ll, src/Config-parse.yy,
src/DispUtil.h, src/EdgeContainer.h, src/Exception.h,
src/ExternalTranslator.cc, src/FormulaWriter.h, src/LbtWrapper.h,
src/NeverClaim-lex.ll, src/NeverClaim-parse.yy,
src/PathIterator.cc, src/PathIterator.h, src/Random.h,
src/SpinWrapper.cc, src/SpinWrapper.h, src/StateSpace.h,
src/StateSpaceProduct.h, src/StateSpaceRandomizer.h,
src/TempFsysName.cc, src/TempFsysName.h, src/translate.cc,
src/translate.h, src/TranslatorInterface.h:
Update copyright information.
* src/Configuration.cc (Configuration::showCommandLineHelp):
Use the PACKAGE_BUGREPORT macro instead of a hard-coded
e-mail address.
2004-08-02 Heikki Tauriainen <heikki.tauriainen@hut.fi> 2004-08-02 Heikki Tauriainen <heikki.tauriainen@hut.fi>
* Version 1.1.2 released. * Version 1.1.2 released.

22
lbtt/NEWS
View file

@ -1,5 +1,5 @@
lbtt NEWS -- history of user-visible changes. 02 Aug 2004 lbtt NEWS -- history of user-visible changes. 30 Aug 2005
Copyright (C) 2004 Heikki Tauriainen Copyright (C) 2005 Heikki Tauriainen
Permission is granted to anyone to make or distribute verbatim copies Permission is granted to anyone to make or distribute verbatim copies
of this document as received, in any medium, provided that the of this document as received, in any medium, provided that the
@ -10,7 +10,23 @@ Copyright (C) 2004 Heikki Tauriainen
provided also that they carry prominent notices stating who last provided also that they carry prominent notices stating who last
changed them. changed them.
Please send bug reports to <heikki.tauriainen@hut.fi>. Please send bug reports to <heikki.tauriainen@tkk.fi>.
Version 1.2.0
* This release adds direct support (contributed by Alexandre Duret-Lutz)
for the LTL-to-Büchi translator distributed with the Spot model
checking library (available at <http://spot.lip6.fr/>).
lbtt 1.2.0 also supports reading input formulas from standard input
(by using the command-line option `--formulafile=-'; when reading input
formulas from an actual file, the filename needs to be different from
"-").
Version 1.1.3
* This release fixes build problems with GCC 4 and more job control
problems.
Version 1.1.2 Version 1.1.2

2
lbtt/README
View file

@ -1,4 +1,4 @@
lbtt version 1.1.2 lbtt version 1.2.0
------------------ ------------------
lbtt is a tool for testing programs that translate formulas lbtt is a tool for testing programs that translate formulas

52
lbtt/configure.ac
View file

@ -1,8 +1,8 @@
# Process this file with autoconf to produce a configure script. # Process this file with autoconf to produce a configure script.
AC_PREREQ([2.59]) AC_PREREQ([2.59])
AC_INIT([lbtt], [1.1.2], [heikki.tauriainen@hut.fi]) AC_INIT([lbtt], [1.2.0], [heikki.tauriainen@tkk.fi])
AC_REVISION([Revision: 1.6]) AC_REVISION([Revision: 1.8])
AC_CONFIG_SRCDIR([src/main.cc]) AC_CONFIG_SRCDIR([src/main.cc])
AC_CONFIG_HEADERS([config.h]) AC_CONFIG_HEADERS([config.h])
AM_INIT_AUTOMAKE AM_INIT_AUTOMAKE
@ -124,52 +124,6 @@ AC_CHECK_HEADERS(
# Checks for typedefs, structures, and compiler characteristics. # Checks for typedefs, structures, and compiler characteristics.
# Check for the availability of the slist header (an extension to the C++
# Standard Template Library). (In GCC 3.x the header is in the ext/
# subdirectory of the directory containing the standard C++ headers.)
AC_MSG_CHECKING([for slist])
for slist_header in slist ext/slist no; do
if test "${slist_header}" != no; then
AC_PREPROC_IFELSE(
[AC_LANG_SOURCE([[#include <${slist_header}>]])],
[break])
fi
done
# Try to determine the C++ namespace in which the class slist resides.
# (For example, GCC versions >= 3.1 put slist into the __gnu_cxx namespace.)
if test "${slist_header}" != no; then
for slist_namespace in std __gnu_cxx error; do
if test "${slist_namespace}" != error; then
AC_COMPILE_IFELSE(
[AC_LANG_PROGRAM(
[[#include <${slist_header}>]],
[[${slist_namespace}::slist<int> s;]])],
[break])
fi
done
if test "${slist_namespace}" != error; then
AC_MSG_RESULT([header <${slist_header}>, typename ${slist_namespace}::slist])
AC_DEFINE(
[HAVE_SLIST],
[1],
[Define to 1 if you have the <slist> or <ext/slist> header file.])
AC_DEFINE_UNQUOTED(
[SLIST_NAMESPACE],
[${slist_namespace}],
[Define as the name of the C++ namespace containing slist.])
AC_SUBST([INCLUDE_SLIST_HEADER], ["#include <${slist_header}>"])
else
slist_header=no
fi
fi
if test "${slist_header}" = no; then
AC_MSG_RESULT([no])
fi
AC_LANG(C) AC_LANG(C)
AC_CHECK_TYPES( AC_CHECK_TYPES(
@ -191,7 +145,7 @@ AC_C_INLINE
# Checks for library functions. # Checks for library functions.
AC_CHECK_FUNCS( AC_CHECK_FUNCS(
[strchr strtod strtol strtoul strerror mkdir mkstemp open read write close popen pclose pipe fork execvp setsid getpid waitpid alarm sigaction sigprocmask sigemptyset sigaddset times sysconf], [strchr strtod strtol strtoul strerror mkdir mkstemp open read write close popen pclose pipe fork execvp getpgrp setpgid tcgetpgrp tcsetpgrp getpid waitpid alarm sigaction sigprocmask sigemptyset sigaddset times sysconf],
[], [],
[AC_MSG_ERROR([missing one of the library functions required for compilation])]) [AC_MSG_ERROR([missing one of the library functions required for compilation])])
AC_CHECK_FUNCS([strsignal isatty getopt_long]) AC_CHECK_FUNCS([strsignal isatty getopt_long])

69
lbtt/doc/lbtt.texi
View file

@ -14,13 +14,13 @@
This file documents how to use the LTL-to-B@"uchi This file documents how to use the LTL-to-B@"uchi
translator testbench @command{lbtt}. translator testbench @command{lbtt}.
Copyright @copyright{} 2004 Heikki Tauriainen Copyright @copyright{} 2005 Heikki Tauriainen
@ifinfo @ifinfo
@email{heikki.tauriainen@@hut.fi} @email{heikki.tauriainen@@tkk.fi}
@end ifinfo @end ifinfo
@ifnotinfo @ifnotinfo
@ifnothtml @ifnothtml
<@email{heikki.tauriainen@@hut.fi}> <@email{heikki.tauriainen@@tkk.fi}>
@end ifnothtml @end ifnothtml
@end ifnotinfo @end ifnotinfo
@ -64,12 +64,12 @@ under the above conditions for modified versions.
@title @command{lbtt} @title @command{lbtt}
@subtitle LTL-to-B@"uchi Translator Testbench @subtitle LTL-to-B@"uchi Translator Testbench
@subtitle @today, @command{lbtt} Versions 1.1.x @subtitle @today, @command{lbtt} Versions 1.2.x
@author Heikki Tauriainen <@email{heikki.tauriainen@@hut.fi}> @author Heikki Tauriainen <@email{heikki.tauriainen@@tkk.fi}>
@page @page
@vskip 0pt plus 1filll @vskip 0pt plus 1filll
Copyright @copyright{} 2004 Heikki Tauriainen Copyright @copyright{} 2005 Heikki Tauriainen
<@email{heikki.tauriainen@@hut.fi}> <@email{heikki.tauriainen@@tkk.fi}>
The latest version of this manual can be obtained from@* The latest version of this manual can be obtained from@*
<@url{http://www.tcs.hut.fi/Software/lbtt/}>. <@url{http://www.tcs.hut.fi/Software/lbtt/}>.
@ -103,8 +103,8 @@ under the above conditions for modified versions.
for translating propositional linear temporal logic formulas into for translating propositional linear temporal logic formulas into
B@"uchi automata. B@"uchi automata.
This is edition 1.1.0 of the @command{lbtt} documentation. This edition This is edition 1.2.0 of the @command{lbtt} documentation. This edition
applies to @command{lbtt} versions 1.1.x. applies to @command{lbtt} versions 1.2.x.
@command{lbtt} is free software, you may change and redistribute it @command{lbtt} is free software, you may change and redistribute it
under the terms of the GNU General Public License. @command{lbtt} under the terms of the GNU General Public License. @command{lbtt}
@ -299,7 +299,7 @@ for more information.
By default, all tests @command{lbtt} makes are based on randomly generated By default, all tests @command{lbtt} makes are based on randomly generated
input. However, the LTL formulas used as input for the LTL-to-B@"uchi input. However, the LTL formulas used as input for the LTL-to-B@"uchi
translators can be optionally given by the user by telling @command{lbtt} to translators can be optionally given by the user by telling @command{lbtt} to
read LTL formulas from a file read LTL formulas from a file or from standard input
(@pxref{--formulafile,,@samp{--formulafile} command line option}). (@pxref{--formulafile,,@samp{--formulafile} command line option}).
@cindex state space @cindex state space
@ -899,7 +899,7 @@ See also the web page@*
@url{http://www.tcs.hut.fi/Software/lbtt/formulaoptions.php} @url{http://www.tcs.hut.fi/Software/lbtt/formulaoptions.php}
@end ifinfo @end ifinfo
@ifnotinfo @ifnotinfo
<@uref{http://www.tcs.hut.fi/Software/lbtt/formulaoptions.php>} <@uref{http://www.tcs.hut.fi/Software/lbtt/formulaoptions.php}>
@end ifnotinfo @end ifnotinfo
for an interface to a small database for adjusting the operator priorities for an interface to a small database for adjusting the operator priorities
towards certain simple distributions. towards certain simple distributions.
@ -2121,12 +2121,13 @@ file @samp{config} in the current working directory.
@item @anchor{--formulafile}--formulafile=@var{FILE-NAME} @item @anchor{--formulafile}--formulafile=@var{FILE-NAME}
@vindex --formulafile @vindex --formulafile
@cindex LTL formula, reading from a file @cindex LTL formula, reading from a file or standard input
@cindex file formats, formula input file for @command{lbtt} @cindex file formats, formula input file for @command{lbtt}
This option instructs @command{lbtt} to read the LTL formulas used in the tests This option instructs @command{lbtt} to read the LTL formulas used in the tests
from a file instead of generating them randomly. The file should contain a from a file (or standard input) instead of generating them randomly. The
list of formulas, each on its own line in the file. The formulas can be special filename @samp{-} refers to standard input. Each
specified either in @command{lbtt}'s own prefix notation input formula should be followed by a newline. The formulas can be specified
either in @command{lbtt}'s own prefix notation
(@pxref{Format for LTL formulas}; also the infix notation used in output (@pxref{Format for LTL formulas}; also the infix notation used in output
messages is supported) or in a variety of formats found in messages is supported) or in a variety of formats found in
some LTL-to-B@"uchi translator implementations (Spin, LTL2BA, LTL2AUT, some LTL-to-B@"uchi translator implementations (Spin, LTL2BA, LTL2AUT,
@ -2522,8 +2523,8 @@ This option sets the priority for the logical ``exclusive or'' operator.
Note also the @samp{--formulafile=@var{FILE-NAME}} option Note also the @samp{--formulafile=@var{FILE-NAME}} option
(@pxref{--formulafile,,@samp{--formulafile} option}), which can be used to (@pxref{--formulafile,,@samp{--formulafile} option}), which can be used to
instruct @command{lbtt} to read LTL formulas from a file instead of generating instruct @command{lbtt} to read LTL formulas from a file (or standard input)
them randomly. instead of generating them randomly.
@ -2665,9 +2666,9 @@ Random state space generation parameters.
@item @item
Random LTL formula generation parameters (unless reading LTL formulas from Random LTL formula generation parameters (unless reading LTL formulas from
a file; @pxref{--formulafile,,@samp{--formulafile} command line option}). an external source; @pxref{--formulafile,,@samp{--formulafile} command line
This includes information about all enabled formula operators and their option}). This includes information about all enabled formula operators and
priorities. When using the command line option their priorities. When using the command line option
@samp{--showoperatordistribution} @samp{--showoperatordistribution}
(@pxref{--showoperatordistribution,,@samp{--showoperatordistribution} option}), (@pxref{--showoperatordistribution,,@samp{--showoperatordistribution} option}),
@command{lbtt} shows also the expected number of occurrence of each @command{lbtt} shows also the expected number of occurrence of each
@ -4025,6 +4026,25 @@ See
<@uref{http://spinroot.com/spin/whatispin.html}> <@uref{http://spinroot.com/spin/whatispin.html}>
@end ifnotinfo @end ifnotinfo
for more information. for more information.
@item
@cindex Spot
@ifnottex
Spot @ref{[DP04]}
@end ifnottex
@iftex
Spot [DP04]
@end iftex
--- a model checking library that includes a module for translating LTL
formulas into B@"uchi automata incorporating optimization techniques from
several different sources. See
@ifinfo
@url{http://spot.lip6.fr/}
@end ifinfo
@ifnotinfo
<@uref{http://spot.lip6.fr/}>
@end ifnotinfo
for more information.
@end itemize @end itemize
To use @command{lbtt} for testing the LTL-to-B@"uchi translators included in To use @command{lbtt} for testing the LTL-to-B@"uchi translators included in
@ -4056,7 +4076,7 @@ LTL formula operators available for generating random LTL formulas with
about which operators are supported, and then change the parameters in about which operators are supported, and then change the parameters in
@command{lbtt}'s configuration file accordingly to disable the unsupported @command{lbtt}'s configuration file accordingly to disable the unsupported
operators (or instruct @command{lbtt} to read the formulas from an external operators (or instruct @command{lbtt} to read the formulas from an external
file by invoking @command{lbtt} with the source by invoking @command{lbtt} with the
@ref{--formulafile,,@samp{--formulafile} command line option}). @ref{--formulafile,,@samp{--formulafile} command line option}).
The @command{lbtt-translate} utility can also be invoked directly from the The @command{lbtt-translate} utility can also be invoked directly from the
@ -4087,6 +4107,13 @@ International Conference on Computer Aided Verification (CAV'99)}, volume 1633
of @i{Lecture Notes in Computer Science}, pages 249---260. Springer-Verlag, of @i{Lecture Notes in Computer Science}, pages 249---260. Springer-Verlag,
1999. 1999.
@item @anchor{[DP04]} [DP04]
A.@: Duret-Lutz and D.@: Poitrenaud. SPOT: An Extensible Model Checking Library
Using Transition-Based Generalized B@"uchi Automata. In
@i{Proceedings of the 12th IEEE/ACM International Symposium on Modeling,
Analysis, and Simulation of Computer and Telecommunication Systems
(MASCOTS 2004)}, pages 76--83. IEEE Computer Society Press, 2004.
@item @anchor{[EH00]} [EH00] @item @anchor{[EH00]} [EH00]
K.@: Etessami and G.@: Holzmann. Optimizing B@"uchi automata. In K.@: Etessami and G.@: Holzmann. Optimizing B@"uchi automata. In
@i{Proceedings of the 11th International Conference on Concurrency Theory @i{Proceedings of the 11th International Conference on Concurrency Theory

4
lbtt/src/BitArray.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

14
lbtt/src/BitArray.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -359,7 +359,10 @@ inline void BitArray::set(const unsigned long int bit_count)
* *
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
{ {
memset(static_cast<void*>(bits), 0xFF, (bit_count + 7) >> 3); unsigned long int bsize = bit_count >> 3;
memset(static_cast<void*>(bits), 0xFF, bsize);
if ((bit_count & 0x07) != 0)
bits[bsize] |= (1 << (bit_count & 7)) - 1;
} }
/* ========================================================================= */ /* ========================================================================= */
@ -390,7 +393,10 @@ inline void BitArray::clear(const unsigned long int bit_count)
* *
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
{ {
memset(static_cast<void*>(bits), 0, (bit_count + 7) >> 3); unsigned long int bsize = bit_count >> 3;
memset(static_cast<void*>(bits), 0, bsize);
if ((bit_count & 0x07) != 0)
bits[bsize] &= ~((1 << (bit_count & 7)) - 1);
} }
/* ========================================================================= */ /* ========================================================================= */

4
lbtt/src/Bitset.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

19
lbtt/src/BuchiAutomaton.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -288,27 +288,20 @@ void BuchiAutomaton::read(istream& input_stream)
* to the interval [0...(number of states - 1)]. * to the interval [0...(number of states - 1)].
*/ */
map<long int, size_type, less<long int>, ALLOC(size_type) > map<long int, size_type> state_number_map;
state_number_map;
pair<long int, size_type> state_mapping(0, 0); pair<long int, size_type> state_mapping(0, 0);
pair<map<long int, size_type, less<long int>, ALLOC(size_type) > pair<map<long int, size_type>::const_iterator, bool> state_finder;
::const_iterator,
bool>
state_finder;
/* /*
* Also the acceptance set numbers will be mapped to the interval * Also the acceptance set numbers will be mapped to the interval
* [0...(number of acceptance sets - 1)]. * [0...(number of acceptance sets - 1)].
*/ */
map<long int, unsigned long int, less<long int>, ALLOC(unsigned long int) > map<long int, unsigned long int> acceptance_set_map;
acceptance_set_map;
pair<long int, unsigned long int> acceptance_set_mapping(0, 0); pair<long int, unsigned long int> acceptance_set_mapping(0, 0);
pair<map<long int, unsigned long int, less<long int>, pair<map<long int, unsigned long int>::const_iterator, bool>
ALLOC(unsigned long int) >::const_iterator,
bool>
acceptance_set_finder; acceptance_set_finder;
/* /*

4
lbtt/src/BuchiAutomaton.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

10
lbtt/src/BuchiProduct.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -28,8 +28,7 @@ namespace Graph
* *
*****************************************************************************/ *****************************************************************************/
map< ::Ltl::LtlFormula*, BuchiProduct::SatisfiabilityMapping, map< ::Ltl::LtlFormula*, BuchiProduct::SatisfiabilityMapping>
less< ::Ltl::LtlFormula*>, ALLOC(BuchiProduct::SatisfiabilityMapping) >
BuchiProduct::sat_cache; BuchiProduct::sat_cache;
@ -73,8 +72,7 @@ bool BuchiProduct::synchronizable
guard_1 = swap_guard; guard_1 = swap_guard;
} }
map<LtlFormula*, SatisfiabilityMapping, less<LtlFormula*>, map<LtlFormula*, SatisfiabilityMapping>::iterator
ALLOC(SatisfiabilityMapping) >::iterator
sat_cache_element = sat_cache.find(guard_1); sat_cache_element = sat_cache.find(guard_1);
if (sat_cache_element == sat_cache.end()) if (sat_cache_element == sat_cache.end())

16
lbtt/src/BuchiProduct.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -142,18 +142,16 @@ private:
* automata. * automata.
*/ */
typedef map< ::Ltl::LtlFormula*, bool, /* Type definition for */ typedef map< ::Ltl::LtlFormula*, bool> /* Type definition for */
less< ::Ltl::LtlFormula*>, /* storing information */ SatisfiabilityMapping; /* storing information
ALLOC(bool) > /* about the */ * about the
SatisfiabilityMapping; /* satisfiability of the * satisfiability of the
* guards of product * guards of product
* transitions. * transitions.
*/ */
static map< ::Ltl::LtlFormula*, /* Result cache for */ static map< ::Ltl::LtlFormula*, /* Result cache for */
SatisfiabilityMapping, /* satisfiability tests. */ SatisfiabilityMapping> /* satisfiability tests. */
less< ::Ltl::LtlFormula*>,
ALLOC(SatisfiabilityMapping) >
sat_cache; sat_cache;
}; };

4
lbtt/src/Config-lex.ll
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

4
lbtt/src/Config-parse.yy
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

62
lbtt/src/Configuration.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -96,8 +96,7 @@ Configuration::~Configuration()
* *
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
{ {
for (vector<AlgorithmInformation, ALLOC(AlgorithmInformation) > for (vector<AlgorithmInformation>::const_iterator it = algorithms.begin();
::const_iterator it = algorithms.begin();
it != algorithms.end(); ++it) it != algorithms.end(); ++it)
{ {
for (vector<string>::size_type p = 0; p <= it->num_parameters; ++p) for (vector<string>::size_type p = 0; p <= it->num_parameters; ++p)
@ -223,7 +222,7 @@ void Configuration::read(int argc, char* argv[])
config_file_line_number = -1; config_file_line_number = -1;
typedef pair<const OPTIONSTRUCT*, const char*> Parameter; typedef pair<const OPTIONSTRUCT*, const char*> Parameter;
vector<Parameter, ALLOC(Parameter) > parameters; vector<Parameter> parameters;
/* /*
* Preprocess the command line parameters. At this point only those special * Preprocess the command line parameters. At this point only those special
@ -351,7 +350,7 @@ void Configuration::read(int argc, char* argv[])
* configuration file. * configuration file.
*/ */
vector<Parameter, ALLOC(Parameter) >::const_iterator parameter; vector<Parameter>::const_iterator parameter;
try try
{ {
@ -655,7 +654,7 @@ void Configuration::read(int argc, char* argv[])
try try
{ {
IntervalList algorithm_ids; IntervalList algorithm_ids;
vector<string, ALLOC(string) > nonnumeric_algorithm_ids; vector<string> nonnumeric_algorithm_ids;
string id_string string id_string
= substituteInQuotedString(parameter->second, ",", "\n", = substituteInQuotedString(parameter->second, ",", "\n",
INSIDE_QUOTES); INSIDE_QUOTES);
@ -664,14 +663,13 @@ void Configuration::read(int argc, char* argv[])
algorithms.size() - 1, algorithms.size() - 1,
&nonnumeric_algorithm_ids); &nonnumeric_algorithm_ids);
for (vector<string, ALLOC(string) >::iterator for (vector<string>::iterator
id = nonnumeric_algorithm_ids.begin(); id = nonnumeric_algorithm_ids.begin();
id != nonnumeric_algorithm_ids.end(); id != nonnumeric_algorithm_ids.end();
++id) ++id)
{ {
*id = unquoteString(substituteInQuotedString(*id, "\n", ",")); *id = unquoteString(substituteInQuotedString(*id, "\n", ","));
map<string, unsigned long int, less<string>, map<string, unsigned long int>::const_iterator id_finder
ALLOC(unsigned long int) >::const_iterator id_finder
= algorithm_names.find(*id); = algorithm_names.find(*id);
if (id_finder == algorithm_names.end()) if (id_finder == algorithm_names.end())
throw ConfigurationException throw ConfigurationException
@ -777,8 +775,7 @@ void Configuration::read(int argc, char* argv[])
bool unary_operator_allowed = false; bool unary_operator_allowed = false;
for (map<int, int, less<int>, ALLOC(int) >::iterator for (map<int, int>::iterator it = formula_options.symbol_priority.begin();
it = formula_options.symbol_priority.begin();
it != formula_options.symbol_priority.end(); ++it) it != formula_options.symbol_priority.end(); ++it)
{ {
if (it->second == -1) if (it->second == -1)
@ -804,7 +801,7 @@ void Configuration::read(int argc, char* argv[])
int total_long_unary_priority = 0; int total_long_unary_priority = 0;
int total_binary_priority = 0; int total_binary_priority = 0;
for (map<int, int, less<int>, ALLOC(int) >::const_iterator for (map<int, int>::const_iterator
it = formula_options.symbol_priority.begin(); it = formula_options.symbol_priority.begin();
it != formula_options.symbol_priority.end(); ++it) it != formula_options.symbol_priority.end(); ++it)
{ {
@ -873,7 +870,7 @@ void Configuration::read(int argc, char* argv[])
k <= formula_options.formula_generator.max_size; k <= formula_options.formula_generator.max_size;
k++) k++)
{ {
for (map<int, int, less<int>, ALLOC(int) >::const_iterator for (map<int, int>::const_iterator
op = formula_options.symbol_priority.begin(); op = formula_options.symbol_priority.begin();
op != formula_options.symbol_priority.end(); op != formula_options.symbol_priority.end();
++op) ++op)
@ -984,11 +981,9 @@ void Configuration::print(ostream& stream, int indent) const
estream << '\n' + string(indent + 2, ' ') + "Implementations:\n"; estream << '\n' + string(indent + 2, ' ') + "Implementations:\n";
vector<AlgorithmInformation, ALLOC(AlgorithmInformation) >::size_type vector<AlgorithmInformation>::size_type algorithm_number = 0;
algorithm_number = 0;
for (vector<AlgorithmInformation, ALLOC(AlgorithmInformation) > for (vector<AlgorithmInformation>::const_iterator a = algorithms.begin();
::const_iterator a = algorithms.begin();
a != algorithms.end(); a != algorithms.end();
++a) ++a)
{ {
@ -1161,9 +1156,13 @@ void Configuration::print(ostream& stream, int indent) const
number_of_available_variables == 1 ? "" : "s"); number_of_available_variables == 1 ? "" : "s");
} }
else else
estream << "Reading LTL formulas from `" {
+ global_options.formula_input_filename estream << "Reading LTL formulas from ";
+ "'."; if (global_options.formula_input_filename == "-")
estream << "standard input.";
else
estream << "`" + global_options.formula_input_filename + "'.";
}
estream << '\n' + string(indent + 4, ' '); estream << '\n' + string(indent + 4, ' ');
@ -1222,7 +1221,7 @@ void Configuration::print(ostream& stream, int indent) const
bool first_printed = false; bool first_printed = false;
for (map<int, int, less<int>, ALLOC(int) >::const_iterator for (map<int, int>::const_iterator
op = formula_options.symbol_priority.begin(); op = formula_options.symbol_priority.begin();
op != formula_options.symbol_priority.end(); op != formula_options.symbol_priority.end();
++op) ++op)
@ -1263,7 +1262,7 @@ void Configuration::print(ostream& stream, int indent) const
int max_operators_per_line int max_operators_per_line
= (formula_options.symbol_distribution.empty() ? 7 : 6); = (formula_options.symbol_distribution.empty() ? 7 : 6);
for (map<int, int, less<int>, ALLOC(int) >::const_iterator op for (map<int, int>::const_iterator op
= formula_options.symbol_priority.begin(); = formula_options.symbol_priority.begin();
op != formula_options.symbol_priority.end(); op != formula_options.symbol_priority.end();
++op) ++op)
@ -1340,9 +1339,7 @@ void Configuration::print(ostream& stream, int indent) const
/* ========================================================================= */ /* ========================================================================= */
string Configuration::algorithmString string Configuration::algorithmString
(vector<Configuration::AlgorithmInformation, (vector<Configuration::AlgorithmInformation>::size_type algorithm_id) const
ALLOC(Configuration::AlgorithmInformation) >::size_type
algorithm_id) const
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Constructs a string with an algorithm identifer and the name * Description: Constructs a string with an algorithm identifer and the name
@ -1387,7 +1384,8 @@ void Configuration::showCommandLineHelp(const char* program_name)
" --enable=IMPLEMENTATION-ID[,IMPLEMENTATION-ID,...]\n" " --enable=IMPLEMENTATION-ID[,IMPLEMENTATION-ID,...]\n"
" Include implementation(s) into " " Include implementation(s) into "
"tests\n" "tests\n"
" --formulafile=FILE Read LTL formulas from FILE\n" " --formulafile=FILE Read LTL formulas from FILE "
"(- = standard input)\n"
" --globalmodelcheck Use global model checking in " " --globalmodelcheck Use global model checking in "
"tests\n" "tests\n"
" (equivalent to " " (equivalent to "
@ -1543,7 +1541,7 @@ void Configuration::showCommandLineHelp(const char* program_name)
" --truthprobability=PROBABILITY\n" " --truthprobability=PROBABILITY\n"
" Set truth probability of " " Set truth probability of "
"propositions (0.0--1.0)\n\n" "propositions (0.0--1.0)\n\n"
"Report bugs to <heikki.tauriainen@hut.fi>.\n"; "Report bugs to <" PACKAGE_BUGREPORT ">.\n";
} }
/* ========================================================================= */ /* ========================================================================= */
@ -1673,7 +1671,7 @@ void Configuration::registerAlgorithm
: string("")), : string("")),
error); error);
vector<string, ALLOC(string) > params; vector<string> params;
sliceString(unquoteString(substituteInQuotedString(parameters, " \t", "\n\n", sliceString(unquoteString(substituteInQuotedString(parameters, " \t", "\n\n",
OUTSIDE_QUOTES)), OUTSIDE_QUOTES)),
"\n", "\n",
@ -1702,7 +1700,7 @@ void Configuration::registerAlgorithm
memcpy(static_cast<void*>(algorithm_information.parameters[0]), memcpy(static_cast<void*>(algorithm_information.parameters[0]),
static_cast<const void*>(path.c_str()), path.size() + 1); static_cast<const void*>(path.c_str()), path.size() + 1);
for (vector<string, ALLOC(string) >::size_type p = 0; for (vector<string>::size_type p = 0;
p < algorithm_information.num_parameters; p < algorithm_information.num_parameters;
++p) ++p)
{ {
@ -1875,9 +1873,9 @@ void Configuration::readInteractivity(const string& value)
global_options.interactive = NEVER; global_options.interactive = NEVER;
global_options.handle_breaks = false; global_options.handle_breaks = false;
vector<string, ALLOC(string) > modes; vector<string> modes;
::StringUtil::sliceString(value, ",", modes); ::StringUtil::sliceString(value, ",", modes);
for (vector<string, ALLOC(string) >::const_iterator mode = modes.begin(); for (vector<string>::const_iterator mode = modes.begin();
mode != modes.end(); mode != modes.end();
++mode) ++mode)
{ {

44
lbtt/src/Configuration.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -62,9 +62,9 @@ public:
struct AlgorithmInformation; /* See below. */ struct AlgorithmInformation; /* See below. */
string algorithmString /* Formats the the id */ string algorithmString /* Formats the the id */
(vector<AlgorithmInformation, /* of an algorithm and */ (vector<AlgorithmInformation>::size_type /* of an algorithm and */
ALLOC(AlgorithmInformation) >::size_type/* the name of the */ algorithm_id) const; /* the name of the
algorithm_id) const; /* algorithm into a * algorithm into a
* string. * string.
*/ */
@ -311,11 +311,12 @@ public:
* LTL formula symbols. * LTL formula symbols.
*/ */
map<int, int, less<int>, ALLOC(int) > /* Priorities for LTL */ map<int, int> symbol_priority; /* Priorities for LTL
symbol_priority; /* formula symbols. */ * formula symbols.
*/
map<int, double, less<int>, ALLOC(double) > /* Expected numbers of */ map<int, double> symbol_distribution; /* Expected numbers of
symbol_distribution; /* occurrence for the * occurrence for the
* different formula * different formula
* operators. * operators.
*/ */
@ -375,15 +376,15 @@ public:
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
vector<AlgorithmInformation, /* A vector containing */ vector<AlgorithmInformation> algorithms; /* A vector containing
ALLOC(AlgorithmInformation) > algorithms; /* information about the * information about the
* algorithms used in * algorithms used in
* the tests. * the tests.
*/ */
map<string, unsigned long int, less<string>, /* Mapping between */ map<string, unsigned long int> algorithm_names; /* Mapping between
ALLOC(unsigned long int) > /* algorithm names and */ * algorithm names and
algorithm_names; /* their numeric * their numeric
* identifiers. * identifiers.
*/ */
@ -511,14 +512,13 @@ private:
OPT_STATESPACEPROPOSITIONS, OPT_STATESPACEPROPOSITIONS,
OPT_STATESPACESIZE, OPT_TRUTHPROBABILITY}; OPT_STATESPACESIZE, OPT_TRUTHPROBABILITY};
typedef map<pair<int, int>, double, /* Type definitions for */ typedef map<pair<int, int>, double> /* Type definitions for */
less<pair<int, int> >, /* the result cache used */ ProbabilityMapElement; /* the result cache used */
ALLOC(double) > /* for computing the */ /* for computing the */
ProbabilityMapElement; /* probability */ typedef map<int, ProbabilityMapElement> /* probability */
typedef map<int, ProbabilityMapElement, /* distribution of LTL */ ProbabilityMap; /* distribution of LTL
less<int>, /* formula operators. */ * formula operators.
ALLOC(ProbabilityMapElement) > */
ProbabilityMap;
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */

12
lbtt/src/DispUtil.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -32,10 +32,10 @@
namespace DispUtil namespace DispUtil
{ {
stack<StreamFormatting, /* Stack for storing the */ stack<StreamFormatting, deque<StreamFormatting> > /* Stack for storing the */
deque<StreamFormatting, /* previous states of an */ stream_formatting_stack; /* previous states of an
ALLOC(StreamFormatting) > > /* output stream. */ * output stream.
stream_formatting_stack; */
/* ========================================================================= */ /* ========================================================================= */
void changeStreamFormatting void changeStreamFormatting

4
lbtt/src/DispUtil.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

4
lbtt/src/EdgeContainer.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

4
lbtt/src/Exception.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

4
lbtt/src/ExternalTranslator.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

13
lbtt/src/ExternalTranslator.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -174,12 +174,13 @@ private:
* objects. * objects.
*/ */
stack<TempFsysName*, /* Stack for storing */ stack<TempFsysName*, deque<TempFsysName*> > /* Stack for storing */
deque<TempFsysName*, /* temporary file */ temporary_file_objects; /* temporary file
ALLOC(TempFsysName*) > > /* information. */ * information.
temporary_file_objects; */
friend class SpinWrapper; /* Friend declarations. */ friend class SpinWrapper; /* Friend declarations. */
friend class SpotWrapper;
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */

6
lbtt/src/FormulaRandomizer.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -92,7 +92,7 @@ LtlFormula* FormulaRandomizer::recGenerate(unsigned long int target_size)
* *
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
{ {
vector<IntegerPair, ALLOC(IntegerPair) >::const_iterator symbol_priority; vector<IntegerPair>::const_iterator symbol_priority;
LtlFormula* formula; LtlFormula* formula;
long int x; long int x;

55
lbtt/src/FormulaRandomizer.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -87,16 +87,16 @@ public:
* `reset'. * `reset'.
*/ */
const map<unsigned long int, unsigned long int, /* Get the numbers of */ const map<unsigned long int, unsigned long int>& /* Get the numbers of */
less<unsigned long int>, /* different atomic */ propositionStatistics() const; /* different atomic
ALLOC(unsigned long int) >& /* propositions */ * propositions
propositionStatistics() const; /* generated since the * generated since the
* last call to `reset'. * last call to `reset'.
*/ */
const map<int, unsigned long int, less<int>, /* Get the numbers of */ const map<int, unsigned long int>& /* Get the numbers of */
ALLOC(unsigned long int) >& /* different symbols */ symbolStatistics() const; /* different symbols
symbolStatistics() const; /* generated since the * generated since the
* last call to `reset'. * last call to `reset'.
*/ */
@ -124,21 +124,20 @@ private:
typedef pair<int, int> IntegerPair; typedef pair<int, int> IntegerPair;
vector<IntegerPair, ALLOC(IntegerPair) > /* Operand symbols and */ vector<IntegerPair> /* Operand symbols and */
propositional_symbol_priorities; /* their priorities in propositional_symbol_priorities; /* their priorities in
* random formulae. * random formulae.
*/ */
vector<IntegerPair, ALLOC(IntegerPair) > /* Operators and their */ vector<IntegerPair> short_formula_operators; /* Operators and their
short_formula_operators; /* priorities in random * priorities in random
* formulae of size * formulae of size two.
* two.
*/ */
vector<IntegerPair, ALLOC(IntegerPair) > /* Operators and their */ vector<IntegerPair> long_formula_operators; /* Operators and their
long_formula_operators; /* priorities in random * priorities in random
* formulae of size * formulae of size greater
* greater than two. * than two.
*/ */
unsigned long int number_of_generated_formulas; /* Number of generated unsigned long int number_of_generated_formulas; /* Number of generated
@ -146,14 +145,15 @@ private:
* last call to `reset'. * last call to `reset'.
*/ */
map<unsigned long int, unsigned long int, /* Number of different */ map<unsigned long int, unsigned long int> /* Number of different */
less<unsigned long int>, /* atomic propositions */ proposition_statistics; /* atomic propositions
ALLOC(unsigned long int) > /* generated since the */ * generated since the
proposition_statistics; /* last call to `reset' */ * last call to `reset'
*/
map<int, unsigned long int, less<int>, /* Number of different */ map<int, unsigned long int> symbol_statistics; /* Number of different
ALLOC(unsigned long int) > /* formula symbols */ * formula symbols
symbol_statistics; /* generated since the * generated since the
* last call to `reset'. * last call to `reset'.
*/ */
}; };
@ -289,8 +289,7 @@ inline unsigned long int FormulaRandomizer::numberOfFormulas() const
} }
/* ========================================================================= */ /* ========================================================================= */
inline const map<unsigned long int, unsigned long int, less<unsigned long int>, inline const map<unsigned long int, unsigned long int>&
ALLOC(unsigned long int) >&
FormulaRandomizer::propositionStatistics() const FormulaRandomizer::propositionStatistics() const
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
@ -308,7 +307,7 @@ FormulaRandomizer::propositionStatistics() const
} }
/* ========================================================================= */ /* ========================================================================= */
inline const map<int, unsigned long int, less<int>, ALLOC(unsigned long int) >& inline const map<int, unsigned long int>&
FormulaRandomizer::symbolStatistics() const FormulaRandomizer::symbolStatistics() const
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *

4
lbtt/src/FormulaWriter.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

127
lbtt/src/Graph.h.in
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -193,16 +193,16 @@ public:
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
protected: protected:
vector<Node*, ALLOC(Node*) > nodes; /* Nodes of the graph. vector<Node*> nodes; /* Nodes of the graph.
* Derived classes can * Derived classes can
* access this vector * access this vector
* directly. * directly.
*/ */
public: public:
typedef typename /* Type definition for */ typedef typename vector<Node*>::size_type /* Type definition for */
vector<Node*, ALLOC(Node*) >::size_type /* the size of the */ size_type; /* the size of the
size_type; /* graph. The size can * graph. The size can
* be no greater than * be no greater than
* the maximum size of * the maximum size of
* the vector containing * the vector containing
@ -214,8 +214,9 @@ public:
* edges. * edges.
*/ */
typedef deque<PathElement, ALLOC(PathElement) > /* Type definition for */ typedef deque<PathElement> Path; /* Type definition for
Path; /* paths in a graph. */ * paths in a graph.
*/
typedef pair<size_type, size_type> StateIdPair; /* Type definition for a typedef pair<size_type, size_type> StateIdPair; /* Type definition for a
* pair of state * pair of state
@ -502,8 +503,7 @@ public:
* *
*****************************************************************************/ *****************************************************************************/
class EdgeList : public list<Graph<EdgeList>::Edge*, class EdgeList : public list<Graph<EdgeList>::Edge*>
ALLOC(Graph<EdgeList>::Edge*) >
{ {
public: public:
EdgeList(); /* Constructor. */ EdgeList(); /* Constructor. */
@ -518,14 +518,12 @@ public:
* the end of the list. * the end of the list.
*/ */
list<Graph<EdgeList>::Edge*, /* Functions for finding */ list<Graph<EdgeList>::Edge*>::const_iterator /* Functions for finding */
ALLOC(Graph<EdgeList>::Edge*) > /* an element in the */ find(const Graph<EdgeList>::Edge* edge) const; /* an element in the
::const_iterator /* list. */ * list.
find(const Graph<EdgeList>::Edge* edge) const; */
list<Graph<EdgeList>::Edge*, list<Graph<EdgeList>::Edge*>::iterator
ALLOC(Graph<EdgeList>::Edge*) >
::iterator
find(const Graph<EdgeList>::Edge* edge); find(const Graph<EdgeList>::Edge* edge);
}; };
@ -540,8 +538,7 @@ public:
#ifdef HAVE_SLIST #ifdef HAVE_SLIST
class EdgeSlist : public slist<Graph<EdgeSlist>::Edge*, class EdgeSlist : public slist<Graph<EdgeSlist>::Edge*>
ALLOC(Graph<EdgeSlist>::Edge*) >
{ {
public: public:
EdgeSlist(); /* Constructor. */ EdgeSlist(); /* Constructor. */
@ -557,14 +554,12 @@ public:
* list. * list.
*/ */
slist<Graph<EdgeSlist>::Edge*, /* Functions for finding */ slist<Graph<EdgeSlist>::Edge*>::const_iterator /* Functions for finding */
ALLOC(Graph<EdgeSlist>::Edge*) > /* an element in the */ find(const Graph<EdgeSlist>::Edge* edge) const; /* an element in the
::const_iterator /* list. */ * list.
find(const Graph<EdgeSlist>::Edge* edge) const; */
slist<Graph<EdgeSlist>::Edge*, slist<Graph<EdgeSlist>::Edge*>::iterator
ALLOC(Graph<EdgeSlist>::Edge*) >
::iterator
find(const Graph<EdgeSlist>::Edge* edge); find(const Graph<EdgeSlist>::Edge* edge);
}; };
@ -578,8 +573,7 @@ public:
* *
*****************************************************************************/ *****************************************************************************/
class EdgeVector : public vector<Graph<EdgeVector>::Edge*, class EdgeVector : public vector<Graph<EdgeVector>::Edge*>
ALLOC(Graph<EdgeVector>::Edge*) >
{ {
public: public:
EdgeVector(); /* Constructor. */ EdgeVector(); /* Constructor. */
@ -595,15 +589,11 @@ public:
* to edges. * to edges.
*/ */
vector<Graph<EdgeVector>::Edge*, /* Functions for finding */ vector<Graph<EdgeVector>::Edge*>::const_iterator /* Functions for finding */
ALLOC(Graph<EdgeVector>::Edge*) > /* an element in the */ find(const Graph<EdgeVector>::Edge* edge) /* an element in the */
::const_iterator /* container. */ const; /* container. */
find(const Graph<EdgeVector>::Edge* edge)
const;
vector<Graph<EdgeVector>::Edge*, vector<Graph<EdgeVector>::Edge*>::iterator
ALLOC(Graph<EdgeVector>::Edge*) >
::iterator
find(const Graph<EdgeVector>::Edge* edge); find(const Graph<EdgeVector>::Edge* edge);
}; };
@ -616,8 +606,7 @@ public:
*****************************************************************************/ *****************************************************************************/
class EdgeSet : public set<Graph<EdgeSet>::Edge*, class EdgeSet : public set<Graph<EdgeSet>::Edge*,
Graph<EdgeSet>::Edge::ptr_less, Graph<EdgeSet>::Edge::ptr_less>
ALLOC(Graph<EdgeSet>::Edge*) >
{ {
}; };
@ -630,8 +619,7 @@ class EdgeSet : public set<Graph<EdgeSet>::Edge*,
*****************************************************************************/ *****************************************************************************/
class EdgeMultiSet : public multiset<Graph<EdgeMultiSet>::Edge*, class EdgeMultiSet : public multiset<Graph<EdgeMultiSet>::Edge*,
Graph<EdgeMultiSet>::Edge::ptr_less, Graph<EdgeMultiSet>::Edge::ptr_less>
ALLOC(Graph<EdgeMultiSet>::Edge*) >
{ {
}; };
@ -757,7 +745,7 @@ Graph<EdgeContainer>::Graph(const size_type initial_number_of_nodes) :
{ {
nodes.reserve(initial_number_of_nodes); nodes.reserve(initial_number_of_nodes);
for (typename vector<Node*, ALLOC(Node*) >::iterator node = nodes.begin(); for (typename vector<Node*>::iterator node = nodes.begin();
node != nodes.end(); node != nodes.end();
++node) ++node)
*node = new Node(); *node = new Node();
@ -779,8 +767,7 @@ Graph<EdgeContainer>::Graph(const Graph<EdgeContainer>& graph)
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
{ {
nodes.reserve(graph.nodes.size()); nodes.reserve(graph.nodes.size());
for (typename vector<Node*, ALLOC(Node*) >::const_iterator for (typename vector<Node*>::const_iterator node = graph.nodes.begin();
node = graph.nodes.begin();
node != graph.nodes.end(); ++node) node != graph.nodes.end(); ++node)
nodes.push_back(new Node(**node)); nodes.push_back(new Node(**node));
} }
@ -806,8 +793,7 @@ Graph<EdgeContainer>& Graph<EdgeContainer>::operator=
clear(); clear();
nodes.reserve(graph.nodes.size()); nodes.reserve(graph.nodes.size());
for (typename vector<Node*, ALLOC(Node*) >::const_iterator for (typename vector<Node*>::const_iterator node = graph.nodes.begin();
node = graph.nodes.begin();
node != graph.nodes.end(); node != graph.nodes.end();
++node) ++node)
nodes.push_back(new Node(**node)); nodes.push_back(new Node(**node));
@ -850,8 +836,7 @@ void Graph<EdgeContainer>::clear()
* *
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
{ {
for (typename vector<Node*, ALLOC(Node*) >::reverse_iterator for (typename vector<Node*>::reverse_iterator node = nodes.rbegin();
node = nodes.rbegin();
node != nodes.rend(); node != nodes.rend();
++node) ++node)
delete *node; delete *node;
@ -997,8 +982,7 @@ Graph<EdgeContainer>::stats() const
result.first = nodes.size(); result.first = nodes.size();
result.second = 0; result.second = 0;
for (typename vector<Node*, ALLOC(Node*) >::const_iterator for (typename vector<Node*>::const_iterator node = nodes.begin();
node = nodes.begin();
node != nodes.end(); ++node) node != nodes.end(); ++node)
result.second += (*node)->edges().size(); result.second += (*node)->edges().size();
@ -1032,7 +1016,7 @@ Graph<EdgeContainer>::subgraphStats(const size_type index) const
if (index >= s) if (index >= s)
throw NodeIndexException(); throw NodeIndexException();
stack<size_type, deque<size_type, ALLOC(size_type) > > unprocessed_nodes; stack<size_type, deque<size_type> > unprocessed_nodes;
BitArray visited_nodes(s); BitArray visited_nodes(s);
visited_nodes.clear(s); visited_nodes.clear(s);
@ -1764,8 +1748,7 @@ inline void EdgeList::insert(Graph<EdgeList>::Edge* edge)
} }
/* ========================================================================= */ /* ========================================================================= */
inline list<Graph<EdgeList>::Edge*, ALLOC(Graph<EdgeList>::Edge*) > inline list<Graph<EdgeList>::Edge*>::const_iterator
::const_iterator
EdgeList::find(const Graph<EdgeList>::Edge* edge) const EdgeList::find(const Graph<EdgeList>::Edge* edge) const
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
@ -1776,9 +1759,9 @@ EdgeList::find(const Graph<EdgeList>::Edge* edge) const
* between the actual values of the edges (not the * between the actual values of the edges (not the
* pointers). * pointers).
* *
* Returns: A list<Graph<EdgeList>::Edge*, ALLOC>::const_iterator * Returns: A list<Graph<EdgeList>::Edge*>::const_iterator
* pointing to the edge in the list or * pointing to the edge in the list or
* list<Graph<EdgeList>::Edge*, ALLOC>::end() if the edge is * list<Graph<EdgeList>::Edge*>::end() if the edge is
* not found in the list. * not found in the list.
* *
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
@ -1793,7 +1776,7 @@ EdgeList::find(const Graph<EdgeList>::Edge* edge) const
} }
/* ========================================================================= */ /* ========================================================================= */
inline list<Graph<EdgeList>::Edge*, ALLOC(Graph<EdgeList>::Edge*) >::iterator inline list<Graph<EdgeList>::Edge*>::iterator
EdgeList::find(const Graph<EdgeList>::Edge* edge) EdgeList::find(const Graph<EdgeList>::Edge* edge)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
@ -1804,9 +1787,9 @@ EdgeList::find(const Graph<EdgeList>::Edge* edge)
* between the actual values of the edges (not the * between the actual values of the edges (not the
* pointers). * pointers).
* *
* Returns: A list<Graph<EdgeList>::Edge*, ALLOC>::iterator pointing * Returns: A list<Graph<EdgeList>::Edge*>::iterator pointing
* to the edge in the list or * to the edge in the list or
* list<Graph<EdgeList>::Edge*, ALLOC>::end() if the edge is * list<Graph<EdgeList>::Edge*>::end() if the edge is
* not found in the list. * not found in the list.
* *
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
@ -1875,8 +1858,7 @@ inline void EdgeSlist::insert(Graph<EdgeSlist>::Edge* edge)
} }
/* ========================================================================= */ /* ========================================================================= */
inline slist<Graph<EdgeSlist>::Edge*, ALLOC(Graph<EdgeSlist>::Edge*) > inline slist<Graph<EdgeSlist>::Edge*>::const_iterator
::const_iterator
EdgeSlist::find(const Graph<EdgeSlist>::Edge* edge) const EdgeSlist::find(const Graph<EdgeSlist>::Edge* edge) const
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
@ -1887,9 +1869,9 @@ EdgeSlist::find(const Graph<EdgeSlist>::Edge* edge) const
* between the actual values of the edges (not the * between the actual values of the edges (not the
* pointers). * pointers).
* *
* Returns: A slist<Graph<EdgeSlist>::Edge*, ALLOC>::const_iterator * Returns: A slist<Graph<EdgeSlist>::Edge*>::const_iterator
* pointing to the edge in the list or * pointing to the edge in the list or
* slist<Graph<EdgeSlist>::Edge*, ALLOC>::end() if the edge * slist<Graph<EdgeSlist>::Edge*>::end() if the edge
* is not found in the list. * is not found in the list.
* *
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
@ -1904,8 +1886,7 @@ EdgeSlist::find(const Graph<EdgeSlist>::Edge* edge) const
} }
/* ========================================================================= */ /* ========================================================================= */
inline slist<Graph<EdgeSlist>::Edge*, ALLOC(Graph<EdgeSlist>::Edge*) > inline slist<Graph<EdgeSlist>::Edge*>::iterator
::iterator
EdgeSlist::find(const Graph<EdgeSlist>::Edge* edge) EdgeSlist::find(const Graph<EdgeSlist>::Edge* edge)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
@ -1916,9 +1897,9 @@ EdgeSlist::find(const Graph<EdgeSlist>::Edge* edge)
* between the actual values of the edges (not the * between the actual values of the edges (not the
* pointers). * pointers).
* *
* Returns: A slist<Graph<EdgeSlist>::Edge*, ALLOC>::iterator * Returns: A slist<Graph<EdgeSlist>::Edge*>::iterator
* pointing to the edge in the list or * pointing to the edge in the list or
* slist<Graph<EdgeSlist>::Edge*, ALLOC>::end() if the edge * slist<Graph<EdgeSlist>::Edge*>::end() if the edge
* is not found in the list. * is not found in the list.
* *
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
@ -1987,8 +1968,7 @@ inline void EdgeVector::insert(Graph<EdgeVector>::Edge* edge)
} }
/* ========================================================================= */ /* ========================================================================= */
inline vector<Graph<EdgeVector>::Edge*, ALLOC(Graph<EdgeVector>::Edge*) > inline vector<Graph<EdgeVector>::Edge*>::const_iterator
::const_iterator
EdgeVector::find(const Graph<EdgeVector>::Edge* edge) const EdgeVector::find(const Graph<EdgeVector>::Edge* edge) const
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
@ -1999,9 +1979,9 @@ EdgeVector::find(const Graph<EdgeVector>::Edge* edge) const
* between the actual values of the edges (not the * between the actual values of the edges (not the
* pointers). * pointers).
* *
* Returns: A vector<Graph<EdgeVector>::Edge*, ALLOC>::const_iterator * Returns: A vector<Graph<EdgeVector>::Edge*>::const_iterator
* pointing to the edge in the container or * pointing to the edge in the container or
* vector<Graph<EdgeVector>::Edge*, ALLOC>::end() if the * vector<Graph<EdgeVector>::Edge*>::end() if the
* edge is not found in the container. * edge is not found in the container.
* *
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
@ -2016,8 +1996,7 @@ EdgeVector::find(const Graph<EdgeVector>::Edge* edge) const
} }
/* ========================================================================= */ /* ========================================================================= */
inline vector<Graph<EdgeVector>::Edge*, ALLOC(Graph<EdgeVector>::Edge*) > inline vector<Graph<EdgeVector>::Edge*>::iterator
::iterator
EdgeVector::find(const Graph<EdgeVector>::Edge* edge) EdgeVector::find(const Graph<EdgeVector>::Edge* edge)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
@ -2028,9 +2007,9 @@ EdgeVector::find(const Graph<EdgeVector>::Edge* edge)
* between the actual values of the edges (not the * between the actual values of the edges (not the
* pointers). * pointers).
* *
* Returns: A vector<Graph<EdgeVector>::Edge*, ALLOC>::iterator * Returns: A vector<Graph<EdgeVector>::Edge*>::iterator
* pointing to the edge in the container or * pointing to the edge in the container or
* vector<Graph<EdgeSlist>::Edge*, ALLOC>::end() if the edge * vector<Graph<EdgeSlist>::Edge*>::end() if the edge
* is not found in the container. * is not found in the container.
* *
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */

19
lbtt/src/IntervalList.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 2004 * Copyright (C) 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -41,7 +41,7 @@ void IntervalList::merge(unsigned long int min, unsigned long int max)
if (min > max) if (min > max)
return; return;
list<Interval, ALLOC(Interval) >::iterator interval; list<Interval>::iterator interval;
for (interval = intervals.begin(); for (interval = intervals.begin();
interval != intervals.end() && interval->second + 1 < min; interval != intervals.end() && interval->second + 1 < min;
++interval) ++interval)
@ -68,14 +68,14 @@ void IntervalList::merge(unsigned long int min, unsigned long int max)
if (interval->second < max) if (interval->second < max)
{ {
interval->second = max; interval->second = max;
list<Interval, ALLOC(Interval) >::iterator interval2 = interval; list<Interval>::iterator interval2 = interval;
++interval2; ++interval2;
while (interval2 != intervals.end() while (interval2 != intervals.end()
&& interval2->first <= interval->second + 1) && interval2->first <= interval->second + 1)
{ {
if (interval->second < interval2->second) if (interval->second < interval2->second)
interval->second = interval2->second; interval->second = interval2->second;
list<Interval, ALLOC(Interval) >::iterator interval_to_erase = interval2; list<Interval>::iterator interval_to_erase = interval2;
++interval2; ++interval2;
intervals.erase(interval_to_erase); intervals.erase(interval_to_erase);
} }
@ -97,7 +97,7 @@ void IntervalList::remove(unsigned long int min, unsigned long int max)
if (min > max) if (min > max)
return; return;
list<Interval, ALLOC(Interval) >::iterator interval; list<Interval>::iterator interval;
for (interval = intervals.begin(); for (interval = intervals.begin();
interval != intervals.end() && interval->second < min; interval != intervals.end() && interval->second < min;
++interval) ++interval)
@ -126,7 +126,7 @@ void IntervalList::remove(unsigned long int min, unsigned long int max)
} }
else /* min <= imin <= imax <= max */ else /* min <= imin <= imax <= max */
{ {
list<Interval, ALLOC(Interval) >::iterator interval_to_erase = interval; list<Interval>::iterator interval_to_erase = interval;
++interval; ++interval;
intervals.erase(interval_to_erase); intervals.erase(interval_to_erase);
} }
@ -148,7 +148,7 @@ bool IntervalList::covers(unsigned long int min, unsigned long int max) const
if (min > max) if (min > max)
return true; /* empty interval is always covered */ return true; /* empty interval is always covered */
list<Interval, ALLOC(Interval) >::const_iterator interval; list<Interval>::const_iterator interval;
for (interval = intervals.begin(); for (interval = intervals.begin();
interval != intervals.end() && min > interval->second; interval != intervals.end() && min > interval->second;
++interval) ++interval)
@ -173,8 +173,7 @@ string IntervalList::toString() const
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
{ {
string s; string s;
for (list<Interval, ALLOC(Interval) >::const_iterator for (list<Interval>::const_iterator interval = intervals.begin();
interval = intervals.begin();
interval != intervals.end(); interval != intervals.end();
++interval) ++interval)
{ {

23
lbtt/src/IntervalList.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 2004 * Copyright (C) 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -74,13 +74,15 @@ public:
unsigned long int operator++(int); /* Postfix increment. */ unsigned long int operator++(int); /* Postfix increment. */
private: private:
const list<Interval, ALLOC(Interval) >* /* The interval list */ const list<Interval>* interval_list; /* The interval list
interval_list; /* associated with the */ * associated with the
/* iterator. */ * iterator.
*/
list<Interval, ALLOC(Interval) > /* An iterator pointing */ list<Interval>::const_iterator interval; /* An iterator pointing at
::const_iterator interval; /* at the current */ * the current intrerval
/* interval list. */ * list.
*/
unsigned long int element; /* Element currently unsigned long int element; /* Element currently
* pointed to by the * pointed to by the
@ -143,8 +145,7 @@ public:
* iterators. * iterators.
*/ */
typedef list<Interval, ALLOC(Interval) > /* Size type. */ typedef list<Interval>::size_type size_type; /* Size type. */
::size_type size_type;
size_type size() const; /* Tell the number of size_type size() const; /* Tell the number of
* disjoint intervals in * disjoint intervals in
@ -170,7 +171,7 @@ public:
*/ */
private: private:
list<Interval, ALLOC(Interval) > intervals; /* List of intervals. */ list<Interval> intervals; /* List of intervals. */
friend class const_iterator; friend class const_iterator;
}; };

4
lbtt/src/LbtWrapper.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

6
lbtt/src/LbttAlloc.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -22,8 +22,6 @@
#include <config.h> #include <config.h>
#define ALLOC(typename) allocator<typename>
#ifdef HAVE_OBSTACK_H #ifdef HAVE_OBSTACK_H
/* GNU libc 2.3.2's copy of obstack.h uses a definition of __INT_TO_PTR /* GNU libc 2.3.2's copy of obstack.h uses a definition of __INT_TO_PTR

14
lbtt/src/Ltl-parse.yy
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 2004 * Copyright (C) 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -44,9 +44,9 @@ static LtlFormula* result; /* This variable stores the
* ltl_parse. * ltl_parse.
*/ */
static std::set<LtlFormula*, less<LtlFormula*>, /* Intermediate results. */ static std::set<LtlFormula*> intermediate_results; /* Intermediate results.
ALLOC(LtlFormula*) > /* (This set is used */ * (This set is used
intermediate_results; /* for keeping track of * for keeping track of
* the subformulas of a * the subformulas of a
* partially constructed * partially constructed
* formula in case the * formula in case the
@ -426,8 +426,8 @@ LtlFormula* parseFormula(istream& stream)
} }
catch (...) catch (...)
{ {
for (std::set<LtlFormula*, less<LtlFormula*>, ALLOC(LtlFormula*) > for (std::set<LtlFormula*>::const_iterator
::const_iterator f = intermediate_results.begin(); f = intermediate_results.begin();
f != intermediate_results.end(); f != intermediate_results.end();
++f) ++f)
LtlFormula::destruct(*f); LtlFormula::destruct(*f);

29
lbtt/src/LtlFormula.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -24,9 +24,8 @@
namespace Ltl namespace Ltl
{ {
set<LtlFormula*, LtlFormula::ptr_less, /* Shared storage for */ set<LtlFormula*, LtlFormula::ptr_less> /* Shared storage for */
ALLOC(LtlFormula*) > /* LTL formulae. */ LtlFormula::formula_storage; /* LTL formulae. */
LtlFormula::formula_storage;
unsigned long int /* Upper limit for the */ unsigned long int /* Upper limit for the */
LtlFormula::eval_proposition_id_limit; /* atomic proposition LtlFormula::eval_proposition_id_limit; /* atomic proposition
@ -140,12 +139,10 @@ public:
*/ */
private: private:
stack<LtlFormula*, stack<LtlFormula*, deque<LtlFormula*> >
deque<LtlFormula*, ALLOC(LtlFormula*) > >
formula_stack; formula_stack;
stack<bool, deque<bool, ALLOC(bool) > > stack<bool, deque<bool> > negation_stack;
negation_stack;
NnfConverter(const NnfConverter&); /* Prevent copying and */ NnfConverter(const NnfConverter&); /* Prevent copying and */
NnfConverter& operator=(const NnfConverter&); /* assignment of NnfConverter& operator=(const NnfConverter&); /* assignment of
@ -196,8 +193,7 @@ class SubformulaCollector
public: public:
SubformulaCollector /* Constructor. */ SubformulaCollector /* Constructor. */
(stack<const LtlFormula*, (stack<const LtlFormula*,
deque<const LtlFormula*, deque<const LtlFormula*> >&
ALLOC(const LtlFormula*) > >&
result_stack); result_stack);
~SubformulaCollector(); /* Destructor. */ ~SubformulaCollector(); /* Destructor. */
@ -209,8 +205,7 @@ public:
private: private:
stack<const LtlFormula*, /* Stack of subformulae. */ stack<const LtlFormula*, /* Stack of subformulae. */
deque<const LtlFormula*, deque<const LtlFormula*> >&
ALLOC(const LtlFormula*) > >&
subformula_stack; subformula_stack;
SubformulaCollector(const SubformulaCollector&); /* Prevent copying and */ SubformulaCollector(const SubformulaCollector&); /* Prevent copying and */
@ -382,9 +377,7 @@ inline void FormulaSizeCounter::operator()(const LtlFormula*, int)
/* ========================================================================= */ /* ========================================================================= */
inline SubformulaCollector::SubformulaCollector inline SubformulaCollector::SubformulaCollector
(stack<const LtlFormula*, deque<const LtlFormula*, (stack<const LtlFormula*, deque<const LtlFormula*> >& result_stack) :
ALLOC(const LtlFormula*) > >&
result_stack) :
subformula_stack(result_stack) subformula_stack(result_stack)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
@ -766,9 +759,7 @@ unsigned long int LtlFormula::size() const
/* ========================================================================= */ /* ========================================================================= */
void LtlFormula::collectSubformulae void LtlFormula::collectSubformulae
(stack<const LtlFormula*, deque<const LtlFormula*, (stack<const LtlFormula*, deque<const LtlFormula*> >& result_stack) const
ALLOC(const LtlFormula*) > >&
result_stack) const
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Collects the subformulae of a LtlFormula into a stack. After * Description: Collects the subformulae of a LtlFormula into a stack. After

23
lbtt/src/LtlFormula.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -261,21 +261,18 @@ private:
void collectSubformulae /* Builds a stack of the */ void collectSubformulae /* Builds a stack of the */
(stack<const LtlFormula*, /* subformulae of the */ (stack<const LtlFormula*, /* subformulae of the */
deque<const LtlFormula*, /* formula. */ deque<const LtlFormula*> >& /* formula. */
ALLOC(const LtlFormula*) > >&
result_stack) const; result_stack) const;
typedef pair<bool, const LtlFormula*> /* Shorthand type */ typedef pair<bool, const LtlFormula*> /* Shorthand type */
FormulaStackElement; /* definitions for the */ FormulaStackElement; /* definitions for the */
typedef stack<FormulaStackElement, /* propositional */ typedef stack<FormulaStackElement, /* propositional */
deque<FormulaStackElement, /* satisfiability */ deque<FormulaStackElement> > /* satisfiability */
ALLOC(FormulaStackElement) > >/* checking algorithm. */ FormulaStack; /* checking algorithm. */
FormulaStack;
typedef pair<FormulaStack, Bitset> typedef pair<FormulaStack, Bitset>
TableauStackElement; TableauStackElement;
typedef stack<TableauStackElement, typedef stack<TableauStackElement,
deque<TableauStackElement, deque<TableauStackElement> >
ALLOC(TableauStackElement) > >
TableauStack; TableauStack;
bool sat_eval /* Helper function for */ bool sat_eval /* Helper function for */
@ -285,9 +282,8 @@ private:
* formula. * formula.
*/ */
static set<LtlFormula*, ptr_less, /* Shared storage for */ static set<LtlFormula*, ptr_less> /* Shared storage for */
ALLOC(LtlFormula*) > /* LTL formulae. */ formula_storage; /* LTL formulae. */
formula_storage;
static unsigned long int /* Upper limit for the */ static unsigned long int /* Upper limit for the */
eval_proposition_id_limit; /* atomic proposition eval_proposition_id_limit; /* atomic proposition
@ -1314,8 +1310,7 @@ inline LtlFormula& LtlFormula::insertToStorage(LtlFormula* f)
* *
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
{ {
set<LtlFormula*, ptr_less, ALLOC(LtlFormula*) >::iterator inserter set<LtlFormula*, ptr_less>::iterator inserter = formula_storage.find(f);
= formula_storage.find(f);
if (inserter != formula_storage.end()) if (inserter != formula_storage.end())
{ {
delete f; delete f;

2
lbtt/src/Makefile.am
View file

@ -79,6 +79,8 @@ lbtt_translate_SOURCES = \
NeverClaimAutomaton.cc \ NeverClaimAutomaton.cc \
SpinWrapper.h \ SpinWrapper.h \
SpinWrapper.cc \ SpinWrapper.cc \
SpotWrapper.h \
SpotWrapper.cc \
StringUtil.h \ StringUtil.h \
StringUtil.cc \ StringUtil.cc \
TempFsysName.h \ TempFsysName.h \

4
lbtt/src/NeverClaim-lex.ll
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

4
lbtt/src/NeverClaim-parse.yy
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

14
lbtt/src/NeverClaimAutomaton.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -62,8 +62,7 @@ void NeverClaimAutomaton::clear()
* *
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
{ {
for (vector<StateInfo*, ALLOC(StateInfo*) >::iterator for (vector<StateInfo*>::iterator state = state_list.begin();
state = state_list.begin();
state != state_list.end(); state != state_list.end();
++state) ++state)
delete (*state); delete (*state);
@ -154,8 +153,7 @@ void NeverClaimAutomaton::write(const char* output_filename)
* `-1'. * `-1'.
*/ */
for (vector<StateInfo*, ALLOC(StateInfo*) >::const_iterator for (vector<StateInfo*>::const_iterator state = state_list.begin();
state = state_list.begin();
state != state_list.end(); state != state_list.end();
++state) ++state)
{ {
@ -163,7 +161,7 @@ void NeverClaimAutomaton::write(const char* output_filename)
+ ((*state)->initial() ? "1" : "0") + ' ' + ((*state)->initial() ? "1" : "0") + ' '
+ ((*state)->accepting() ? "0 " : "") + "-1\n"; + ((*state)->accepting() ? "0 " : "") + "-1\n";
for (multimap<Cstr, Cstr*, less<Cstr>, ALLOC(Cstr*) >::const_iterator for (multimap<Cstr, Cstr*>::const_iterator
transition = (*state)->transitions().begin(); transition = (*state)->transitions().begin();
transition != (*state)->transitions().end(); ++transition) transition != (*state)->transitions().end(); ++transition)
{ {
@ -268,7 +266,7 @@ NeverClaimAutomaton::StateInfo::~StateInfo()
* *
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
{ {
for (multimap<Cstr, Cstr*, less<Cstr>, ALLOC(Cstr*) >::const_iterator for (multimap<Cstr, Cstr*>::const_iterator
transition = state_transitions.begin(); transition = state_transitions.begin();
transition != state_transitions.end(); transition != state_transitions.end();
++transition) ++transition)

29
lbtt/src/NeverClaimAutomaton.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -93,12 +93,13 @@ public:
*/ */
private: private:
vector<StateInfo*, ALLOC(StateInfo*) > /* States of the */ vector<StateInfo*> state_list; /* States of the automaton.
state_list; /* automaton. */ */
map<string, StateInfo*, less<string>, /* Mapping from state */ map<string, StateInfo*> label_mapping; /* Mapping from state
ALLOC(StateInfo*) > /* labels to the states */ * labels to the states
label_mapping; /* itself. */ * itself.
*/
StateInfo* current_state; /* Pointer to the state StateInfo* current_state; /* Pointer to the state
* introduced most recently * introduced most recently
@ -142,9 +143,9 @@ public:
/* of the state. /* of the state.
*/ */
const multimap<Cstr, Cstr*, less<Cstr>, /* Returns the labels of */ const multimap<Cstr, Cstr*>& transitions() const; /* Returns the labels of
ALLOC(Cstr*) >& /* the state's successor */ * the state's successor
transitions() const; /* states, including the * states, including the
* conditions controlling * conditions controlling
* the enabledness of the * the enabledness of the
* transition. * transition.
@ -174,8 +175,8 @@ private:
* accepting state? * accepting state?
*/ */
multimap<Cstr, Cstr*, less<Cstr>, ALLOC(Cstr*) > /* Labels of the state's */ multimap<Cstr, Cstr*> state_transitions; /* Labels of the state's
state_transitions; /* successors, including * successors, including
* the guard formulae * the guard formulae
* controlling the * controlling the
* enabledness of the * enabledness of the
@ -373,9 +374,7 @@ inline bool& NeverClaimAutomaton::StateInfo::accepting()
} }
/* ========================================================================= */ /* ========================================================================= */
inline const multimap<NeverClaimAutomaton::Cstr, NeverClaimAutomaton::Cstr*, inline const multimap<NeverClaimAutomaton::Cstr, NeverClaimAutomaton::Cstr*>&
less<NeverClaimAutomaton::Cstr>,
ALLOC(NeverClaimAutomaton::Cstr*) >&
NeverClaimAutomaton::StateInfo::transitions() const NeverClaimAutomaton::StateInfo::transitions() const
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *

16
lbtt/src/PathEvaluator.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -49,9 +49,8 @@ void PathEvaluator::reset()
current_loop_state = 0; current_loop_state = 0;
path_states.clear(); path_states.clear();
for (map<const LtlFormula*, BitArray*, LtlFormula::ptr_less, for (map<const LtlFormula*, BitArray*, LtlFormula::ptr_less>::iterator
ALLOC(BitArray*) >::iterator it it = eval_info.begin();
= eval_info.begin();
it != eval_info.end(); it != eval_info.end();
++it) ++it)
delete it->second; delete it->second;
@ -131,8 +130,7 @@ bool PathEvaluator::evaluate
current_formula = &formula; current_formula = &formula;
current_path = &statespace; current_path = &statespace;
map<StateSpace::size_type, StateSpace::size_type, map<StateSpace::size_type, StateSpace::size_type> ordering;
less<StateSpace::size_type>, ALLOC(StateSpace::size_type) > ordering;
StateSpace::size_type state = statespace.initialState(); StateSpace::size_type state = statespace.initialState();
StateSpace::size_type state_count = 0; StateSpace::size_type state_count = 0;
@ -176,9 +174,7 @@ bool PathEvaluator::eval()
* *
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
{ {
stack<const LtlFormula*, deque<const LtlFormula*, stack<const LtlFormula*, deque<const LtlFormula*> > subformula_stack;
ALLOC(const LtlFormula*) > >
subformula_stack;
const LtlFormula* f; const LtlFormula* f;
BitArray* val; BitArray* val;

12
lbtt/src/PathEvaluator.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -105,15 +105,15 @@ private:
* the current path. * the current path.
*/ */
vector<StateSpace::size_type, /* Correspondence */ vector<StateSpace::size_type> path_states; /* Correspondence
ALLOC(StateSpace::size_type) > /* between states of the */ * between states of the
path_states; /* path and the states * path and the states
* of the current state * of the current state
* space. * space.
*/ */
map<const LtlFormula*, BitArray*, /* Information about the */ map<const LtlFormula*, BitArray*, /* Information about the */
LtlFormula::ptr_less, ALLOC(BitArray*) > /* truth values of the */ LtlFormula::ptr_less> /* truth values of the */
eval_info; /* subformulae of the eval_info; /* subformulae of the
* formula to be * formula to be
* evaluated. * evaluated.

4
lbtt/src/PathIterator.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

4
lbtt/src/PathIterator.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

41
lbtt/src/Product.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -393,8 +393,8 @@ public:
typedef ProductEdgeCollection EdgeContainerType; /* required for making */ typedef ProductEdgeCollection EdgeContainerType; /* required for making */
/* Product<Operations> */ /* Product<Operations> */
struct PathElement; /* suitable for */ struct PathElement; /* suitable for */
typedef deque<PathElement, ALLOC(PathElement) > /* instantiating the */ typedef deque<PathElement> Path; /* instantiating the
Path; /* SccCollection * SccCollection
* template (see * template (see
* SccCollection.h). * SccCollection.h).
*/ */
@ -419,9 +419,7 @@ private:
Graph<GraphEdgeContainer>::Path >& cycle, /* segment of the cycle */ Graph<GraphEdgeContainer>::Path >& cycle, /* segment of the cycle */
size_type source_state_id, Edge transition, /* in a witness for the */ size_type source_state_id, Edge transition, /* in a witness for the */
const size_type root_id, /* nonemptiness of the */ const size_type root_id, /* nonemptiness of the */
const map<size_type, PathElement, /* product. */ const map<size_type, PathElement>& /* product. */
less<size_type>,
ALLOC(PathElement) >&
predecessor) const; predecessor) const;
Operations operations; /* Operations for Operations operations; /* Operations for
@ -655,9 +653,10 @@ protected:
* acceptance sets. * acceptance sets.
*/ */
typedef deque<AcceptanceStackElement, /* Stack formed from */ typedef deque<AcceptanceStackElement> /* Stack formed from */
ALLOC(AcceptanceStackElement) > /* the above */ AcceptanceStack; /* the above
AcceptanceStack; /* associations. */ * associations.
*/
AcceptanceStack acceptance_stack; /* Stack for storing the AcceptanceStack acceptance_stack; /* Stack for storing the
* dfs numbers of roots * dfs numbers of roots
@ -877,9 +876,9 @@ private:
* reachable. * reachable.
*/ */
set<size_type, less<size_type>, /* Set of states from */ set<size_type> reachability_info; /* Set of states from
ALLOC(size_type) > /* which an accepting */ * which an accepting
reachability_info; /* component is known to * component is known to
* be reachable in the * be reachable in the
* product. * product.
*/ */
@ -928,9 +927,9 @@ public:
~AcceptingComponentFinder(); /* Destructor. */ ~AcceptingComponentFinder(); /* Destructor. */
typedef set<size_type, less<size_type>, /* Type definition for */ typedef set<size_type> SccType; /* Type definition for
ALLOC(size_type) > /* the set of product */ * the set of product
SccType; /* state identifiers in * state identifiers in
* an accepting * an accepting
* strongly connected * strongly connected
* component. * component.
@ -1369,10 +1368,9 @@ void Product<Operations>::findWitness
unsigned long int number_of_collected_acceptance_sets unsigned long int number_of_collected_acceptance_sets
= collected_acceptance_sets.count(number_of_acceptance_sets); = collected_acceptance_sets.count(number_of_acceptance_sets);
deque<size_type, ALLOC(size_type) > search_queue; deque<size_type> search_queue;
set<size_type, less<size_type>, ALLOC(size_type) > visited; set<size_type> visited;
map<size_type, PathElement, less<size_type>, ALLOC(PathElement) > map<size_type, PathElement> shortest_path_predecessor;
shortest_path_predecessor;
size_type bfs_root = search_start_state; size_type bfs_root = search_start_state;
@ -1475,8 +1473,7 @@ void Product<Operations>::addCycleSegment
(pair<Graph<GraphEdgeContainer>::Path, Graph<GraphEdgeContainer>::Path>& (pair<Graph<GraphEdgeContainer>::Path, Graph<GraphEdgeContainer>::Path>&
cycle, cycle,
size_type source_state_id, Edge transition, const size_type root_id, size_type source_state_id, Edge transition, const size_type root_id,
const map<size_type, PathElement, less<size_type>, ALLOC(PathElement) >& const map<size_type, PathElement>& predecessor) const
predecessor) const
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Helper function for constructing a segment of an accepting * Description: Helper function for constructing a segment of an accepting

4
lbtt/src/Random.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

34
lbtt/src/SccCollection.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -195,10 +195,8 @@ public:
/* default assignment operator */ /* default assignment operator */
typedef set<typename GraphType::size_type, /* Type definition for */ typedef set<typename GraphType::size_type> /* Type definition for */
less<typename GraphType::size_type>, /* a set of node id's. */ SccType; /* a set of node id's. */
ALLOC(typename GraphType::size_type) >
SccType;
const SccType& operator()() const; /* Returns the set of node const SccType& operator()() const; /* Returns the set of node
* identifiers in a * identifiers in a
@ -338,10 +336,10 @@ public:
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
typedef map<typename GraphType::size_type, /* Type definition for a */ typedef map<typename GraphType::size_type, /* Type definition for a */
typename GraphType::size_type, /* mapping between node */ typename GraphType::size_type> /* mapping between node */
less<typename GraphType::size_type>, /* identifiers and the */ DfsOrdering; /* identifiers and the
ALLOC(typename GraphType::size_type) >/* order in which they */ * order in which they
DfsOrdering; /* were encountered in * were encountered in
* the search for * the search for
* strongly connected * strongly connected
* components. * components.
@ -433,18 +431,19 @@ public:
typename GraphType::size_type lowlink; typename GraphType::size_type lowlink;
}; };
deque<NodeStackElement, /* Depth-first search */ deque<NodeStackElement> node_stack; /* Depth-first search
ALLOC(NodeStackElement) > /* backtracking stack. */ * backtracking stack.
node_stack; */
NodeStackElement* current_node; /* Pointer to the top NodeStackElement* current_node; /* Pointer to the top
* element of the * element of the
* backtracking stack. * backtracking stack.
*/ */
deque<typename GraphType::size_type, /* Stack used for */ deque<typename GraphType::size_type> scc_stack; /* Stack used for
ALLOC(typename GraphType::size_type) > /* collecting the nodes */ * collecting the nodes
scc_stack; /* in a strongly * in a strongly
* connected component, * connected component,
* excluding the root * excluding the root
* nodes of the * nodes of the
@ -998,8 +997,7 @@ void SccCollection<GraphType, NodeVisitor>::iterator::getPath
* when exiting from this function). * when exiting from this function).
*/ */
typename deque<NodeStackElement, ALLOC(NodeStackElement) >::const_iterator typename deque<NodeStackElement>::const_iterator n = node_stack.begin();
n = node_stack.begin();
if (n != node_stack.end()) if (n != node_stack.end())
{ {
for (++n; n != node_stack.end(); ++n) for (++n; n != node_stack.end(); ++n)

18
lbtt/src/SharedTestData.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -42,14 +42,14 @@ extern TestRoundInfo round_info; /* Data structure for
* round. * round.
*/ */
extern vector<AlgorithmTestResults, /* Test results for each */ extern vector<AlgorithmTestResults> test_results; /* Test results for each
ALLOC(AlgorithmTestResults) > /* implementation. */ * implementation.
test_results; */
extern vector<TestStatistics, /* Overall test */
ALLOC(TestStatistics) > /* statistics for each */
final_statistics; /* implementation. */
extern vector<TestStatistics> final_statistics; /* Overall test
* statistics for each
* implementation.
*/
} }
#endif /* !SHAREDTESTDATA_H */ #endif /* !SHAREDTESTDATA_H */

4
lbtt/src/SpinWrapper.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

4
lbtt/src/SpinWrapper.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

102
lbtt/src/SpotWrapper.cc Normal file
View file

@ -0,0 +1,102 @@
/*
* Copyright (C) 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* Derived from SpinWrapper.cc by Alexandre Duret-Lutz <adl@src.lip6.fr>.
*
* This program 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.
*
* This program 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 this program; if not, write to the Free Software
* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*/
#include <config.h>
#ifdef HAVE_SSTREAM
#include <sstream>
#else
#include <strstream>
#endif /* HAVE_SSTREAM */
#include "Exception.h"
#include "FormulaWriter.h"
#include "NeverClaimAutomaton.h"
#include "SpotWrapper.h"
/******************************************************************************
*
* Definitions for operator symbols specific to Spot.
*
*****************************************************************************/
const char SpotWrapper::SPOT_AND[] = "&&";
const char SpotWrapper::SPOT_OR[] = "||";
const char SpotWrapper::SPOT_XOR[] = "^";
/******************************************************************************
*
* Function definitions for class SpotWrapper.
*
*****************************************************************************/
/* ========================================================================= */
void SpotWrapper::translateFormula
(const ::Ltl::LtlFormula& formula, string& translated_formula)
/* ----------------------------------------------------------------------------
*
* Description: Translates an LtlFormula into a string which contains the
* formula in the input syntax of Spot.
*
* Arguments: formula -- The LtlFormula to be translated.
* translated_formula -- A reference to a string for storing
* the results.
*
* Returns: Nothing. The result of the translation can be found in
* the string `translated_formula'.
*
* ------------------------------------------------------------------------- */
{
using namespace Ltl;
#ifdef HAVE_SSTREAM
ostringstream translated_formula_stream;
#else
ostrstream translated_formula_stream;
#endif /* HAVE_SSTREAM */
Exceptional_ostream estream(&translated_formula_stream, ios::goodbit);
FormulaWriter<ConstantWriter<LtlTrue::infix_symbol>,
ConstantWriter<LtlFalse::infix_symbol>,
AtomWriter,
UnaryOperatorWriter<LtlNegation::infix_symbol>,
UnaryOperatorWriter<LtlNext::infix_symbol>,
UnaryOperatorWriter<LtlFinally::infix_symbol>,
UnaryOperatorWriter<LtlGlobally::infix_symbol>,
BinaryOperatorInfixWriter<SPOT_AND>,
BinaryOperatorInfixWriter<SPOT_OR>,
BinaryOperatorInfixWriter<LtlImplication::infix_symbol>,
BinaryOperatorInfixWriter<LtlEquivalence::infix_symbol>,
BinaryOperatorInfixWriter<SPOT_XOR>,
BinaryOperatorInfixWriter<LtlUntil::infix_symbol>,
BinaryOperatorInfixWriter<LtlV::infix_symbol>,
WriterErrorReporter,
WriterErrorReporter,
WriterErrorReporter>
fw(estream);
formula.traverse(fw, LTL_PREORDER | LTL_INORDER | LTL_POSTORDER);
translated_formula = translated_formula_stream.str();
#ifndef HAVE_SSTREAM
translated_formula_stream.freeze(0);
#endif /* HAVE_SSTREAM */
}

143
lbtt/src/SpotWrapper.h Normal file
View file

@ -0,0 +1,143 @@
/*
* Copyright (C) 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* Derived from SpinWrapper.h by Alexandre Duret-Lutz <adl@src.lip6.fr>.
*
* This program 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.
*
* This program 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 this program; if not, write to the Free Software
* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*/
#ifndef SPOTWRAPPER_H
#define SPOTWRAPPER_H
#include <config.h>
#include <string>
#include "ExternalTranslator.h"
#include "LtlFormula.h"
/******************************************************************************
*
* Interface class for Spot.
*
*****************************************************************************/
class SpotWrapper : public ExternalTranslator
{
public:
SpotWrapper(); /* Constructor. */
~SpotWrapper(); /* Destructor. */
void translateFormula /* Translates a formula */
(const ::Ltl::LtlFormula& formula, /* into a Büchi */
string& translated_formula); /* automaton. */
/* `formatInput' inherited from ExternalTranslator */
string commandLine /* Prepares the command */
(const string& input_filename, /* line for executing */
const string& output_filename); /* Spot. */
/* `execSuccess' inherited from ExternalTranslator */
void parseAutomaton /* Translates the output */
(const string& input_filename, /* of the translation */
const string& output_filename); /* algorithm into lbtt
* format.
*/
private:
SpotWrapper(const SpotWrapper&); /* Prevent copying and */
SpotWrapper& operator=(const SpotWrapper&); /* assignment of
* SpotWrapper objects.
*/
static const char SPOT_AND[]; /* Symbols for */
static const char SPOT_OR[]; /* operators. */
static const char SPOT_XOR[];
};
/******************************************************************************
*
* Inline function definitions for class SpotWrapper.
*
*****************************************************************************/
/* ========================================================================= */
inline SpotWrapper::SpotWrapper()
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class SpotWrapper.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline SpotWrapper::~SpotWrapper()
/* ----------------------------------------------------------------------------
*
* Description: Destructor for class SpotWrapper.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline string SpotWrapper::commandLine
(const string& input_filename, const string&)
/* ----------------------------------------------------------------------------
*
* Description: Prepares the command line for Spot.
*
* Arguments: input_filename -- Name of the input file.
* The other argument is only needed for supporting the
* ExternalTranslator interface; the output will be written to
* the filename stored in `command_line_arguments[4]'.
*
* Returns: The command line string.
*
* ------------------------------------------------------------------------- */
{
return (string(" ") + input_filename
+ " >" + string(command_line_arguments[4]));
}
/* ========================================================================= */
inline void SpotWrapper::parseAutomaton(const string&, const string&)
/* ----------------------------------------------------------------------------
*
* Description: Dummy function which is needed to support the
* ExternalTranslator interface.
*
* Arguments: References to two constant strings.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
#endif /* !SPOTWRAPPER_H */

46
lbtt/src/StatDisplay.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -78,8 +78,7 @@ void printStatTableHeader(ostream& stream, int indent)
/* ========================================================================= */ /* ========================================================================= */
void printBuchiAutomatonStats void printBuchiAutomatonStats
(ostream& stream, int indent, (ostream& stream, int indent,
vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type vector<AlgorithmTestResults>::size_type algorithm,
algorithm,
int result_id) int result_id)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
@ -173,8 +172,7 @@ void printBuchiAutomatonStats
/* ========================================================================= */ /* ========================================================================= */
void printProductAutomatonStats void printProductAutomatonStats
(ostream& stream, int indent, (ostream& stream, int indent,
vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type vector<AlgorithmTestResults>::size_type algorithm,
algorithm,
int result_id) int result_id)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
@ -264,8 +262,7 @@ void printProductAutomatonStats
/* ========================================================================= */ /* ========================================================================= */
void printAcceptanceCycleStats void printAcceptanceCycleStats
(ostream& stream, int indent, (ostream& stream, int indent,
vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type vector<AlgorithmTestResults>::size_type algorithm,
algorithm,
int result_id) int result_id)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
@ -350,8 +347,7 @@ void printAcceptanceCycleStats
/* ========================================================================= */ /* ========================================================================= */
void printConsistencyCheckStats void printConsistencyCheckStats
(ostream& stream, int indent, (ostream& stream, int indent,
vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type vector<AlgorithmTestResults>::size_type algorithm)
algorithm)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Displays information about the consistency check result for * Description: Displays information about the consistency check result for
@ -462,8 +458,7 @@ void printCrossComparisonStats
alg_1_pos_results = &test_results[*alg_1].automaton_stats[0]; alg_1_pos_results = &test_results[*alg_1].automaton_stats[0];
alg_1_neg_results = &test_results[*alg_1].automaton_stats[1]; alg_1_neg_results = &test_results[*alg_1].automaton_stats[1];
for (vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type for (vector<AlgorithmTestResults>::size_type alg_2 = 0;
alg_2 = 0;
alg_2 < round_info.number_of_translators; alg_2 < round_info.number_of_translators;
alg_2++) alg_2++)
{ {
@ -558,8 +553,7 @@ void printBuchiIntersectionCheckStats
alg_1_pos_results = &test_results[*alg_1].automaton_stats[0]; alg_1_pos_results = &test_results[*alg_1].automaton_stats[0];
alg_1_neg_results = &test_results[*alg_1].automaton_stats[1]; alg_1_neg_results = &test_results[*alg_1].automaton_stats[1];
for (vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type for (vector<AlgorithmTestResults>::size_type alg_2 = 0;
alg_2 = 0;
alg_2 < round_info.number_of_translators; alg_2 < round_info.number_of_translators;
alg_2++) alg_2++)
{ {
@ -631,8 +625,7 @@ void printBuchiIntersectionCheckStats
/* ========================================================================= */ /* ========================================================================= */
void printAllStats void printAllStats
(ostream& stream, int indent, (ostream& stream, int indent,
vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type vector<AlgorithmTestResults>::size_type algorithm)
algorithm)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Displays all test information (Büchi automaton and product * Description: Displays all test information (Büchi automaton and product
@ -701,8 +694,8 @@ void printAllStats
/* ========================================================================= */ /* ========================================================================= */
void printCollectiveCrossComparisonStats void printCollectiveCrossComparisonStats
(ostream& stream, (ostream& stream,
vector<TestStatistics, ALLOC(TestStatistics) >::size_type algorithm_y, vector<TestStatistics>::size_type algorithm_y,
vector<TestStatistics, ALLOC(TestStatistics) >::size_type algorithm_x, vector<TestStatistics>::size_type algorithm_x,
int data_type) int data_type)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
@ -892,13 +885,12 @@ void printCollectiveStats(ostream& stream, int indent)
if (round_info.num_processed_formulae > 0 if (round_info.num_processed_formulae > 0
&& configuration.global_options.formula_input_filename.empty()) && configuration.global_options.formula_input_filename.empty())
{ {
const map<unsigned long int, unsigned long int, less<unsigned long int>, const map<unsigned long int, unsigned long int>&
ALLOC(unsigned long int) >&
proposition_statistics proposition_statistics
= configuration.formula_options.formula_generator. = configuration.formula_options.formula_generator.
propositionStatistics(); propositionStatistics();
const map<int, unsigned long int, less<int>, ALLOC(unsigned long int) > const map<int, unsigned long int>
symbol_statistics symbol_statistics
= configuration.formula_options.formula_generator.symbolStatistics(); = configuration.formula_options.formula_generator.symbolStatistics();
@ -944,9 +936,8 @@ void printCollectiveStats(ostream& stream, int indent)
number_of_symbols_printed++; number_of_symbols_printed++;
} }
for (map<unsigned long int, unsigned long int, for (map<unsigned long int, unsigned long int>::const_iterator
less<unsigned long int>, ALLOC(unsigned long int) > proposition = proposition_statistics.begin();
::const_iterator proposition = proposition_statistics.begin();
proposition != proposition_statistics.end(); proposition != proposition_statistics.end();
++proposition) ++proposition)
{ {
@ -993,8 +984,8 @@ void printCollectiveStats(ostream& stream, int indent)
= ""; = "";
number_of_symbols_printed = 0; number_of_symbols_printed = 0;
for (map<int, unsigned long int, less<int>, ALLOC(unsigned long int) > for (map<int, unsigned long int>::const_iterator
::const_iterator op = symbol_statistics.begin(); op = symbol_statistics.begin();
op != symbol_statistics.end(); op != symbol_statistics.end();
++op) ++op)
{ {
@ -1468,8 +1459,7 @@ void printCollectiveStats(ostream& stream, int indent)
estream << ind + " Result inconsistency statistics\n" estream << ind + " Result inconsistency statistics\n"
+ ind + " " + string(31, '=') + '\n'; + ind + " " + string(31, '=') + '\n';
vector<TestStatistics, ALLOC(TestStatistics) >::size_type vector<TestStatistics>::size_type algorithm_x, algorithm_y;
algorithm_x, algorithm_y;
for (algorithm_x = 0; algorithm_x < number_of_algorithms; for (algorithm_x = 0; algorithm_x < number_of_algorithms;
algorithm_x += 2) algorithm_x += 2)

30
lbtt/src/StatDisplay.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -50,32 +50,28 @@ void printStatTableHeader /* Displays a table */
void printBuchiAutomatonStats /* Displays information */ void printBuchiAutomatonStats /* Displays information */
(ostream& stream, /* about a Büchi */ (ostream& stream, /* about a Büchi */
int indent, /* automaton. */ int indent, /* automaton. */
vector<AlgorithmTestResults, vector<AlgorithmTestResults>::size_type
ALLOC(AlgorithmTestResults) >::size_type
algorithm, algorithm,
int result_id); int result_id);
void printProductAutomatonStats /* Displays information */ void printProductAutomatonStats /* Displays information */
(ostream& stream, /* about a product */ (ostream& stream, /* about a product */
int indent, /* automaton. */ int indent, /* automaton. */
vector<AlgorithmTestResults, vector<AlgorithmTestResults>::size_type
ALLOC(AlgorithmTestResults) >::size_type
algorithm, algorithm,
int result_id); int result_id);
void printAcceptanceCycleStats /* Displays information */ void printAcceptanceCycleStats /* Displays information */
(ostream& stream, /* about the acceptance */ (ostream& stream, /* about the acceptance */
int indent, /* cycles of a product */ int indent, /* cycles of a product */
vector<AlgorithmTestResults, /* automaton. */ vector<AlgorithmTestResults>::size_type /* automaton. */
ALLOC(AlgorithmTestResults) >::size_type
algorithm, algorithm,
int result_id); int result_id);
void printConsistencyCheckStats /* Displays the result */ void printConsistencyCheckStats /* Displays the result */
(ostream& stream, /* of the consistency */ (ostream& stream, /* of the consistency */
int indent, /* check for a given */ int indent, /* check for a given */
vector<AlgorithmTestResults, /* algorithm. */ vector<AlgorithmTestResults>::size_type /* algorithm. */
ALLOC(AlgorithmTestResults) >::size_type
algorithm); algorithm);
void printCrossComparisonStats /* Displays information */ void printCrossComparisonStats /* Displays information */
@ -92,18 +88,14 @@ void printBuchiIntersectionCheckStats /* Displays the results */
void printAllStats /* A shorthand for */ void printAllStats /* A shorthand for */
(ostream& stream, /* showing all the */ (ostream& stream, /* showing all the */
int indent, /* information displayed */ int indent, /* information displayed */
vector<TestStatistics, /* by the previous five */ vector<TestStatistics>::size_type algorithm); /* by the previous five
ALLOC(TestStatistics)>::size_type /* functions. */ * functions.
algorithm); */
void printCollectiveCrossComparisonStats /* Displays a single */ void printCollectiveCrossComparisonStats /* Displays a single */
(ostream& stream, /* `cell' of the final */ (ostream& stream, /* `cell' of the final */
vector<TestStatistics, /* result cross- */ vector<TestStatistics>::size_type algorithm_y, /* result cross- */
ALLOC(TestStatistics) >::size_type /* comparison table. */ vector<TestStatistics>::size_type algorithm_x, /* comparison table. */
algorithm_y,
vector<TestStatistics,
ALLOC(TestStatistics) >::size_type
algorithm_x,
int data_type); int data_type);
void printCollectiveStats /* Displays average test */ void printCollectiveStats /* Displays average test */

7
lbtt/src/StateSpace.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -144,8 +144,7 @@ void StateSpace::clear()
initial_state = 0; initial_state = 0;
#ifdef HAVE_OBSTACK_H #ifdef HAVE_OBSTACK_H
for (vector<Node*, ALLOC(Node*) >::iterator state = nodes.begin(); for (vector<Node*>::iterator state = nodes.begin(); state != nodes.end();
state != nodes.end();
++state) ++state)
static_cast<State*>(*state)->~State(); static_cast<State*>(*state)->~State();

4
lbtt/src/StateSpace.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

4
lbtt/src/StateSpaceProduct.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

8
lbtt/src/StateSpaceRandomizer.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -174,9 +174,7 @@ StateSpace* StateSpaceRandomizer::generateConnectedGraph() const
StateSpace::size_type first_unreachable_state = 1, random_node; StateSpace::size_type first_unreachable_state = 1, random_node;
multimap<long int, StateSpace::size_type, less<long int>, multimap<long int, StateSpace::size_type> reachable_but_unprocessed;
ALLOC(StateSpace::size_type) >
reachable_but_unprocessed;
reachable_but_unprocessed.insert(make_pair(0, 0)); reachable_but_unprocessed.insert(make_pair(0, 0));

4
lbtt/src/StateSpaceRandomizer.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

14
lbtt/src/StringUtil.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -61,8 +61,7 @@ string toString(const double d, const int precision, const ios::fmtflags flags)
/* ========================================================================= */ /* ========================================================================= */
void sliceString void sliceString
(const string& s, const char* slice_chars, (const string& s, const char* slice_chars, vector<string>& slices)
vector<string, ALLOC(string) >& slices)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Slices a string into a vector of strings, using a given set * Description: Slices a string into a vector of strings, using a given set
@ -415,7 +414,7 @@ int parseInterval
/* ========================================================================= */ /* ========================================================================= */
void parseIntervalList void parseIntervalList
(const string& token, IntervalList& intervals, unsigned long int min, (const string& token, IntervalList& intervals, unsigned long int min,
unsigned long int max, vector<string, ALLOC(string) >* extra_tokens) unsigned long int max, vector<string>* extra_tokens)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Parses a string of number intervals into an IntervalList. * Description: Parses a string of number intervals into an IntervalList.
@ -443,14 +442,13 @@ void parseIntervalList
* *
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
{ {
vector<string, ALLOC(string) > interval_strings; vector<string> interval_strings;
int interval_type; int interval_type;
intervals.clear(); intervals.clear();
sliceString(token, ",", interval_strings); sliceString(token, ",", interval_strings);
for (vector<string, ALLOC(string) >::const_iterator for (vector<string>::const_iterator i = interval_strings.begin();
i = interval_strings.begin();
i != interval_strings.end(); i != interval_strings.end();
++i) ++i)
{ {

11
lbtt/src/StringUtil.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -58,7 +58,7 @@ template<typename T> string toString(const T& t); /* Template function for
void sliceString /* Breaks a string into */ void sliceString /* Breaks a string into */
(const string& s, const char* slice_chars, /* `slices', using a */ (const string& s, const char* slice_chars, /* `slices', using a */
vector<string, ALLOC(string) >& slices); /* given set of vector<string>& slices); /* given set of
* characters as * characters as
* separators. * separators.
*/ */
@ -114,8 +114,9 @@ void parseIntervalList /* Converts a list of */
IntervalList& intervals, /* the set of unsigned */ IntervalList& intervals, /* the set of unsigned */
unsigned long int min, /* long integers */ unsigned long int min, /* long integers */
unsigned long int max, /* corresponding to the */ unsigned long int max, /* corresponding to the */
vector<string, ALLOC(string) >* extra_tokens /* union of the */ vector<string>* extra_tokens = 0); /* union of the
= 0); /* intervals. */ * intervals.
*/
void parseTime /* Parses a time string. */ void parseTime /* Parses a time string. */
(const string& time_string, (const string& time_string,

4
lbtt/src/TempFsysName.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 2004 * Copyright (C) 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

4
lbtt/src/TempFsysName.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 2004 * Copyright (C) 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

116
lbtt/src/TestOperations.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -63,6 +63,8 @@
extern pid_t translator_process;
/****************************************************************************** /******************************************************************************
* *
* Implementations for the operations used in the main test loop. * Implementations for the operations used in the main test loop.
@ -595,7 +597,7 @@ void generateFormulae(istream* formula_input_stream)
{ {
bool fatal_io_error bool fatal_io_error
= (configuration.global_options.formula_input_filename.empty() = (configuration.global_options.formula_input_filename.empty()
|| !round_info.formula_input_file.eof()); || !round_info.formula_input_stream->eof());
printText(string("[") + (fatal_io_error printText(string("[") + (fatal_io_error
? "Error reading formula" ? "Error reading formula"
@ -823,8 +825,7 @@ void writeFormulaeToFiles()
/* ========================================================================= */ /* ========================================================================= */
void generateBuchiAutomaton void generateBuchiAutomaton
(int f, (int f,
vector<Configuration::AlgorithmInformation, vector<Configuration::AlgorithmInformation>::size_type algorithm_id)
ALLOC(Configuration::AlgorithmInformation) >::size_type algorithm_id)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Constructs a BuchiAutomaton by invoking an external program * Description: Constructs a BuchiAutomaton by invoking an external program
@ -867,17 +868,11 @@ void generateBuchiAutomaton
int stdout_capture_fileno = -1, stderr_capture_fileno = -1; int stdout_capture_fileno = -1, stderr_capture_fileno = -1;
int exitcode; int exitcode;
sigset_t sigint_mask;
sigemptyset(&sigint_mask);
sigaddset(&sigint_mask, SIGINT);
struct sigaction timeout_sa; struct sigaction timeout_sa;
timeout_sa.sa_handler = timeoutHandler; timeout_sa.sa_handler = timeoutHandler;
sigemptyset(&timeout_sa.sa_mask); sigemptyset(&timeout_sa.sa_mask);
timeout_sa.sa_flags = 0; timeout_sa.sa_flags = 0;
pid_t pid = 0;
truncateFile(round_info.automaton_file_name->get(), 10); truncateFile(round_info.automaton_file_name->get(), 10);
truncateFile(round_info.cout_capture_file->get(), 10); truncateFile(round_info.cout_capture_file->get(), 10);
truncateFile(round_info.cerr_capture_file->get(), 10); truncateFile(round_info.cerr_capture_file->get(), 10);
@ -932,13 +927,13 @@ void generateBuchiAutomaton
= const_cast<char*>(round_info.automaton_file_name->get()); = const_cast<char*>(round_info.automaton_file_name->get());
times(&timing_information_begin); times(&timing_information_begin);
pid = fork(); translator_process = fork();
switch (pid) switch (translator_process)
{ {
case 0 : /* child */ case 0 : /* child */
close(error_pipe[0]); close(error_pipe[0]);
if (setsid() != -1 if (setpgid(0, 0) != -1
&& dup2(stdout_capture_fileno, STDOUT_FILENO) != -1 && dup2(stdout_capture_fileno, STDOUT_FILENO) != -1
&& dup2(stderr_capture_fileno, STDERR_FILENO) != -1) && dup2(stderr_capture_fileno, STDERR_FILENO) != -1)
execvp(algorithm.parameters[0], algorithm.parameters); execvp(algorithm.parameters[0], algorithm.parameters);
@ -952,17 +947,32 @@ void generateBuchiAutomaton
exit(0); exit(0);
case -1 : /* fork failed */ case -1 : /* fork failed */
pid = 0; translator_process = 0;
error_number = errno; error_number = errno;
close(error_pipe[0]); close(error_pipe[0]);
close(error_pipe[1]); close(error_pipe[1]);
break; break;
default : /* parent */ default : /* parent */
/* Block SIGINT signals while the child process is running. */ setpgid(translator_process, translator_process);
if (configuration.global_options.handle_breaks) if (configuration.global_options.handle_breaks)
sigprocmask(SIG_BLOCK, &sigint_mask, static_cast<sigset_t*>(0)); {
/* If lbtt is currently in the foreground (and has a controlling
terminal), transfer the controlling terminal to the translator
process. */
const pid_t foreground_pgrp = tcgetpgrp(STDIN_FILENO);
if (foreground_pgrp != -1 && foreground_pgrp == getpgrp())
{
sigset_t mask;
sigemptyset(&mask);
sigaddset(&mask, SIGTTOU);
sigprocmask(SIG_BLOCK, &mask, 0);
tcsetpgrp(STDIN_FILENO, translator_process);
sigprocmask(SIG_UNBLOCK, &mask, 0);
}
}
/* Install handler for timeouts if necessary. */ /* Install handler for timeouts if necessary. */
@ -976,12 +986,11 @@ void generateBuchiAutomaton
close(error_pipe[1]); close(error_pipe[1]);
if (waitpid(pid, &exitcode, 0) == -1) /* waitpid failed */ if (waitpid(translator_process, &exitcode, 0) == -1)
/* waitpid failed */
{ {
error_number = errno; error_number = errno;
if (error_number == EINTR /* failure due to timeout */ if (kill(translator_process, 0) == 0) /* child still running */
&& configuration.global_options.translator_timeout > 0
&& timeout)
{ {
/* /*
* Try to terminate the child process three times with SIGTERM * Try to terminate the child process three times with SIGTERM
@ -995,12 +1004,12 @@ void generateBuchiAutomaton
for (int attempts_to_terminate = 0; attempts_to_terminate < 4; for (int attempts_to_terminate = 0; attempts_to_terminate < 4;
++attempts_to_terminate) ++attempts_to_terminate)
{ {
kill(-pid, sig); kill(-translator_process, sig);
sleep(delay); sleep(delay);
if (waitpid(pid, &exitcode, WNOHANG) != 0) if (waitpid(translator_process, &exitcode, WNOHANG) != 0)
{ {
times(&timing_information_end); times(&timing_information_end);
pid = 0; translator_process = 0;
break; break;
} }
if (attempts_to_terminate == 2) if (attempts_to_terminate == 2)
@ -1010,13 +1019,13 @@ void generateBuchiAutomaton
} }
} }
} }
else else if (errno != EPERM)
pid = 0; translator_process = 0;
} }
else /* child exited successfully */ else /* child exited successfully */
{ {
times(&timing_information_end); times(&timing_information_end);
pid = 0; translator_process = 0;
/* /*
* If there is something to be read from error_pipe, then there * If there is something to be read from error_pipe, then there
@ -1043,10 +1052,21 @@ void generateBuchiAutomaton
} }
if (configuration.global_options.handle_breaks) if (configuration.global_options.handle_breaks)
sigprocmask(SIG_UNBLOCK, &sigint_mask, {
static_cast<sigset_t*>(0)); /* Put lbtt again in the foreground. */
if (pid == 0 if (tcgetpgrp(STDIN_FILENO) != -1)
{
sigset_t mask;
sigemptyset(&mask);
sigaddset(&mask, SIGTTOU);
sigprocmask(SIG_BLOCK, &mask, 0);
tcsetpgrp(STDIN_FILENO, getpgrp());
sigprocmask(SIG_UNBLOCK, &mask, 0);
}
}
if (translator_process == 0
&& timing_information_begin.tms_utime && timing_information_begin.tms_utime
!= static_cast<clock_t>(-1) != static_cast<clock_t>(-1)
&& timing_information_begin.tms_cutime && timing_information_begin.tms_cutime
@ -1069,15 +1089,15 @@ void generateBuchiAutomaton
close(stderr_capture_fileno); close(stderr_capture_fileno);
/* /*
* If pid != 0 at this point, then a timeout occurred, but lbtt was * If translator_process != 0 at this point, then a timeout occurred,
* unable to terminate the child process. The exception handler will * but lbtt was unable to terminate the child process. The exception
* in this case throw an unexpected exception (see below) so that lbtt * handler will in this case throw an unexpected exception (see below)
* will terminate (for example, it is not safe to use the temporary * so that lbtt will terminate (for example, it is not safe to use the
* file names any longer if the (still running) child process happens to * temporary file names any longer if the (still running) child process
* write to them). * happens to write to them).
*/ */
if (pid != 0) if (translator_process != 0)
{ {
stdout_capture_fileno = stderr_capture_fileno = -1; stdout_capture_fileno = stderr_capture_fileno = -1;
throw Exception("could not terminate child process"); throw Exception("could not terminate child process");
@ -1286,7 +1306,7 @@ void generateBuchiAutomaton
round_info.transcript_file.flush(); round_info.transcript_file.flush();
} }
if (pid != 0) /* fatal error, lbtt should be terminated */ if (translator_process != 0) /* fatal error, lbtt should be terminated */
throw Exception throw Exception
("fatal internal error while generating Büchi automaton"); ("fatal internal error while generating Büchi automaton");
@ -1345,9 +1365,7 @@ void generateBuchiAutomaton
/* ========================================================================= */ /* ========================================================================= */
void performEmptinessCheck void performEmptinessCheck
(int f, (int f,
vector<Configuration::AlgorithmInformation, vector<Configuration::AlgorithmInformation>::size_type algorithm_id)
ALLOC(Configuration::AlgorithmInformation) >::size_type
algorithm_id)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Performs the emptiness check on a ProductAutomaton, i.e., * Description: Performs the emptiness check on a ProductAutomaton, i.e.,
@ -1473,9 +1491,7 @@ void performEmptinessCheck
/* ========================================================================= */ /* ========================================================================= */
void performConsistencyCheck void performConsistencyCheck
(vector<Configuration::AlgorithmInformation, (vector<Configuration::AlgorithmInformation>::size_type algorithm_id)
ALLOC(Configuration::AlgorithmInformation) >::size_type
algorithm_id)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Checks the model checking results for consistency for a * Description: Checks the model checking results for consistency for a
@ -1570,8 +1586,7 @@ void compareResults()
AutomatonStats* alg_1_stats; AutomatonStats* alg_1_stats;
AutomatonStats* alg_2_stats; AutomatonStats* alg_2_stats;
for (vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type for (vector<AlgorithmTestResults>::size_type alg_1 = 0;
alg_1 = 0;
alg_1 < test_results.size(); alg_1 < test_results.size();
++alg_1) ++alg_1)
{ {
@ -1579,8 +1594,7 @@ void compareResults()
{ {
alg_1_stats = &test_results[alg_1].automaton_stats[counter]; alg_1_stats = &test_results[alg_1].automaton_stats[counter];
for (vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) > for (vector<AlgorithmTestResults>::size_type alg_2 = alg_1 + 1;
::size_type alg_2 = alg_1 + 1;
alg_2 < test_results.size(); alg_2 < test_results.size();
++alg_2) ++alg_2)
{ {
@ -1681,13 +1695,11 @@ void performBuchiIntersectionCheck()
::Graph::BuchiProduct::clearSatisfiabilityCache(); ::Graph::BuchiProduct::clearSatisfiabilityCache();
for (vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type for (vector<AlgorithmTestResults>::size_type alg_1 = 0;
alg_1 = 0;
alg_1 < round_info.number_of_translators; alg_1 < round_info.number_of_translators;
++alg_1) ++alg_1)
{ {
for (vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type for (vector<AlgorithmTestResults>::size_type alg_2 = 0;
alg_2 = 0;
alg_2 < round_info.number_of_translators; alg_2 < round_info.number_of_translators;
++alg_2) ++alg_2)
{ {

24
lbtt/src/TestOperations.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -95,25 +95,25 @@ void writeFormulaeToFiles(); /* Writes LTL formulas */
void generateBuchiAutomaton /* Generates a Büchi */ void generateBuchiAutomaton /* Generates a Büchi */
(int f, /* automaton from a LTL */ (int f, /* automaton from a LTL */
vector<Configuration::AlgorithmInformation, /* formula stored in a */ vector<Configuration::AlgorithmInformation> /* formula stored in a */
ALLOC(Configuration::AlgorithmInformation) > /* given file, using a */ ::size_type /* given file, using a */
::size_type /* given LTL-to-Büchi */ algorithm_id); /* given LTL-to-Büchi
algorithm_id); /* translation algorithm * translation algorithm
* for the conversion. * for the conversion.
*/ */
void performEmptinessCheck /* Performs an emptiness */ void performEmptinessCheck /* Performs an emptiness */
(int f, /* check on a product */ (int f, /* check on a product */
vector<Configuration::AlgorithmInformation, /* automaton. */ vector<Configuration::AlgorithmInformation> /* automaton. */
ALLOC(Configuration::AlgorithmInformation) >
::size_type ::size_type
algorithm_id); algorithm_id);
void performConsistencyCheck /* Performs a */ void performConsistencyCheck /* Performs a */
(vector<Configuration::AlgorithmInformation, /* consistency check on */ (vector<Configuration::AlgorithmInformation> /* consistency check on */
ALLOC(Configuration::AlgorithmInformation) > /* the test results */ ::size_type /* the test results */
::size_type /* for a formula and its */ algorithm_id); /* for a formula and its
algorithm_id); /* negation. */ * negation.
*/
void compareResults(); /* Compares the model void compareResults(); /* Compares the model
* checking results * checking results

18
lbtt/src/TestRoundInfo.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -55,7 +55,11 @@ public:
* stream for messages. * stream for messages.
*/ */
ifstream formula_input_file; /* Stream for reading input istream* formula_input_stream; /* Stream for reading input
* formulae.
*/
ifstream formula_input_file; /* File for reading input
* formulae. * formulae.
*/ */
@ -149,9 +153,9 @@ public:
* current round. * current round.
*/ */
vector<class ::Ltl::LtlFormula*, /* Formulae used in the */ vector<class ::Ltl::LtlFormula*> formulae; /* Formulae used in the
ALLOC(class ::Ltl::LtlFormula*) > /* current round: */ * current round:
formulae; /* formulae[0]: * formulae[0]:
* positive formula in * positive formula in
* negation normal * negation normal
* form * form
@ -167,7 +171,7 @@ public:
* generated * generated
*/ */
vector<bool, ALLOC(bool) > formula_in_file; /* The values in this vector<bool> formula_in_file; /* The values in this
* vector will be set to * vector will be set to
* true when the * true when the
* corresponding * corresponding

9
lbtt/src/TestStatistics.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -50,8 +50,7 @@ void AlgorithmTestResults::emptinessReset()
automaton_stats[i].emptiness_check_result.clear(); automaton_stats[i].emptiness_check_result.clear();
automaton_stats[i].emptiness_check_performed = false; automaton_stats[i].emptiness_check_performed = false;
for (vector<AutomatonStats::CrossComparisonStats, for (vector<AutomatonStats::CrossComparisonStats>::iterator it
ALLOC(AutomatonStats::CrossComparisonStats) >::iterator it
= automaton_stats[i].cross_comparison_stats.begin(); = automaton_stats[i].cross_comparison_stats.begin();
it != automaton_stats[i].cross_comparison_stats.end(); it != automaton_stats[i].cross_comparison_stats.end();
++it) ++it)
@ -87,7 +86,7 @@ void AlgorithmTestResults::fullReset()
automaton_stats[i].number_of_msccs = 0; automaton_stats[i].number_of_msccs = 0;
automaton_stats[i].buchi_generation_time = 0.0; automaton_stats[i].buchi_generation_time = 0.0;
for (vector<int, ALLOC(int) >::iterator it for (vector<int>::iterator it
= automaton_stats[i].buchi_intersection_check_stats.begin(); = automaton_stats[i].buchi_intersection_check_stats.begin();
it != automaton_stats[i].buchi_intersection_check_stats.end(); it != automaton_stats[i].buchi_intersection_check_stats.end();
++it) ++it)

72
lbtt/src/TestStatistics.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -43,9 +43,8 @@ using Graph::StateSpace;
struct AutomatonStats struct AutomatonStats
{ {
explicit AutomatonStats /* Constructor. */ explicit AutomatonStats /* Constructor. */
(vector<Configuration::AlgorithmInformation, (vector<Configuration::AlgorithmInformation>
ALLOC(Configuration::AlgorithmInformation) > ::size_type number_of_algorithms,
::size_type number_of_algorithms,
StateSpace::size_type max_statespace_size); StateSpace::size_type max_statespace_size);
/* default copy constructor */ /* default copy constructor */
@ -127,9 +126,9 @@ struct AutomatonStats
typedef pair<bool, unsigned long int> typedef pair<bool, unsigned long int>
CrossComparisonStats; CrossComparisonStats;
vector<CrossComparisonStats, /* Emptiness check */ vector<CrossComparisonStats> /* Emptiness check */
ALLOC(CrossComparisonStats) > /* cross-comparison */ cross_comparison_stats; /* cross-comparison
cross_comparison_stats; /* results. The `first' * results. The `first'
* element of the pair * element of the pair
* tells whether a cross- * tells whether a cross-
* comparison with a given * comparison with a given
@ -142,8 +141,8 @@ struct AutomatonStats
* differ. * differ.
*/ */
vector<int, ALLOC(int) > /* Büchi automaton */ vector<int> buchi_intersection_check_stats; /* Büchi automaton
buchi_intersection_check_stats; /* intersection * intersection
* emptiness check * emptiness check
* results. The elements * results. The elements
* of the vector tell * of the vector tell
@ -173,8 +172,7 @@ struct AutomatonStats
struct AlgorithmTestResults struct AlgorithmTestResults
{ {
explicit AlgorithmTestResults /* Constructor. */ explicit AlgorithmTestResults /* Constructor. */
(vector<Configuration::AlgorithmInformation, (vector<Configuration::AlgorithmInformation>
ALLOC(Configuration::AlgorithmInformation) >
::size_type ::size_type
number_of_algorithms, number_of_algorithms,
StateSpace::size_type max_statespace_size); StateSpace::size_type max_statespace_size);
@ -214,8 +212,8 @@ struct AlgorithmTestResults
* check. * check.
*/ */
vector<AutomatonStats, ALLOC(AutomatonStats) > /* A two-element vector */ vector<AutomatonStats> automaton_stats; /* A two-element vector
automaton_stats; /* storing test results * storing test results
* for an algorithm. * for an algorithm.
*/ */
}; };
@ -232,8 +230,7 @@ struct AlgorithmTestResults
struct TestStatistics struct TestStatistics
{ {
explicit TestStatistics /* Constructor. */ explicit TestStatistics /* Constructor. */
(vector<TestStatistics, (vector<TestStatistics>::size_type
ALLOC(TestStatistics) >::size_type
number_of_algorithms); number_of_algorithms);
/* default copy constructor */ /* default copy constructor */
@ -303,24 +300,26 @@ struct TestStatistics
* automata. * automata.
*/ */
vector<unsigned long int, /* Number of failed */ vector<unsigned long int> /* Number of failed */
ALLOC(unsigned long int) > /* result cross- */ cross_comparison_mismatches; /* result cross-
cross_comparison_mismatches; /* comparisons. */ * comparisons.
*/
vector<unsigned long int, /* Number of failed */ vector<unsigned long int> /* Number of failed */
ALLOC(unsigned long int) > /* result cross- */ initial_cross_comparison_mismatches; /* result cross-
initial_cross_comparison_mismatches; /* comparisons in the * comparisons in the
* initial state of the * initial state of the
* state space. * state space.
*/ */
vector<unsigned long int, /* Number of result */ vector<unsigned long int> /* Number of result */
ALLOC(unsigned long int) > /* cross-comparisons */ cross_comparisons_performed; /* cross-comparisons
cross_comparisons_performed; /* performed. */ * performed.
*/
vector<unsigned long int, /* Number of failed */ vector<unsigned long int> /* Number of failed */
ALLOC(unsigned long int) > /* Büchi automaton */ buchi_intersection_check_failures; /* Büchi automaton
buchi_intersection_check_failures; /* emptiness checks * emptiness checks
* against the automata * against the automata
* constructed from the * constructed from the
* negated formula * negated formula
@ -328,9 +327,9 @@ struct TestStatistics
* algorithms. * algorithms.
*/ */
vector<unsigned long int, /* Number of Büchi */ vector<unsigned long int> /* Number of Büchi */
ALLOC(unsigned long int) > /* automaton emptiness */ buchi_intersection_checks_performed; /* automaton emptiness
buchi_intersection_checks_performed; /* checks performed * checks performed
* against the automata * against the automata
* constructed from the * constructed from the
* negated formula using * negated formula using
@ -348,9 +347,7 @@ struct TestStatistics
/* ========================================================================= */ /* ========================================================================= */
inline AutomatonStats::AutomatonStats inline AutomatonStats::AutomatonStats
(vector<Configuration::AlgorithmInformation, (vector<Configuration::AlgorithmInformation>::size_type number_of_algorithms,
ALLOC(Configuration::AlgorithmInformation) >::size_type
number_of_algorithms,
StateSpace::size_type max_statespace_size) : StateSpace::size_type max_statespace_size) :
buchi_automaton(0), number_of_buchi_states(0), buchi_automaton(0), number_of_buchi_states(0),
number_of_buchi_transitions(0), number_of_acceptance_sets(0), number_of_buchi_transitions(0), number_of_acceptance_sets(0),
@ -472,9 +469,7 @@ AutomatonStats::buchiIntersectionCheckPerformed(unsigned long int algorithm)
/* ========================================================================= */ /* ========================================================================= */
inline AlgorithmTestResults::AlgorithmTestResults inline AlgorithmTestResults::AlgorithmTestResults
(vector<Configuration::AlgorithmInformation, (vector<Configuration::AlgorithmInformation>::size_type number_of_algorithms,
ALLOC(Configuration::AlgorithmInformation) >::size_type
number_of_algorithms,
StateSpace::size_type max_statespace_size) : StateSpace::size_type max_statespace_size) :
consistency_check_result(-1), consistency_check_comparisons(0), consistency_check_result(-1), consistency_check_comparisons(0),
failed_consistency_check_comparisons(0), failed_consistency_check_comparisons(0),
@ -519,8 +514,7 @@ inline AlgorithmTestResults::~AlgorithmTestResults()
/* ========================================================================= */ /* ========================================================================= */
inline TestStatistics::TestStatistics inline TestStatistics::TestStatistics
(vector<TestStatistics, ALLOC(TestStatistics) >::size_type (vector<TestStatistics>::size_type number_of_algorithms) :
number_of_algorithms) :
consistency_check_failures(0), consistency_checks_performed(0), consistency_check_failures(0), consistency_checks_performed(0),
cross_comparison_mismatches(number_of_algorithms, 0), cross_comparison_mismatches(number_of_algorithms, 0),
initial_cross_comparison_mismatches(number_of_algorithms, 0), initial_cross_comparison_mismatches(number_of_algorithms, 0),

4
lbtt/src/TranslatorInterface.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License

20
lbtt/src/UserCommandReader.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -86,7 +86,7 @@ void executeUserCommands()
* ------------------------------------------------------------------------ */ * ------------------------------------------------------------------------ */
{ {
string input_line; string input_line;
vector<string, ALLOC(string) > input_tokens; vector<string> input_tokens;
TokenType token; TokenType token;
bool formula_type = true; bool formula_type = true;
@ -230,9 +230,7 @@ void executeUserCommands()
{ {
bool all_algorithms_disabled = true; bool all_algorithms_disabled = true;
for (vector<Configuration::AlgorithmInformation, for (vector<Configuration::AlgorithmInformation>::const_iterator
ALLOC(Configuration::AlgorithmInformation) >
::const_iterator
algorithm = configuration.algorithms.begin(); algorithm = configuration.algorithms.begin();
algorithm != configuration.algorithms.end(); algorithm != configuration.algorithms.end();
++algorithm) ++algorithm)
@ -799,9 +797,8 @@ TokenType parseCommand(const string& token)
/* ========================================================================= */ /* ========================================================================= */
void verifyArgumentCount void verifyArgumentCount
(const vector<string, ALLOC(string) >& command, (const vector<string>& command, vector<string>::size_type min_arg_count,
vector<string, ALLOC(string) >::size_type min_arg_count, vector<string>::size_type max_arg_count)
vector<string, ALLOC(string) >::size_type max_arg_count)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Verifies that the number of arguments given for a user * Description: Verifies that the number of arguments given for a user
@ -824,8 +821,7 @@ void verifyArgumentCount
} }
/* ========================================================================= */ /* ========================================================================= */
pair<string, bool> parseRedirection pair<string, bool> parseRedirection(vector<string>& input_tokens)
(vector<string, ALLOC(string) >& input_tokens)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Tests whether the last argument to a user command specifies * Description: Tests whether the last argument to a user command specifies
@ -888,7 +884,7 @@ pair<string, bool> parseRedirection
} }
/* ========================================================================= */ /* ========================================================================= */
bool parseFormulaType(vector<string, ALLOC(string) >& input_tokens) bool parseFormulaType(vector<string>& input_tokens)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Tests whether the first argument of a command specifies a * Description: Tests whether the first argument of a command specifies a

17
lbtt/src/UserCommandReader.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -65,22 +65,19 @@ TokenType parseCommand(const string& token); /* Translates a command
*/ */
void verifyArgumentCount /* Checks that the */ void verifyArgumentCount /* Checks that the */
(const vector<string, ALLOC(string) >& /* number of arguments */ (const vector<string>& arguments, /* number of arguments */
arguments, /* for a command is */ vector<string>::size_type min_arg_count, /* for a command is */
vector<string, ALLOC(string) >::size_type /* within given limits. */ vector<string>::size_type max_arg_count); /* within given limits. */
min_arg_count,
vector<string, ALLOC(string) >::size_type
max_arg_count);
pair<string, bool> parseRedirection /* Checks whether an */ pair<string, bool> parseRedirection /* Checks whether an */
(vector<string, ALLOC(string) >& input_tokens); /* user command given (vector<string>& input_tokens); /* user command given
* will require * will require
* redirecting its * redirecting its
* output to a file. * output to a file.
*/ */
bool parseFormulaType /* Checks whether an */ bool parseFormulaType /* Checks whether an */
(vector<string, ALLOC(string) >& input_tokens); /* user command (vector<string>& input_tokens); /* user command
* specified a positive * specified a positive
* or a negative * or a negative
* formula. * formula.

56
lbtt/src/UserCommands.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -73,8 +73,7 @@ unsigned long int parseAlgorithmId(const string& id)
} }
catch (const NotANumberException&) catch (const NotANumberException&)
{ {
map<string, unsigned long int, less<string>, ALLOC(unsigned long int) > map<string, unsigned long int>::const_iterator id_finder
::const_iterator id_finder
= configuration.algorithm_names.find(unquoted_id); = configuration.algorithm_names.find(unquoted_id);
if (id_finder == configuration.algorithm_names.end()) if (id_finder == configuration.algorithm_names.end())
throw CommandErrorException throw CommandErrorException
@ -113,20 +112,18 @@ void parseAlgorithmIdList(const string& ids, IntervalList& algorithms)
try try
{ {
vector<string, ALLOC(string) > nonnumeric_algorithm_ids; vector<string> nonnumeric_algorithm_ids;
parseIntervalList(id_string, algorithms, 0, parseIntervalList(id_string, algorithms, 0,
round_info.number_of_translators - 1, round_info.number_of_translators - 1,
&nonnumeric_algorithm_ids); &nonnumeric_algorithm_ids);
for (vector<string, ALLOC(string) >::iterator for (vector<string>::iterator id = nonnumeric_algorithm_ids.begin();
id = nonnumeric_algorithm_ids.begin();
id != nonnumeric_algorithm_ids.end(); id != nonnumeric_algorithm_ids.end();
++id) ++id)
{ {
*id = unquoteString(substituteInQuotedString(*id, "\n", ",")); *id = unquoteString(substituteInQuotedString(*id, "\n", ","));
map<string, unsigned long int, less<string>, ALLOC(unsigned long int) > map<string, unsigned long int>::const_iterator
::const_iterator
id_finder = configuration.algorithm_names.find(*id); id_finder = configuration.algorithm_names.find(*id);
if (id_finder == configuration.algorithm_names.end()) if (id_finder == configuration.algorithm_names.end())
throw CommandErrorException throw CommandErrorException
@ -181,7 +178,7 @@ void printAlgorithmList(ostream& stream, int indent)
/* ========================================================================= */ /* ========================================================================= */
void printCrossComparisonAnalysisResults void printCrossComparisonAnalysisResults
(ostream& stream, int indent, bool formula_type, (ostream& stream, int indent, bool formula_type,
const vector<string, ALLOC(string) >& input_tokens) const vector<string>& input_tokens)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Implements the user command `resultanalysis', i.e., analyzes * Description: Implements the user command `resultanalysis', i.e., analyzes
@ -494,8 +491,7 @@ void printCrossComparisonAnalysisResults
/* ========================================================================= */ /* ========================================================================= */
void printConsistencyAnalysisResults void printConsistencyAnalysisResults
(ostream& stream, int indent, (ostream& stream, int indent, const vector<string>& input_tokens)
const vector<string, ALLOC(string) >& input_tokens)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Implements the user command `consistencyanalysis', i.e., * Description: Implements the user command `consistencyanalysis', i.e.,
@ -607,11 +603,9 @@ void printConsistencyAnalysisResults
} }
} }
vector<StateSpace::size_type, ALLOC(StateSpace::size_type) > path; vector<StateSpace::size_type> path;
StateSpace::Path prefix, cycle; StateSpace::Path prefix, cycle;
map<StateSpace::size_type, StateSpace::size_type, map<StateSpace::size_type, StateSpace::size_type> ordering;
less<StateSpace::size_type>, ALLOC(StateSpace::size_type) >
ordering;
StateSpace::size_type state_count = 0; StateSpace::size_type state_count = 0;
StateSpace::size_type loop_state; StateSpace::size_type loop_state;
@ -663,8 +657,7 @@ void printConsistencyAnalysisResults
/* ========================================================================= */ /* ========================================================================= */
void printAutomatonAnalysisResults void printAutomatonAnalysisResults
(ostream& stream, int indent, (ostream& stream, int indent, const vector<string>& input_tokens)
const vector<string, ALLOC(string) >& input_tokens)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Implements the user command `buchianalysis', i.e., analyzes * Description: Implements the user command `buchianalysis', i.e., analyzes
@ -977,9 +970,7 @@ void printPath
/* ========================================================================= */ /* ========================================================================= */
void printAcceptingCycle void printAcceptingCycle
(ostream& stream, int indent, (ostream& stream, int indent,
vector<Configuration::AlgorithmInformation, vector<Configuration::AlgorithmInformation>::size_type algorithm_id,
ALLOC(Configuration::AlgorithmInformation) >::size_type
algorithm_id,
const BuchiAutomaton::Path& aut_prefix, const BuchiAutomaton::Path& aut_prefix,
const BuchiAutomaton::Path& aut_cycle, const BuchiAutomaton::Path& aut_cycle,
const BuchiAutomaton& automaton, const StateSpace::Path& path_prefix, const BuchiAutomaton& automaton, const StateSpace::Path& path_prefix,
@ -1121,8 +1112,7 @@ void printAcceptingCycle
/* ========================================================================= */ /* ========================================================================= */
void printBuchiAutomaton void printBuchiAutomaton
(ostream& stream, int indent, bool formula_type, (ostream& stream, int indent, bool formula_type,
vector<string, ALLOC(string) >& input_tokens, vector<string>& input_tokens, Graph::GraphOutputFormat fmt)
Graph::GraphOutputFormat fmt)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Implements the user command `buchi', i.e., writes information * Description: Implements the user command `buchi', i.e., writes information
@ -1231,8 +1221,8 @@ void printBuchiAutomaton
/* ========================================================================= */ /* ========================================================================= */
void evaluateFormula void evaluateFormula
(ostream& stream, int indent, bool formula_type, (ostream& stream, int indent, bool formula_type,
vector<string, ALLOC(string) >& input_tokens) vector<string>& input_tokens)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Implements the user command `evaluate', i.e., tells whether * Description: Implements the user command `evaluate', i.e., tells whether
@ -1346,7 +1336,7 @@ void evaluateFormula
/* ========================================================================= */ /* ========================================================================= */
void printFormula void printFormula
(ostream& stream, int indent, bool formula_type, (ostream& stream, int indent, bool formula_type,
const vector<string, ALLOC(string) >& input_tokens) const vector<string>& input_tokens)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Implements the user command `formula', i.e., displays the * Description: Implements the user command `formula', i.e., displays the
@ -1401,8 +1391,7 @@ void printFormula
/* ========================================================================= */ /* ========================================================================= */
void printCommandHelp void printCommandHelp
(ostream& stream, int indent, (ostream& stream, int indent, const vector<string>& input_tokens)
const vector<string, ALLOC(string) >& input_tokens)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Implements the user command `help', i.e., gives instructions * Description: Implements the user command `help', i.e., gives instructions
@ -1714,7 +1703,7 @@ void printCommandHelp
/* ========================================================================= */ /* ========================================================================= */
void printInconsistencies void printInconsistencies
(ostream& stream, int indent, vector<string, ALLOC(string) >& input_tokens) (ostream& stream, int indent, vector<string>& input_tokens)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Implements the user command `inconsistencies', i.e., lists * Description: Implements the user command `inconsistencies', i.e., lists
@ -1818,7 +1807,7 @@ void printInconsistencies
/* ========================================================================= */ /* ========================================================================= */
void printTestResults void printTestResults
(ostream& stream, int indent, vector<string, ALLOC(string) >& input_tokens) (ostream& stream, int indent, vector<string>& input_tokens)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Implements the user command `results', i.e., displays the * Description: Implements the user command `results', i.e., displays the
@ -1877,7 +1866,7 @@ void printTestResults
/* ========================================================================= */ /* ========================================================================= */
void printStateSpace void printStateSpace
(ostream& stream, int indent, vector<string, ALLOC(string) >& input_tokens, (ostream& stream, int indent, vector<string>& input_tokens,
Graph::GraphOutputFormat fmt) Graph::GraphOutputFormat fmt)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
@ -1950,7 +1939,7 @@ void printStateSpace
} }
/* ========================================================================= */ /* ========================================================================= */
void changeVerbosity(const vector<string, ALLOC(string) >& input_tokens) void changeVerbosity(const vector<string>& input_tokens)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Implements the user command `verbosity', i.e., displays or * Description: Implements the user command `verbosity', i.e., displays or
@ -1987,8 +1976,7 @@ void changeVerbosity(const vector<string, ALLOC(string) >& input_tokens)
} }
/* ========================================================================= */ /* ========================================================================= */
void changeAlgorithmState void changeAlgorithmState(vector<string>& input_tokens, bool enable)
(vector<string, ALLOC(string) >& input_tokens, bool enable)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Changes the enabledness of a set of algorithms used in the * Description: Changes the enabledness of a set of algorithms used in the

44
lbtt/src/UserCommands.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -67,20 +67,19 @@ void printAlgorithmList /* Displays a list of */
void printCrossComparisonAnalysisResults /* Analyzes a */ void printCrossComparisonAnalysisResults /* Analyzes a */
(ostream& stream, int indent, /* contradiction between */ (ostream& stream, int indent, /* contradiction between */
bool formula_type, /* test results of two */ bool formula_type, /* test results of two */
const vector<string, ALLOC(string) >& /* implementations. */ const vector<string>& input_tokens); /* implementations. */
input_tokens);
void printConsistencyAnalysisResults /* Analyzes a */ void printConsistencyAnalysisResults /* Analyzes a */
(ostream& stream, int indent, /* contradicition in the */ (ostream& stream, int indent, /* contradicition in the */
const vector<string, ALLOC(string) >& /* model checking result */ const vector<string>& input_tokens); /* model checking result
input_tokens); /* consistency check for * consistency check for
* an implementation. * an implementation.
*/ */
void printAutomatonAnalysisResults /* Analyzes a */ void printAutomatonAnalysisResults /* Analyzes a */
(ostream& stream, int indent, /* contradiction in the */ (ostream& stream, int indent, /* contradiction in the */
const vector<string, ALLOC(string) >& /* Büchi automata */ const vector<string>& input_tokens); /* Büchi automata
input_tokens); /* intersection * intersection
* emptiness check. * emptiness check.
*/ */
@ -92,8 +91,7 @@ void printPath /* Displays information */
void printAcceptingCycle /* Displays information */ void printAcceptingCycle /* Displays information */
(ostream& stream, int indent, /* a single automaton */ (ostream& stream, int indent, /* a single automaton */
vector<Configuration::AlgorithmInformation, /* execution. */ vector<Configuration::AlgorithmInformation> /* execution. */
ALLOC(Configuration::AlgorithmInformation) >
::size_type ::size_type
algorithm_id, algorithm_id,
const BuchiAutomaton::Path& aut_prefix, const BuchiAutomaton::Path& aut_prefix,
@ -106,47 +104,47 @@ void printAcceptingCycle /* Displays information */
void printBuchiAutomaton /* Displays information */ void printBuchiAutomaton /* Displays information */
(ostream& stream, int indent, /* about a Büchi */ (ostream& stream, int indent, /* about a Büchi */
bool formula_type, /* automaton. */ bool formula_type, /* automaton. */
vector<string, ALLOC(string) >& input_tokens, vector<string>& input_tokens,
Graph::GraphOutputFormat fmt); Graph::GraphOutputFormat fmt);
void evaluateFormula /* Displays information */ void evaluateFormula /* Displays information */
(ostream& stream, int indent, /* about existence of */ (ostream& stream, int indent, /* about existence of */
bool formula_type, /* accepting system */ bool formula_type, /* accepting system */
vector<string, ALLOC(string) >& input_tokens); /* executions. */ vector<string>& input_tokens); /* executions. */
void printFormula /* Displays a formula */ void printFormula /* Displays a formula */
(ostream& stream, int indent, /* used for testing. */ (ostream& stream, int indent, /* used for testing. */
bool formula_type, bool formula_type,
const vector<string, ALLOC(string) >& const vector<string>& input_tokens);
input_tokens);
void printCommandHelp /* Displays help about */ void printCommandHelp /* Displays help about */
(ostream& stream, int indent, /* user commands. */ (ostream& stream, int indent, /* user commands. */
const vector<string, ALLOC(string) >& const vector<string>& input_tokens);
input_tokens);
void printInconsistencies /* Lists the system */ void printInconsistencies /* Lists the system */
(ostream& stream, int indent, /* states failing the */ (ostream& stream, int indent, /* states failing the */
vector<string, ALLOC(string) >& input_tokens); /* consistency check vector<string>& input_tokens); /* consistency check
* for an algorihm. * for an algorihm.
*/ */
void printTestResults /* Displays the test */ void printTestResults /* Displays the test */
(ostream& stream, int indent, /* results of the last */ (ostream& stream, int indent, /* results of the last */
vector<string, ALLOC(string) >& input_tokens); /* round performed. */ vector<string>& input_tokens); /* round performed. */
void printStateSpace /* Displays information */ void printStateSpace /* Displays information */
(ostream& stream, int indent, /* about a state space. */ (ostream& stream, int indent, /* about a state space. */
vector<string, ALLOC(string) >& input_tokens, vector<string>& input_tokens,
Graph::GraphOutputFormat fmt); Graph::GraphOutputFormat fmt);
void changeVerbosity /* Displays or changes */ void changeVerbosity /* Displays or changes */
(const vector<string, ALLOC(string) >& /* the verbosity of */ (const vector<string>& input_tokens); /* the verbosity of
input_tokens); /* output. */ * output.
*/
void changeAlgorithmState /* Enables or disables a */ void changeAlgorithmState /* Enables or disables a */
(vector<string, ALLOC(string) >& input_tokens, /* set of algorithms */ (vector<string>& input_tokens, bool enable); /* set of algorithms
bool enable); /* used in the tests. */ * used in the tests.
*/
} }

68
lbtt/src/main.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -21,6 +21,9 @@
#include <csignal> #include <csignal>
#include <cstdlib> #include <cstdlib>
#include <ctime> #include <ctime>
#ifdef HAVE_SYS_TYPES_H
#include <sys/types.h>
#endif /* HAVE_SYS_TYPES_H */
#include <iostream> #include <iostream>
#include <vector> #include <vector>
#ifdef HAVE_READLINE #ifdef HAVE_READLINE
@ -28,6 +31,11 @@
#include <readline/readline.h> #include <readline/readline.h>
#include <readline/history.h> #include <readline/history.h>
#endif /* HAVE_READLINE */ #endif /* HAVE_READLINE */
#ifdef HAVE_ISATTY
#ifdef HAVE_UNISTD_H
#include <unistd.h>
#endif /* HAVE_UNISTD_H */
#endif /* HAVE_ISATTY */
#include "LbttAlloc.h" #include "LbttAlloc.h"
#include "Configuration.h" #include "Configuration.h"
#include "DispUtil.h" #include "DispUtil.h"
@ -82,12 +90,12 @@ TestRoundInfo round_info; /* Data structure for
* round. * round.
*/ */
vector<AlgorithmTestResults, /* Test results for each */ vector<AlgorithmTestResults> test_results; /* Test results for each
ALLOC(AlgorithmTestResults) > /* individual algorithm. */ * individual algorithm.
test_results; */
vector<TestStatistics, ALLOC(TestStatistics) > /* Overall test */ vector<TestStatistics> final_statistics; /* Overall test
final_statistics; /* statistics for each * statistics for each
* algorithm. * algorithm.
*/ */
@ -167,9 +175,13 @@ static void breakHandler(int)
* *
*****************************************************************************/ *****************************************************************************/
pid_t translator_process = 0; /* Process group for translator process */
static void abortHandler(int signum) static void abortHandler(int signum)
{ {
deallocateTempFilenames(); deallocateTempFilenames();
if (translator_process != 0 && kill(translator_process, 0) == 0)
kill(-translator_process, SIGTERM);
struct sigaction s; struct sigaction s;
s.sa_handler = SIG_DFL; s.sa_handler = SIG_DFL;
sigemptyset(&s.sa_mask); sigemptyset(&s.sa_mask);
@ -274,16 +286,24 @@ bool testLoop()
/* /*
* If a formula file name was given in the configuration, open the file for * If a formula file name was given in the configuration, open the file for
* reading. * reading. The special filename "-" refers to the standard input.
*/ */
try try
{ {
if (!global_options.formula_input_filename.empty()) if (!global_options.formula_input_filename.empty())
openFile(global_options.formula_input_filename.c_str(), {
round_info.formula_input_file, if (global_options.formula_input_filename == "-")
ios::in, round_info.formula_input_stream = &cin;
0); else
{
openFile(global_options.formula_input_filename.c_str(),
round_info.formula_input_file,
ios::in,
0);
round_info.formula_input_stream = &round_info.formula_input_file;
}
}
} }
catch (const FileOpenException& e) catch (const FileOpenException& e)
{ {
@ -383,8 +403,7 @@ bool testLoop()
round_info.next_round_to_change_statespace round_info.next_round_to_change_statespace
+= global_options.statespace_change_interval; += global_options.statespace_change_interval;
for (vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) > for (vector<AlgorithmTestResults>::iterator it = test_results.begin();
::iterator it = test_results.begin();
it != test_results.end(); it != test_results.end();
++it) ++it)
it->emptinessReset(); it->emptinessReset();
@ -437,8 +456,7 @@ bool testLoop()
round_info.formula_in_file[0] = round_info.formula_in_file[1] = false; round_info.formula_in_file[0] = round_info.formula_in_file[1] = false;
for (vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) > for (vector<AlgorithmTestResults>::iterator it = test_results.begin();
::iterator it = test_results.begin();
it != test_results.end(); it != test_results.end();
++it) ++it)
it->fullReset(); it->fullReset();
@ -449,8 +467,8 @@ bool testLoop()
{ {
try try
{ {
generateFormulae(round_info.formula_input_file.is_open() generateFormulae(!global_options.formula_input_filename.empty()
? &round_info.formula_input_file ? round_info.formula_input_stream
: 0); : 0);
} }
catch (const FormulaGenerationException&) catch (const FormulaGenerationException&)
@ -667,8 +685,7 @@ bool testLoop()
::Ltl::LtlFormula::destruct(round_info.formulae[f]); ::Ltl::LtlFormula::destruct(round_info.formulae[f]);
} }
for (vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) > for (vector<AlgorithmTestResults>::iterator it = test_results.begin();
::iterator it = test_results.begin();
it != test_results.end(); it != test_results.end();
++it) ++it)
it->fullReset(); it->fullReset();
@ -735,10 +752,19 @@ int main(int argc, char* argv[])
if (!e.line_info.empty()) if (!e.line_info.empty())
cerr << ":" << configuration.global_options.cfg_filename << ":" cerr << ":" << configuration.global_options.cfg_filename << ":"
<< e.line_info; << e.line_info;
cerr << ":" << e.what() << endl; cerr << ": " << e.what() << endl;
exit(2); exit(2);
} }
#ifdef HAVE_ISATTY
if (configuration.global_options.formula_input_filename == "-"
&& !isatty(STDIN_FILENO))
{
configuration.global_options.interactive = Configuration::NEVER;
configuration.global_options.handle_breaks = false;
}
#endif /* HAVE_ISATTY */
if (configuration.global_options.verbosity >= 3) if (configuration.global_options.verbosity >= 3)
configuration.print(cout); configuration.print(cout);

15
lbtt/src/translate.cc
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License
@ -25,6 +25,7 @@
#include "LbtWrapper.h" #include "LbtWrapper.h"
#include "LtlFormula.h" #include "LtlFormula.h"
#include "SpinWrapper.h" #include "SpinWrapper.h"
#include "SpotWrapper.h"
#ifdef HAVE_GETOPT_LONG #ifdef HAVE_GETOPT_LONG
#include <getopt.h> #include <getopt.h>
#define OPTIONSTRUCT struct option #define OPTIONSTRUCT struct option
@ -59,7 +60,7 @@ static TranslatorInterface* translator = 0;
/****************************************************************************** /******************************************************************************
* *
* A function for showing warnings to the user. * A function for showing warnings to the user.
* *
*****************************************************************************/ *****************************************************************************/
void printWarning(const string& msg) void printWarning(const string& msg)
@ -119,7 +120,7 @@ static void installSignalHandler(int signum)
int main(int argc, char** argv) int main(int argc, char** argv)
{ {
typedef enum {OPT_HELP = 'h', OPT_LBT, OPT_SPIN, OPT_VERSION = 'V'} typedef enum {OPT_HELP = 'h', OPT_LBT, OPT_SPIN, OPT_SPOT, OPT_VERSION = 'V'}
OptionType; OptionType;
static OPTIONSTRUCT command_line_options[] = static OPTIONSTRUCT command_line_options[] =
@ -127,6 +128,7 @@ int main(int argc, char** argv)
{"help", no_argument, 0, OPT_HELP}, {"help", no_argument, 0, OPT_HELP},
{"lbt", no_argument, 0, OPT_LBT}, {"lbt", no_argument, 0, OPT_LBT},
{"spin", no_argument, 0, OPT_SPIN}, {"spin", no_argument, 0, OPT_SPIN},
{"spot", no_argument, 0, OPT_SPOT},
{"version", no_argument, 0, OPT_VERSION}, {"version", no_argument, 0, OPT_VERSION},
{0, 0, 0, 0} {0, 0, 0, 0}
}; };
@ -154,6 +156,7 @@ int main(int argc, char** argv)
"Translator options:\n" "Translator options:\n"
" --lbt lbt\n" " --lbt lbt\n"
" --spin Spin\n" " --spin Spin\n"
" --spot Spot\n"
"The command line for these translators must be given as a " "The command line for these translators must be given as a "
"single argument\n" "single argument\n"
"including the name (and location) of an external program to " "including the name (and location) of an external program to "
@ -171,6 +174,10 @@ int main(int argc, char** argv)
translator = new SpinWrapper(); translator = new SpinWrapper();
break; break;
case OPT_SPOT :
translator = new SpotWrapper();
break;
case OPT_VERSION : case OPT_VERSION :
cout << "lbtt-translate " PACKAGE_VERSION "\n" cout << "lbtt-translate " PACKAGE_VERSION "\n"
"lbtt-translate is free software; you may change and " "lbtt-translate is free software; you may change and "

4
lbtt/src/translate.h
View file

@ -1,6 +1,6 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License * modify it under the terms of the GNU General Public License