diff --git a/ChangeLog b/ChangeLog index ab420218e..d093879e8 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,7 @@ +2005-08-31 Alexandre Duret-Lutz + + * lbtt/: Merge lbtt 1.2.0. + 2005-06-06 Alexandre Duret-Lutz * src/tgbaalgos/reductgba_sim_del.cc diff --git a/lbtt/ChangeLog b/lbtt/ChangeLog index 8d5f93dee..02f78630f 100644 --- a/lbtt/ChangeLog +++ b/lbtt/ChangeLog @@ -1,25 +1,115 @@ -2004-02-11 Alexandre Duret-Lutz +2005-08-30 Heikki Tauriainen - * src/SpotWrapper.cc (SpotWrapper::SPOT_AND, SpotWrapper::SPOT_OR): - Define as && and || as in Spin. - * src/SpotWrapper.hh: Update by email. + * 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. -2003-07-10 Alexandre Duret-Lutz + * 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). - Spot wants `^', not `xor'. - * src/SpotWrapper.hh (SpotWrapper::SPOT_XOR): Declare. - * src/SpotWrapper.cc (SpotWrapper::SPOT_XOR): Define. - (SpotWrapper::translateFormula): Use SPOT_XOR. + * 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. -2003-07-09 Alexandre Duret-Lutz + * NEWS, README, configure.ac: Update. - * src/ExternalTranslator.h (class ExternalTranslator): - Declare class SpotWrapper as a friend. - * src/SpotWrapper.h, src/SpotWrapper.cc: New files. - * src/Makefile.am (lbtt_translate_SOURCES): Add SpotWrapper.cc - and SpotWrapper.h. - * src/translate.cc (main): Add the --spot option, and build - a SpotWrapper if required. + * 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 diff --git a/lbtt/INSTALL b/lbtt/INSTALL index 56b077d6a..23e5f25d0 100644 --- a/lbtt/INSTALL +++ b/lbtt/INSTALL @@ -102,16 +102,16 @@ for another architecture. Installation Names ================== -By default, `make install' will install the package's files in -`/usr/local/bin', `/usr/local/man', etc. You can specify an -installation prefix other than `/usr/local' by giving `configure' the -option `--prefix=PREFIX'. +By default, `make install' installs the package's commands under +`/usr/local/bin', include files under `/usr/local/include', etc. You +can specify an installation prefix other than `/usr/local' by giving +`configure' the option `--prefix=PREFIX'. You can specify separate installation prefixes for architecture-specific files and architecture-independent files. If you -give `configure' the option `--exec-prefix=PREFIX', the package will -use PREFIX as the prefix for installing programs and libraries. -Documentation and other data files will still use the regular prefix. +pass the option `--exec-prefix=PREFIX' to `configure', the package uses +PREFIX as the prefix for installing programs and libraries. +Documentation and other data files still use the regular prefix. In addition, if you use an unusual directory layout you can give options like `--bindir=DIR' to specify different values for particular @@ -159,7 +159,7 @@ where SYSTEM can have one of these forms: need to know the machine type. If you are _building_ compiler tools for cross-compiling, you should -use the `--target=TYPE' option to select the type of system they will +use the option `--target=TYPE' to select the type of system they will produce code for. If you want to _use_ a cross compiler, that generates code for a diff --git a/lbtt/src/ExternalTranslator.h b/lbtt/src/ExternalTranslator.h index 3a5a878eb..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,10 +174,10 @@ 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/SpotWrapper.cc b/lbtt/src/SpotWrapper.cc index 2512dcd51..03731763e 100644 --- a/lbtt/src/SpotWrapper.cc +++ b/lbtt/src/SpotWrapper.cc @@ -1,6 +1,6 @@ /* * Copyright (C) 2003, 2004 - * Heikki Tauriainen + * Heikki Tauriainen * * Derived from SpinWrapper.cc by Alexandre Duret-Lutz . * @@ -19,10 +19,6 @@ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. */ -#ifdef __GNUC__ -#pragma implementation -#endif /* __GNUC__ */ - #include #ifdef HAVE_SSTREAM #include diff --git a/lbtt/src/SpotWrapper.h b/lbtt/src/SpotWrapper.h index cccd36e06..206c5f601 100644 --- a/lbtt/src/SpotWrapper.h +++ b/lbtt/src/SpotWrapper.h @@ -1,6 +1,6 @@ /* * Copyright (C) 2003, 2004 - * Heikki Tauriainen + * Heikki Tauriainen * * Derived from SpinWrapper.h by Alexandre Duret-Lutz . * @@ -22,10 +22,6 @@ #ifndef SPOTWRAPPER_H #define SPOTWRAPPER_H -#ifdef __GNUC__ -#pragma interface -#endif /* __GNUC__ */ - #include #include #include "ExternalTranslator.h" @@ -144,4 +140,4 @@ inline void SpotWrapper::parseAutomaton(const string&, const string&) { } -#endif /* !SPINWRAPPER_H */ +#endif /* !SPOTWRAPPER_H */ diff --git a/lbtt/src/translate.cc b/lbtt/src/translate.cc index f2653c196..a1a6cc0a0 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 @@ -149,20 +149,20 @@ int main(int argc, char** argv) case OPT_HELP : cout << string("Usage: ") << command_line_arguments[0] << " [translator] [command line for translator] [formula " - "file] [automaton file]\n" - "General options:\n" - " --h, --help Show this help\n" - " --V, --version Show version and exit\n\n" - "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 " - "execute, together\n" - "with any optional parameters to be passed to the " - "program.\n\n"; + "file] [automaton file]\n" + "General options:\n" + " -h, --help Show this help\n" + " -V, --version Show version and exit\n\n" + "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 " + "execute, together\n" + "with any optional parameters to be passed to the " + "program.\n\n"; exit(0); break;