From e11da2e3af07fb276563f2644489968d1d86ae5d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 7 Jul 2004 17:41:42 +0000 Subject: [PATCH] * lbtt/: Merge lbtt 1.1.0. * src/tgbatest/spotlbtt.test: Adjust config file syntax to please lbtt 1.1.0. --- ChangeLog | 4 + lbtt/ChangeLog | 775 +++++++++++++++++++++++- lbtt/src/ExternalTranslator.h | 120 +--- lbtt/src/Makefile.am | 60 +- lbtt/src/ProductAutomaton.cc | 1061 --------------------------------- lbtt/src/ProductAutomaton.h | 596 ------------------ lbtt/src/SccIterator.h | 752 ----------------------- lbtt/src/translate.cc | 75 ++- src/tgbatest/spotlbtt.test | 142 +++-- 9 files changed, 952 insertions(+), 2633 deletions(-) delete mode 100644 lbtt/src/ProductAutomaton.cc delete mode 100644 lbtt/src/ProductAutomaton.h delete mode 100644 lbtt/src/SccIterator.h diff --git a/ChangeLog b/ChangeLog index b5468de3f..6ed5996a2 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,9 @@ 2004-07-07 Alexandre Duret-Lutz + * lbtt/: Merge lbtt 1.1.0. + * src/tgbatest/spotlbtt.test: Adjust config file syntax to + please lbtt 1.1.0. + * src/tgbaalgos/gtec/gtec.hh (emptiness_check_shy::find_state): Add comments. * iface/gspn/ssp.cc (emptiness_check_shy_ssp::find_state): Likewise. diff --git a/lbtt/ChangeLog b/lbtt/ChangeLog index 641d21d29..517d7818b 100644 --- a/lbtt/ChangeLog +++ b/lbtt/ChangeLog @@ -1,37 +1,9 @@ -2004-03-09 Alexandre Duret-Lutz - - * src/Makefile.am (EXTRA_lbtt_SOURCES): Remove Config-parse.h, - it is automatically distributed. - (EXTRA_lbtt_translate_SOURCES): Likewise, remove NeverClaim-parse.h. - -2004-03-08 Alexandre Duret-Lutz - - * configure.ac (YACC): Do not add `-d' here... - * src/Makefile.am (AM_YFLAGS): ... do it here. - (BUILT_SOURCES): New variable. - - * doc/texinfo.tex: New upstream version. - 2004-02-11 Alexandre Duret-Lutz - * src/ExternalTranslator.cc: Include sys/wait.h. - * src/SpotWrapper.cc (SpotWrapper::SPOT_AND, SpotWrapper::SPOT_OR): Define as && and || as in Spin. * src/SpotWrapper.hh: Update by email. -2004-01-16 Alexandre Duret-Lutz - - * src/TestOperations.cc: Include sys/wait.h. - -2003-07-29 Alexandre Duret-Lutz - - * src/TestOperations.cc (generateBuchiAutomaton): Forward SIGINT - and SIGQUIT. - * src/ExternalTranslator.cc (ExternalTranslator::translate): Likewise. - * src/main.cc (main): Do not intercept SIGINT in - non-interactive runs. - 2003-07-10 Alexandre Duret-Lutz Spot wants `^', not `xor'. @@ -41,10 +13,6 @@ 2003-07-09 Alexandre Duret-Lutz - I want $? = 1 whenever some test fails. - * src/main.cc (testLoop): Return 1 iff an error occured. - (main): Use testLoop's output as exit status. - * src/ExternalTranslator.h (class ExternalTranslator): Declare class SpotWrapper as a friend. * src/SpotWrapper.h, src/SpotWrapper.cc: New files. @@ -53,6 +21,747 @@ * src/translate.cc (main): Add the --spot option, and build a SpotWrapper if required. +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}, @@ -67,6 +776,8 @@ 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. diff --git a/lbtt/src/ExternalTranslator.h b/lbtt/src/ExternalTranslator.h index b0f973a81..3a5a878eb 100644 --- a/lbtt/src/ExternalTranslator.h +++ b/lbtt/src/ExternalTranslator.h @@ -33,6 +33,7 @@ #include "Exception.h" #include "LtlFormula.h" #include "translate.h" +#include "TempFsysName.h" #include "TranslatorInterface.h" /****************************************************************************** @@ -98,13 +99,21 @@ * from the names of the input/output files. Each of these files should be * "registered" before calling the external program with the function * - * void registerTempFileObject - * (const string& filename, TempFileObject::Type t) + * const char* registerTempFileObject + * (const string& filename, const TempFsysName::NameType t, + * const bool literal) * - * where `filename' is the full name of the temporary file and `t' is a type - * of the object (TempFileObject::FILE or TempFileObject::DIRECTORY). + * where `filename' is the prefix of a temporary file name, `t' is a type + * of the object (TempFsysName::FILE or TempFsysName::DIRECTORY), and + * `literal' specifies whether `filename' should be interpreted literally or + * not (if not, `filename' will be treated as a suggestion for the name + * of the temporary file). If the name is to be interpreted literally, + * `filename' should contain the full path name of the temporary file to be + * created. In all cases, the function returns the full path name of the + * temporary file or directory, or it throws an IOException (defined in + * Exception.h) if the creation fails. * - * All files or directories registered using this function will then be + * All files or directories registered using this function will be * automatically deleted after the translation is finished or aborted. * The files or directories will be deleted in the reverse order of * registration, i.e., the most recently registered file/directory will be @@ -115,55 +124,15 @@ class ExternalTranslator : public TranslatorInterface { public: - /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ - - class TempFileObject /* A class for storing */ - { /* information about */ - public: /* temporary files and - * directories. - */ - - enum Type {FILE, DIRECTORY}; /* Types for a temporary - * file object. - */ - - TempFileObject /* Constructor. */ - (const string& filename = "", Type t = FILE); - - ~TempFileObject(); /* Destructor. */ - - const string& getName() const; /* Returns the filename - * associated with the - * object. - */ - - Type getType() const; /* Returns the type of - * the object. - */ - - private: - string name; /* Name of the file object. - */ - - Type type; /* Type of the file object. - */ - - TempFileObject(const TempFileObject&); /* Prevent copying and */ - TempFileObject& operator= /* assignment of */ - (const TempFileObject&); /* TempFileObjects. */ - }; - - /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ - ExternalTranslator(); /* Constructor. */ ~ExternalTranslator(); /* Destructor. */ - TempFileObject& registerTempFileObject /* Registers a temporary */ + const char* registerTempFileObject /* Registers a temporary */ (const string& filename = "", /* file or directory */ - TempFileObject::Type /* such that it will be */ - t = TempFileObject::FILE); /* automatically deleted - * when the translation + const TempFsysName::NameType /* such that it will be */ + t = TempFsysName::FILE, /* automatically deleted */ + const bool literal = false); /* when the translation * is complete. */ @@ -205,18 +174,13 @@ private: * objects. */ - stack > /* information. */ + stack > /* information. */ temporary_file_objects; - friend class KecWrapper; /* Friend declarations. */ - friend class Ltl2AutWrapper; - friend class Ltl2BaWrapper; - friend class ProdWrapper; - friend class SpinWrapper; + friend class SpinWrapper; /* Friend declarations. */ friend class SpotWrapper; - friend class WringWrapper; /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ @@ -317,46 +281,6 @@ inline bool ExternalTranslator::execSuccess(int exitcode) -/****************************************************************************** - * - * Inline function definitions for class ExternalTranslator::TempFileObject. - * - *****************************************************************************/ - -/* ========================================================================= */ -inline const string& ExternalTranslator::TempFileObject::getName() const -/* ---------------------------------------------------------------------------- - * - * Description: Returns the name associated with the - * ExternalTranslator::TempFileObject. - * - * Arguments: None. - * - * Returns: The name associated with the object. - * - * ------------------------------------------------------------------------- */ -{ - return name; -} - -/* ========================================================================= */ -inline ExternalTranslator::TempFileObject::Type -ExternalTranslator::TempFileObject::getType() const -/* ---------------------------------------------------------------------------- - * - * Description: Returns the type of the ExternalTranslator::TempFileObject. - * - * Arguments: None. - * - * Returns: The type associated with the object. - * - * ------------------------------------------------------------------------- */ -{ - return type; -} - - - /****************************************************************************** * * Inline function definitions for class diff --git a/lbtt/src/Makefile.am b/lbtt/src/Makefile.am index 3421b7b97..bc244ba83 100644 --- a/lbtt/src/Makefile.am +++ b/lbtt/src/Makefile.am @@ -3,55 +3,61 @@ AM_YFLAGS = -d bin_PROGRAMS = lbtt lbtt-translate lbtt_SOURCES = \ - BitArray.cc \ BitArray.h \ Bitset.h \ - BuchiAutomaton.cc \ + BitArray.cc \ BuchiAutomaton.h \ - Config-lex.ll \ + BuchiAutomaton.cc \ + BuchiProduct.h \ + BuchiProduct.cc \ Config-parse.yy \ - Configuration.cc \ + Config-lex.ll \ Configuration.h \ - DispUtil.cc \ + Configuration.cc \ DispUtil.h \ + DispUtil.cc \ EdgeContainer.h \ Exception.h \ - FormulaRandomizer.cc \ FormulaRandomizer.h \ + FormulaRandomizer.cc \ FormulaWriter.h \ + IntervalList.h \ + IntervalList.cc \ LbttAlloc.h \ - LtlFormula.cc \ LtlFormula.h \ + LtlFormula.cc \ + Ltl-parse.yy \ main.cc \ - PathEvaluator.cc \ PathEvaluator.h \ - PathIterator.cc \ + PathEvaluator.cc \ PathIterator.h \ - ProductAutomaton.cc \ - ProductAutomaton.h \ + PathIterator.cc \ + Product.h \ Random.h \ - SccIterator.h \ + SccCollection.h \ SharedTestData.h \ - StatDisplay.cc \ StatDisplay.h \ - StateSpace.cc \ + StatDisplay.cc \ StateSpace.h \ - StateSpaceRandomizer.cc \ + StateSpace.cc \ + StateSpaceProduct.h \ StateSpaceRandomizer.h \ - StringUtil.cc \ + StateSpaceRandomizer.cc \ StringUtil.h \ - TestOperations.cc \ + StringUtil.cc \ + TempFsysName.h \ + TempFsysName.cc \ TestOperations.h \ + TestOperations.cc \ TestRoundInfo.h \ - TestStatistics.cc \ TestStatistics.h \ - UserCommandReader.cc \ + TestStatistics.cc \ UserCommandReader.h \ - UserCommands.cc \ - UserCommands.h - + UserCommandReader.cc \ + UserCommands.h \ + UserCommands.cc EXTRA_lbtt_SOURCES = gnu-getopt.h -lbtt_LDADD = $(LIBOBJS) $(READLINELIBS) +lbtt_LDADD = @LIBOBJS@ @READLINELIBS@ lbtt_translate_SOURCES = \ BitArray.h \ @@ -60,10 +66,13 @@ lbtt_translate_SOURCES = \ ExternalTranslator.h \ ExternalTranslator.cc \ FormulaWriter.h \ + IntervalList.h \ + IntervalList.cc \ LbttAlloc.h \ LbtWrapper.h \ LtlFormula.h \ LtlFormula.cc \ + Ltl-parse.yy \ NeverClaim-parse.yy \ NeverClaim-lex.ll \ NeverClaimAutomaton.h \ @@ -74,9 +83,10 @@ lbtt_translate_SOURCES = \ SpotWrapper.cc \ StringUtil.h \ StringUtil.cc \ + TempFsysName.h \ + TempFsysName.cc \ translate.h \ translate.cc \ TranslatorInterface.h - EXTRA_lbtt_translate_SOURCES = gnu-getopt.h -lbtt_translate_LDADD = $(LIBOBJS) +lbtt_translate_LDADD = @LIBOBJS@ diff --git a/lbtt/src/ProductAutomaton.cc b/lbtt/src/ProductAutomaton.cc deleted file mode 100644 index c0513404a..000000000 --- a/lbtt/src/ProductAutomaton.cc +++ /dev/null @@ -1,1061 +0,0 @@ -/* - * Copyright (C) 1999, 2000, 2001, 2002 - * Heikki Tauriainen - * - * 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. - */ - -#ifdef __GNUC__ -#pragma implementation -#endif /* __GNUC__ */ - -#include -#include "ProductAutomaton.h" -#include "SccIterator.h" - -namespace Graph -{ - -/****************************************************************************** - * - * Function definitions for class ProductAutomaton. - * - *****************************************************************************/ - -/* ========================================================================= */ -void ProductAutomaton::clear() -/* ---------------------------------------------------------------------------- - * - * Description: Makes the automaton empty. - * - * Arguments: None. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ - buchi_automaton = 0; - statespace_size = 0; - -#ifdef HAVE_OBSTACK_H - for (vector::iterator state = nodes.begin(); - state != nodes.end(); - ++state) - static_cast(*state)->~ProductState(); - - if (!nodes.empty()) - { - store.free(*nodes.begin()); - nodes.clear(); - nodes.reserve(0); - } - -#endif /* HAVE_OBSTACK_H */ - - Graph::clear(); -} - -/* ========================================================================= */ -ProductAutomaton::size_type ProductAutomaton::expand(size_type node_count) -/* ---------------------------------------------------------------------------- - * - * Description: Inserts states to a ProductAutomaton. - * - * Argument: node_count -- Number of states to be inserted. - * - * Returns: The index of the last state inserted. - * - * ------------------------------------------------------------------------- */ -{ - nodes.reserve(nodes.size() + node_count); - - while (node_count > 0) - { -#ifdef HAVE_OBSTACK_H - void* state_storage = store.alloc(sizeof(ProductState)); - ProductState* new_product_state = new(state_storage) ProductState(); -#else - ProductState* new_product_state = new ProductState(); -#endif /* HAVE_OBSTACK_H */ - - try - { - nodes.push_back(new_product_state); - } - catch (...) - { -#ifdef HAVE_OBSTACK_H - new_product_state->~ProductState(); - store.free(state_storage); -#else - delete new_product_state; -#endif /* HAVE_OBSTACK_H */ - throw; - } - node_count--; - } - - return size() - 1; -} - -/* ========================================================================= */ -void ProductAutomaton::connect(const size_type father, const size_type child) -/* ---------------------------------------------------------------------------- - * - * Description: Connects two states of the product automaton. - * - * Arguments: father, child -- State identifiers. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ - Edge* edge = operator[](child).incoming_edge; - - if (edge != 0) - { - nodes[father]->outgoing_edges.insert(edge); - return; - } - -#ifdef HAVE_OBSTACK_H - void* edge_storage = store.alloc(sizeof(Edge)); - edge = new(edge_storage) Edge(child); -#else - edge = new Edge(child); -#endif /* HAVE_OBSTACK_H */ - - try - { - nodes[father]->outgoing_edges.insert(edge); - } - catch (...) - { -#ifdef HAVE_OBSTACK_H - edge->~Edge(); - store.free(edge_storage); -#else - delete edge; -#endif /* HAVE_OBSTACK_H */ - throw; - } - - operator[](child).incoming_edge = edge; -} - -/* ========================================================================= */ -void ProductAutomaton::disconnect - (const size_type father, const size_type child) -/* ---------------------------------------------------------------------------- - * - * Description: Disconnects two states of the product automaton. - * - * Arguments: father, child -- Identifiers for two states. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ - Edge e(child); - - /* - * Scan the set of `father''s outgoing transitions for a transition to the - * given target state and remove it if such a transition exists. - */ - - GraphEdgeContainer::iterator search_edge - = nodes[father]->outgoing_edges.find(&e); - - if (search_edge != nodes[father]->outgoing_edges.end()) - nodes[father]->outgoing_edges.erase(search_edge); -} - -/* ========================================================================= */ -void ProductAutomaton::print - (ostream& stream, const int indent, const GraphOutputFormat) const -/* ---------------------------------------------------------------------------- - * - * Description: Writes information about a product automaton to a stream. - * - * Arguments: stream -- A reference to an output stream. - * indent -- Number of spaces to leave to the left of output. - * - * The third (dummy) parameter is needed to support the - * function interface defined in the base class. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ - Exceptional_ostream estream(&stream, ios::failbit | ios::badbit); - - if (nodes.empty()) - estream << string(indent, ' ') + "The product automaton is empty.\n"; - else - { - pair statistics = stats(); - bool first_printed; - - estream << string(indent, ' ') + "The product automaton consists of\n" - + string(indent + 4, ' ') - << statistics.first - << " states and\n" + string(indent + 4, ' ') - << statistics.second - << " transitions.\n"; - - size_type s = nodes.size(); - for (size_type state = 0; state < s; ++state) - { - estream << string(indent, ' ') + "State " << state << ":\n" - + string(indent + 4, ' ') + "Automaton state: " - << buchiState(state) - << " (acceptance sets: {"; - - for (unsigned long int acceptance_set = 0; - acceptance_set < buchi_automaton->numberOfAcceptanceSets(); - acceptance_set++) - { - if ((*buchi_automaton)[buchiState(state)].acceptanceSets(). - test(acceptance_set)) - { - if (first_printed) - estream << ", "; - else - first_printed = true; - estream << acceptance_set; - } - } - - estream << "}\n" + string(indent + 4, ' ') + "System state: " - << systemState(state) - << '\n'; - - operator[](state).print(stream, indent + 4); - } - } - - estream.flush(); -} - -/* ========================================================================= */ -void ProductAutomaton::computeProduct - (const BuchiAutomaton& automaton, const StateSpace& statespace, - const bool global_product) -/* ---------------------------------------------------------------------------- - * - * Description: Initializes the synchronous product of a Büchi automaton and - * a state space. - * - * Arguments: automaton -- A reference to a constant BuchiAutomaton. - * statespace -- A reference to a constant StateSpace. - * global_product -- Controls whether the synchronous product - * of the automaton and the statespace is - * computed `globally' (i.e., with respect - * to all states in the state space) or - * `locally' (i.e., with respect only to the - * initial state of the state space). - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ - clear(); - - buchi_automaton = &automaton; - statespace_size = statespace.size(); - - /* - * If either the Büchi automaton or the state space is empty, their product - * is also empty. - */ - - if (automaton.empty() || statespace.empty()) - return; - - /* - * If the (worst-case) product of the size of the automaton and the state - * space size exceeds the maximum size of a product automaton, throw an - * exception (if this holds, the simple product state hashing technique - * used below will not work correctly). - */ - - if (automaton.size() > (nodes.max_size() / statespace.size())) - throw ProductSizeException(); - - /* - * Product states will be numerically encoded using the equation - * - * #P = #S + |S| * #B - * - * where - * |S| is the number of states in the state space, - * #P is an identifier of a product state, - * #S is an identifier of a state in the state space (0...|S|-1), - * #B is an identifier of a state in the Büchi automaton (0...|B|-1) - * and - * - * From this encoding we obtain - * #S = #P % |S|, and - * #B = #P / |S|. - */ - - map, ALLOC(size_type) > - product_state_mapping; - - /* - * Initialize the product automaton. If the product is to be computed - * globally, initialize the result with state pairs (q_0, s) where q_0 is - * the initial state of the Büchi automaton and s goes through all states - * in the state space. (These states will have the lowest indices in the - * product automaton, i.e. covering the index interval - * 0 ... [statespace.size() - 1] .) In the case of a local product, - * initialize the result with the single state (q_0, s_0), a pair consisting - * of the initial states of the two other structures. - * - * The final product automaton is obtained by computing the closure of this - * set of states under the product transition relation. For this purpose, - * a depth-first search will be used (with `mapping_stack' as the search - * stack; initially, it contains the same states as described above). - */ - - expand(global_product ? statespace.size() : 1); - - stack > mapping_stack; - - pair state_map_entry - = make_pair(automaton.initialState() * statespace_size, 0); - - for (state_map_entry.second = 0; - state_map_entry.second < (global_product ? statespace_size : 1); - ++state_map_entry.first, ++state_map_entry.second) - { - product_state_mapping.insert(state_map_entry); - mapping_stack.push(state_map_entry.first); - - operator[](state_map_entry.second).hashValue() = state_map_entry.first; - } - - /* - * Compute the product automaton by using a depth-first search. - */ - - const GraphEdgeContainer* automaton_transitions; - const GraphEdgeContainer* system_transitions; - - BuchiAutomaton::size_type current_automaton_state; - StateSpace::size_type current_system_state; - size_type current_product_state; - bool current_product_state_valid; - size_type current_mapping; - - try - { - while (!mapping_stack.empty()) - { - if (::user_break) - throw UserBreakException(); - - /* - * Pop a state mapping off the stack. - */ - - current_product_state_valid = false; - current_mapping = mapping_stack.top(); - mapping_stack.pop(); - - current_automaton_state = current_mapping / statespace_size; - current_system_state = current_mapping % statespace_size; - - /* - * Go through the transitions of the original Büchi automaton. For all - * transitions enabled in the current state of the state space: - * - * - Compute all product states that can be reached by firing the - * transition. These are the states (q', s') where q' is the - * state of the automaton after firing the transition and s' - * is a successor of the current state of the system. - * - * - If there is no corresponding product state for the state pair - * (q', s'), create a new product state and insert it into the - * product automaton. Push the mapping also on the stack so that - * the newly created product state will be eventually processed. - * - * - Connect the target product state to the current product state - * (in effect, storing information only about the _predecessors_ of - * each product state). This will result in a product space in - * which all edges are reversed. However, this is all that is - * needed since no information is needed about the successors of - * any product state when searching for the accepting cycles in the - * product graph (this will be performed using a backward search, - * see the functions `emptinessCheck' and - * `findAcceptingExecution'). - */ - - automaton_transitions = &automaton[current_automaton_state].edges(); - - for (GraphEdgeContainer::const_iterator - automaton_transition = automaton_transitions->begin(); - automaton_transition != automaton_transitions->end(); - ++automaton_transition) - { - if ((static_cast - (*automaton_transition))-> - enabled(statespace[current_system_state].positiveAtoms(), - statespace.numberOfPropositions())) - { - if (!current_product_state_valid) - { - current_product_state = product_state_mapping[current_mapping]; - current_product_state_valid = true; - system_transitions = &statespace[current_system_state].edges(); - } - - pair, ALLOC(size_type) > - ::iterator, - bool> - check_state; - - for (GraphEdgeContainer::const_iterator - system_transition = system_transitions->begin(); - system_transition != system_transitions->end(); - ++system_transition) - { - /* - * Compute a hash value for the target product state and test - * whether it has already been included in the product. - */ - - state_map_entry.first = - (*system_transition)->targetNode() - + statespace_size * (*automaton_transition)->targetNode(); - - check_state = product_state_mapping.insert(state_map_entry); - - if (check_state.second) /* insertion occurred */ - { - /* - * Create a new product state and adjust its hash value. - * `state_map_entry.second' holds the next free identifier for a - * new product state. - */ - - expand(); - - operator[](state_map_entry.second).hashValue() - = state_map_entry.first; - - connect(state_map_entry.second, current_product_state); - state_map_entry.second++; - - mapping_stack.push(state_map_entry.first); - } - else - { - size_type existing_state = (check_state.first)->second; - connect(existing_state, current_product_state); - } - } - } - } - } - } - catch (...) - { - clear(); - throw; - } -} - -/* ========================================================================= */ -void ProductAutomaton::emptinessCheck(Bitset& result) const -/* ---------------------------------------------------------------------------- - * - * Description: Performs an emptiness check on the product automaton, i.e. - * finds the set of system states starting an execution - * sequence accepted by the Büchi automaton. - * - * Argument: result -- A reference to the Bitset in which the result - * is stored. The Bitset must have enough space for - * as many states as there are in the state space. - * A `0' bit in some position n in the result means - * that no accepting executions begin from system - * state n; a `1' bit means the opposite. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ - BitArray visited(nodes.size()); - visited.clear(nodes.size()); - - result.clear(); - - /* - * Scan the maximal strongly connected components of the product space to - * find any fair MSCCs (nontrivial MSCCs containing an accepting cycle of - * the Büchi automaton used for constructing the product). Note that - * although the product space contains only back edges (i.e., we are - * actually scanning the product space with all edges reversed), the - * reversal of the edges does not affect the MSCCs of the product space. - */ - - for (SccIterator - strongly_connected_component(*this); - !strongly_connected_component.atEnd(); - ++strongly_connected_component) - { - if (::user_break) - throw UserBreakException(); - - if (strongly_connected_component->fair(*this)) - { - /* - * Search for a previously unvisited state in the strongly connected - * component. - */ - - ProductScc::const_iterator st; - for (st = strongly_connected_component->begin(); - st != strongly_connected_component->end() && visited[*st]; - ++st) - ; - - if (st != strongly_connected_component->end()) - { - /* - * Starting from the unvisited state, perform a backward depth-first - * search to find all states (q_0, s) such that q_0 is the initial - * state of the automaton (the product states (q_0, s) are recognized - * by the product state numbering scheme, in which these states have - * the lowest indices). Add the corresponding system states to the - * result (these are the system states from which the nontrivial MSCC - * containing the accepting cycle can be reached). - */ - - size_type state = *st; - stack > - backward_search_stack; - const GraphEdgeContainer* predecessors; - - visited.setBit(state); - backward_search_stack.push(state); - - while (!backward_search_stack.empty()) - { - state = backward_search_stack.top(); - backward_search_stack.pop(); - - if (state < result.capacity() && state < statespace_size) - result.setBit(systemState(state)); - - predecessors = &(operator[](state).edges()); /* note that only back - * edges are stored in - * the product! */ - - for (GraphEdgeContainer::const_iterator predecessor - = predecessors->begin(); - predecessor != predecessors->end(); - ++predecessor) - { - if (!visited[(*predecessor)->targetNode()]) - { - backward_search_stack.push((*predecessor)->targetNode()); - visited.setBit((*predecessor)->targetNode()); - } - } - } - } - } - } -} - -/* ========================================================================= */ -void ProductAutomaton::findAcceptingExecution - (const StateSpace::size_type initial_state, - pair, - deque >& execution) const -/* ---------------------------------------------------------------------------- - * - * Description: Extracts an execution (beginning from a given system - * state) accepted by the Büchi automaton from the product - * space. The function behaves basically like - * ProductAutomaton::emptinessCheck, but it keeps additional - * information about the path of processed states during the - * backward search. This information is then used to extract - * the desired system execution from the graph. - * - * Arguments: initial_state -- Identifier of the system state. - * execution -- A reference to a pair of deques for - * storing the result. The `first' component - * of the pair represents an execution - * `prefix' (a sequence of - * - * pairs) leading from `initial_state' - * to an accepting cycle. The `second' - * component of the pair contains the cycle - * itself. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ - BitArray visited(nodes.size()); - visited.clear(nodes.size()); - - deque& prefix = execution.first; - deque& cycle = execution.second; - - prefix.clear(); - cycle.clear(); - - /* - * Scan the non-trivial maximal strongly connected components of the - * product space to find the fair MSCCs (non-trivial MSCCs containing an - * accepting cycle of the Büchi automaton used for constructing the - * product). Note that although the product space contains only back edges - * (i.e., we are actually scanning the product space with all edges - * reversed), the reversal of the edges does not affect the MSCCs of the - * product space. - */ - - for (SccIterator nmscc(*this); - !nmscc.atEnd(); - ++nmscc) - { - if (nmscc->fair(*this)) - { - const unsigned long int num_accept_sets - = buchi_automaton->numberOfAcceptanceSets(); - - /* - * Search the fair non-trivial maximal strongly connected component for - * a state belonging to some acceptance set of the Büchi automaton from - * which the product was constructed (or if the automaton has no - * acceptance sets, any state in the non-trivial MSCC). - */ - - ProductScc::const_iterator st = nmscc->begin(); - - if (buchi_automaton->numberOfAcceptanceSets() > 0) - { - while (st != nmscc->end()) - { - if ((*buchi_automaton)[buchiState(*st)].acceptanceSets(). - find(num_accept_sets) - < num_accept_sets) - break; - - ++st; - } - } - - if (st != nmscc->end()) - { - /* - * Try to find a (backward) path from the state in the MSCC back to - * the caller-given `initial state'. - */ - - size_type search_start_state = *st; - - if (search_start_state != initial_state) - { - typedef pair - BackwardSearchStackElement; - - deque - backward_search_stack; - - visited.clear(nodes.size()); - visited.setBit(search_start_state); - backward_search_stack.push_back - (make_pair(search_start_state, - operator[](search_start_state).edges().begin())); - - size_type predecessor; - - while (!backward_search_stack.empty()) - { - /* - * If it may be possible to find a shorter path to the initial - * state by still extending the current path (or if no path to - * the initial state has yet been found), scan through the - * predecessors of the `current' state (the last state inserted - * onto `backward_search_stack'). - */ - - while ((backward_search_stack.size() < prefix.size() - || prefix.empty()) - && backward_search_stack.back().second - != operator[](backward_search_stack.back().first) - .edges().end()) - { - predecessor - = (*backward_search_stack.back().second)->targetNode(); - - backward_search_stack.back().second++; - - /* - * If the given `initial state' is a predecessor of the current - * state, extract the path from the initial state to the state - * from where the backward search was started. - */ - - if (buchiState(predecessor) == buchi_automaton->initialState() - && systemState(predecessor) == initial_state) - { - prefix.clear(); - for (deque - ::const_iterator - state = backward_search_stack.begin(); - state != backward_search_stack.end(); - ++state) - { - prefix.push_front(make_pair(buchiState((*state).first), - systemState((*state).first))); - } - prefix.push_front(make_pair(buchiState(predecessor), - systemState(predecessor))); - } - - /* - * If some predecessor of the current state has not yet been - * visited, push it onto the backward search stack, then proceed - * with checking its predecessors. - */ - - else if (!visited[predecessor]) - { - visited.setBit(predecessor); - backward_search_stack.push_back - (make_pair(predecessor, - operator[](predecessor).edges().begin())); - } - } - - /* - * If all predecessors of a state have been processed, backtrack - * to the previous state on the path. - */ - - backward_search_stack.pop_back(); - } - } - - /* - * If a path was found from the `initial state' to the state in the - * MSCC, construct an accepting cycle by performing a breadth-first - * search in the MSCC. - */ - - if (!prefix.empty() || search_start_state == initial_state) - { - BitArray in_nmscc(nodes.size()); - in_nmscc.clear(nodes.size()); - - for (ProductScc::const_iterator state = nmscc->begin(); - state != nmscc->end(); - ++state) - in_nmscc.setBit(*state); - - BitArray collected_acc_sets; - collected_acc_sets.copy - ((*buchi_automaton)[buchiState(search_start_state)] - .acceptanceSets(), - num_accept_sets); - bool all_acceptance_sets_on_path - = (collected_acc_sets.count(num_accept_sets) == num_accept_sets); - - deque backward_search_queue; - map, ALLOC(size_type) > - shortest_path_predecessor; - - size_type bfs_root = search_start_state; - const GraphEdgeContainer* predecessors; - size_type state; - - visited.clear(nodes.size()); - visited.setBit(bfs_root); - backward_search_queue.push_back(bfs_root); - - bool cycle_finished = false; - - while (!cycle_finished) - { - predecessors = &operator[](backward_search_queue.front()).edges(); - - for (GraphEdgeContainer::const_iterator - predecessor = predecessors->begin(); - predecessor != predecessors->end(); - ++predecessor) - { - state = (*predecessor)->targetNode(); - - if (in_nmscc[state]) - { - /* - * If all acceptance sets have been collected and the search - * finds the first state of the cycle again, the cycle is - * complete. - */ - - if (all_acceptance_sets_on_path && state == search_start_state) - { - cycle_finished = true; - state = backward_search_queue.front(); - break; - } - else if (!visited[state]) - { - /* - * Update information about the breadth-first predecessor of - * an unvisited state. - */ - - shortest_path_predecessor[state] - = backward_search_queue.front(); - - /* - * If the unvisited state does not cover any `new' - * acceptance conditions, prepare to continue the search in - * that state by inserting the state into the search queue. - */ - - if (all_acceptance_sets_on_path - || (*buchi_automaton)[buchiState(state)].acceptanceSets() - .subset(collected_acc_sets, num_accept_sets)) - { - visited.setBit(state); - backward_search_queue.push_back(state); - } - - /* - * If the search finds an unvisited state which covers new - * acceptance sets, begin a new breadth-first search in - * that state. - */ - - else - { - all_acceptance_sets_on_path = true; - - for (unsigned long int accept_set = 0; - accept_set - < buchi_automaton->numberOfAcceptanceSets(); - accept_set++) - { - if ((*buchi_automaton)[buchiState(state)] - .acceptanceSets().test(accept_set)) - collected_acc_sets.setBit(accept_set); - else if (!collected_acc_sets.test(accept_set)) - all_acceptance_sets_on_path = false; - } - - while (state != bfs_root) - { - cycle.push_back(make_pair(buchiState(state), - systemState(state))); - state = shortest_path_predecessor[state]; - } - - bfs_root = (*predecessor)->targetNode(); - visited.clear(nodes.size()); - visited.setBit(bfs_root); - backward_search_queue.clear(); - backward_search_queue.push_back(bfs_root); - backward_search_queue.push_back(bfs_root); - - break; - } - } - } - } - - backward_search_queue.pop_front(); - } - - while (state != bfs_root) - { - cycle.push_back(make_pair(buchiState(state), - systemState(state))); - state = shortest_path_predecessor[state]; - } - - cycle.push_back(make_pair(buchiState(search_start_state), - systemState(search_start_state))); - - /* - * "Synchronize" the prefix of the witness execution with its cycle - * by removing from the end of the prefix the longest subsequence of - * states which occurs in the end of the cycle. The states in the - * cycle must be "rotated" accordingly to align the first state of - * the cycle correctly. - */ - - while (!prefix.empty() && prefix.back() == cycle.back()) - { - cycle.push_front(cycle.back()); - prefix.pop_back(); - cycle.pop_back(); - } - - return; - } - } - } - } - - /* - * The result will be empty if no accepting execution beginning from the - * given initial state could be found. - */ -} - - - -/****************************************************************************** - * - * Function definitions for class ProductAutomaton::ProductState. - * - *****************************************************************************/ - -/* ========================================================================= */ -void ProductAutomaton::ProductState::print - (ostream& stream, const int indent, const GraphOutputFormat) const -/* ---------------------------------------------------------------------------- - * - * Description: Writes information about the ProductState to a stream. - * - * Arguments: stream -- A reference to an output stream. - * indent -- Number of spaces to leave to the left of output. - * - * The third (dummy) argument is needed to support the function - * interface defined in the base class. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ - Exceptional_ostream estream(&stream, ios::failbit | ios::badbit); - - if (edges().empty()) - estream << string(indent,' ') + "The product state has no predecessors.\n"; - else - { - bool first_printed = false; - estream << string(indent, ' ') + "Predecessor states: {"; - - for (GraphEdgeContainer::const_iterator predecessor = edges().begin(); - predecessor != edges().end(); ++predecessor) - { - if (first_printed) - estream << ", "; - else - first_printed = true; - estream << (*predecessor)->targetNode(); - } - estream << "}\n"; - } - - estream.flush(); -} - - - -/****************************************************************************** - * - * Function definitions for class ProductAutomaton::ProductScc. - * - *****************************************************************************/ - -/* ========================================================================= */ -bool ProductAutomaton::ProductScc::fair - (const ProductAutomaton& product_automaton) const -/* ---------------------------------------------------------------------------- - * - * Description: Tests whether a strongly connected component is fair in - * a product automaton. A strongly connected component is - * fair if and only if it is nontrivial (i.e. empty or - * containing a single state with a self-loop) and contains a - * state corresponding to a state from every acceptance set of - * the Büchi automaton used for constructing the given product. - * - * Arguments: product_automaton -- A constant reference to a - * ProductAutomaton. - * - * Returns: A truth value telling whether the strongly connected - * component is fair. - * - * ------------------------------------------------------------------------- */ -{ - /* - * A maximal strongly connected component is not fair if it is trivial. - */ - - if (empty() - || (size() == 1 && !product_automaton.connected(*begin(), *begin()))) - return false; - - /* - * Check whether the strongly connected component contains a state from each - * acceptance set of the Büchi automaton used for constructing the product - * (in this case, the component contains an accepting cycle of the - * automaton and is therefore fair). - */ - - const BuchiAutomaton* buchi_automaton = product_automaton.buchi_automaton; - const BitArray* acceptance_sets; - const unsigned long int number_of_acceptance_sets - = buchi_automaton->numberOfAcceptanceSets(); - - BitArray acceptance_sets_in_scc(number_of_acceptance_sets); - acceptance_sets_in_scc.clear(number_of_acceptance_sets); - - unsigned long int accept_set; - unsigned long int acceptance_set_counter = 0; - - for (const_iterator st = begin(); - st != end() && acceptance_set_counter < number_of_acceptance_sets; - ++st) - { - acceptance_sets = &(*buchi_automaton)[product_automaton.buchiState(*st)]. - acceptanceSets(); - - accept_set = acceptance_set_counter; - while (accept_set < number_of_acceptance_sets) - { - if (acceptance_sets->test(accept_set)) - { - acceptance_sets_in_scc.setBit(accept_set); - if (accept_set == acceptance_set_counter) - { - do - acceptance_set_counter++; - while (acceptance_set_counter < number_of_acceptance_sets - && acceptance_sets_in_scc[acceptance_set_counter]); - accept_set = acceptance_set_counter; - continue; - } - } - - accept_set++; - } - } - - return (acceptance_set_counter == number_of_acceptance_sets); -} - -} diff --git a/lbtt/src/ProductAutomaton.h b/lbtt/src/ProductAutomaton.h deleted file mode 100644 index 060491c7d..000000000 --- a/lbtt/src/ProductAutomaton.h +++ /dev/null @@ -1,596 +0,0 @@ -/* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen - * - * 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 PRODUCTAUTOMATON_H -#define PRODUCTAUTOMATON_H - -#include -#include -#include -#include -#include "LbttAlloc.h" -#include "BitArray.h" -#include "BuchiAutomaton.h" -#include "EdgeContainer.h" -#include "Exception.h" -#include "Graph.h" -#include "StateSpace.h" - -using namespace std; - -extern bool user_break; - -namespace UserCommands -{ - extern void printAutomatonAnalysisResults - (ostream&, int, unsigned long int, unsigned long int); -} - -namespace Graph -{ - -/****************************************************************************** - * - * A class for representing the synchronous product of a Büchi automaton and - * a state space. - * - *****************************************************************************/ - -class ProductAutomaton : public Graph -{ -private: - /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ - - class ProductState : /* A class for */ - public Graph::Node /* representing the */ - { /* states of the product - * automaton. - */ - public: - explicit ProductState /* Constructor. */ - (const size_type hash_val = 0); - - ~ProductState(); /* Destructor. */ - - /* `edges' inherited from Graph::Node */ - - size_type hashValue() const; /* Get or set the hash */ - size_type& hashValue(); /* value for the product - * state (this value can - * be used to extract - * the identifiers of - * the original state - * space and the Büchi - * automaton with which - * the product state is - * associated). - */ - - void print /* Writes information */ - (ostream& stream = cout, /* about the product */ - const int indent = 0, /* state to a stream. */ - const GraphOutputFormat fmt = NORMAL) const; - - private: - friend class ProductAutomaton; - - ProductState(const ProductState&); /* Prevent copying and */ - ProductState& operator=(const ProductState&); /* assignment of - * ProductState objects. - */ - - size_type hash_value; /* Hash value for the - * product state (can be - * used to extract the - * identifiers of the - * original state space and - * the Büchi automaton with - * which the product state - * is associated). - */ - - Edge* incoming_edge; /* The unique edge pointing - * to `this' ProductState. - */ - }; - - /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ - - class ProductScc : /* A class for storing */ - public vector /* connected components */ - { /* of the product. - */ - public: - ProductScc(); /* Constructor. */ - - /* default copy constructor */ - - ~ProductScc(); /* Destructor. */ - - /* default assignment operator */ - - bool fair /* Tests whether the */ - (const ProductAutomaton& product_automaton) /* component is fair, */ - const; /* i.e. it is a - * nontrivial component - * with a state from - * each acceptance set - * of the Büchi - * automaton used for - * constructing a - * given product. - */ - - void insert /* Inserts a state into */ - (const ProductAutomaton::size_type /* the container. */ - product_state); - }; - - /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ - -public: - class ProductSizeException; /* An exception class for - * reporting the situation - * where the size of the - * product automaton may - * be too big. - */ - - friend class ProductScc; - friend void UserCommands::printAutomatonAnalysisResults - (ostream&, int, unsigned long int, unsigned long int); - - ProductAutomaton(); /* Constructor. */ - - ~ProductAutomaton(); /* Destructor. */ - - ProductState& operator[](const size_type index) /* Indexing operator. No */ - const; /* range check is performed - * on the argument. - */ - - ProductState& node(const size_type index) const; /* Synonym for the indexing - * operator. This function - * also checks the range of - * the argument. - */ - - /* `size' inherited from Graph */ - - /* `empty' inherited from Graph */ - - void clear(); /* Makes the automaton - * empty. - */ - - void connect /* Connects two states */ - (const size_type father, /* of the product */ - const size_type child); /* automaton. */ - - void disconnect /* Disconnects two */ - (const size_type father, /* states of the product */ - const size_type child); /* automaton. */ - - /* `connected' inherited from Graph */ - - /* `stats' inherited from Graph */ - - /* `subgraphStats' inherited from Graph */ - - void computeProduct /* Function for */ - (const BuchiAutomaton& automaton, /* initializing the */ - const StateSpace& statespace, /* product automaton. */ - const bool global_product); - - StateSpace::size_type systemState /* Returns the */ - (const size_type state) const; /* identifier of the - * state of the original - * state space with - * which a given product - * state is associated. - */ - - BuchiAutomaton::size_type buchiState /* Returns the */ - (const size_type state) const; /* identifier of the - * state of the original - * automaton with which - * a given product state - * is associated. - */ - - void emptinessCheck(Bitset& result) const; /* Performs an emptiness - * check on the product. - */ - - void findAcceptingExecution /* Extracts an accepting */ - (const StateSpace::size_type initial_state, /* execution from the */ - pair, /* product automaton. */ - deque >& - execution) const; - - void print /* Writes information */ - (ostream& stream = cout, /* about the product */ - const int indent = 0, /* automaton to a */ - const GraphOutputFormat fmt = NORMAL) const; /* stream. */ - -private: - ProductAutomaton(const ProductAutomaton&); /* Prevent copying and */ - ProductAutomaton& operator= /* assignment of */ - (const ProductAutomaton&); /* ProductAutomaton - * objects. - */ - - size_type expand(size_type node_count = 1); /* Inserts states to the - * product automaton. - */ - - const BuchiAutomaton* buchi_automaton; /* A pointer to the - * Büchi automaton used for - * constructing the - * product. - */ - - StateSpace::size_type statespace_size; /* Size of the state space - * used for constructing - * the product automaton. - */ - -#ifdef HAVE_OBSTACK_H /* Storage for product */ - ObstackAllocator store; /* states and */ -#endif /* HAVE_OBSTACK_H */ /* transitions. */ -}; - - - -/****************************************************************************** - * - * An exception class for reporting the situation where the product may be too - * big to compute. - * - *****************************************************************************/ - -class ProductAutomaton::ProductSizeException : public Exception -{ -public: - ProductSizeException(); /* Constructor. */ - - /* default copy constructor */ - - ~ProductSizeException() throw(); /* Destructor. */ - - ProductSizeException& /* Assignment operator. */ - operator=(const ProductSizeException& e); - - /* `what' inherited from class Exception */ -}; - - - -/****************************************************************************** - * - * Inline function definitions for class ProductAutomaton. - * - *****************************************************************************/ - -/* ========================================================================= */ -inline ProductAutomaton::ProductAutomaton() : - buchi_automaton(0), statespace_size(0) -#ifdef HAVE_OBSTACK_H -, store() -#endif /* HAVE_OBSTACK_H */ -/* ---------------------------------------------------------------------------- - * - * Description: Constructor for class ProductAutomaton. Initializes a - * new object for storing the product of a Büchi automaton and a - * state space. The product must then be explicitly initialized - * by calling the function `computeProduct' on the object. - * - * Arguments: None. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ -} - -/* ========================================================================= */ -inline ProductAutomaton::~ProductAutomaton() -/* ---------------------------------------------------------------------------- - * - * Description: Destructor for class ProductAutomaton. - * - * Arguments: None. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ - clear(); -} - -/* ========================================================================= */ -inline ProductAutomaton::ProductState& -ProductAutomaton::operator[](const size_type index) const -/* ---------------------------------------------------------------------------- - * - * Description: Indexing operator for class ProductAutomaton. Can be used to - * refer to the individual states of the product automaton. No - * range check will be performed on the argument. - * - * Argument: index -- Index of a state of the product automaton. - * - * Returns: A reference to the product state corresponding to the index. - * - * ------------------------------------------------------------------------- */ -{ - return static_cast(*nodes[index]); -} - -/* ========================================================================= */ -inline ProductAutomaton::ProductState& -ProductAutomaton::node(const size_type index) const -/* ---------------------------------------------------------------------------- - * - * Description: Function for referring to a single state of a - * ProductAutomaton. This function will also check the range - * argument. - * - * Argument: index -- Index of a state of the product automaton. - * - * Returns: A reference to the corresponding product state. - * - * ------------------------------------------------------------------------- */ -{ - return static_cast(Graph::node(index)); -} - -/* ========================================================================= */ -inline StateSpace::size_type ProductAutomaton::systemState - (const size_type state) const -/* ---------------------------------------------------------------------------- - * - * Description: Returns the identifier of the system state with which a - * given product state is associated. This function will perform - * no range checks on its argument. - * - * Argument: state -- Identifier of a product state. - * - * Returns: Identifier of a state in a state space. - * - * ------------------------------------------------------------------------- */ -{ - return operator[](state).hashValue() % statespace_size; -} - -/* ========================================================================= */ -inline StateSpace::size_type ProductAutomaton::buchiState - (const size_type state) const -/* ---------------------------------------------------------------------------- - * - * Description: Returns the identifier of the state of the Büchi automaton - * with which a given product state is associated. This function - * will perform no range checks on its argument. - * - * Argument: state -- Identifier of a product state. - * - * Returns: Identifier of a state in a Büchi automaton. - * - * ------------------------------------------------------------------------- */ -{ - return operator[](state).hashValue() / statespace_size; -} - - - -/****************************************************************************** - * - * Inline function definitions for class ProductAutomaton::ProductState. - * - *****************************************************************************/ - -/* ========================================================================= */ -inline ProductAutomaton::ProductState::ProductState(const size_type hash_val) : - Graph::Node(), hash_value(hash_val), incoming_edge(0) -/* ---------------------------------------------------------------------------- - * - * Description: Constructor for class ProductAutomaton::ProductState. Creates - * a new object representing a synchronous product of a state of - * a Büchi automaton with a state of a state space. - * - * Arguments: hash_val -- Hash value for the product state. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ -} - -/* ========================================================================= */ -inline ProductAutomaton::ProductState::~ProductState() -/* ---------------------------------------------------------------------------- - * - * Description: Destructor for class ProductAutomaton::ProductState. - * - * Arguments: None. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ - if (incoming_edge != 0) - { -#ifdef HAVE_OBSTACK_H - incoming_edge->~Edge(); -#else - delete incoming_edge; -#endif /* HAVE_OBSTACK_H */ - } - outgoing_edges.clear(); -} - -/* ========================================================================= */ -inline ProductAutomaton::size_type ProductAutomaton::ProductState::hashValue() - const -/* ---------------------------------------------------------------------------- - * - * Description: Returns the product state's hash value by value. - * - * Arguments: None. - * - * Returns: The hash value of the product state. - * - * ------------------------------------------------------------------------- */ -{ - return hash_value; -} - -/* ========================================================================= */ -inline ProductAutomaton::size_type& ProductAutomaton::ProductState::hashValue() -/* ---------------------------------------------------------------------------- - * - * Description: Returns the product state's hash value by reference. (This - * function can therefore be used to change the value.) - * - * Arguments: None. - * - * Returns: A reference to the hash value of the product state. - * - * ------------------------------------------------------------------------- */ -{ - return hash_value; -} - - - -/****************************************************************************** - * - * Inline function definitions for class ProductAutomaton::ProductScc. - * - *****************************************************************************/ - -/* ========================================================================= */ -inline ProductAutomaton::ProductScc::ProductScc() -/* ---------------------------------------------------------------------------- - * - * Description: Constructor for class ProductAutomaton::ProductScc. Creates a - * new container for storing a maximal strongly connected - * component of a ProductAutomaton. - * - * Arguments: None. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ -} - -/* ========================================================================= */ -inline ProductAutomaton::ProductScc::~ProductScc() -/* ---------------------------------------------------------------------------- - * - * Description: Destructor for class ProductAutomaton::ProductScc. - * - * Arguments: None. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ -} - -/* ========================================================================= */ -inline void ProductAutomaton::ProductScc::insert - (const ProductAutomaton::size_type product_state) -/* ---------------------------------------------------------------------------- - * - * Description: Inserts a new product state identifier to the container. - * - * Argument: product_state -- Identifier of a product state. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ - push_back(product_state); -} - - - -/****************************************************************************** - * - * Inline function definitions for class - * ProductAutomaton::ProductSizeException. - * - *****************************************************************************/ - -/* ========================================================================= */ -inline ProductAutomaton::ProductSizeException::ProductSizeException() : - Exception("product may be too large") -/* ---------------------------------------------------------------------------- - * - * Description: Constructor for class ProductAutomaton::ProductSizeException. - * - * Arguments: None. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ -} - -/* ========================================================================= */ -inline ProductAutomaton::ProductSizeException::~ProductSizeException() throw() -/* ---------------------------------------------------------------------------- - * - * Description: Destructor for class ProductAutomaton::ProductSizeException. - * - * Arguments: None. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ -} - -/* ========================================================================= */ -inline ProductAutomaton::ProductSizeException& -ProductAutomaton::ProductSizeException::operator= - (const ProductAutomaton::ProductSizeException& e) -/* ---------------------------------------------------------------------------- - * - * Description: Assignment operator for class - * ProductAutomaton::ProductSizeException. Assigns the value of - * another ProductAutomaton::ProductSizeException to `this' one. - * - * Arguments: e -- A reference to a constant - * ProductAutomaton::ProductSizeException. - * - * Returns: A reference to the object whose value was changed. - * - * ------------------------------------------------------------------------- */ -{ - Exception::operator=(e); - return *this; -} - -} - -#endif /* !PRODUCTAUTOMATON_H */ diff --git a/lbtt/src/SccIterator.h b/lbtt/src/SccIterator.h deleted file mode 100644 index fceaceeea..000000000 --- a/lbtt/src/SccIterator.h +++ /dev/null @@ -1,752 +0,0 @@ -/* - * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 - * Heikki Tauriainen - * - * 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 SCCITERATOR_H -#define SCCITERATOR_H - -#include -#include -#include -#include -#include -#include "LbttAlloc.h" -#include "Graph.h" - -using namespace std; - -namespace Graph -{ - -/****************************************************************************** - * - * A template iterator class for computing the maximal strongly connected - * components of a graph represented as an object of class - * Graph. - * - * The iterator class has three template arguments: - * class EdgeContainer -- Container class storing the edges in the - * graph with which the iterator is associated. - * - * class SccContainer -- Container for storing the identifiers of the - * nodes belonging to some maximal strongly - * connected component. The container class - * must be able to store elements of type - * Graph::size_type. The container - * class interface must support the following - * operations: - * - * Default constructor which can be called - * without any arguments - * Copy constructor - * Assignment operator - * clear() - * [makes the container empty] - * insert(Graph::size_type s) - * [inserts an element into the - * container] - * - * If the container class is left unspecified, - * it defaults to - * set::size_type, - * less::size_type>, - * ALLOC(Graph::size_type)>. - * - * class Filter -- Class for representing function objects that - * can be used to restrict the iterator - * dereferencing operators to return only - * those nodes of a strongly connected component - * which satisfy a certain condition that can be - * tested using Filter::operator(). This function - * has to accept a single parameter of type - * Graph::Node*. It must return a - * Boolean value. The nodes for which the - * function returns `false' will then not be - * included in the collection of nodes returned - * by the iterator dereferencing operators. - * - * If the Filter class is left unspecified, it - * defaults to the NullSccFilter - * class, which does not restrict the set of - * nodes in any way. - * - *****************************************************************************/ - -template -class NullSccFilter; - -template::size_type, - less::size_type>, - ALLOC(typename Graph::size_type) >, - class Filter = NullSccFilter > -class SccIterator -{ -public: - SccIterator(const Graph& g); /* Constructor. */ - - /* default copy constructor */ - - ~SccIterator(); /* Destructor. */ - - /* default assignment operator */ - - bool operator== /* Equality test for */ - (const SccIterator& it) const; - - bool operator!= /* Inequality test for */ - (const SccIterator& it) const; - - bool operator< /* `Less than' relation */ - (const SccIterator& it) const; - - bool operator<= /* `Less than or equal' */ - (const SccIterator& it) const; - - bool operator> /* `Greater than' */ - (const SccIterator& it) const; - - bool operator>= /* `Greater than or */ - (const SccIterator& it) const; /* iterators. */ - - const SccContainer& operator*() const; /* Dereferencing */ - const SccContainer* operator->() const; /* operators. */ - - const SccContainer& operator++(); /* Prefix and postfix */ - const SccContainer operator++(int); /* increment operators. */ - - bool atEnd() const; /* Tests whether the - * iterator has scanned - * through all the - * strongly connected - * components of the - * graph. - */ - -private: - const Graph& graph; /* Reference to the graph - * with which the iterator - * is associated. - */ - - typename Graph::size_type /* Number of graph */ - dfs_number; /* nodes processed by - * the iterator. - */ - - vector::size_type, /* dfs_ordering[i] */ - ALLOC(typename Graph /* indicates the */ - ::size_type) > /* position of graph */ - dfs_ordering; /* node i in the depth- - * first search order. - * (If the node has not - * yet been visited, - * dfs_ordering[i]==0.) - */ - - vector::size_type, /* lowlink[i] indicates */ - ALLOC(typename Graph /* the least graph node */ - ::size_type) > /* (in the depth-first */ - lowlink; /* search order) that - * is reachable from - * graph node i and - * does not belong to - * any strongly - * connected component - * which has already been - * processed. - */ - - typedef pair::size_type, - typename EdgeContainer::const_iterator> - NodeStackElement; - - stack > - node_stack; - - typename Graph::size_type /* Current graph node */ - current_node; /* the depth-first - * search. - */ - - typename EdgeContainer::const_iterator edge; /* Iterator to scan - * through the successors - * of the current node. - */ - - stack::size_type, /* Stack used for */ - deque /* collecting the nodes */ - ::size_type, /* in a strongly */ - ALLOC(typename Graph /* connected component. */ - ::size_type) - > - > - scc_stack; - - SccContainer current_scc; /* Container of nodes - * forming the maximal - * strongly connected - * graph component - * currently `pointed to' - * by the iterator. - */ - - Filter cond; /* Function object for - * filtering out a subset - * of nodes in the - * strongly connected - * components. - */ - - void reset(); /* Initializes the - * iterator to point to - * the first strongly - * connected component of - * the graph. - */ - - void computeNextScc(); /* Updates the iterator to - * point to the next - * strongly connected - * component. - */ -}; - - - -/****************************************************************************** - * - * Default test for collecting the nodes in a strongly connected component. - * (See documentation on class SccIterator for information about the purpose - * of the class.) - * - *****************************************************************************/ - -template -class NullSccFilter -{ -public: - bool operator()(const typename Graph::Node*) const; -}; - - - -/****************************************************************************** - * - * Inline function definitions for template class - * SccIterator. - * - *****************************************************************************/ - -/* ========================================================================= */ -template -inline SccIterator::SccIterator - (const Graph& g) : - graph(g), dfs_ordering(graph.size()), lowlink(graph.size()) -/* ---------------------------------------------------------------------------- - * - * Description: Constructor for class - * SccIterator. - * Initializes a new iterator for scanning the maximal strongly - * connected components of a graph. - * - * Arguments: g -- The graph with which the iterator is to be associated - * (a Graph object). - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ - reset(); - computeNextScc(); -} - -/* ========================================================================= */ -template -inline SccIterator::~SccIterator() -/* ---------------------------------------------------------------------------- - * - * Description: Destructor for class - * SccIterator. - * - * Arguments: None. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ -} - -/* ========================================================================= */ -template -inline bool SccIterator::operator== - (const SccIterator& it) const -/* ---------------------------------------------------------------------------- - * - * Description: Equality test for two SccIterators. Two SccIterators are - * `equal' if and only if both of them are associated with - * exactly the same graph object in memory and the iterators - * have processed the same amount of graph nodes. - * - * Arguments: it -- A constant reference to another SccIterator. - * - * Returns: A truth value according to the result of the equality test. - * - * ------------------------------------------------------------------------- */ -{ - return (&graph == &(it.graph) && dfs_number == it.dfs_number); -} - -/* ========================================================================= */ -template -inline bool SccIterator::operator!= - (const SccIterator& it) const -/* ---------------------------------------------------------------------------- - * - * Description: Inequality test for two SccIterators. Two SccIterators are - * not equal if and only if they are associated with different - * graphs or they are associated with the same graph object in - * memory but the iterators have processed a different number of - * graph nodes. - * - * Arguments: it -- A constant reference to another SccIterator. - * - * Returns: A truth value according to the result of the inequality test. - * - * ------------------------------------------------------------------------- */ -{ - return (&graph != &(it.graph) || dfs_number != it.dfs_number); -} - -/* ========================================================================= */ -template -inline bool SccIterator::operator< - (const SccIterator& it) const -/* ---------------------------------------------------------------------------- - * - * Description: `Less than' relation between two SccIterators. An - * SccIterator is `less than' another if and only if the - * iterators relate to the same graph object in memory and - * the first iterator has processed a smaller number of nodes - * than the second one. - * - * Arguments: it -- A constant reference to another SccIterator. - * - * Returns: A truth value according to the result of the test. - * - * ------------------------------------------------------------------------- */ -{ - return (&graph == &(it.graph) && dfs_number < it.dfs_number); -} - -/* ========================================================================= */ -template -inline bool SccIterator::operator<= - (const SccIterator& it) const -/* ---------------------------------------------------------------------------- - * - * Description: `Less than or equal' relation between two SccIterators. An - * SccIterator is `less than or equal to' another if and only - * if the iterators relate to the same graph object in memory - * and the first iterator has processed a number of nodes not - * exceeding the number of nodes the second iterator has - * processed. - * - * Arguments: it -- A constant reference to another SccIterator. - * - * Returns: A truth value according to the result of the test. - * - * ------------------------------------------------------------------------- */ -{ - return (&graph == &(it.graph) && dfs_number <= it.dfs_number); -} - -/* ========================================================================= */ -template -inline bool SccIterator::operator> - (const SccIterator& it) const -/* ---------------------------------------------------------------------------- - * - * Description: `Greater than' relation between two SccIterators. An - * SccIterator is `greater than' another if and only if the - * iterators relate to the same graph object in memory and - * the first iterator has processed a greater number of nodes - * than the second one. - * - * Arguments: it -- A constant reference to another SccIterator. - * - * Returns: A truth value according to the result of the test. - * - * ------------------------------------------------------------------------- */ -{ - return (&graph == &(it.graph) && dfs_number > it.dfs_number); -} - -/* ========================================================================= */ -template -inline bool SccIterator::operator>= - (const SccIterator& it) const -/* ---------------------------------------------------------------------------- - * - * Description: `Greater than or equal' relation between two SccIterators. An - * SccIterator is `greater than or equal to' another if and - * only if the iterators relate to the same graph object in - * memory and the first iterator has processed at least as many - * nodes as the second iterator has processed. - * - * Arguments: it -- A constant reference to another SccIterator. - * - * Returns: A truth value according to the result of the test. - * - * ------------------------------------------------------------------------- */ -{ - return (&graph == &(it.graph) && dfs_number >= it.dfs_number); -} - -/* ========================================================================= */ -template -inline const SccContainer& -SccIterator::operator*() const -/* ---------------------------------------------------------------------------- - * - * Description: Dereferencing operator for a SccIterator. Returns the - * collection of nodes which belong to the maximal strongly - * connected component that the iterator currently points to. - * - * Arguments: None. - * - * Returns: A collection of nodes representing some maximal strongly - * connected component. - * - * ------------------------------------------------------------------------- */ -{ - return current_scc; -} - -/* ========================================================================= */ -template -inline const SccContainer* -SccIterator::operator->() const -/* ---------------------------------------------------------------------------- - * - * Description: Dereferencing operator for a SccIterator. Returns the - * collection of nodes which belong to the maximal strongly - * connected component that the iterator currently points to. - * - * Arguments: None. - * - * Returns: A collection of nodes representing some maximal strongly - * connected component. - * - * ------------------------------------------------------------------------- */ -{ - return ¤t_scc; -} - -/* ========================================================================= */ -template -inline const SccContainer& -SccIterator::operator++() -/* ---------------------------------------------------------------------------- - * - * Description: Prefix increment operator for a SccIterator. Computes the - * next maximal strongly connected component of the graph and - * then returns it. - * - * Arguments: None. - * - * Returns: A collection of nodes representing some maximal strongly - * connected component. - * - * ------------------------------------------------------------------------- */ -{ - computeNextScc(); - return current_scc; -} - -/* ========================================================================= */ -template -inline const SccContainer -SccIterator::operator++(int) -/* ---------------------------------------------------------------------------- - * - * Description: Postfix increment operator for a SccIterator. Effectively - * returns the maximal strongly connected component of the graph - * currently pointed to by the iterator and then updates the - * iterator to point to the next strongly connected component. - * - * Arguments: None (the `int' is only required to distinguish this operator - * from the prefix increment operator). - * - * Returns: A collection of nodes representing some maximal strongly - * connected component. - * - * ------------------------------------------------------------------------- */ -{ - SccContainer old_scc = current_scc; - computeNextScc(); - return old_scc; -} - -/* ========================================================================= */ -template -inline bool SccIterator::atEnd() const -/* ---------------------------------------------------------------------------- - * - * Description: Tells whether there are still more strongly connected - * components in the graph for the iterator to process. - * - * Arguments: None. - * - * Returns: A truth value. - * - * ------------------------------------------------------------------------- */ -{ - return (current_node == graph.size()); -} - - - -/****************************************************************************** - * - * Function definitions for template class - * SccIterator. - * - *****************************************************************************/ - -/* ========================================================================= */ -template -void SccIterator::reset() -/* ---------------------------------------------------------------------------- - * - * Description: Initializes the iterator to point to the first maximal - * strongly connected component of the graph with which the - * iterator it associated. - * - * Arguments: None. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ - dfs_number = 0; - - for (typename vector::size_type, - ALLOC(typename Graph::size_type) > - ::iterator node = dfs_ordering.begin(); - node != dfs_ordering.end(); - ++node) - *node = 0; - - while (!node_stack.empty()) - node_stack.pop(); - - while (!scc_stack.empty()) - scc_stack.pop(); - - current_scc.clear(); -} - -/* ========================================================================= */ -template -void SccIterator::computeNextScc() -/* ---------------------------------------------------------------------------- - * - * Description: Updates the state of the iterator to `point to' the next - * maximal strongly connected component of the graph, using the - * algorithm due to Tarjan [R. Tarjan. Depth-first search and - * linear graph algorithms. SIAM Journal on Computing, - * 1(2):146--160, June 1972] for computing the next maximal - * strongly connected component of the graph. - * - * Arguments: None. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ - current_scc.clear(); - - if (scc_stack.empty() && node_stack.empty()) - { - /* - * If both `scc_stack' and `node_stack' are empty (this holds if we have - * recently finished processing some component of the graph), try to find - * a graph node that has not yet been visited. If no such node is found, - * all nodes have been visited and there are no more strongly connected - * components to be found in the graph. - */ - - current_node = 0; - for (typename vector::size_type, - ALLOC(typename Graph::size_type) > - ::const_iterator node = dfs_ordering.begin(); - node != dfs_ordering.end() && (*node) != 0; - ++node) - ++current_node; - - if (current_node == graph.size()) - return; - - /* - * Prepare to continue the depth-first search in the unvisited node. - */ - - edge = graph[current_node].edges().begin(); - - scc_stack.push(current_node); - ++dfs_number; - dfs_ordering[current_node] = lowlink[current_node] = dfs_number; - } - - typename Graph::size_type child_node; - - while (1) - { - /* - * If there are still nodes left in the depth-first search backtracking - * stack, pop a node and its next unprocessed outgoing edge off the stack. - * Before continuing the depth-first search in the popped node, update - * its lowlink value if necessary. (This has to be done if the lowlink of - * the current node---a successor of the popped node---is less than the - * lowlink of the popped node but not equal to zero.) - */ - - if (!node_stack.empty()) - { - typename Graph::size_type father_node - = node_stack.top().first; - edge = node_stack.top().second; - node_stack.pop(); - - if (lowlink[current_node] < lowlink[father_node] - && lowlink[current_node] != 0) - lowlink[father_node] = lowlink[current_node]; - - current_node = father_node; - } - - /* - * Scan through the successors of the current node. - * - * If the current nodes has an unvisited successor node (a successor i - * with dfs_ordering[i] == 0), push the current node and its next - * unprocessed edge onto the backtracking stack and then continue the - * search in the successor node. Push also the successor node onto the - * strongly connected component stack. - * - * Otherwise, update the lowlink of the current node to the lowlink of - * its already visited successor if necessary. - */ - - while (edge != graph[current_node].edges().end()) - { - child_node = (*edge)->targetNode(); - ++edge; - - if (dfs_ordering[child_node] == 0) - { - node_stack.push(make_pair(current_node, edge)); - scc_stack.push(child_node); - - ++dfs_number; - dfs_ordering[child_node] = lowlink[child_node] = dfs_number; - - current_node = child_node; - edge = graph[current_node].edges().begin(); - } - else if (lowlink[child_node] < lowlink[current_node] - && lowlink[child_node] != 0) - lowlink[current_node] = lowlink[child_node]; - } - - /* - * If the least node in the depth-first search order reachable from the - * current node is the current node itself at the end of the previous - * loop, we have found a maximal strongly connected component of the - * graph. In this case, collect the states satisfying `cond' in the - * strongly connected component stack to form the component and exit. - * (Otherwise, return to the start of the outermost while loop and - * continue by popping a state off the depth-first search backtracking - * stack.) - */ - - if (dfs_ordering[current_node] == lowlink[current_node]) - { - do - { - child_node = scc_stack.top(); - scc_stack.pop(); - if (cond(&graph[child_node])) - current_scc.insert(child_node); - lowlink[child_node] = 0; - } - while (child_node != current_node); - - break; - } - } -} - - - -/****************************************************************************** - * - * Inline function definitions for template class NullSccFilter. - * - *****************************************************************************/ - -/* ========================================================================= */ -template -inline bool NullSccFilter::operator() - (const typename Graph::Node*) const -/* ---------------------------------------------------------------------------- - * - * Description: Default test for filtering the nodes in a strongly connected - * graph component. The default is to simply include all nodes - * in the result. - * - * Arguments: A constant pointer to a Graph::Node (required - * only to satisfy the class interface requirements). - * - * Returns: true, so the test will succeed for every node in the - * component. - * - * ------------------------------------------------------------------------- */ -{ - return true; -} - -} - -#endif /* !SCCITERATOR_H */ diff --git a/lbtt/src/translate.cc b/lbtt/src/translate.cc index e21a08287..f2653c196 100644 --- a/lbtt/src/translate.cc +++ b/lbtt/src/translate.cc @@ -46,6 +46,17 @@ char** command_line_arguments; +/****************************************************************************** + * + * Pointer to an object providing operations for translating a formula into an + * automaton. + * + *****************************************************************************/ + +static TranslatorInterface* translator = 0; + + + /****************************************************************************** * * A function for showing warnings to the user. @@ -61,21 +72,46 @@ void printWarning(const string& msg) /****************************************************************************** * - * Signal handler for debugging purposes. + * Handler for SIGINT, SIGQUIT, SIGABRT and SIGTERM. * *****************************************************************************/ -RETSIGTYPE signalHandler(int signal_number) +static void signalHandler(int signal_number) { - cerr << string(command_line_arguments[0]) + ": received signal " - << signal_number - << endl; - signal(signal_number, SIG_DFL); + if (translator != 0) + delete translator; + struct sigaction s; + s.sa_handler = SIG_DFL; + sigemptyset(&s.sa_mask); + s.sa_flags = 0; + sigaction(signal_number, &s, static_cast(0)); raise(signal_number); } +/****************************************************************************** + * + * Function for installing signal handlers. + * + *****************************************************************************/ + +static void installSignalHandler(int signum) +{ + struct sigaction s; + sigaction(signum, static_cast(0), &s); + + if (s.sa_handler != SIG_IGN) + { + s.sa_handler = signalHandler; + sigemptyset(&s.sa_mask); + s.sa_flags = 0; + sigaction(signum, &s, static_cast(0)); + } +} + + + /****************************************************************************** * * Main function. @@ -84,7 +120,7 @@ RETSIGTYPE signalHandler(int signal_number) int main(int argc, char** argv) { - typedef enum {OPT_HELP = 'h', OPT_LBT, OPT_SPIN, OPT_SPOT, OPT_VERSION = 'v'} + typedef enum {OPT_HELP = 'h', OPT_LBT, OPT_SPIN, OPT_SPOT, OPT_VERSION = 'V'} OptionType; static OPTIONSTRUCT command_line_options[] = @@ -102,12 +138,10 @@ int main(int argc, char** argv) opterr = 1; int opttype, option_index; - TranslatorInterface* translator = 0; - do { option_index = 0; - opttype = getopt_long(argc, argv, "hv", command_line_options, + opttype = getopt_long(argc, argv, "hV", command_line_options, &option_index); switch (opttype) @@ -118,7 +152,7 @@ int main(int argc, char** argv) "file] [automaton file]\n" "General options:\n" " --h, --help Show this help\n" - " --v, --version Show version and exit\n\n" + " --V, --version Show version and exit\n\n" "Translator options:\n" " --lbt lbt\n" " --spin Spin\n" @@ -175,16 +209,15 @@ int main(int argc, char** argv) int exitstatus = 0; - signal(SIGHUP, signalHandler); - signal(SIGINT, signalHandler); - signal(SIGQUIT, signalHandler); - signal(SIGILL, signalHandler); - signal(SIGABRT, signalHandler); - signal(SIGFPE, signalHandler); - signal(SIGSEGV, signalHandler); - signal(SIGPIPE, signalHandler); - signal(SIGALRM, signalHandler); - signal(SIGTERM, signalHandler); + installSignalHandler(SIGHUP); + installSignalHandler(SIGINT); + installSignalHandler(SIGQUIT); + installSignalHandler(SIGABRT); + installSignalHandler(SIGPIPE); + installSignalHandler(SIGALRM); + installSignalHandler(SIGTERM); + installSignalHandler(SIGUSR1); + installSignalHandler(SIGUSR2); ::Ltl::LtlFormula* formula(0); diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index 79c327319..144334e7a 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -31,330 +31,376 @@ cat > config <