2004-02-11 Alexandre Duret-Lutz * src/SpotWrapper.cc (SpotWrapper::SPOT_AND, SpotWrapper::SPOT_OR): Define as && and || as in Spin. * src/SpotWrapper.hh: Update by email. 2003-07-10 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. 2003-07-09 Alexandre Duret-Lutz * 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. 2004-08-02 Heikki Tauriainen * Version 1.1.2 released. 2004-08-01 Heikki Tauriainen * src/TestOperations.cc (generateBuchiAutomaton): Use process groups to terminate the child process along with all of its children (if any) on timeouts. Do not write the time elapsed before a timeout into the log file. * configure.ac: Add test for the setsid library function. 2004-07-31 Heikki Tauriainen * src/Product.h (ProductEdge::edge_1, ProductEdge::edge_2): Change type to GraphEdgeContainer::const_iterators to move all edge dereference operations to member functions instead of the class constructor (where dereferencing is not always safe). (ProductEdge::ProductEdge, ProductEdge::firstComponent) (ProductEdge::secondComponent, ProductEdge::targetNode): Change member initialization and access accordingly. * configure.ac, NEWS, README: Update version. 2004-07-30 Heikki Tauriainen * Version 1.1.1 released. 2004-07-30 Heikki Tauriainen * src/TestOperations.cc (generateBuchiAutomaton): Protect against referencing a null pointer returned by strsignal on some platforms. (performBuchiIntersectionCheck): Handle product size exceptions gracefully. Skip redundant writes to an unopened transcript file. * configure.ac: Update version. * NEWS: Update. * README: Update. 2004-07-16 Alexandre Duret-Lutz * configure.ac: Call AC_GNU_SOURCE to make glibc's strsignal definition visible even to non-GNU compilers. 2004-07-07 Heikki Tauriainen * Version 1.1.0 released. 2004-07-06 Heikki Tauriainen * configure.ac: Make detection of the need for obstack.h compilation workaround with glibc 2.3.2 more accurate. Remove check for single_client_alloc. * src/LbttAlloc.h: Remove conditional definition of the ALLOC macro. * src/UserCommandReader.cc: Remove workaround for compilation with gcc 2.95. 2004-07-02 Heikki Tauriainen * doc/texinfo.tex: New upstream version. * doc/lbtt.texi: Update to edition 1.1.0. * NEWS: Update. 2004-07-02 Heikki Tauriainen * src/UserCommandReader.cc (parseCommand): Recognize `implementations' and `translators' as aliases of the `algorithms' command. * src/UserCommands.cc (printCommandHelp): List `implementations' and `translators' as aliases of the `algorithms' command. 2004-06-30 Heikki Tauriainen * src/Configuration.h (CommandLineOptionType): Rearrange the values to list constants with an explicit character value first. Change the value of OPT_VERSION to `V'. * src/Configuration.cc (Configuration::read): Treat the single- character option `V' as an alias of the `--version' option. (Configuration::showCommandLineHelp): Describe the `-V' option. * src/translate.cc (main): Rename the single character option `v' to `V'. 2004-06-29 Heikki Tauriainen * src/BuchiAutomaton.h (BuchiAutomaton::regularize) (BuchiAutomaton::intersect): Remove. (BuchiAutomaton::BuchiTransition::print(_, _, _)): Override the corresponding virtual function in parent class explicitly. * src/BuchiAutomaton.cc (BuchiAutomaton::regularize) (BuchiAutomaton::intersect): Remove. 2004-05-31 Heikki Tauriainen * src/LtlFormula.h: Do not include the map header. Include the set header instead. (LtlFormula::refcount): New variable. (LtlFormula::formula_storage): Change type to a set of pointers to LtlFormulas. (LtlFormula::LtlFormula): Initialize `this->refcount' to 1. Do not initialize `info_flags' explicitly (this is always done in subclasses). (LtlFormula::destruct): Update the reference counts of formulas directly. (LtlFormula::clone, LtlFormula::insertToStorage): Likewise. (Atom::Atom): Do not call parent class constructor explicitly. (UnaryFormula::UnaryFormula): Likewise. (BinaryFormula::BinaryFormula): Likewise. * src/LtlFormula.cc: Update definition of the static member `LtlFormula::formula_storage'. * src/FormulaRandomizer.h: Include the map header. 2004-05-19 Heikki Tauriainen * configure.ac (BIGUINT): Define as unsigned long long int if the compiler supports it (unsigned long int otherwise). * src/TestStatistics.h (TestStatistics::total_number_of_buchi_states) (TestStatistics::total_number_of_buchi_transitions) (TestStatistics::total_number_of_acceptance_sets) (TestStatistics::total_number_of_product_states) (TestStatistics::total_number_of_product_transitions): Change type to BIGUINT. (TestStatistics::total_number_of_msccs): Remove. (TestStatistics::TestStatistics): Remove initialization of `total_number_of_msccs'. * src/StatDisplay.cc (printCollectiveStats): Use BIGUINTs for referencing total state, transition and acceptance set counts. 2004-05-18 Heikki Tauriainen * src/ProductAutomaton.h, src/ProductAutomaton.cc, src/SccIterator.h: Remove. The functionality provided by these files has been rearranged into more general product computation and emptiness checking routines in: * src/Product.h, src/SccCollection.h: New files. * src/BuchiProduct.h, src/BuchiProduct.cc, src/StateSpaceProduct.h: New files for providing specializations of the general product computation operation applicable to Büchi automata and state spaces. * src/Makefile.am: Add BuchiProduct.h, BuchiProduct.cc, Product.h, SccCollection.h and StateSpaceProduct.h to lbtt_SOURCES. Remove ProductAutomaton.h, ProductAutomaton.cc and SccIterator.h from lbtt_SOURCES. * src/Graph.h.in (Graph::EdgeContainerType, Graph::Path): New type definitions. (Graph::PathElement): New class. * src/PathEvaluator.h (evaluate): Change prototype to accept a path prefix and a cycle as parameters. * src/PathEvaluator.cc (evaluate): Rewrite to support the changed prototype. * src/TestRoundInfo.h: Do not include the ProductAutomaton.h header. (TestRoundInfo::product_automaton): Remove. (TestRoundInfo::TestRoundInfo): Remove initialization of `product_automaton'. * src/TestStatistics.h: Do not include the ProductAutomaton.h header. Include the EdgeContainer.h and Graph.h headers. (AutomatonStats::number_of_product_states): Change type to Graph::size_type. * src/main.cc (testLoop): Remove references to `round_info.product_automaton' and `generateProductAutomaton'. * src/TestOperations.h (generateProductAutomaton): Remove. * src/TestOperations.cc: Include the BuchiProduct.h, Product.h, SccCollection.h and StateSpaceProduct.h headers. Do not include the ProductAutomaton.h and SccIterator.h headers. Define static members of Product and Product. (generateProductAutomaton): Remove. (performEmptinessCheck): Display output messages from the removed `generateProductAutomaton' function here. Do the same for updating product automaton statistics. Use the Product interface for constructing the product and checking it for emptiness. (performBuchiIntersectionCheck): Use the Product interface for constructing the intersection of Büchi automata and checking it for emptiness. * src/UserCommandReader.cc: Do not include the ProductAutomaton.h header. (executeUserCommands): Remove the variables `product_automaton' and `last_computed_product_automaton'. * src/UserCommands.h: Do not include the ProductAutomaton.h header. Include the EdgeContainer.h, Graph.h and Product.h headers. (computeProductAutomaton): Remove. (synchronizePrefixAndCycle): Remove. (printCrossComparisonAnalysisResults): Remove `product_automaton' and `last_product_automaton' from prototype. (printPath): Change the types of `prefix' and `cycle' to constant references to StateSpace::Path objects. (printAcceptingCycle). Expect also a prefix and cycle of a state space as parameters. Represent the path segments as constant references to {BuchiAutomaton,StateSpace}::Path objects. * src/UserCommands.cc: Include the BuchiProduct.h, Product.h and StateSpaceProduct.h headers. (computeProductAutomaton): Remove. (synchronizePrefixAndCycle): Remove. (printCrossComparisonAnalysisResults): Update parameter list and documentation. Use the Product interface for constructing and analyzing a witness for the nonemptiness of a product automaton. (printAutomatonAnalysisResults): Use the Product interface for constructing and analyzing a witness for the nonemptiness of the intersection of two Büchi automata. (printPath): Update parameter list and documentation. Standardize the output to resemble that produced by printAcceptingCycle. (printAcceptingCycle): Update parameter list and documentation. Display all relevant information about an accepting execution of a Büchi automaton. 2004-05-18 Heikki Tauriainen * configure.ac (YACC): Do not add `-d' here. * src/Makefile.am: Rearrange to make future updates easier. (BUILT_SOURCES): New variable. (AM_YFLAGS): New variable for adding the `-d' flag to be passed to YACC. Move Config-parse.h and NeverClaim-parse.h from EXTRA_lbtt_SOURCES and EXTRA_lbtt_translate_SOURCES to BUILT_SOURCES. Thanks to Alexandre Duret-Lutz for patches. 2004-05-13 Heikki Tauriainen * configure.ac: Add checks for the sys/times.h and sys/wait.h headers. Add checks for the strerror, mkstemp, open, read, write, close, popen, pclose, pipe, fork, execvp, getpid, waitpid, alarm, sigaction, sigprocmask, sigemptyset, sigaddset, times, sysconf, and strsignal library functions. Remove check for the return type of signal. 2004-05-13 Heikki Tauriainen * src/NeverClaim-lex.ll: Add %option nounput to avoid a compiler warning. * src/ExternalTranslator.h: Include the TempFsysName.h header. (ExternalTranslator::TempFileObject): Remove. (ExternalTranslator::registerTempFileObject): Change prototype to match that of TempFsysName::allocate. (ExternalTranslator::temporary_file_objects): Change to a stack of pointers to TempFsysName objects. * src/ExternalTranslator.cc (ExternalTranslator::registerTempFileObject): Use the TempFsysName interface for creating temporary names. (ExternalTranslator::translate): Handle temporary file names as C-style strings. (ExternalTranslator::TempFileObject): Remove. * src/translate.cc: Make `translator' a static variable. (signalHandler): Delete `translator' if necessary to remove any temporary files before aborting. Restore the default signal handler using sigaction. (installSignalHandler): New function. (main): Fix the number of dashes in the descriptions of single-character command line options. Install handler for signals that terminate the process. * src/Makefile.am: Add TempFsysName.h and TempFsysName.cc to lbtt_translate_SOURCES. 2004-05-12 Heikki Tauriainen * src/Graph.h.in (Graph::Edge) Fix return type of targetNode() and the type of the `target_node' variable to allow compilation with gcc 3.4.0. (Graph::stats): Fix type definition of `result' to allow compilation with gcc 3.4.0. * src/FormulaWriter.h: Include the LtlFormula.h header to allow compilation with gcc 3.4.0. Remove forward declarations of class LtlFormula and class Atom. 2004-03-18 Heikki Tauriainen * src/UserCommandReader.cc (executeUserCommands): Print a newline after each nonempty input line regardless of whether the line consists only of an external command or not. Don't print a newline after piping the output of a command to an external program. Print a newline after the output of a command. Do not interpret failures when writing to pipe as errors to allow external programs to ignore some of the input. * src/UserCommands.cc (printAlgorithmList) (printCrossComparisonAnalysisResults) (printConsistencyAnalysisResults, printAutomatonAnalysisResults) (printAcceptingCycle, printBuchiAutomaton, evaluateFormula) (printCommandHelp, printInconsistencies, printStateSpace): Remove extra newlines from the end of output. * src/StatDisplay.cc (printBuchiIntersectionCheckStats): Remove extra newlines from the end of output. * src/TestOperations.cc (performBuchiIntersectionCheck): Print a newline after the results to transcript file and to console in verbosity modes >= 3. 2004-03-17 Heikki Tauriainen * src/BuchiAutomaton.h: Include the cstdlib header. Fix description of the BuchiAutomaton class. (BuchiAutomaton::connect): Add parameters for the acceptance sets associated with a transition. (BuchiAutomaton::BuchiTransition::BuchiTransition): Add parameters for the acceptance sets associated with a transition. Remove copy constructor. (BuchiAutomaton::BuchiTransition::print): Remove default values for arguments. Add parameter for the number of acceptance sets associated with a transition. (BuchiAutomaton::BuchiTransition::acceptanceSets) New functions. (BuchiAutomaton::BuchiTransition::acceptance_sets): New variable. * src/BuchiAutomaton.cc (BuchiAutomaton::BuchiAutomaton(const BuchiAutomaton&): Copy also the acceptance sets of each transition. (BuchiAutomaton::operator=): Copy also the acceptance sets of each transition. (BuchiAutomaton::regularize): Handle also acceptance sets on transitions. (BuchiAutomaton::read): Update description. Accept automata with acceptance sets on states and/or transitions. (BuchiAutomaton::intersect): Take care of acceptance sets associated with transitions when forming the intersection of two automata. (BuchiAutomaton::print): Change output to refer to "acceptance sets" instead of "sets of accepting states". Pass the number of acceptance sets to BuchiAutomaton::BuchiTransition::print when displaying the automaton in dot format. (BuchiAutomaton::BuchiTransition::print): List the acceptance sets associated with each transition in all output modes. (BuchiAutomaton::BuchiState::print): Pass the number of acceptance sets to BuchiAutomaton::BuchiTransition::print. 2004-03-15 Heikki Tauriainen * src/UserCommands.h (printFormula): Change prototype to accept the vector of input tokens as an additional parameter. * src/UserCommands.cc (printFormula): Accept the vector of input tokens as an additional parameter. Use the optional parameter "nnf" or "normal" to choose the display mode. Display only the formula to accommodate feeding the output (if redirected to a file) back to lbtt using the --formulafile command line option. (printCommandHelp): Update the description of the `formula' command. * src/UserCommandReader.cc (executeUserCommands): Accept one optional parameter for the `formula' command. Pass the input tokens as an additional parameter in the printFormula call. Print an additional newline after the call if the output is not redirected to a file. 2004-03-12 Heikki Tauriainen * src/Exception.h: Include the istream header. (Exceptional_istream::get, Exceptional_istream::read): New functions. * src/Ltl-parse.yy: New file. * src/LtlFormula.h (parseFormula): Declare. (LtlFormula::read(istream&)): Read the formula by calling parseFormula (provided by Ltl-parse.yy). (LtlFormula::read(Exceptional_istream&)): Remove. * src/LtlFormula.cc (LtlFormula::read(Exceptional_istream&)): Remove. * src/Makefile.am: Add Ltl-parse.yy to lbtt_SOURCES and lbtt_translate_SOURCES. 2004-03-08 Heikki Tauriainen * src/TempFsysName.h, src/TempFsysName.cc New files. * src/Makefile.am: Add TempFsysName.h and TempFsysName.cc to lbtt_SOURCES. * src/TestRoundInfo.h: Include the TempFsysName.h header. (TestRoundInfo::formula_file_name[]) (TestRoundInfo::automaton_file_name) (TestRoundInfo::{cout,cerr}_capture_file): Change type to TempFsysName*. (TestRoundInfo::TestRoundInfo): Initialize temporary file name pointers to 0. * src/main.cc: Include the TempFsysName.h header. (allocateTempFilenames, deallocateTempFilenames): New functions. (abortHandler): New signal handler. (installSignalHandler): New function. (testLoop): Do not explicitly remove the temporary formula files. (main): Use the above functions for allocating and deallocating names for temporary files. Handle signals that terminate the process by cleaning up temporary files before aborting; however, for SIGINT, do this only if user breaks are not handled by lbtt. * src/TestOperations.h (removeFile): Rename as truncateFile. * src/TestOperations.cc: Include the TempFsysName.h header. (removeFile): Rename as truncateFile; truncate file instead of removing it. (writeFormulaeToFiles): Use the TempFsysName interface for referring to the names of temporary files. (generateBuchiAutomaton): Truncate all temporary files before exec'ing an external process. Use the TempFsysName interface for referring to the names of temporary files. * src/ExternalTranslator.cc: Include the cstring header. (ExternalTranslator::TempFileObject::TempFileObject): Use mkstemp instead of tmpnam to allocate a name for a temporary file. 2004-03-08 Heikki Tauriainen * src/StringUtil.h (findInQuotedString): New function prototype. * src/StringUtil.cc (findInQuotedString): New function. * src/UserCommandReader.cc (executeUserCommands): [HAVE_READLINE] Add the input line to history before extracting the external command from the line. Ignore white space within quotes when splitting input line into tokens. Move parsing the algorithm identifiers given for the `buchianalysis' command to src/UserCommands.cc (printAutomatonAnalysisResults). (parseRedirection): Explicitly unquote the file name. * src/UserCommands.h: Include the map and the IntervalList.h headers. (parseAlgorithmId, parseAlgorithmIdList): New function prototypes. (printAutomatonAnalysisResults): Change function prototype to accept a list of tokens instead of two algorithm identifiers. * src/ProductAutomaton.h: Include the string header. Rewrite the friend declaration of UserCommands::printAutomatonAnalysisResults. * src/UserCommands.cc (parseAlgorithmId, parseAlgorithmIdList): New functions. (printCrossComparisonAnalysisResults) (printConsistencyAnalysisResults): Parse algorithm identifier using the parseAlgorithmId function. (printAutomatonAnalysisResults): Parse algorithm identifiers using the parseAlgorithmId function. Throw a CommandErrorException in the case one of the algorithm identifiers refers to lbtt's internal model checking algorithm. (printBuchiAutomaton): Parse algorithm identifier using the parseAlgorithmId function. Throw a CommandErrorException in the case the identifier refers to lbtt's internal model checking algorithm. (printCommandHelp): Do not treat the internal model checking algorithm as a special case in command descriptions. (evaluateFormula, printInconsistencies, printTestResults) (printStateSpace, changeAlgorithmState): Parse lists of algorithms and states using the parseAlgorithmIdList and the StringUtil::parseIntervalList functions, respectively. Access the numeric algorithm and state identifiers via IntervalLists. Make error messages more consistent. 2004-03-07 Heikki Tauriainen * src/StatDisplay.h: Include the IntervalList.h header. (printStatTableHeader): New function prototype. (printCrossComparisonStats, printBuchiIntersectionCheckStats): Change the function prototypes to accept a reference to an IntervalList for the algorithm identifiers. * src/StatDisplay.cc (printStatTableHeader): New function. * src/StatDisplay.cc (printBuchiAutomatonStats) (printProductAutomatonStats, printAcceptanceCycleStats) (printConsistencyCheckStats): Display statistics in a table in verbosity mode <= 2. (printCrossComparisonStats): Iterate over the set of algorithms using an IntervalList. Do not handle the internal model checking algorithm as a special case. (printBuchiIntersectionCheckStats) Iterate over the set of algorithms using an IntervalList. Skip the internal model checking algorithm when displaying automata generation or intersection check statistics. (printAllStats): Display statistics in a table in verbosity mode <= 2. (printCollectiveStats): Skip the internal algorithm when displaying the rows of the cross-comparison result table. Use the changed semantics of Configuration::AlgorithmInformation to find the name of an implementation. * src/main.cc (testLoop): Display test statistics in a table in verbosity modes 1 and 2. * src/TestOperations.cc: Include the IntervalList.h header. Remove inclusion of the TestStatistics.h header. (generateBuchiAutomaton, generateProductAutomaton) (performEmptinessCheck): Display the test statistics in a table in verbosity modes 1 and 2. (compareResults, performBuchiIntersectionCheck): Display the result of the test also in verbosity mode 2. Show test statistics using the changed semantics of StatDisplay::printCrossComparisonStats and StatDisplay::printBuchiIntersectionCheckStats. (verifyFormulaOnPath, generateProductAutomaton) (performEmptinessCheck, performBuchiIntersectionCheck): More consistent error messages when the test is aborted. * src/UserCommands.cc (evaluateFormula): Use the changed semantics of Configuration::AlgorithmInformation to find the name of an implementation. (printTestResults): Display the test results using the changed semantics of StatDisplay::printCrossComparisonStats and StatDisplay::printBuchiIntersectionCheckStats. 2004-03-04 Heikki Tauriainen * src/TestOperations.h (openFile(const char*, int&, int, int)): New function prototype. * src/TestOperations.cc: Include the csignal, cstring, cerrno, [HAVE_SYS_TYPES_H] sys/types.h, [HAVE_SYS_STAT_H] sys/stat.h, [HAVE_FCNTL_H] fcntl.h, and [HAVE_SYS_WAIT_H] sys/wait.h headers. (timeout): New variable. (timeoutHandler): New function. (openFile(const char*, int&, int, int)): New function. (verifyFormulaOnPath): Fix references to the internal model checking algorithm. (generateBuchiAutomaton): Execute external program using fork/exec instead of `system' to improve the detection of the case when an external program was terminated by a signal (the behavior of "system" in the presence of signals varies between architectures). Handle timeouts when running the external programs. Discard I/O exceptions while displaying the stdout/stderr capture file. (performBuchiIntersectionCheck): Skip the internal model checking algorithm when iterating over algorithms. 2004-03-04 Heikki Tauriainen * src/main.cc (breakHandler): Make function static and change return type to void. (testLoop): Do not add the internal model checking algorithm to the list of implementations (it is done in Configuration::read). Apply the internal model checking algorithm if it is enabled. Otherwise skip the automata generation loop as it is not applicable for this algorithm. (main): Enable interrupt handler only if mandated by the program configuration. Use sigaction instead of signal to register the signal handler. 2004-03-04 Heikki Tauriainen * src/Config-lex.ll, src/Config-parse.yy, src/Configuration.h, src/Configuration.cc: Rewrite the configuration file parser to allow reusing a common set of functions for changing the various settings independently of whether the settings were given in the configuration file or as command-line options. Rearrange the structure of Configuration::AlgorithmInformation, remove the "nopause" and "pauseonbreak" command line options (and make "pause" an alias of "interactive"), recognize lists of interactivity modes (with the new mode "onbreak") both in the configuration file and command line, and add the new configuration setting "translatortimeout". In more detail, the changes are: * src/Config-lex.ll: Do not include any standard headers. Add %option nounput to suppress a compiler warning. Accept "Implementation" or "Translator" as an alias of the Algorithm block identifier. Do not accept newlines in "option = value" strings. Do not interpret option values in the lexer. Make specifying option values more flexible: quotes are now needed only for values including white space. Both single and double quotes may be used (as before, \ works as an escape character in double quotes). Reject values with unmatched quotes. Remove the getCharacter function (add rules for matching unknown tokens in full). * src/Config-parse.yy: Do not include the cstdio header. Add namespace StringUtil to the current namespace. ([declarations]) Change %union declaration to make all semantic values constant C-style strings. Remove tokens CFG_TRUTH_VALUE, CFG_INTERACTIVITY_VALUE, CFG_FORMULA_MODE_VALUE, CFG_STATESPACE_MODE_VALUE, CFG_PRODUCT_TYPE_VALUE, CFG_INTEGER, CFG_REAL, CFG_INTEGER_INTERVAL and CFG_STRING_CONSTANT. Add new token CFG_VALUE and nonterminal equals_value. (algorithm_information): Replaced with `algorithm_name', `algorithm_path', `algorithm_parameters' and `algorithm_enabled'. (current_block_type, current_option_type): Removed. (yyerror): Make parameter const. Remove the loop for reading the remainder of the current token (the token is recognized in full directly by the lexer). Remove error messages for all tokens in the above list. (checkIntegerRange, checkProbability, isLocked): Removed. ([grammar rule `equals_value']): New rule. ([grammar rules for the "Algorithm" configuration file section]): Read the implementation information into `algorithm_name', `algorithm_path', `algorithm_parameters' and `algorithm_enabled'. Use the functions provided by the Configuration class to update the configuration. ([grammar rules for the other configuration file sections]): Use the functions provided by the Configuration class to update the configuration. Remove the rules `formula_size' and `statespace_size'. * src/Configuration.h: Include the cstdio header. Add declarations for variables and functions provided by the parser. Declare yyparse() as a friend. (Configuration::AlgorithmInformation::path_to_program) (Configuration::IntPair, Configuration::locked_options) (Configuration::GENERATION_RANGE, Configuration::PRIORITY_RANGE) (Configuration::PROPOSITION_COUNT_RANGE) (Configuration::FORMULA_SIZE_RANGE) (Configuration::FORMULA_MAX_SIZE_RANGE) (Configuration::STATESPACE_SIZE_RANGE) (Configuration::STATESPACE_MAX_SIZE_RANGE) (Configuration::OPT_NOCOMPARISONTEST) (Configuration::OPT_NOCONSISTENCYTEST) (Configuration::OPT_NOINTERSECTIONTEST) (Configuration::OPT_NOABBREVIATEDOPERATORS) (Configuration::OPT_PAUSE, Configuration::OPT_NOPAUSE) (Configuration::OPT_PAUSEONERROR): Remove. (Configuration::AlgorithmInformation::extra_parameters): Redefine as `char** parameters'. (Configuration::AlgorithmInformation::num_parameters) (Configuration::GlobalConfiguration::handle_breaks) (Configuration::GlobalConfiguration::translator_timeout) (Configuration::algorithm_names: New variables. (Configuration::IntegerRange): Change the type of lower and upper bounds to unsigned long int. Make `error_message' const. (Configuration::DEFAULT_RANGE, Configuration::RANDOM_SEED_RANGE) (Configuration::ATOMIC_PRIORITY_RANGE) (Configuration::OPERATOR_PRIORITY_RANGE): New IntegerRange declarations. (Configuration::OPT_TRANSLATORTIMEOUT): New OPT_ constant. (Configuration::registerAlgorithm, Configuration::readProbability) (Configuration::readSize, Configuration::readTruthValue) (Configuration::readInteractivity, Configuration::readProductType) (Configuration::readFormulaMode, Configuration::readStateSpaceMode) (Configuration::readTranslatorTimeout): New function prototypes. (Configuration::isInternalAlgorithm): New function. (Configuration::readInteger): New template function. * src/Configuration.cc: Do not include the cstdio and Config-parse.h headers. Include the IntervalList.h header. Remove declarations for checkIntegerRange and checkProbability. Move remaining extern declarations to Configuration.h. (Configuration::GENERATION_RANGE, Configuration::PRIORITY_RANGE) (Configuration::PROPOSITION_COUNT_RANGE) (Configuration::FORMULA_SIZE_RANGE) (Configuration::FORMULA_MAX_SIZE_RANGE) (Configuration::STATESPACE_SIZE_RANGE) (Configuration::STATESPACE_MAX_SIZE_RANGE) (Configuration::parseCommandLineInteger): Remove. (Configuration::DEFAULT_RANGE, Configuration::RANDOM_SEED_RANGE) (Configuration::ATOMIC_PRIORITY_RANGE) (Configuration::OPERATOR_PRIORITY_RANGE): New IntegerRange definitions. (Configuration::ROUND_COUNT_RANGE): Change upper bound to ULONG_MAX. (Configuration::~Configuration): Use the changed semantics of Configuration::AlgorithmInformation. (Configuration::read): The --{comparison,consistency,intersection}{test,check} and --abbreviatedoperators command line options now take an optional argument. The options --no{{comparison,consistency,intersection}{test,check}, abbreviatedoperators} return the same OPT_ constant as the corresponding positive option. The --interactive and --pause options take an optional argument. Remove the --nopause and --pauseonerror command line options. Store the command line parameters into a vector of pairs (preprocess the special options --configfile, --formulafile, --help, --logfile, --showconfig, --showoperatordistribution, --skip and --version; preprocess also the options accepting an optional argument). Then read the configuration file. Add the internal model checking algorithm to the set of algorithms if necessary here instead of in src/main.cc (testLoop). Finally process the parameter vector again to override any settings made in the configuration file. Use the new functions for modifying the configuration. Allow symbolic algorithm identifiers for the options --enable and --disable. Make error messages more consistent. Exit with the status 2 if an unknown command line option was encountered or an argument for an option was missing. (Configuration::print): Tell whether the user break handler is enabled; tell also the value of the timeout for translators. (Configuration::algorithmString): Use the new structure of Configuration::AlgorithmInformation. (Configuration::showCommandLineHelp): Rewrite the descriptions of the --{comparison,consistency,intersection}test, --abbreviatedoperators, --interactive and --pause command line options. Correct typos in the description of the --abbreviatedoperators option. Remove descriptions of the --nopause and --pauseonerror options. (Configuration::reset): Initialize the values of `global_options.handle_breaks' and `global_options.translator_timeout' to false and 0, respectively. (Configuration::registerAlgorithm): New function for adding a new implementation to the configuration. The names of implementations should be unique and different from the reserved name "lbtt". (Configuration::readProbability, Configuration::readSize) (Configuration::readTruthValue, Configuration::readInteractivity) (Configuration::readProductType, Configuration::readFormulaMode) (Configuration::readStateSpaceMode) (Configuration::readTranslatorTimeout): New functions. The interactivity can now be specified using a comma-separated list of modes that may include the new keyword "onbreak". 2004-03-02 Heikki Tauriainen * src/StringUtil.h (toLowerCase, unquoteString) (substituteInQuotedString, parseTime): New function prototypes. (QuoteMode): New enumeration type. * src/StringUtil.cc: Include the cctype header. (toLowerCase, interpretSpecialCharacters, unquoteString) (substituteInQuotedString, parseTime): New functions. 2004-02-19 Heikki Tauriainen * src/TestRoundInfo.h (TestRoundInfo::all_tests_successful): New variable. (TestRoundInfo::TestRoundInfo): Initialize the value of all_tests_successful to true. * src/main.cc (testLoop): Update the value of round_info.all_tests_successful to indicate the occurrence of an error. Use the value of this variable as return value from testLoop. (main): Return 1 if an error occurred during testing. Return 2 if there was an error in program configuration; remove extra space after colon in output. Return 3 if an unexpected exception occurred. In this case print an additional newline before the error message. 2004-02-19 Heikki Tauriainen * src/StringUtil.h: Include the IntervalList.h header. (IntervalStringType): New enumeration type for describing the boundedness of interval strings. (parseInterval): New function prototype. Renamed the old prototype to `parseIntervalList'. * src/StringUtil.cc: Include the climits header. (parseNumber): Be more strict about ensuring that the numbers are positive. (parseInterval): New function for parsing interval strings. (parseIntervalList): Use the `parseInterval' function as a subroutine when parsing a list of intervals. Add a parameter for optionally storing tokens not recognized as intervals into a vector of strings. Store the result into an IntervalList. Throw an IntervalRangeException if an interval does not fit within the given bounds. 2004-02-18 Heikki Tauriainen * src/IntervalList.h, src/IntervalList.cc: New files. * src/Makefile.am: Add IntervalList.h and IntervalList.cc to lbtt_SOURCES. 2004-02-17 Heikki Tauriainen * src/TestOperations.cc (writeFormulaeToFiles): Make the order of debugging messages (verbosity level 5) more consistent. 2004-02-15 Heikki Tauriainen * src/DispUtil.h (printText): Move function declarations to their correct place (out of struct StreamFormatting). 2004-02-15 Heikki Tauriainen * configure.ac: Require Autoconf 2.59. Remove use of deprecated macros. --with-readline-prefix, --with-readline-includes, --with-readline-libs: New options. 2004-02-13 Heikki Tauriainen * src/BitArray.{h,cc}, src/BuchiAutomaton.{h,cc}, src/Configuration.{h,cc}, src/DispUtil.{h,cc}, src/ExternalTranslator.{h,cc}, src/FormulaRandomizer.{h,cc}, src/LtlFormula.{h,cc}, src/NeverClaimAutomaton.{h,cc}, src/PathEvaluator.{h,cc}, src/PathIterator.{h,cc}, src/ProductAutomaton.{h,cc}, src/SpinWrapper.{h,cc}, src/StatDisplay.{h,cc}, src/StateSpace.{h,cc}, src/StateSpaceRandomizer.{h,cc}, src/StringUtil.{h,cc}, src/TestOperations.{h,cc}, src/TestStatistics.{h,cc}, src/translate.{h,cc}, src/UserCommandReader.{h,cc}, src/UserCommands.{h,cc}: Remove all #pragmas. * Version 1.0.3 released. 2004-02-12 Heikki Tauriainen * doc/texinfo.tex: New upstream version. * doc/lbtt.texi: Update edition to 1.0.2. Remove node names with commands to fix dvi file generation. Move the node about the lbtt-translate utility to correct menu. Reformat the automata file format section to avoid overfull lines in dvi generation. Fix description of the Algorithm block used with lbtt-translate. * doc/testprocedure.txt, doc/intersectioncheck.txt: Add initial newlines. 2004-02-11 Heikki Tauriainen * src/UserCommandReader.cc [HAVE_ISATTY]: Include the unistd.h header. (executeUserCommands) Stop waiting for new commands if an EOF is detected. [HAVE_ISATTY]: If standard input is not connected to a terminal, echo the input line. 2004-02-10 Heikki Tauriainen * configure.ac: Remove duplicate checks for headers. (GLIBC_OBSTACK_WORKAROUND): New config.h macro for checking for a version of the obstack.h header that requires a workaround to be compiled with g++. Add check for the `isatty' library function. Include the stdio.h header when testing for readline libraries. * src/Alloc.h: Rename to LbttAlloc.h to avoid a name conflict with system header files on Darwin. [GLIBC_OBSTACK_WORKAROUND] (__INT_TO_PTR): Redefine macro to work around a C++ bug in the obstack.h header file in glibc 2.3.2. Thanks to Alexandre Duret-Lutz for the original patch. * src/BuchiAutomaton.h, src/Configuration.h, src/DispUtil.cc, src/ExternalTranslator.h, src/FormulaRandomizer.h, src/Graph.h.in, src/LtlFormula.h, src/main.cc, src/Makefile.am, src/NeverClaimAutomaton.h, src/PathEvaluator.h, src/ProductAutomaton.h, src/SccIterator.h, src/SharedTestData.h, src/StatDisplay.h, src/StateSpace.h, src/StateSpaceRandomizer.cc, src/StringUtil.h, src/TestOperations.h, src/TestRoundInfo.h, src/TestStatistics.h, src/UserCommandReader.h, src/UserCommands.h: Adjust includes. * Update copyright information in source files. 2003-07-04 Alexandre Duret-Lutz * src/Config-parse.yy: Remove stray `,' in %token arguments. 2003-07-18 Heikki Tauriainen * UserCommands.cc (printAutomatonAnalysisResults): Ensure that the states in a witness for the nonemptiness of two Bûchi automata are distinct to prevent the truth valuation for the atomic propositions from being defined multiple times in any state of the witness. * Version 1.0.2 released. 2003-07-17 Heikki Tauriainen * NeverClaimAutomaton.cc (ParseErrorException::ParseErrorException): Fix a string buffer overflow. * ProductAutomaton.cc (findAcceptingExecution): Concatenate fragments of an accepting cycle in the correct order. (Thanks to Joachim Klein for pointing out an example uncovering the bug in previous releases.) 2002-11-04 Heikki Tauriainen * StatDisplay.cc (printCollectiveStats): If using more than five formula operators (but the total number of operators is not a multiple of 5), insert an empty line in the output before the last row of the operator distribution table. 2002-10-21 Heikki Tauriainen * BitArray.cc (BitArray::find): Fix bug in testing whether all accessed bytes were zero. 2002-10-01 Heikki Tauriainen * Version 1.0.1 released. 2002-01 -- 2002-09-25 Heikki Tauriainen * Alloc.h: Use preprocessor macro HAVE_SINGLE_CLIENT_ALLOC instead of HAVE_SGI_STL in #ifdef conditionals. * BitArray.cc (BitArray::BitArray): Do not clear the allocated array after initialization. All callers updated to reflect the changed constructor semantics. * BitArray.cc (BitArray::bitwiseAnd, BitArray::bitwiseOr) (BitArray::bitwiseXor): New functions. * BitArray.cc (BitArray::equal, BitArray::subset) (BitArray::count): Fix `&' operator precedence in comparisons. * BitArray.cc (BitArray::hammingDistance): Use the `bit_counts' array to compute the result instead of scanning the array bit by bit. * BitArray.cc: Documentation fixes. * BitArray.h (BitArray::bitwiseAnd, BitArray::bitwiseOr) (BitArray::bitwiseXor): New functions. * BitArray.h: Documentation fixes. * Bitset.h (Bitset::Bitset(const BitArray&, const unsigned long)) (Bitset::Bitset(const Bitset&)): Use `memcpy' instead of `BitArray::copy'. * Bitset.h (Bitset::operator=(const Bitset&)): Reallocate memory only if necessary. * Bitset.h: Documentation fixes. * BuchiAutomaton.cc (BuchiAutomaton::regularize): Changed semantics: instead of modifying the object itself, the function now returns a pointer to a newly allocated BuchiAutomaton (the regularized automaton). * BuchiAutomaton.cc: Documentation fixes. * BuchiAutomaton.h (BuchiAutomaton::regularize): Changed semantics (see above). * BuchiAutomaton.h (BuchiAutomaton::BuchiTransition::enabled(const BitArray&, const unsigned int)): New function. (BuchiAutomaton::BuchiTransition::enabled(const Bitset&)): Use the above function internally. * BuchiAutomaton.h (BuchiAutomaton::BuchiState::print(ostream&, const int, const GraphOutputFormat)): New function. * BuchiAutomaton.h (BuchiAutomaton::BuchiTransition::operator<) (BuchiAutomaton::BuchiTransition::operator==): Fix function prototypes to match those of the base class. Make functions private to prevent external comparison of plain Graph::Edges with BuchiAutomaton::BuchiTransitions. * Configuration.cc (Configuration::read): Use autoconf-generated PACKAGE_VERSION macro for displaying program version instead of including version.h. * configure.in: Renamed to configure.ac. Updated to Autoconf 2.53 and Automake 1.6. Improved checking for the presence of the slist STL extension. Revised checking for the availability of the GNU readline library and the libraries to include. Replace the old preprocessor macro HAVE_SGI_STL with new macros HAVE_SINGLE_CLIENT_ALLOC and HAVE_SLIST. Introduce new preprocessor macro SLIST_NAMESPACE. * EdgeContainer.h: Remove uses of redundant preprocessor macros. * Graph.h: Renamed to Graph.h.in to implement the optional inclusion of the slist header using an autoconf substitution variable. * Graph.h.in: Use HAVE_SLIST macro instead of HAVE_SGI_STL in #ifdef conditionals. * Graph.h.in (Graph::Edge, Graph::Node): Make classes public (to prevent warnings from Intel C++ Compiler). * Graph.h.in (Graph::operator[], Graph::node, Graph::size) (Graph::expand, Graph::stats, Graph::subGraphStats) (Graph::Edge::targetNode, Graph::Node::operator=) (operator<<(ostream&, const Graph::Edge&) (operator<<(ostream&, const Graph::Node&): Added explicit `typename' specifiers to parameter and/or return types (to prevent warnings from gcc 3.1). * Graph.h.in (Graph::subGraphStats): Make `s' a const variable. * Graph.h.in (Graph::Edge::ptr_equal::ptr_equal): Change definition to match that of `Graph::Edge::ptr_less'. All callers modified accordingly. * Graph.h.in (Graph::Edge::operator<, Graph::Edge::operator==): Make member functions protected. Make class Graph::Edge a friend of Graph::Edge::ptr_equal and Graph::Edge::ptr_less. * LtlFormula.cc (LtlFormula): New static variable `eval_proposition_id_limit' stores the maximum proposition id during the evaluation of a strictly propositional formula. * LtlFormula.cc (LtlFormula::sat_eval): Make `max_atom' a const variable. Access the identifier of a proposition through Atom::getId. * LtlFormula.h (LtlFormula::evaluate(const BitArray&, const unsigned long int)): New function. (LtlFormula::evaluate(const Bitset&)): Use the above function internally. * LtlFormula.h (ptr_less): Make class public. * LtlFormula.h (LtlFormula::eval): Use a BitArray instead of a Bitset internally. * LtlFormula.h (Atom::eval, Constant::eval, LtlNegation::eval) (UnaryFormula::eval, LtlNext::eval, LtlFinally::eval) (LtlGlobally::eval, BinaryFormula::eval, LtlDisjunction::eval) (LtlConjunction::eval, LtlImplication::eval, LtlEquivalence::eval) (LtlXor::eval, LtlUntil::eval, LtlV::eval, LtlWeakUntil::eval) (LtlStrongRelease::eval, LtlBefore::eval): Use BitArray instead of a Bitset for evaluation. Make subformula parameters (if any) `const'. * main.cc (testLoop): Use autoconf-generated PACKAGE_VERSION macro for displaying program version instead of including version.h. * src/Makefile.am: Remove redundant references to @LEXLIB@ (the sources are independent of any external lexer library). * NeverClaimAutomaton.cc (NeverClaimAutomaton::write): Add detection for jumps to undefined never claim labels. * NeverClaim-parse.yy (yyerror): Fix computation of the position of a parse error. * PathEvaluator.cc (PathEvaluator::eval) Avoid creating a temporary Bitset object during evaluation of atomic propositions. * ProductAutomaton.cc (ProductAutomaton::computeProduct): Avoid creating a temporary Bitset object when checking the enabledness of a product transition. * ProductAutomaton.cc (ProductAutomaton::findAcceptingExecution) Use BitArrays instead of Bitsets. * ProductAutomaton.h (ProductAutomaton::operator[]) (ProductAutomaton::node): Make state id parameter `const'. * ProductAutomaton.h (ProductAutomaton::ProductState::print): Change function prototype to match that of the base class. * SccIterator.h: Add `typename' specifiers to prevent warnings from gcc 3.1. * SpinWrapper.cc (SpinWrapper::SpinAutomaton::parseAutomaton): Remove redundant `try' block. * StateSpace.cc (StateSpace::State::print): Fix typo when displaying empty sets of propositions in dot format (the open brace was previously missing). * StateSpace.h (StateSpace::print(ostream&, const int, const GraphOutputFormat): New function. * TestOperations.cc (performEmptinessCheck): Added a colon to the end of the "Accepting cycles" message. * TestRoundInfo.h: Removed redundant inclusion of BitArray.h. * translate.cc (main): Use autoconf-generated PACKAGE_VERSION macro for displaying program version. * translate.cc (main): Fix bug in checking the number of command line arguments. * UserCommands.cc (printCrossComparisonAnalysisResults): Fix bug in the construction of the witness path in which the formula should be evaluated when the witness path is extracted directly from the original state space (i.e., when analyzing results against the internal model checking algorithm). * version.h.in: Removed. 2001-11-12 Heikki Tauriainen * Version 1.0.0 released.