diff --git a/lbtt/AUTHORS b/lbtt/AUTHORS index dfd5d7d33..5fd9b83c0 100644 --- a/lbtt/AUTHORS +++ b/lbtt/AUTHORS @@ -1 +1 @@ -Heikki Tauriainen +Heikki Tauriainen diff --git a/lbtt/ChangeLog b/lbtt/ChangeLog index 1184042b1..3d865a4e8 100644 --- a/lbtt/ChangeLog +++ b/lbtt/ChangeLog @@ -1,3 +1,116 @@ +2005-08-30 Heikki Tauriainen + + * 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 + + * NEWS, README: Update to next version. + + * Version 1.1.3 released. + +2005-08-18 Heikki Tauriainen + + * 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 + + * 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 + + * 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 + + * 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 * Version 1.1.2 released. diff --git a/lbtt/NEWS b/lbtt/NEWS index 5e168d954..1f63955f8 100644 --- a/lbtt/NEWS +++ b/lbtt/NEWS @@ -1,5 +1,5 @@ -lbtt NEWS -- history of user-visible changes. 02 Aug 2004 -Copyright (C) 2004 Heikki Tauriainen +lbtt NEWS -- history of user-visible changes. 30 Aug 2005 +Copyright (C) 2005 Heikki Tauriainen Permission is granted to anyone to make or distribute verbatim copies 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 changed them. -Please send bug reports to . +Please send bug reports to . + +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 ). + + 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 diff --git a/lbtt/README b/lbtt/README index f6e9927b6..3fdb6f194 100644 --- a/lbtt/README +++ b/lbtt/README @@ -1,4 +1,4 @@ -lbtt version 1.1.2 +lbtt version 1.2.0 ------------------ lbtt is a tool for testing programs that translate formulas diff --git a/lbtt/configure.ac b/lbtt/configure.ac index 863b97792..5cc044e60 100644 --- a/lbtt/configure.ac +++ b/lbtt/configure.ac @@ -1,8 +1,8 @@ # Process this file with autoconf to produce a configure script. AC_PREREQ([2.59]) -AC_INIT([lbtt], [1.1.2], [heikki.tauriainen@hut.fi]) -AC_REVISION([Revision: 1.6]) +AC_INIT([lbtt], [1.2.0], [heikki.tauriainen@tkk.fi]) +AC_REVISION([Revision: 1.8]) AC_CONFIG_SRCDIR([src/main.cc]) AC_CONFIG_HEADERS([config.h]) AM_INIT_AUTOMAKE @@ -124,52 +124,6 @@ AC_CHECK_HEADERS( # 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 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 or 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_CHECK_TYPES( @@ -191,7 +145,7 @@ AC_C_INLINE # Checks for library functions. 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_CHECK_FUNCS([strsignal isatty getopt_long]) diff --git a/lbtt/doc/lbtt.texi b/lbtt/doc/lbtt.texi index 1d0064048..06a9fd2f6 100644 --- a/lbtt/doc/lbtt.texi +++ b/lbtt/doc/lbtt.texi @@ -14,13 +14,13 @@ This file documents how to use the LTL-to-B@"uchi translator testbench @command{lbtt}. -Copyright @copyright{} 2004 Heikki Tauriainen +Copyright @copyright{} 2005 Heikki Tauriainen @ifinfo -@email{heikki.tauriainen@@hut.fi} +@email{heikki.tauriainen@@tkk.fi} @end ifinfo @ifnotinfo @ifnothtml -<@email{heikki.tauriainen@@hut.fi}> +<@email{heikki.tauriainen@@tkk.fi}> @end ifnothtml @end ifnotinfo @@ -64,12 +64,12 @@ under the above conditions for modified versions. @title @command{lbtt} @subtitle LTL-to-B@"uchi Translator Testbench -@subtitle @today, @command{lbtt} Versions 1.1.x -@author Heikki Tauriainen <@email{heikki.tauriainen@@hut.fi}> +@subtitle @today, @command{lbtt} Versions 1.2.x +@author Heikki Tauriainen <@email{heikki.tauriainen@@tkk.fi}> @page @vskip 0pt plus 1filll -Copyright @copyright{} 2004 Heikki Tauriainen -<@email{heikki.tauriainen@@hut.fi}> +Copyright @copyright{} 2005 Heikki Tauriainen +<@email{heikki.tauriainen@@tkk.fi}> The latest version of this manual can be obtained from@* <@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 B@"uchi automata. -This is edition 1.1.0 of the @command{lbtt} documentation. This edition -applies to @command{lbtt} versions 1.1.x. +This is edition 1.2.0 of the @command{lbtt} documentation. This edition +applies to @command{lbtt} versions 1.2.x. @command{lbtt} is free software, you may change and redistribute it 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 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 -read LTL formulas from a file +read LTL formulas from a file or from standard input (@pxref{--formulafile,,@samp{--formulafile} command line option}). @cindex state space @@ -899,7 +899,7 @@ See also the web page@* @url{http://www.tcs.hut.fi/Software/lbtt/formulaoptions.php} @end ifinfo @ifnotinfo -<@uref{http://www.tcs.hut.fi/Software/lbtt/formulaoptions.php>} +<@uref{http://www.tcs.hut.fi/Software/lbtt/formulaoptions.php}> @end ifnotinfo for an interface to a small database for adjusting the operator priorities towards certain simple distributions. @@ -2121,12 +2121,13 @@ file @samp{config} in the current working directory. @item @anchor{--formulafile}--formulafile=@var{FILE-NAME} @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} 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 -list of formulas, each on its own line in the file. The formulas can be -specified either in @command{lbtt}'s own prefix notation +from a file (or standard input) instead of generating them randomly. The +special filename @samp{-} refers to standard input. Each +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 messages is supported) or in a variety of formats found in 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 (@pxref{--formulafile,,@samp{--formulafile} option}), which can be used to -instruct @command{lbtt} to read LTL formulas from a file instead of generating -them randomly. +instruct @command{lbtt} to read LTL formulas from a file (or standard input) +instead of generating them randomly. @@ -2665,9 +2666,9 @@ Random state space generation parameters. @item Random LTL formula generation parameters (unless reading LTL formulas from -a file; @pxref{--formulafile,,@samp{--formulafile} command line option}). -This includes information about all enabled formula operators and their -priorities. When using the command line option +an external source; @pxref{--formulafile,,@samp{--formulafile} command line +option}). This includes information about all enabled formula operators and +their priorities. When using the command line option @samp{--showoperatordistribution} (@pxref{--showoperatordistribution,,@samp{--showoperatordistribution} option}), @command{lbtt} shows also the expected number of occurrence of each @@ -4025,6 +4026,25 @@ See <@uref{http://spinroot.com/spin/whatispin.html}> @end ifnotinfo 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 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 @command{lbtt}'s configuration file accordingly to disable the unsupported 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}). 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, 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] K.@: Etessami and G.@: Holzmann. Optimizing B@"uchi automata. In @i{Proceedings of the 11th International Conference on Concurrency Theory diff --git a/lbtt/src/BitArray.cc b/lbtt/src/BitArray.cc index 374e3ba39..3c840c6a1 100644 --- a/lbtt/src/BitArray.cc +++ b/lbtt/src/BitArray.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/BitArray.h b/lbtt/src/BitArray.h index ec725d7fc..68ee05285 100644 --- a/lbtt/src/BitArray.h +++ b/lbtt/src/BitArray.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * 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(bits), 0xFF, (bit_count + 7) >> 3); + unsigned long int bsize = bit_count >> 3; + memset(static_cast(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(bits), 0, (bit_count + 7) >> 3); + unsigned long int bsize = bit_count >> 3; + memset(static_cast(bits), 0, bsize); + if ((bit_count & 0x07) != 0) + bits[bsize] &= ~((1 << (bit_count & 7)) - 1); } /* ========================================================================= */ diff --git a/lbtt/src/Bitset.h b/lbtt/src/Bitset.h index a97c40354..a7536d5ad 100644 --- a/lbtt/src/Bitset.h +++ b/lbtt/src/Bitset.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/BuchiAutomaton.cc b/lbtt/src/BuchiAutomaton.cc index 1b6c6d18e..318c75b67 100644 --- a/lbtt/src/BuchiAutomaton.cc +++ b/lbtt/src/BuchiAutomaton.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * 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)]. */ - map, ALLOC(size_type) > - state_number_map; + map state_number_map; pair state_mapping(0, 0); - pair, ALLOC(size_type) > - ::const_iterator, - bool> - state_finder; + pair::const_iterator, bool> state_finder; /* * Also the acceptance set numbers will be mapped to the interval * [0...(number of acceptance sets - 1)]. */ - map, ALLOC(unsigned long int) > - acceptance_set_map; + map acceptance_set_map; pair acceptance_set_mapping(0, 0); - pair, - ALLOC(unsigned long int) >::const_iterator, - bool> + pair::const_iterator, bool> acceptance_set_finder; /* diff --git a/lbtt/src/BuchiAutomaton.h b/lbtt/src/BuchiAutomaton.h index cec62163c..cfd212323 100644 --- a/lbtt/src/BuchiAutomaton.h +++ b/lbtt/src/BuchiAutomaton.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/BuchiProduct.cc b/lbtt/src/BuchiProduct.cc index c5f5c51d5..d3a6157b6 100644 --- a/lbtt/src/BuchiProduct.cc +++ b/lbtt/src/BuchiProduct.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -28,8 +28,7 @@ namespace Graph * *****************************************************************************/ -map< ::Ltl::LtlFormula*, BuchiProduct::SatisfiabilityMapping, - less< ::Ltl::LtlFormula*>, ALLOC(BuchiProduct::SatisfiabilityMapping) > +map< ::Ltl::LtlFormula*, BuchiProduct::SatisfiabilityMapping> BuchiProduct::sat_cache; @@ -73,8 +72,7 @@ bool BuchiProduct::synchronizable guard_1 = swap_guard; } - map, - ALLOC(SatisfiabilityMapping) >::iterator + map::iterator sat_cache_element = sat_cache.find(guard_1); if (sat_cache_element == sat_cache.end()) diff --git a/lbtt/src/BuchiProduct.h b/lbtt/src/BuchiProduct.h index 43200f521..c431d8d36 100644 --- a/lbtt/src/BuchiProduct.h +++ b/lbtt/src/BuchiProduct.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -142,18 +142,16 @@ private: * automata. */ - typedef map< ::Ltl::LtlFormula*, bool, /* Type definition for */ - less< ::Ltl::LtlFormula*>, /* storing information */ - ALLOC(bool) > /* about the */ - SatisfiabilityMapping; /* satisfiability of the + typedef map< ::Ltl::LtlFormula*, bool> /* Type definition for */ + SatisfiabilityMapping; /* storing information + * about the + * satisfiability of the * guards of product * transitions. */ static map< ::Ltl::LtlFormula*, /* Result cache for */ - SatisfiabilityMapping, /* satisfiability tests. */ - less< ::Ltl::LtlFormula*>, - ALLOC(SatisfiabilityMapping) > + SatisfiabilityMapping> /* satisfiability tests. */ sat_cache; }; diff --git a/lbtt/src/Config-lex.ll b/lbtt/src/Config-lex.ll index 145126a89..ea0af40f9 100644 --- a/lbtt/src/Config-lex.ll +++ b/lbtt/src/Config-lex.ll @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/Config-parse.yy b/lbtt/src/Config-parse.yy index 43e228fcb..b5539afbe 100644 --- a/lbtt/src/Config-parse.yy +++ b/lbtt/src/Config-parse.yy @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/Configuration.cc b/lbtt/src/Configuration.cc index 9061e3a1d..0dd3e99be 100644 --- a/lbtt/src/Configuration.cc +++ b/lbtt/src/Configuration.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -96,8 +96,7 @@ Configuration::~Configuration() * * ------------------------------------------------------------------------- */ { - for (vector - ::const_iterator it = algorithms.begin(); + for (vector::const_iterator it = algorithms.begin(); it != algorithms.end(); ++it) { for (vector::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; typedef pair Parameter; - vector parameters; + vector parameters; /* * Preprocess the command line parameters. At this point only those special @@ -351,7 +350,7 @@ void Configuration::read(int argc, char* argv[]) * configuration file. */ - vector::const_iterator parameter; + vector::const_iterator parameter; try { @@ -655,7 +654,7 @@ void Configuration::read(int argc, char* argv[]) try { IntervalList algorithm_ids; - vector nonnumeric_algorithm_ids; + vector nonnumeric_algorithm_ids; string id_string = substituteInQuotedString(parameter->second, ",", "\n", INSIDE_QUOTES); @@ -664,14 +663,13 @@ void Configuration::read(int argc, char* argv[]) algorithms.size() - 1, &nonnumeric_algorithm_ids); - for (vector::iterator + for (vector::iterator id = nonnumeric_algorithm_ids.begin(); id != nonnumeric_algorithm_ids.end(); ++id) { *id = unquoteString(substituteInQuotedString(*id, "\n", ",")); - map, - ALLOC(unsigned long int) >::const_iterator id_finder + map::const_iterator id_finder = algorithm_names.find(*id); if (id_finder == algorithm_names.end()) throw ConfigurationException @@ -777,8 +775,7 @@ void Configuration::read(int argc, char* argv[]) bool unary_operator_allowed = false; - for (map, ALLOC(int) >::iterator - it = formula_options.symbol_priority.begin(); + for (map::iterator it = formula_options.symbol_priority.begin(); it != formula_options.symbol_priority.end(); ++it) { if (it->second == -1) @@ -804,7 +801,7 @@ void Configuration::read(int argc, char* argv[]) int total_long_unary_priority = 0; int total_binary_priority = 0; - for (map, ALLOC(int) >::const_iterator + for (map::const_iterator it = formula_options.symbol_priority.begin(); 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++) { - for (map, ALLOC(int) >::const_iterator + for (map::const_iterator op = formula_options.symbol_priority.begin(); op != formula_options.symbol_priority.end(); ++op) @@ -984,11 +981,9 @@ void Configuration::print(ostream& stream, int indent) const estream << '\n' + string(indent + 2, ' ') + "Implementations:\n"; - vector::size_type - algorithm_number = 0; + vector::size_type algorithm_number = 0; - for (vector - ::const_iterator a = algorithms.begin(); + for (vector::const_iterator a = algorithms.begin(); a != algorithms.end(); ++a) { @@ -1161,9 +1156,13 @@ void Configuration::print(ostream& stream, int indent) const number_of_available_variables == 1 ? "" : "s"); } 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, ' '); @@ -1222,7 +1221,7 @@ void Configuration::print(ostream& stream, int indent) const bool first_printed = false; - for (map, ALLOC(int) >::const_iterator + for (map::const_iterator op = formula_options.symbol_priority.begin(); op != formula_options.symbol_priority.end(); ++op) @@ -1263,7 +1262,7 @@ void Configuration::print(ostream& stream, int indent) const int max_operators_per_line = (formula_options.symbol_distribution.empty() ? 7 : 6); - for (map, ALLOC(int) >::const_iterator op + for (map::const_iterator op = formula_options.symbol_priority.begin(); op != formula_options.symbol_priority.end(); ++op) @@ -1340,9 +1339,7 @@ void Configuration::print(ostream& stream, int indent) const /* ========================================================================= */ string Configuration::algorithmString - (vector::size_type - algorithm_id) const + (vector::size_type algorithm_id) const /* ---------------------------------------------------------------------------- * * 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" " Include implementation(s) into " "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 " "tests\n" " (equivalent to " @@ -1543,7 +1541,7 @@ void Configuration::showCommandLineHelp(const char* program_name) " --truthprobability=PROBABILITY\n" " Set truth probability of " "propositions (0.0--1.0)\n\n" - "Report bugs to .\n"; + "Report bugs to <" PACKAGE_BUGREPORT ">.\n"; } /* ========================================================================= */ @@ -1673,7 +1671,7 @@ void Configuration::registerAlgorithm : string("")), error); - vector params; + vector params; sliceString(unquoteString(substituteInQuotedString(parameters, " \t", "\n\n", OUTSIDE_QUOTES)), "\n", @@ -1702,7 +1700,7 @@ void Configuration::registerAlgorithm memcpy(static_cast(algorithm_information.parameters[0]), static_cast(path.c_str()), path.size() + 1); - for (vector::size_type p = 0; + for (vector::size_type p = 0; p < algorithm_information.num_parameters; ++p) { @@ -1875,9 +1873,9 @@ void Configuration::readInteractivity(const string& value) global_options.interactive = NEVER; global_options.handle_breaks = false; - vector modes; + vector modes; ::StringUtil::sliceString(value, ",", modes); - for (vector::const_iterator mode = modes.begin(); + for (vector::const_iterator mode = modes.begin(); mode != modes.end(); ++mode) { diff --git a/lbtt/src/Configuration.h b/lbtt/src/Configuration.h index 8d491eb8f..e7d9a1b56 100644 --- a/lbtt/src/Configuration.h +++ b/lbtt/src/Configuration.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -62,9 +62,9 @@ public: struct AlgorithmInformation; /* See below. */ string algorithmString /* Formats the the id */ - (vector::size_type/* the name of the */ - algorithm_id) const; /* algorithm into a + (vector::size_type /* of an algorithm and */ + algorithm_id) const; /* the name of the + * algorithm into a * string. */ @@ -311,11 +311,12 @@ public: * LTL formula symbols. */ - map, ALLOC(int) > /* Priorities for LTL */ - symbol_priority; /* formula symbols. */ + map symbol_priority; /* Priorities for LTL + * formula symbols. + */ - map, ALLOC(double) > /* Expected numbers of */ - symbol_distribution; /* occurrence for the + map symbol_distribution; /* Expected numbers of + * occurrence for the * different formula * operators. */ @@ -375,15 +376,15 @@ public: /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ - vector algorithms; /* information about the + vector algorithms; /* A vector containing + * information about the * algorithms used in * the tests. */ - map, /* Mapping between */ - ALLOC(unsigned long int) > /* algorithm names and */ - algorithm_names; /* their numeric + map algorithm_names; /* Mapping between + * algorithm names and + * their numeric * identifiers. */ @@ -511,14 +512,13 @@ private: OPT_STATESPACEPROPOSITIONS, OPT_STATESPACESIZE, OPT_TRUTHPROBABILITY}; - typedef map, double, /* Type definitions for */ - less >, /* the result cache used */ - ALLOC(double) > /* for computing the */ - ProbabilityMapElement; /* probability */ - typedef map, /* formula operators. */ - ALLOC(ProbabilityMapElement) > - ProbabilityMap; + typedef map, double> /* Type definitions for */ + ProbabilityMapElement; /* the result cache used */ + /* for computing the */ + typedef map /* probability */ + ProbabilityMap; /* distribution of LTL + * formula operators. + */ /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ diff --git a/lbtt/src/DispUtil.cc b/lbtt/src/DispUtil.cc index 4bfa825e8..39f0b767f 100644 --- a/lbtt/src/DispUtil.cc +++ b/lbtt/src/DispUtil.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -32,10 +32,10 @@ namespace DispUtil { -stack > /* output stream. */ - stream_formatting_stack; +stack > /* Stack for storing the */ + stream_formatting_stack; /* previous states of an + * output stream. + */ /* ========================================================================= */ void changeStreamFormatting diff --git a/lbtt/src/DispUtil.h b/lbtt/src/DispUtil.h index a7a8bc2f5..6f42e97d1 100644 --- a/lbtt/src/DispUtil.h +++ b/lbtt/src/DispUtil.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/EdgeContainer.h b/lbtt/src/EdgeContainer.h index 2ebbc089f..954eb8a36 100644 --- a/lbtt/src/EdgeContainer.h +++ b/lbtt/src/EdgeContainer.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/Exception.h b/lbtt/src/Exception.h index e6a88d98b..3ab2f3987 100644 --- a/lbtt/src/Exception.h +++ b/lbtt/src/Exception.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/ExternalTranslator.cc b/lbtt/src/ExternalTranslator.cc index 5f8da60ad..60cd80b9b 100644 --- a/lbtt/src/ExternalTranslator.cc +++ b/lbtt/src/ExternalTranslator.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/ExternalTranslator.h b/lbtt/src/ExternalTranslator.h index 12171674b..758ea67fe 100644 --- a/lbtt/src/ExternalTranslator.h +++ b/lbtt/src/ExternalTranslator.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -174,12 +174,13 @@ private: * objects. */ - stack > /* information. */ - temporary_file_objects; + stack > /* Stack for storing */ + temporary_file_objects; /* temporary file + * information. + */ friend class SpinWrapper; /* Friend declarations. */ + friend class SpotWrapper; /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ diff --git a/lbtt/src/FormulaRandomizer.cc b/lbtt/src/FormulaRandomizer.cc index 712e269c1..964360c1b 100644 --- a/lbtt/src/FormulaRandomizer.cc +++ b/lbtt/src/FormulaRandomizer.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -92,7 +92,7 @@ LtlFormula* FormulaRandomizer::recGenerate(unsigned long int target_size) * * ------------------------------------------------------------------------- */ { - vector::const_iterator symbol_priority; + vector::const_iterator symbol_priority; LtlFormula* formula; long int x; diff --git a/lbtt/src/FormulaRandomizer.h b/lbtt/src/FormulaRandomizer.h index cf40472db..915625e58 100644 --- a/lbtt/src/FormulaRandomizer.h +++ b/lbtt/src/FormulaRandomizer.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -87,16 +87,16 @@ public: * `reset'. */ - const map, /* different atomic */ - ALLOC(unsigned long int) >& /* propositions */ - propositionStatistics() const; /* generated since the + const map& /* Get the numbers of */ + propositionStatistics() const; /* different atomic + * propositions + * generated since the * last call to `reset'. */ - const map, /* Get the numbers of */ - ALLOC(unsigned long int) >& /* different symbols */ - symbolStatistics() const; /* generated since the + const map& /* Get the numbers of */ + symbolStatistics() const; /* different symbols + * generated since the * last call to `reset'. */ @@ -124,21 +124,20 @@ private: typedef pair IntegerPair; - vector /* Operand symbols and */ + vector /* Operand symbols and */ propositional_symbol_priorities; /* their priorities in * random formulae. */ - vector /* Operators and their */ - short_formula_operators; /* priorities in random - * formulae of size - * two. + vector short_formula_operators; /* Operators and their + * priorities in random + * formulae of size two. */ - vector /* Operators and their */ - long_formula_operators; /* priorities in random - * formulae of size - * greater than two. + vector long_formula_operators; /* Operators and their + * priorities in random + * formulae of size greater + * than two. */ unsigned long int number_of_generated_formulas; /* Number of generated @@ -146,14 +145,15 @@ private: * last call to `reset'. */ - map, /* atomic propositions */ - ALLOC(unsigned long int) > /* generated since the */ - proposition_statistics; /* last call to `reset' */ + map /* Number of different */ + proposition_statistics; /* atomic propositions + * generated since the + * last call to `reset' + */ - map, /* Number of different */ - ALLOC(unsigned long int) > /* formula symbols */ - symbol_statistics; /* generated since the + map symbol_statistics; /* Number of different + * formula symbols + * generated since the * last call to `reset'. */ }; @@ -289,8 +289,7 @@ inline unsigned long int FormulaRandomizer::numberOfFormulas() const } /* ========================================================================= */ -inline const map, - ALLOC(unsigned long int) >& +inline const map& FormulaRandomizer::propositionStatistics() const /* ---------------------------------------------------------------------------- * @@ -308,7 +307,7 @@ FormulaRandomizer::propositionStatistics() const } /* ========================================================================= */ -inline const map, ALLOC(unsigned long int) >& +inline const map& FormulaRandomizer::symbolStatistics() const /* ---------------------------------------------------------------------------- * diff --git a/lbtt/src/FormulaWriter.h b/lbtt/src/FormulaWriter.h index 34b3c2c8b..feaf2121a 100644 --- a/lbtt/src/FormulaWriter.h +++ b/lbtt/src/FormulaWriter.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/Graph.h.in b/lbtt/src/Graph.h.in index 9b7c4a6b7..ec484f01f 100644 --- a/lbtt/src/Graph.h.in +++ b/lbtt/src/Graph.h.in @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -193,16 +193,16 @@ public: /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ protected: - vector nodes; /* Nodes of the graph. + vector nodes; /* Nodes of the graph. * Derived classes can * access this vector * directly. */ public: - typedef typename /* Type definition for */ - vector::size_type /* the size of the */ - size_type; /* graph. The size can + typedef typename vector::size_type /* Type definition for */ + size_type; /* the size of the + * graph. The size can * be no greater than * the maximum size of * the vector containing @@ -214,8 +214,9 @@ public: * edges. */ - typedef deque /* Type definition for */ - Path; /* paths in a graph. */ + typedef deque Path; /* Type definition for + * paths in a graph. + */ typedef pair StateIdPair; /* Type definition for a * pair of state @@ -502,8 +503,7 @@ public: * *****************************************************************************/ -class EdgeList : public list::Edge*, - ALLOC(Graph::Edge*) > +class EdgeList : public list::Edge*> { public: EdgeList(); /* Constructor. */ @@ -518,14 +518,12 @@ public: * the end of the list. */ - list::Edge*, /* Functions for finding */ - ALLOC(Graph::Edge*) > /* an element in the */ - ::const_iterator /* list. */ - find(const Graph::Edge* edge) const; - - list::Edge*, - ALLOC(Graph::Edge*) > - ::iterator + list::Edge*>::const_iterator /* Functions for finding */ + find(const Graph::Edge* edge) const; /* an element in the + * list. + */ + + list::Edge*>::iterator find(const Graph::Edge* edge); }; @@ -540,8 +538,7 @@ public: #ifdef HAVE_SLIST -class EdgeSlist : public slist::Edge*, - ALLOC(Graph::Edge*) > +class EdgeSlist : public slist::Edge*> { public: EdgeSlist(); /* Constructor. */ @@ -557,14 +554,12 @@ public: * list. */ - slist::Edge*, /* Functions for finding */ - ALLOC(Graph::Edge*) > /* an element in the */ - ::const_iterator /* list. */ - find(const Graph::Edge* edge) const; + slist::Edge*>::const_iterator /* Functions for finding */ + find(const Graph::Edge* edge) const; /* an element in the + * list. + */ - slist::Edge*, - ALLOC(Graph::Edge*) > - ::iterator + slist::Edge*>::iterator find(const Graph::Edge* edge); }; @@ -578,8 +573,7 @@ public: * *****************************************************************************/ -class EdgeVector : public vector::Edge*, - ALLOC(Graph::Edge*) > +class EdgeVector : public vector::Edge*> { public: EdgeVector(); /* Constructor. */ @@ -595,15 +589,11 @@ public: * to edges. */ - vector::Edge*, /* Functions for finding */ - ALLOC(Graph::Edge*) > /* an element in the */ - ::const_iterator /* container. */ - find(const Graph::Edge* edge) - const; + vector::Edge*>::const_iterator /* Functions for finding */ + find(const Graph::Edge* edge) /* an element in the */ + const; /* container. */ - vector::Edge*, - ALLOC(Graph::Edge*) > - ::iterator + vector::Edge*>::iterator find(const Graph::Edge* edge); }; @@ -616,8 +606,7 @@ public: *****************************************************************************/ class EdgeSet : public set::Edge*, - Graph::Edge::ptr_less, - ALLOC(Graph::Edge*) > + Graph::Edge::ptr_less> { }; @@ -630,8 +619,7 @@ class EdgeSet : public set::Edge*, *****************************************************************************/ class EdgeMultiSet : public multiset::Edge*, - Graph::Edge::ptr_less, - ALLOC(Graph::Edge*) > + Graph::Edge::ptr_less> { }; @@ -757,7 +745,7 @@ Graph::Graph(const size_type initial_number_of_nodes) : { nodes.reserve(initial_number_of_nodes); - for (typename vector::iterator node = nodes.begin(); + for (typename vector::iterator node = nodes.begin(); node != nodes.end(); ++node) *node = new Node(); @@ -779,8 +767,7 @@ Graph::Graph(const Graph& graph) * ------------------------------------------------------------------------- */ { nodes.reserve(graph.nodes.size()); - for (typename vector::const_iterator - node = graph.nodes.begin(); + for (typename vector::const_iterator node = graph.nodes.begin(); node != graph.nodes.end(); ++node) nodes.push_back(new Node(**node)); } @@ -806,8 +793,7 @@ Graph& Graph::operator= clear(); nodes.reserve(graph.nodes.size()); - for (typename vector::const_iterator - node = graph.nodes.begin(); + for (typename vector::const_iterator node = graph.nodes.begin(); node != graph.nodes.end(); ++node) nodes.push_back(new Node(**node)); @@ -850,8 +836,7 @@ void Graph::clear() * * ------------------------------------------------------------------------- */ { - for (typename vector::reverse_iterator - node = nodes.rbegin(); + for (typename vector::reverse_iterator node = nodes.rbegin(); node != nodes.rend(); ++node) delete *node; @@ -997,8 +982,7 @@ Graph::stats() const result.first = nodes.size(); result.second = 0; - for (typename vector::const_iterator - node = nodes.begin(); + for (typename vector::const_iterator node = nodes.begin(); node != nodes.end(); ++node) result.second += (*node)->edges().size(); @@ -1032,7 +1016,7 @@ Graph::subgraphStats(const size_type index) const if (index >= s) throw NodeIndexException(); - stack > unprocessed_nodes; + stack > unprocessed_nodes; BitArray visited_nodes(s); visited_nodes.clear(s); @@ -1764,8 +1748,7 @@ inline void EdgeList::insert(Graph::Edge* edge) } /* ========================================================================= */ -inline list::Edge*, ALLOC(Graph::Edge*) > - ::const_iterator +inline list::Edge*>::const_iterator EdgeList::find(const Graph::Edge* edge) const /* ---------------------------------------------------------------------------- * @@ -1776,9 +1759,9 @@ EdgeList::find(const Graph::Edge* edge) const * between the actual values of the edges (not the * pointers). * - * Returns: A list::Edge*, ALLOC>::const_iterator + * Returns: A list::Edge*>::const_iterator * pointing to the edge in the list or - * list::Edge*, ALLOC>::end() if the edge is + * list::Edge*>::end() if the edge is * not found in the list. * * ------------------------------------------------------------------------- */ @@ -1793,7 +1776,7 @@ EdgeList::find(const Graph::Edge* edge) const } /* ========================================================================= */ -inline list::Edge*, ALLOC(Graph::Edge*) >::iterator +inline list::Edge*>::iterator EdgeList::find(const Graph::Edge* edge) /* ---------------------------------------------------------------------------- * @@ -1804,9 +1787,9 @@ EdgeList::find(const Graph::Edge* edge) * between the actual values of the edges (not the * pointers). * - * Returns: A list::Edge*, ALLOC>::iterator pointing + * Returns: A list::Edge*>::iterator pointing * to the edge in the list or - * list::Edge*, ALLOC>::end() if the edge is + * list::Edge*>::end() if the edge is * not found in the list. * * ------------------------------------------------------------------------- */ @@ -1875,8 +1858,7 @@ inline void EdgeSlist::insert(Graph::Edge* edge) } /* ========================================================================= */ -inline slist::Edge*, ALLOC(Graph::Edge*) > - ::const_iterator +inline slist::Edge*>::const_iterator EdgeSlist::find(const Graph::Edge* edge) const /* ---------------------------------------------------------------------------- * @@ -1887,9 +1869,9 @@ EdgeSlist::find(const Graph::Edge* edge) const * between the actual values of the edges (not the * pointers). * - * Returns: A slist::Edge*, ALLOC>::const_iterator + * Returns: A slist::Edge*>::const_iterator * pointing to the edge in the list or - * slist::Edge*, ALLOC>::end() if the edge + * slist::Edge*>::end() if the edge * is not found in the list. * * ------------------------------------------------------------------------- */ @@ -1904,8 +1886,7 @@ EdgeSlist::find(const Graph::Edge* edge) const } /* ========================================================================= */ -inline slist::Edge*, ALLOC(Graph::Edge*) > - ::iterator +inline slist::Edge*>::iterator EdgeSlist::find(const Graph::Edge* edge) /* ---------------------------------------------------------------------------- * @@ -1916,9 +1897,9 @@ EdgeSlist::find(const Graph::Edge* edge) * between the actual values of the edges (not the * pointers). * - * Returns: A slist::Edge*, ALLOC>::iterator + * Returns: A slist::Edge*>::iterator * pointing to the edge in the list or - * slist::Edge*, ALLOC>::end() if the edge + * slist::Edge*>::end() if the edge * is not found in the list. * * ------------------------------------------------------------------------- */ @@ -1987,8 +1968,7 @@ inline void EdgeVector::insert(Graph::Edge* edge) } /* ========================================================================= */ -inline vector::Edge*, ALLOC(Graph::Edge*) > - ::const_iterator +inline vector::Edge*>::const_iterator EdgeVector::find(const Graph::Edge* edge) const /* ---------------------------------------------------------------------------- * @@ -1999,9 +1979,9 @@ EdgeVector::find(const Graph::Edge* edge) const * between the actual values of the edges (not the * pointers). * - * Returns: A vector::Edge*, ALLOC>::const_iterator + * Returns: A vector::Edge*>::const_iterator * pointing to the edge in the container or - * vector::Edge*, ALLOC>::end() if the + * vector::Edge*>::end() if the * edge is not found in the container. * * ------------------------------------------------------------------------- */ @@ -2016,8 +1996,7 @@ EdgeVector::find(const Graph::Edge* edge) const } /* ========================================================================= */ -inline vector::Edge*, ALLOC(Graph::Edge*) > - ::iterator +inline vector::Edge*>::iterator EdgeVector::find(const Graph::Edge* edge) /* ---------------------------------------------------------------------------- * @@ -2028,9 +2007,9 @@ EdgeVector::find(const Graph::Edge* edge) * between the actual values of the edges (not the * pointers). * - * Returns: A vector::Edge*, ALLOC>::iterator + * Returns: A vector::Edge*>::iterator * pointing to the edge in the container or - * vector::Edge*, ALLOC>::end() if the edge + * vector::Edge*>::end() if the edge * is not found in the container. * * ------------------------------------------------------------------------- */ diff --git a/lbtt/src/IntervalList.cc b/lbtt/src/IntervalList.cc index 52a5ebb35..d35c9b66e 100644 --- a/lbtt/src/IntervalList.cc +++ b/lbtt/src/IntervalList.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 2004 - * Heikki Tauriainen + * Copyright (C) 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * 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) return; - list::iterator interval; + list::iterator interval; for (interval = intervals.begin(); interval != intervals.end() && interval->second + 1 < min; ++interval) @@ -68,14 +68,14 @@ void IntervalList::merge(unsigned long int min, unsigned long int max) if (interval->second < max) { interval->second = max; - list::iterator interval2 = interval; + list::iterator interval2 = interval; ++interval2; while (interval2 != intervals.end() && interval2->first <= interval->second + 1) { if (interval->second < interval2->second) interval->second = interval2->second; - list::iterator interval_to_erase = interval2; + list::iterator interval_to_erase = interval2; ++interval2; intervals.erase(interval_to_erase); } @@ -97,7 +97,7 @@ void IntervalList::remove(unsigned long int min, unsigned long int max) if (min > max) return; - list::iterator interval; + list::iterator interval; for (interval = intervals.begin(); interval != intervals.end() && interval->second < min; ++interval) @@ -126,7 +126,7 @@ void IntervalList::remove(unsigned long int min, unsigned long int max) } else /* min <= imin <= imax <= max */ { - list::iterator interval_to_erase = interval; + list::iterator interval_to_erase = interval; ++interval; intervals.erase(interval_to_erase); } @@ -148,7 +148,7 @@ bool IntervalList::covers(unsigned long int min, unsigned long int max) const if (min > max) return true; /* empty interval is always covered */ - list::const_iterator interval; + list::const_iterator interval; for (interval = intervals.begin(); interval != intervals.end() && min > interval->second; ++interval) @@ -173,8 +173,7 @@ string IntervalList::toString() const * ------------------------------------------------------------------------- */ { string s; - for (list::const_iterator - interval = intervals.begin(); + for (list::const_iterator interval = intervals.begin(); interval != intervals.end(); ++interval) { diff --git a/lbtt/src/IntervalList.h b/lbtt/src/IntervalList.h index 2a55b9641..b8276bf34 100644 --- a/lbtt/src/IntervalList.h +++ b/lbtt/src/IntervalList.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 2004 - * Heikki Tauriainen + * Copyright (C) 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -74,13 +74,15 @@ public: unsigned long int operator++(int); /* Postfix increment. */ private: - const list* /* The interval list */ - interval_list; /* associated with the */ - /* iterator. */ + const list* interval_list; /* The interval list + * associated with the + * iterator. + */ - list /* An iterator pointing */ - ::const_iterator interval; /* at the current */ - /* interval list. */ + list::const_iterator interval; /* An iterator pointing at + * the current intrerval + * list. + */ unsigned long int element; /* Element currently * pointed to by the @@ -143,8 +145,7 @@ public: * iterators. */ - typedef list /* Size type. */ - ::size_type size_type; + typedef list::size_type size_type; /* Size type. */ size_type size() const; /* Tell the number of * disjoint intervals in @@ -170,7 +171,7 @@ public: */ private: - list intervals; /* List of intervals. */ + list intervals; /* List of intervals. */ friend class const_iterator; }; diff --git a/lbtt/src/LbtWrapper.h b/lbtt/src/LbtWrapper.h index 03a2d8a80..bd889b18d 100644 --- a/lbtt/src/LbtWrapper.h +++ b/lbtt/src/LbtWrapper.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/LbttAlloc.h b/lbtt/src/LbttAlloc.h index 2f8ef8cc3..c98ceaa07 100644 --- a/lbtt/src/LbttAlloc.h +++ b/lbtt/src/LbttAlloc.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -22,8 +22,6 @@ #include -#define ALLOC(typename) allocator - #ifdef HAVE_OBSTACK_H /* GNU libc 2.3.2's copy of obstack.h uses a definition of __INT_TO_PTR diff --git a/lbtt/src/Ltl-parse.yy b/lbtt/src/Ltl-parse.yy index d558db0b7..805d5965b 100644 --- a/lbtt/src/Ltl-parse.yy +++ b/lbtt/src/Ltl-parse.yy @@ -1,6 +1,6 @@ /* - * Copyright (C) 2004 - * Heikki Tauriainen + * Copyright (C) 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -44,9 +44,9 @@ static LtlFormula* result; /* This variable stores the * ltl_parse. */ -static std::set, /* Intermediate results. */ - ALLOC(LtlFormula*) > /* (This set is used */ - intermediate_results; /* for keeping track of +static std::set intermediate_results; /* Intermediate results. + * (This set is used + * for keeping track of * the subformulas of a * partially constructed * formula in case the @@ -426,8 +426,8 @@ LtlFormula* parseFormula(istream& stream) } catch (...) { - for (std::set, ALLOC(LtlFormula*) > - ::const_iterator f = intermediate_results.begin(); + for (std::set::const_iterator + f = intermediate_results.begin(); f != intermediate_results.end(); ++f) LtlFormula::destruct(*f); diff --git a/lbtt/src/LtlFormula.cc b/lbtt/src/LtlFormula.cc index 2fa3d4723..faad76f56 100644 --- a/lbtt/src/LtlFormula.cc +++ b/lbtt/src/LtlFormula.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -24,9 +24,8 @@ namespace Ltl { -set /* LTL formulae. */ - LtlFormula::formula_storage; +set /* Shared storage for */ + LtlFormula::formula_storage; /* LTL formulae. */ unsigned long int /* Upper limit for the */ LtlFormula::eval_proposition_id_limit; /* atomic proposition @@ -140,12 +139,10 @@ public: */ private: - stack > + stack > formula_stack; - stack > - negation_stack; + stack > negation_stack; NnfConverter(const NnfConverter&); /* Prevent copying and */ NnfConverter& operator=(const NnfConverter&); /* assignment of @@ -196,8 +193,7 @@ class SubformulaCollector public: SubformulaCollector /* Constructor. */ (stack >& + deque >& result_stack); ~SubformulaCollector(); /* Destructor. */ @@ -209,8 +205,7 @@ public: private: stack >& + deque >& subformula_stack; SubformulaCollector(const SubformulaCollector&); /* Prevent copying and */ @@ -382,9 +377,7 @@ inline void FormulaSizeCounter::operator()(const LtlFormula*, int) /* ========================================================================= */ inline SubformulaCollector::SubformulaCollector - (stack >& - result_stack) : + (stack >& result_stack) : subformula_stack(result_stack) /* ---------------------------------------------------------------------------- * @@ -766,9 +759,7 @@ unsigned long int LtlFormula::size() const /* ========================================================================= */ void LtlFormula::collectSubformulae - (stack >& - result_stack) const + (stack >& result_stack) const /* ---------------------------------------------------------------------------- * * Description: Collects the subformulae of a LtlFormula into a stack. After diff --git a/lbtt/src/LtlFormula.h b/lbtt/src/LtlFormula.h index a9209be7c..a53303ba7 100644 --- a/lbtt/src/LtlFormula.h +++ b/lbtt/src/LtlFormula.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -261,21 +261,18 @@ private: void collectSubformulae /* Builds a stack of the */ (stack >& + deque >& /* formula. */ result_stack) const; typedef pair /* Shorthand type */ FormulaStackElement; /* definitions for the */ typedef stack >/* checking algorithm. */ - FormulaStack; + deque > /* satisfiability */ + FormulaStack; /* checking algorithm. */ typedef pair TableauStackElement; typedef stack > + deque > TableauStack; bool sat_eval /* Helper function for */ @@ -285,9 +282,8 @@ private: * formula. */ - static set /* LTL formulae. */ - formula_storage; + static set /* Shared storage for */ + formula_storage; /* LTL formulae. */ static unsigned long int /* Upper limit for the */ eval_proposition_id_limit; /* atomic proposition @@ -1314,8 +1310,7 @@ inline LtlFormula& LtlFormula::insertToStorage(LtlFormula* f) * * ------------------------------------------------------------------------- */ { - set::iterator inserter - = formula_storage.find(f); + set::iterator inserter = formula_storage.find(f); if (inserter != formula_storage.end()) { delete f; diff --git a/lbtt/src/Makefile.am b/lbtt/src/Makefile.am index 6ca8f0e46..bc244ba83 100644 --- a/lbtt/src/Makefile.am +++ b/lbtt/src/Makefile.am @@ -79,6 +79,8 @@ lbtt_translate_SOURCES = \ NeverClaimAutomaton.cc \ SpinWrapper.h \ SpinWrapper.cc \ + SpotWrapper.h \ + SpotWrapper.cc \ StringUtil.h \ StringUtil.cc \ TempFsysName.h \ diff --git a/lbtt/src/NeverClaim-lex.ll b/lbtt/src/NeverClaim-lex.ll index e59a56ea6..54f8d3cb9 100644 --- a/lbtt/src/NeverClaim-lex.ll +++ b/lbtt/src/NeverClaim-lex.ll @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/NeverClaim-parse.yy b/lbtt/src/NeverClaim-parse.yy index 3fd0e54df..bdbdfb4da 100644 --- a/lbtt/src/NeverClaim-parse.yy +++ b/lbtt/src/NeverClaim-parse.yy @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/NeverClaimAutomaton.cc b/lbtt/src/NeverClaimAutomaton.cc index 57494c7c5..122f389b7 100644 --- a/lbtt/src/NeverClaimAutomaton.cc +++ b/lbtt/src/NeverClaimAutomaton.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -62,8 +62,7 @@ void NeverClaimAutomaton::clear() * * ------------------------------------------------------------------------- */ { - for (vector::iterator - state = state_list.begin(); + for (vector::iterator state = state_list.begin(); state != state_list.end(); ++state) delete (*state); @@ -154,8 +153,7 @@ void NeverClaimAutomaton::write(const char* output_filename) * `-1'. */ - for (vector::const_iterator - state = state_list.begin(); + for (vector::const_iterator state = state_list.begin(); state != state_list.end(); ++state) { @@ -163,7 +161,7 @@ void NeverClaimAutomaton::write(const char* output_filename) + ((*state)->initial() ? "1" : "0") + ' ' + ((*state)->accepting() ? "0 " : "") + "-1\n"; - for (multimap, ALLOC(Cstr*) >::const_iterator + for (multimap::const_iterator transition = (*state)->transitions().begin(); transition != (*state)->transitions().end(); ++transition) { @@ -268,7 +266,7 @@ NeverClaimAutomaton::StateInfo::~StateInfo() * * ------------------------------------------------------------------------- */ { - for (multimap, ALLOC(Cstr*) >::const_iterator + for (multimap::const_iterator transition = state_transitions.begin(); transition != state_transitions.end(); ++transition) diff --git a/lbtt/src/NeverClaimAutomaton.h b/lbtt/src/NeverClaimAutomaton.h index 0ab31b905..49cf37324 100644 --- a/lbtt/src/NeverClaimAutomaton.h +++ b/lbtt/src/NeverClaimAutomaton.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -93,12 +93,13 @@ public: */ private: - vector /* States of the */ - state_list; /* automaton. */ + vector state_list; /* States of the automaton. + */ - map, /* Mapping from state */ - ALLOC(StateInfo*) > /* labels to the states */ - label_mapping; /* itself. */ + map label_mapping; /* Mapping from state + * labels to the states + * itself. + */ StateInfo* current_state; /* Pointer to the state * introduced most recently @@ -142,9 +143,9 @@ public: /* of the state. */ - const multimap, /* Returns the labels of */ - ALLOC(Cstr*) >& /* the state's successor */ - transitions() const; /* states, including the + const multimap& transitions() const; /* Returns the labels of + * the state's successor + * states, including the * conditions controlling * the enabledness of the * transition. @@ -174,8 +175,8 @@ private: * accepting state? */ - multimap, ALLOC(Cstr*) > /* Labels of the state's */ - state_transitions; /* successors, including + multimap state_transitions; /* Labels of the state's + * successors, including * the guard formulae * controlling the * enabledness of the @@ -373,9 +374,7 @@ inline bool& NeverClaimAutomaton::StateInfo::accepting() } /* ========================================================================= */ -inline const multimap, - ALLOC(NeverClaimAutomaton::Cstr*) >& +inline const multimap& NeverClaimAutomaton::StateInfo::transitions() const /* ---------------------------------------------------------------------------- * diff --git a/lbtt/src/PathEvaluator.cc b/lbtt/src/PathEvaluator.cc index 936d1ff98..7737ae251 100644 --- a/lbtt/src/PathEvaluator.cc +++ b/lbtt/src/PathEvaluator.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -49,9 +49,8 @@ void PathEvaluator::reset() current_loop_state = 0; path_states.clear(); - for (map::iterator it - = eval_info.begin(); + for (map::iterator + it = eval_info.begin(); it != eval_info.end(); ++it) delete it->second; @@ -131,8 +130,7 @@ bool PathEvaluator::evaluate current_formula = &formula; current_path = &statespace; - map, ALLOC(StateSpace::size_type) > ordering; + map ordering; StateSpace::size_type state = statespace.initialState(); StateSpace::size_type state_count = 0; @@ -176,9 +174,7 @@ bool PathEvaluator::eval() * * ------------------------------------------------------------------------- */ { - stack > - subformula_stack; + stack > subformula_stack; const LtlFormula* f; BitArray* val; diff --git a/lbtt/src/PathEvaluator.h b/lbtt/src/PathEvaluator.h index 794e7ea59..4d361d8f8 100644 --- a/lbtt/src/PathEvaluator.h +++ b/lbtt/src/PathEvaluator.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -105,15 +105,15 @@ private: * the current path. */ - vector /* between states of the */ - path_states; /* path and the states + vector path_states; /* Correspondence + * between states of the + * path and the states * of the current state * space. */ map /* truth values of the */ + LtlFormula::ptr_less> /* truth values of the */ eval_info; /* subformulae of the * formula to be * evaluated. diff --git a/lbtt/src/PathIterator.cc b/lbtt/src/PathIterator.cc index 81c939512..6489b7b1b 100644 --- a/lbtt/src/PathIterator.cc +++ b/lbtt/src/PathIterator.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/PathIterator.h b/lbtt/src/PathIterator.h index e194c60f2..28e02a2f5 100644 --- a/lbtt/src/PathIterator.h +++ b/lbtt/src/PathIterator.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/Product.h b/lbtt/src/Product.h index 9a856cadf..041ff5d36 100644 --- a/lbtt/src/Product.h +++ b/lbtt/src/Product.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -393,8 +393,8 @@ public: typedef ProductEdgeCollection EdgeContainerType; /* required for making */ /* Product */ struct PathElement; /* suitable for */ - typedef deque /* instantiating the */ - Path; /* SccCollection + typedef deque Path; /* instantiating the + * SccCollection * template (see * SccCollection.h). */ @@ -419,9 +419,7 @@ private: Graph::Path >& cycle, /* segment of the cycle */ size_type source_state_id, Edge transition, /* in a witness for the */ const size_type root_id, /* nonemptiness of the */ - const map, - ALLOC(PathElement) >& + const map& /* product. */ predecessor) const; Operations operations; /* Operations for @@ -655,9 +653,10 @@ protected: * acceptance sets. */ - typedef deque /* the above */ - AcceptanceStack; /* associations. */ + typedef deque /* Stack formed from */ + AcceptanceStack; /* the above + * associations. + */ AcceptanceStack acceptance_stack; /* Stack for storing the * dfs numbers of roots @@ -877,9 +876,9 @@ private: * reachable. */ - set, /* Set of states from */ - ALLOC(size_type) > /* which an accepting */ - reachability_info; /* component is known to + set reachability_info; /* Set of states from + * which an accepting + * component is known to * be reachable in the * product. */ @@ -928,9 +927,9 @@ public: ~AcceptingComponentFinder(); /* Destructor. */ - typedef set, /* Type definition for */ - ALLOC(size_type) > /* the set of product */ - SccType; /* state identifiers in + typedef set SccType; /* Type definition for + * the set of product + * state identifiers in * an accepting * strongly connected * component. @@ -1369,10 +1368,9 @@ void Product::findWitness unsigned long int number_of_collected_acceptance_sets = collected_acceptance_sets.count(number_of_acceptance_sets); - deque search_queue; - set, ALLOC(size_type) > visited; - map, ALLOC(PathElement) > - shortest_path_predecessor; + deque search_queue; + set visited; + map shortest_path_predecessor; size_type bfs_root = search_start_state; @@ -1475,8 +1473,7 @@ void Product::addCycleSegment (pair::Path, Graph::Path>& cycle, size_type source_state_id, Edge transition, const size_type root_id, - const map, ALLOC(PathElement) >& - predecessor) const + const map& predecessor) const /* ---------------------------------------------------------------------------- * * Description: Helper function for constructing a segment of an accepting diff --git a/lbtt/src/Random.h b/lbtt/src/Random.h index 0096e64a4..bd69ec27c 100644 --- a/lbtt/src/Random.h +++ b/lbtt/src/Random.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/SccCollection.h b/lbtt/src/SccCollection.h index ea31ac97f..32c5fc294 100644 --- a/lbtt/src/SccCollection.h +++ b/lbtt/src/SccCollection.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -195,10 +195,8 @@ public: /* default assignment operator */ - typedef set, /* a set of node id's. */ - ALLOC(typename GraphType::size_type) > - SccType; + typedef set /* Type definition for */ + SccType; /* a set of node id's. */ const SccType& operator()() const; /* Returns the set of node * identifiers in a @@ -338,10 +336,10 @@ public: /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ typedef map, /* identifiers and the */ - ALLOC(typename GraphType::size_type) >/* order in which they */ - DfsOrdering; /* were encountered in + typename GraphType::size_type> /* mapping between node */ + DfsOrdering; /* identifiers and the + * order in which they + * were encountered in * the search for * strongly connected * components. @@ -433,18 +431,19 @@ public: typename GraphType::size_type lowlink; }; - deque /* backtracking stack. */ - node_stack; + deque node_stack; /* Depth-first search + * backtracking stack. + */ + NodeStackElement* current_node; /* Pointer to the top * element of the * backtracking stack. */ - deque /* collecting the nodes */ - scc_stack; /* in a strongly + deque scc_stack; /* Stack used for + * collecting the nodes + * in a strongly * connected component, * excluding the root * nodes of the @@ -998,8 +997,7 @@ void SccCollection::iterator::getPath * when exiting from this function). */ - typename deque::const_iterator - n = node_stack.begin(); + typename deque::const_iterator n = node_stack.begin(); if (n != node_stack.end()) { for (++n; n != node_stack.end(); ++n) diff --git a/lbtt/src/SharedTestData.h b/lbtt/src/SharedTestData.h index 6403c52d4..6820d310d 100644 --- a/lbtt/src/SharedTestData.h +++ b/lbtt/src/SharedTestData.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -42,14 +42,14 @@ extern TestRoundInfo round_info; /* Data structure for * round. */ -extern vector /* implementation. */ - test_results; - -extern vector /* statistics for each */ - final_statistics; /* implementation. */ +extern vector test_results; /* Test results for each + * implementation. + */ +extern vector final_statistics; /* Overall test + * statistics for each + * implementation. + */ } #endif /* !SHAREDTESTDATA_H */ diff --git a/lbtt/src/SpinWrapper.cc b/lbtt/src/SpinWrapper.cc index 74a09c887..f98d59792 100644 --- a/lbtt/src/SpinWrapper.cc +++ b/lbtt/src/SpinWrapper.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/SpinWrapper.h b/lbtt/src/SpinWrapper.h index edbd0b6b1..1e4a7ed52 100644 --- a/lbtt/src/SpinWrapper.h +++ b/lbtt/src/SpinWrapper.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/SpotWrapper.cc b/lbtt/src/SpotWrapper.cc new file mode 100644 index 000000000..03731763e --- /dev/null +++ b/lbtt/src/SpotWrapper.cc @@ -0,0 +1,102 @@ +/* + * Copyright (C) 2003, 2004 + * Heikki Tauriainen + * + * Derived from SpinWrapper.cc by Alexandre Duret-Lutz . + * + * 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 +#ifdef HAVE_SSTREAM +#include +#else +#include +#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, + AtomWriter, + UnaryOperatorWriter, + UnaryOperatorWriter, + UnaryOperatorWriter, + UnaryOperatorWriter, + BinaryOperatorInfixWriter, + BinaryOperatorInfixWriter, + BinaryOperatorInfixWriter, + BinaryOperatorInfixWriter, + BinaryOperatorInfixWriter, + BinaryOperatorInfixWriter, + BinaryOperatorInfixWriter, + 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 */ +} diff --git a/lbtt/src/SpotWrapper.h b/lbtt/src/SpotWrapper.h new file mode 100644 index 000000000..206c5f601 --- /dev/null +++ b/lbtt/src/SpotWrapper.h @@ -0,0 +1,143 @@ +/* + * Copyright (C) 2003, 2004 + * Heikki Tauriainen + * + * Derived from SpinWrapper.h by Alexandre Duret-Lutz . + * + * 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 +#include +#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 */ diff --git a/lbtt/src/StatDisplay.cc b/lbtt/src/StatDisplay.cc index 8d6250626..8f8b772d0 100644 --- a/lbtt/src/StatDisplay.cc +++ b/lbtt/src/StatDisplay.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -78,8 +78,7 @@ void printStatTableHeader(ostream& stream, int indent) /* ========================================================================= */ void printBuchiAutomatonStats (ostream& stream, int indent, - vector::size_type - algorithm, + vector::size_type algorithm, int result_id) /* ---------------------------------------------------------------------------- * @@ -173,8 +172,7 @@ void printBuchiAutomatonStats /* ========================================================================= */ void printProductAutomatonStats (ostream& stream, int indent, - vector::size_type - algorithm, + vector::size_type algorithm, int result_id) /* ---------------------------------------------------------------------------- * @@ -264,8 +262,7 @@ void printProductAutomatonStats /* ========================================================================= */ void printAcceptanceCycleStats (ostream& stream, int indent, - vector::size_type - algorithm, + vector::size_type algorithm, int result_id) /* ---------------------------------------------------------------------------- * @@ -350,8 +347,7 @@ void printAcceptanceCycleStats /* ========================================================================= */ void printConsistencyCheckStats (ostream& stream, int indent, - vector::size_type - algorithm) + vector::size_type algorithm) /* ---------------------------------------------------------------------------- * * 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_neg_results = &test_results[*alg_1].automaton_stats[1]; - for (vector::size_type - alg_2 = 0; + for (vector::size_type alg_2 = 0; alg_2 < round_info.number_of_translators; alg_2++) { @@ -558,8 +553,7 @@ void printBuchiIntersectionCheckStats alg_1_pos_results = &test_results[*alg_1].automaton_stats[0]; alg_1_neg_results = &test_results[*alg_1].automaton_stats[1]; - for (vector::size_type - alg_2 = 0; + for (vector::size_type alg_2 = 0; alg_2 < round_info.number_of_translators; alg_2++) { @@ -631,8 +625,7 @@ void printBuchiIntersectionCheckStats /* ========================================================================= */ void printAllStats (ostream& stream, int indent, - vector::size_type - algorithm) + vector::size_type algorithm) /* ---------------------------------------------------------------------------- * * Description: Displays all test information (Büchi automaton and product @@ -701,8 +694,8 @@ void printAllStats /* ========================================================================= */ void printCollectiveCrossComparisonStats (ostream& stream, - vector::size_type algorithm_y, - vector::size_type algorithm_x, + vector::size_type algorithm_y, + vector::size_type algorithm_x, int data_type) /* ---------------------------------------------------------------------------- * @@ -892,13 +885,12 @@ void printCollectiveStats(ostream& stream, int indent) if (round_info.num_processed_formulae > 0 && configuration.global_options.formula_input_filename.empty()) { - const map, - ALLOC(unsigned long int) >& + const map& proposition_statistics = configuration.formula_options.formula_generator. propositionStatistics(); - const map, ALLOC(unsigned long int) > + const map symbol_statistics = configuration.formula_options.formula_generator.symbolStatistics(); @@ -944,9 +936,8 @@ void printCollectiveStats(ostream& stream, int indent) number_of_symbols_printed++; } - for (map, ALLOC(unsigned long int) > - ::const_iterator proposition = proposition_statistics.begin(); + for (map::const_iterator + proposition = proposition_statistics.begin(); proposition != proposition_statistics.end(); ++proposition) { @@ -993,8 +984,8 @@ void printCollectiveStats(ostream& stream, int indent) = ""; number_of_symbols_printed = 0; - for (map, ALLOC(unsigned long int) > - ::const_iterator op = symbol_statistics.begin(); + for (map::const_iterator + op = symbol_statistics.begin(); op != symbol_statistics.end(); ++op) { @@ -1468,8 +1459,7 @@ void printCollectiveStats(ostream& stream, int indent) estream << ind + " Result inconsistency statistics\n" + ind + " " + string(31, '=') + '\n'; - vector::size_type - algorithm_x, algorithm_y; + vector::size_type algorithm_x, algorithm_y; for (algorithm_x = 0; algorithm_x < number_of_algorithms; algorithm_x += 2) diff --git a/lbtt/src/StatDisplay.h b/lbtt/src/StatDisplay.h index 212aa6091..a5cb99b45 100644 --- a/lbtt/src/StatDisplay.h +++ b/lbtt/src/StatDisplay.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -50,32 +50,28 @@ void printStatTableHeader /* Displays a table */ void printBuchiAutomatonStats /* Displays information */ (ostream& stream, /* about a Büchi */ int indent, /* automaton. */ - vector::size_type + vector::size_type algorithm, int result_id); void printProductAutomatonStats /* Displays information */ (ostream& stream, /* about a product */ int indent, /* automaton. */ - vector::size_type + vector::size_type algorithm, int result_id); void printAcceptanceCycleStats /* Displays information */ (ostream& stream, /* about the acceptance */ int indent, /* cycles of a product */ - vector::size_type + vector::size_type /* automaton. */ algorithm, int result_id); void printConsistencyCheckStats /* Displays the result */ (ostream& stream, /* of the consistency */ int indent, /* check for a given */ - vector::size_type + vector::size_type /* algorithm. */ algorithm); void printCrossComparisonStats /* Displays information */ @@ -92,18 +88,14 @@ void printBuchiIntersectionCheckStats /* Displays the results */ void printAllStats /* A shorthand for */ (ostream& stream, /* showing all the */ int indent, /* information displayed */ - vector::size_type /* functions. */ - algorithm); + vector::size_type algorithm); /* by the previous five + * functions. + */ void printCollectiveCrossComparisonStats /* Displays a single */ (ostream& stream, /* `cell' of the final */ - vector::size_type /* comparison table. */ - algorithm_y, - vector::size_type - algorithm_x, + vector::size_type algorithm_y, /* result cross- */ + vector::size_type algorithm_x, /* comparison table. */ int data_type); void printCollectiveStats /* Displays average test */ diff --git a/lbtt/src/StateSpace.cc b/lbtt/src/StateSpace.cc index 78e2238e7..3c16064ea 100644 --- a/lbtt/src/StateSpace.cc +++ b/lbtt/src/StateSpace.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -144,8 +144,7 @@ void StateSpace::clear() initial_state = 0; #ifdef HAVE_OBSTACK_H - for (vector::iterator state = nodes.begin(); - state != nodes.end(); + for (vector::iterator state = nodes.begin(); state != nodes.end(); ++state) static_cast(*state)->~State(); diff --git a/lbtt/src/StateSpace.h b/lbtt/src/StateSpace.h index 338a5a4d1..cb67a6782 100644 --- a/lbtt/src/StateSpace.h +++ b/lbtt/src/StateSpace.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/StateSpaceProduct.h b/lbtt/src/StateSpaceProduct.h index 87fab2fbd..25a5c8a4b 100644 --- a/lbtt/src/StateSpaceProduct.h +++ b/lbtt/src/StateSpaceProduct.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/StateSpaceRandomizer.cc b/lbtt/src/StateSpaceRandomizer.cc index 951b4567c..f836d72a1 100644 --- a/lbtt/src/StateSpaceRandomizer.cc +++ b/lbtt/src/StateSpaceRandomizer.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * 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; - multimap, - ALLOC(StateSpace::size_type) > - reachable_but_unprocessed; + multimap reachable_but_unprocessed; reachable_but_unprocessed.insert(make_pair(0, 0)); diff --git a/lbtt/src/StateSpaceRandomizer.h b/lbtt/src/StateSpaceRandomizer.h index 0aff152ba..f74474490 100644 --- a/lbtt/src/StateSpaceRandomizer.h +++ b/lbtt/src/StateSpaceRandomizer.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/StringUtil.cc b/lbtt/src/StringUtil.cc index c1ff6d428..45d31b2ec 100644 --- a/lbtt/src/StringUtil.cc +++ b/lbtt/src/StringUtil.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * 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 - (const string& s, const char* slice_chars, - vector& slices) + (const string& s, const char* slice_chars, vector& slices) /* ---------------------------------------------------------------------------- * * Description: Slices a string into a vector of strings, using a given set @@ -415,7 +414,7 @@ int parseInterval /* ========================================================================= */ void parseIntervalList (const string& token, IntervalList& intervals, unsigned long int min, - unsigned long int max, vector* extra_tokens) + unsigned long int max, vector* extra_tokens) /* ---------------------------------------------------------------------------- * * Description: Parses a string of number intervals into an IntervalList. @@ -443,14 +442,13 @@ void parseIntervalList * * ------------------------------------------------------------------------- */ { - vector interval_strings; + vector interval_strings; int interval_type; intervals.clear(); sliceString(token, ",", interval_strings); - for (vector::const_iterator - i = interval_strings.begin(); + for (vector::const_iterator i = interval_strings.begin(); i != interval_strings.end(); ++i) { diff --git a/lbtt/src/StringUtil.h b/lbtt/src/StringUtil.h index 4965cf64f..954f936d6 100644 --- a/lbtt/src/StringUtil.h +++ b/lbtt/src/StringUtil.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -58,7 +58,7 @@ template string toString(const T& t); /* Template function for void sliceString /* Breaks a string into */ (const string& s, const char* slice_chars, /* `slices', using a */ - vector& slices); /* given set of + vector& slices); /* given set of * characters as * separators. */ @@ -114,8 +114,9 @@ void parseIntervalList /* Converts a list of */ IntervalList& intervals, /* the set of unsigned */ unsigned long int min, /* long integers */ unsigned long int max, /* corresponding to the */ - vector* extra_tokens /* union of the */ - = 0); /* intervals. */ + vector* extra_tokens = 0); /* union of the + * intervals. + */ void parseTime /* Parses a time string. */ (const string& time_string, diff --git a/lbtt/src/TempFsysName.cc b/lbtt/src/TempFsysName.cc index 51dc9c335..45f9ad676 100644 --- a/lbtt/src/TempFsysName.cc +++ b/lbtt/src/TempFsysName.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 2004 - * Heikki Tauriainen + * Copyright (C) 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/TempFsysName.h b/lbtt/src/TempFsysName.h index f2845ebb6..d9fa07994 100644 --- a/lbtt/src/TempFsysName.h +++ b/lbtt/src/TempFsysName.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 2004 - * Heikki Tauriainen + * Copyright (C) 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/TestOperations.cc b/lbtt/src/TestOperations.cc index 8dd515b66..01e41b2a2 100644 --- a/lbtt/src/TestOperations.cc +++ b/lbtt/src/TestOperations.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * 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. @@ -595,7 +597,7 @@ void generateFormulae(istream* formula_input_stream) { bool fatal_io_error = (configuration.global_options.formula_input_filename.empty() - || !round_info.formula_input_file.eof()); + || !round_info.formula_input_stream->eof()); printText(string("[") + (fatal_io_error ? "Error reading formula" @@ -823,8 +825,7 @@ void writeFormulaeToFiles() /* ========================================================================= */ void generateBuchiAutomaton (int f, - vector::size_type algorithm_id) + vector::size_type algorithm_id) /* ---------------------------------------------------------------------------- * * 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 exitcode; - sigset_t sigint_mask; - sigemptyset(&sigint_mask); - sigaddset(&sigint_mask, SIGINT); - struct sigaction timeout_sa; timeout_sa.sa_handler = timeoutHandler; sigemptyset(&timeout_sa.sa_mask); timeout_sa.sa_flags = 0; - pid_t pid = 0; - truncateFile(round_info.automaton_file_name->get(), 10); truncateFile(round_info.cout_capture_file->get(), 10); truncateFile(round_info.cerr_capture_file->get(), 10); @@ -932,13 +927,13 @@ void generateBuchiAutomaton = const_cast(round_info.automaton_file_name->get()); times(&timing_information_begin); - pid = fork(); - switch (pid) + translator_process = fork(); + switch (translator_process) { case 0 : /* child */ close(error_pipe[0]); - if (setsid() != -1 + if (setpgid(0, 0) != -1 && dup2(stdout_capture_fileno, STDOUT_FILENO) != -1 && dup2(stderr_capture_fileno, STDERR_FILENO) != -1) execvp(algorithm.parameters[0], algorithm.parameters); @@ -952,17 +947,32 @@ void generateBuchiAutomaton exit(0); case -1 : /* fork failed */ - pid = 0; + translator_process = 0; error_number = errno; close(error_pipe[0]); close(error_pipe[1]); break; default : /* parent */ - /* Block SIGINT signals while the child process is running. */ + setpgid(translator_process, translator_process); if (configuration.global_options.handle_breaks) - sigprocmask(SIG_BLOCK, &sigint_mask, static_cast(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. */ @@ -976,12 +986,11 @@ void generateBuchiAutomaton close(error_pipe[1]); - if (waitpid(pid, &exitcode, 0) == -1) /* waitpid failed */ + if (waitpid(translator_process, &exitcode, 0) == -1) + /* waitpid failed */ { error_number = errno; - if (error_number == EINTR /* failure due to timeout */ - && configuration.global_options.translator_timeout > 0 - && timeout) + if (kill(translator_process, 0) == 0) /* child still running */ { /* * 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; ++attempts_to_terminate) { - kill(-pid, sig); + kill(-translator_process, sig); sleep(delay); - if (waitpid(pid, &exitcode, WNOHANG) != 0) + if (waitpid(translator_process, &exitcode, WNOHANG) != 0) { times(&timing_information_end); - pid = 0; + translator_process = 0; break; } if (attempts_to_terminate == 2) @@ -1010,13 +1019,13 @@ void generateBuchiAutomaton } } } - else - pid = 0; + else if (errno != EPERM) + translator_process = 0; } else /* child exited successfully */ { times(&timing_information_end); - pid = 0; + translator_process = 0; /* * If there is something to be read from error_pipe, then there @@ -1043,10 +1052,21 @@ void generateBuchiAutomaton } if (configuration.global_options.handle_breaks) - sigprocmask(SIG_UNBLOCK, &sigint_mask, - static_cast(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 != static_cast(-1) && timing_information_begin.tms_cutime @@ -1069,15 +1089,15 @@ void generateBuchiAutomaton close(stderr_capture_fileno); /* - * If pid != 0 at this point, then a timeout occurred, but lbtt was - * unable to terminate the child process. The exception handler will - * in this case throw an unexpected exception (see below) so that lbtt - * will terminate (for example, it is not safe to use the temporary - * file names any longer if the (still running) child process happens to - * write to them). + * If translator_process != 0 at this point, then a timeout occurred, + * but lbtt was unable to terminate the child process. The exception + * handler will in this case throw an unexpected exception (see below) + * so that lbtt will terminate (for example, it is not safe to use the + * temporary file names any longer if the (still running) child process + * happens to write to them). */ - if (pid != 0) + if (translator_process != 0) { stdout_capture_fileno = stderr_capture_fileno = -1; throw Exception("could not terminate child process"); @@ -1286,7 +1306,7 @@ void generateBuchiAutomaton 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 ("fatal internal error while generating Büchi automaton"); @@ -1345,9 +1365,7 @@ void generateBuchiAutomaton /* ========================================================================= */ void performEmptinessCheck (int f, - vector::size_type - algorithm_id) + vector::size_type algorithm_id) /* ---------------------------------------------------------------------------- * * Description: Performs the emptiness check on a ProductAutomaton, i.e., @@ -1473,9 +1491,7 @@ void performEmptinessCheck /* ========================================================================= */ void performConsistencyCheck - (vector::size_type - algorithm_id) + (vector::size_type algorithm_id) /* ---------------------------------------------------------------------------- * * Description: Checks the model checking results for consistency for a @@ -1570,8 +1586,7 @@ void compareResults() AutomatonStats* alg_1_stats; AutomatonStats* alg_2_stats; - for (vector::size_type - alg_1 = 0; + for (vector::size_type alg_1 = 0; alg_1 < test_results.size(); ++alg_1) { @@ -1579,8 +1594,7 @@ void compareResults() { alg_1_stats = &test_results[alg_1].automaton_stats[counter]; - for (vector - ::size_type alg_2 = alg_1 + 1; + for (vector::size_type alg_2 = alg_1 + 1; alg_2 < test_results.size(); ++alg_2) { @@ -1681,13 +1695,11 @@ void performBuchiIntersectionCheck() ::Graph::BuchiProduct::clearSatisfiabilityCache(); - for (vector::size_type - alg_1 = 0; + for (vector::size_type alg_1 = 0; alg_1 < round_info.number_of_translators; ++alg_1) { - for (vector::size_type - alg_2 = 0; + for (vector::size_type alg_2 = 0; alg_2 < round_info.number_of_translators; ++alg_2) { diff --git a/lbtt/src/TestOperations.h b/lbtt/src/TestOperations.h index 9c31a0ad0..74b9cdfd1 100644 --- a/lbtt/src/TestOperations.h +++ b/lbtt/src/TestOperations.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * 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 */ (int f, /* automaton from a LTL */ - vector /* given file, using a */ - ::size_type /* given LTL-to-Büchi */ - algorithm_id); /* translation algorithm + vector /* formula stored in a */ + ::size_type /* given file, using a */ + algorithm_id); /* given LTL-to-Büchi + * translation algorithm * for the conversion. */ void performEmptinessCheck /* Performs an emptiness */ (int f, /* check on a product */ - vector + vector /* automaton. */ ::size_type algorithm_id); void performConsistencyCheck /* Performs a */ - (vector /* the test results */ - ::size_type /* for a formula and its */ - algorithm_id); /* negation. */ + (vector /* consistency check on */ + ::size_type /* the test results */ + algorithm_id); /* for a formula and its + * negation. + */ void compareResults(); /* Compares the model * checking results diff --git a/lbtt/src/TestRoundInfo.h b/lbtt/src/TestRoundInfo.h index 6a2f94b38..8b396b9d7 100644 --- a/lbtt/src/TestRoundInfo.h +++ b/lbtt/src/TestRoundInfo.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -55,7 +55,11 @@ public: * 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. */ @@ -149,9 +153,9 @@ public: * current round. */ - vector /* current round: */ - formulae; /* formulae[0]: + vector formulae; /* Formulae used in the + * current round: + * formulae[0]: * positive formula in * negation normal * form @@ -167,7 +171,7 @@ public: * generated */ - vector formula_in_file; /* The values in this + vector formula_in_file; /* The values in this * vector will be set to * true when the * corresponding diff --git a/lbtt/src/TestStatistics.cc b/lbtt/src/TestStatistics.cc index b3c82bd54..053df05b0 100644 --- a/lbtt/src/TestStatistics.cc +++ b/lbtt/src/TestStatistics.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * 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_performed = false; - for (vector::iterator it + for (vector::iterator it = automaton_stats[i].cross_comparison_stats.begin(); it != automaton_stats[i].cross_comparison_stats.end(); ++it) @@ -87,7 +86,7 @@ void AlgorithmTestResults::fullReset() automaton_stats[i].number_of_msccs = 0; automaton_stats[i].buchi_generation_time = 0.0; - for (vector::iterator it + for (vector::iterator it = automaton_stats[i].buchi_intersection_check_stats.begin(); it != automaton_stats[i].buchi_intersection_check_stats.end(); ++it) diff --git a/lbtt/src/TestStatistics.h b/lbtt/src/TestStatistics.h index 71fb30de8..e6a16500c 100644 --- a/lbtt/src/TestStatistics.h +++ b/lbtt/src/TestStatistics.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -43,9 +43,8 @@ using Graph::StateSpace; struct AutomatonStats { explicit AutomatonStats /* Constructor. */ - (vector - ::size_type number_of_algorithms, + (vector + ::size_type number_of_algorithms, StateSpace::size_type max_statespace_size); /* default copy constructor */ @@ -127,9 +126,9 @@ struct AutomatonStats typedef pair CrossComparisonStats; - vector /* cross-comparison */ - cross_comparison_stats; /* results. The `first' + vector /* Emptiness check */ + cross_comparison_stats; /* cross-comparison + * results. The `first' * element of the pair * tells whether a cross- * comparison with a given @@ -142,8 +141,8 @@ struct AutomatonStats * differ. */ - vector /* Büchi automaton */ - buchi_intersection_check_stats; /* intersection + vector buchi_intersection_check_stats; /* Büchi automaton + * intersection * emptiness check * results. The elements * of the vector tell @@ -173,8 +172,7 @@ struct AutomatonStats struct AlgorithmTestResults { explicit AlgorithmTestResults /* Constructor. */ - (vector + (vector ::size_type number_of_algorithms, StateSpace::size_type max_statespace_size); @@ -214,8 +212,8 @@ struct AlgorithmTestResults * check. */ - vector /* A two-element vector */ - automaton_stats; /* storing test results + vector automaton_stats; /* A two-element vector + * storing test results * for an algorithm. */ }; @@ -232,8 +230,7 @@ struct AlgorithmTestResults struct TestStatistics { explicit TestStatistics /* Constructor. */ - (vector::size_type + (vector::size_type number_of_algorithms); /* default copy constructor */ @@ -303,24 +300,26 @@ struct TestStatistics * automata. */ - vector /* result cross- */ - cross_comparison_mismatches; /* comparisons. */ + vector /* Number of failed */ + cross_comparison_mismatches; /* result cross- + * comparisons. + */ - vector /* result cross- */ - initial_cross_comparison_mismatches; /* comparisons in the + vector /* Number of failed */ + initial_cross_comparison_mismatches; /* result cross- + * comparisons in the * initial state of the * state space. */ - vector /* cross-comparisons */ - cross_comparisons_performed; /* performed. */ + vector /* Number of result */ + cross_comparisons_performed; /* cross-comparisons + * performed. + */ - vector /* Büchi automaton */ - buchi_intersection_check_failures; /* emptiness checks + vector /* Number of failed */ + buchi_intersection_check_failures; /* Büchi automaton + * emptiness checks * against the automata * constructed from the * negated formula @@ -328,9 +327,9 @@ struct TestStatistics * algorithms. */ - vector /* automaton emptiness */ - buchi_intersection_checks_performed; /* checks performed + vector /* Number of Büchi */ + buchi_intersection_checks_performed; /* automaton emptiness + * checks performed * against the automata * constructed from the * negated formula using @@ -348,9 +347,7 @@ struct TestStatistics /* ========================================================================= */ inline AutomatonStats::AutomatonStats - (vector::size_type - number_of_algorithms, + (vector::size_type number_of_algorithms, StateSpace::size_type max_statespace_size) : buchi_automaton(0), number_of_buchi_states(0), number_of_buchi_transitions(0), number_of_acceptance_sets(0), @@ -472,9 +469,7 @@ AutomatonStats::buchiIntersectionCheckPerformed(unsigned long int algorithm) /* ========================================================================= */ inline AlgorithmTestResults::AlgorithmTestResults - (vector::size_type - number_of_algorithms, + (vector::size_type number_of_algorithms, StateSpace::size_type max_statespace_size) : consistency_check_result(-1), consistency_check_comparisons(0), failed_consistency_check_comparisons(0), @@ -519,8 +514,7 @@ inline AlgorithmTestResults::~AlgorithmTestResults() /* ========================================================================= */ inline TestStatistics::TestStatistics - (vector::size_type - number_of_algorithms) : + (vector::size_type number_of_algorithms) : consistency_check_failures(0), consistency_checks_performed(0), cross_comparison_mismatches(number_of_algorithms, 0), initial_cross_comparison_mismatches(number_of_algorithms, 0), diff --git a/lbtt/src/TranslatorInterface.h b/lbtt/src/TranslatorInterface.h index ac70bfc55..eca8e172d 100644 --- a/lbtt/src/TranslatorInterface.h +++ b/lbtt/src/TranslatorInterface.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License diff --git a/lbtt/src/UserCommandReader.cc b/lbtt/src/UserCommandReader.cc index a91b71403..051c56306 100644 --- a/lbtt/src/UserCommandReader.cc +++ b/lbtt/src/UserCommandReader.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -86,7 +86,7 @@ void executeUserCommands() * ------------------------------------------------------------------------ */ { string input_line; - vector input_tokens; + vector input_tokens; TokenType token; bool formula_type = true; @@ -230,9 +230,7 @@ void executeUserCommands() { bool all_algorithms_disabled = true; - for (vector - ::const_iterator + for (vector::const_iterator algorithm = configuration.algorithms.begin(); algorithm != configuration.algorithms.end(); ++algorithm) @@ -799,9 +797,8 @@ TokenType parseCommand(const string& token) /* ========================================================================= */ void verifyArgumentCount - (const vector& command, - vector::size_type min_arg_count, - vector::size_type max_arg_count) + (const vector& command, vector::size_type min_arg_count, + vector::size_type max_arg_count) /* ---------------------------------------------------------------------------- * * Description: Verifies that the number of arguments given for a user @@ -824,8 +821,7 @@ void verifyArgumentCount } /* ========================================================================= */ -pair parseRedirection - (vector& input_tokens) +pair parseRedirection(vector& input_tokens) /* ---------------------------------------------------------------------------- * * Description: Tests whether the last argument to a user command specifies @@ -888,7 +884,7 @@ pair parseRedirection } /* ========================================================================= */ -bool parseFormulaType(vector& input_tokens) +bool parseFormulaType(vector& input_tokens) /* ---------------------------------------------------------------------------- * * Description: Tests whether the first argument of a command specifies a diff --git a/lbtt/src/UserCommandReader.h b/lbtt/src/UserCommandReader.h index dfe489291..b9a510519 100644 --- a/lbtt/src/UserCommandReader.h +++ b/lbtt/src/UserCommandReader.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * 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 */ - (const vector& /* number of arguments */ - arguments, /* for a command is */ - vector::size_type /* within given limits. */ - min_arg_count, - vector::size_type - max_arg_count); + (const vector& arguments, /* number of arguments */ + vector::size_type min_arg_count, /* for a command is */ + vector::size_type max_arg_count); /* within given limits. */ pair parseRedirection /* Checks whether an */ - (vector& input_tokens); /* user command given + (vector& input_tokens); /* user command given * will require * redirecting its * output to a file. */ bool parseFormulaType /* Checks whether an */ - (vector& input_tokens); /* user command + (vector& input_tokens); /* user command * specified a positive * or a negative * formula. diff --git a/lbtt/src/UserCommands.cc b/lbtt/src/UserCommands.cc index e5ae8c72e..08980d028 100644 --- a/lbtt/src/UserCommands.cc +++ b/lbtt/src/UserCommands.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * 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&) { - map, ALLOC(unsigned long int) > - ::const_iterator id_finder + map::const_iterator id_finder = configuration.algorithm_names.find(unquoted_id); if (id_finder == configuration.algorithm_names.end()) throw CommandErrorException @@ -113,20 +112,18 @@ void parseAlgorithmIdList(const string& ids, IntervalList& algorithms) try { - vector nonnumeric_algorithm_ids; + vector nonnumeric_algorithm_ids; parseIntervalList(id_string, algorithms, 0, round_info.number_of_translators - 1, &nonnumeric_algorithm_ids); - for (vector::iterator - id = nonnumeric_algorithm_ids.begin(); + for (vector::iterator id = nonnumeric_algorithm_ids.begin(); id != nonnumeric_algorithm_ids.end(); ++id) { *id = unquoteString(substituteInQuotedString(*id, "\n", ",")); - map, ALLOC(unsigned long int) > - ::const_iterator + map::const_iterator id_finder = configuration.algorithm_names.find(*id); if (id_finder == configuration.algorithm_names.end()) throw CommandErrorException @@ -181,7 +178,7 @@ void printAlgorithmList(ostream& stream, int indent) /* ========================================================================= */ void printCrossComparisonAnalysisResults (ostream& stream, int indent, bool formula_type, - const vector& input_tokens) + const vector& input_tokens) /* ---------------------------------------------------------------------------- * * Description: Implements the user command `resultanalysis', i.e., analyzes @@ -494,8 +491,7 @@ void printCrossComparisonAnalysisResults /* ========================================================================= */ void printConsistencyAnalysisResults - (ostream& stream, int indent, - const vector& input_tokens) + (ostream& stream, int indent, const vector& input_tokens) /* ---------------------------------------------------------------------------- * * Description: Implements the user command `consistencyanalysis', i.e., @@ -607,11 +603,9 @@ void printConsistencyAnalysisResults } } - vector path; + vector path; StateSpace::Path prefix, cycle; - map, ALLOC(StateSpace::size_type) > - ordering; + map ordering; StateSpace::size_type state_count = 0; StateSpace::size_type loop_state; @@ -663,8 +657,7 @@ void printConsistencyAnalysisResults /* ========================================================================= */ void printAutomatonAnalysisResults - (ostream& stream, int indent, - const vector& input_tokens) + (ostream& stream, int indent, const vector& input_tokens) /* ---------------------------------------------------------------------------- * * Description: Implements the user command `buchianalysis', i.e., analyzes @@ -977,9 +970,7 @@ void printPath /* ========================================================================= */ void printAcceptingCycle (ostream& stream, int indent, - vector::size_type - algorithm_id, + vector::size_type algorithm_id, const BuchiAutomaton::Path& aut_prefix, const BuchiAutomaton::Path& aut_cycle, const BuchiAutomaton& automaton, const StateSpace::Path& path_prefix, @@ -1121,8 +1112,7 @@ void printAcceptingCycle /* ========================================================================= */ void printBuchiAutomaton (ostream& stream, int indent, bool formula_type, - vector& input_tokens, - Graph::GraphOutputFormat fmt) + vector& input_tokens, Graph::GraphOutputFormat fmt) /* ---------------------------------------------------------------------------- * * Description: Implements the user command `buchi', i.e., writes information @@ -1231,8 +1221,8 @@ void printBuchiAutomaton /* ========================================================================= */ void evaluateFormula - (ostream& stream, int indent, bool formula_type, - vector& input_tokens) + (ostream& stream, int indent, bool formula_type, + vector& input_tokens) /* ---------------------------------------------------------------------------- * * Description: Implements the user command `evaluate', i.e., tells whether @@ -1346,7 +1336,7 @@ void evaluateFormula /* ========================================================================= */ void printFormula (ostream& stream, int indent, bool formula_type, - const vector& input_tokens) + const vector& input_tokens) /* ---------------------------------------------------------------------------- * * Description: Implements the user command `formula', i.e., displays the @@ -1401,8 +1391,7 @@ void printFormula /* ========================================================================= */ void printCommandHelp - (ostream& stream, int indent, - const vector& input_tokens) + (ostream& stream, int indent, const vector& input_tokens) /* ---------------------------------------------------------------------------- * * Description: Implements the user command `help', i.e., gives instructions @@ -1714,7 +1703,7 @@ void printCommandHelp /* ========================================================================= */ void printInconsistencies - (ostream& stream, int indent, vector& input_tokens) + (ostream& stream, int indent, vector& input_tokens) /* ---------------------------------------------------------------------------- * * Description: Implements the user command `inconsistencies', i.e., lists @@ -1818,7 +1807,7 @@ void printInconsistencies /* ========================================================================= */ void printTestResults - (ostream& stream, int indent, vector& input_tokens) + (ostream& stream, int indent, vector& input_tokens) /* ---------------------------------------------------------------------------- * * Description: Implements the user command `results', i.e., displays the @@ -1877,7 +1866,7 @@ void printTestResults /* ========================================================================= */ void printStateSpace - (ostream& stream, int indent, vector& input_tokens, + (ostream& stream, int indent, vector& input_tokens, Graph::GraphOutputFormat fmt) /* ---------------------------------------------------------------------------- * @@ -1950,7 +1939,7 @@ void printStateSpace } /* ========================================================================= */ -void changeVerbosity(const vector& input_tokens) +void changeVerbosity(const vector& input_tokens) /* ---------------------------------------------------------------------------- * * Description: Implements the user command `verbosity', i.e., displays or @@ -1987,8 +1976,7 @@ void changeVerbosity(const vector& input_tokens) } /* ========================================================================= */ -void changeAlgorithmState - (vector& input_tokens, bool enable) +void changeAlgorithmState(vector& input_tokens, bool enable) /* ---------------------------------------------------------------------------- * * Description: Changes the enabledness of a set of algorithms used in the diff --git a/lbtt/src/UserCommands.h b/lbtt/src/UserCommands.h index 756717387..51ed74ef5 100644 --- a/lbtt/src/UserCommands.h +++ b/lbtt/src/UserCommands.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * 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 */ (ostream& stream, int indent, /* contradiction between */ bool formula_type, /* test results of two */ - const vector& /* implementations. */ - input_tokens); + const vector& input_tokens); /* implementations. */ void printConsistencyAnalysisResults /* Analyzes a */ (ostream& stream, int indent, /* contradicition in the */ - const vector& /* model checking result */ - input_tokens); /* consistency check for + const vector& input_tokens); /* model checking result + * consistency check for * an implementation. */ void printAutomatonAnalysisResults /* Analyzes a */ (ostream& stream, int indent, /* contradiction in the */ - const vector& /* Büchi automata */ - input_tokens); /* intersection + const vector& input_tokens); /* Büchi automata + * intersection * emptiness check. */ @@ -92,8 +91,7 @@ void printPath /* Displays information */ void printAcceptingCycle /* Displays information */ (ostream& stream, int indent, /* a single automaton */ - vector + vector /* execution. */ ::size_type algorithm_id, const BuchiAutomaton::Path& aut_prefix, @@ -106,47 +104,47 @@ void printAcceptingCycle /* Displays information */ void printBuchiAutomaton /* Displays information */ (ostream& stream, int indent, /* about a Büchi */ bool formula_type, /* automaton. */ - vector& input_tokens, + vector& input_tokens, Graph::GraphOutputFormat fmt); void evaluateFormula /* Displays information */ (ostream& stream, int indent, /* about existence of */ bool formula_type, /* accepting system */ - vector& input_tokens); /* executions. */ + vector& input_tokens); /* executions. */ void printFormula /* Displays a formula */ (ostream& stream, int indent, /* used for testing. */ bool formula_type, - const vector& - input_tokens); + const vector& input_tokens); void printCommandHelp /* Displays help about */ (ostream& stream, int indent, /* user commands. */ - const vector& - input_tokens); + const vector& input_tokens); void printInconsistencies /* Lists the system */ (ostream& stream, int indent, /* states failing the */ - vector& input_tokens); /* consistency check + vector& input_tokens); /* consistency check * for an algorihm. */ void printTestResults /* Displays the test */ (ostream& stream, int indent, /* results of the last */ - vector& input_tokens); /* round performed. */ + vector& input_tokens); /* round performed. */ void printStateSpace /* Displays information */ (ostream& stream, int indent, /* about a state space. */ - vector& input_tokens, + vector& input_tokens, Graph::GraphOutputFormat fmt); void changeVerbosity /* Displays or changes */ - (const vector& /* the verbosity of */ - input_tokens); /* output. */ + (const vector& input_tokens); /* the verbosity of + * output. + */ void changeAlgorithmState /* Enables or disables a */ - (vector& input_tokens, /* set of algorithms */ - bool enable); /* used in the tests. */ + (vector& input_tokens, bool enable); /* set of algorithms + * used in the tests. + */ } diff --git a/lbtt/src/main.cc b/lbtt/src/main.cc index c217ac4f7..4c4093da2 100644 --- a/lbtt/src/main.cc +++ b/lbtt/src/main.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -21,6 +21,9 @@ #include #include #include +#ifdef HAVE_SYS_TYPES_H +#include +#endif /* HAVE_SYS_TYPES_H */ #include #include #ifdef HAVE_READLINE @@ -28,6 +31,11 @@ #include #include #endif /* HAVE_READLINE */ +#ifdef HAVE_ISATTY +#ifdef HAVE_UNISTD_H +#include +#endif /* HAVE_UNISTD_H */ +#endif /* HAVE_ISATTY */ #include "LbttAlloc.h" #include "Configuration.h" #include "DispUtil.h" @@ -82,12 +90,12 @@ TestRoundInfo round_info; /* Data structure for * round. */ -vector /* individual algorithm. */ - test_results; +vector test_results; /* Test results for each + * individual algorithm. + */ -vector /* Overall test */ - final_statistics; /* statistics for each +vector final_statistics; /* Overall test + * statistics for each * algorithm. */ @@ -167,9 +175,13 @@ static void breakHandler(int) * *****************************************************************************/ +pid_t translator_process = 0; /* Process group for translator process */ + static void abortHandler(int signum) { deallocateTempFilenames(); + if (translator_process != 0 && kill(translator_process, 0) == 0) + kill(-translator_process, SIGTERM); struct sigaction s; s.sa_handler = SIG_DFL; sigemptyset(&s.sa_mask); @@ -274,16 +286,24 @@ bool testLoop() /* * 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 { if (!global_options.formula_input_filename.empty()) - openFile(global_options.formula_input_filename.c_str(), - round_info.formula_input_file, - ios::in, - 0); + { + if (global_options.formula_input_filename == "-") + round_info.formula_input_stream = &cin; + 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) { @@ -383,8 +403,7 @@ bool testLoop() round_info.next_round_to_change_statespace += global_options.statespace_change_interval; - for (vector - ::iterator it = test_results.begin(); + for (vector::iterator it = test_results.begin(); it != test_results.end(); ++it) it->emptinessReset(); @@ -437,8 +456,7 @@ bool testLoop() round_info.formula_in_file[0] = round_info.formula_in_file[1] = false; - for (vector - ::iterator it = test_results.begin(); + for (vector::iterator it = test_results.begin(); it != test_results.end(); ++it) it->fullReset(); @@ -449,8 +467,8 @@ bool testLoop() { try { - generateFormulae(round_info.formula_input_file.is_open() - ? &round_info.formula_input_file + generateFormulae(!global_options.formula_input_filename.empty() + ? round_info.formula_input_stream : 0); } catch (const FormulaGenerationException&) @@ -667,8 +685,7 @@ bool testLoop() ::Ltl::LtlFormula::destruct(round_info.formulae[f]); } - for (vector - ::iterator it = test_results.begin(); + for (vector::iterator it = test_results.begin(); it != test_results.end(); ++it) it->fullReset(); @@ -735,10 +752,19 @@ int main(int argc, char* argv[]) if (!e.line_info.empty()) cerr << ":" << configuration.global_options.cfg_filename << ":" << e.line_info; - cerr << ":" << e.what() << endl; + cerr << ": " << e.what() << endl; 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) configuration.print(cout); diff --git a/lbtt/src/translate.cc b/lbtt/src/translate.cc index eab9a9037..173f796dc 100644 --- a/lbtt/src/translate.cc +++ b/lbtt/src/translate.cc @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -25,6 +25,7 @@ #include "LbtWrapper.h" #include "LtlFormula.h" #include "SpinWrapper.h" +#include "SpotWrapper.h" #ifdef HAVE_GETOPT_LONG #include #define OPTIONSTRUCT struct option @@ -59,7 +60,7 @@ static TranslatorInterface* translator = 0; /****************************************************************************** * * A function for showing warnings to the user. - * + * *****************************************************************************/ void printWarning(const string& msg) @@ -119,7 +120,7 @@ static void installSignalHandler(int signum) 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; static OPTIONSTRUCT command_line_options[] = @@ -127,6 +128,7 @@ int main(int argc, char** argv) {"help", no_argument, 0, OPT_HELP}, {"lbt", no_argument, 0, OPT_LBT}, {"spin", no_argument, 0, OPT_SPIN}, + {"spot", no_argument, 0, OPT_SPOT}, {"version", no_argument, 0, OPT_VERSION}, {0, 0, 0, 0} }; @@ -154,6 +156,7 @@ int main(int argc, char** argv) "Translator options:\n" " --lbt lbt\n" " --spin Spin\n" + " --spot Spot\n" "The command line for these translators must be given as a " "single argument\n" "including the name (and location) of an external program to " @@ -171,6 +174,10 @@ int main(int argc, char** argv) translator = new SpinWrapper(); break; + case OPT_SPOT : + translator = new SpotWrapper(); + break; + case OPT_VERSION : cout << "lbtt-translate " PACKAGE_VERSION "\n" "lbtt-translate is free software; you may change and " diff --git a/lbtt/src/translate.h b/lbtt/src/translate.h index 4d7971859..af028f4f4 100644 --- a/lbtt/src/translate.h +++ b/lbtt/src/translate.h @@ -1,6 +1,6 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 + * Heikki Tauriainen * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License