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

* lbtt/: Merge lbtt 1.1.0.

Browse source 
* src/tgbatest/spotlbtt.test: Adjust config file syntax to
please lbtt 1.1.0.
This commit is contained in:
Alexandre Duret-Lutz 2004-07-07 17:41:42 +00:00
parent cfdd81a919
commit e11da2e3af
9 changed files with 952 additions and 2633 deletions
Download patch file Download diff file Expand all files Collapse all files

775
lbtt/ChangeLog
View file

@ -1,37 +1,9 @@
2004-03-09 Alexandre Duret-Lutz <adl@src.lip6.fr>
* 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 <adl@src.lip6.fr>
* 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 <adl@src.lip6.fr>
* 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 <adl@src.lip6.fr>
* src/TestOperations.cc: Include sys/wait.h.
2003-07-29 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* 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 <aduret@src.lip6.fr>
Spot wants `^', not `xor'.
@ -41,10 +13,6 @@
2003-07-09 Alexandre Duret-Lutz <aduret@src.lip6.fr>
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 <heikki.tauriainen@hut.fi>
* Version 1.1.0 released.
2004-07-06 Heikki Tauriainen <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* doc/texinfo.tex: New upstream version.
* doc/lbtt.texi: Update to edition 1.1.0.
* NEWS: Update.
2004-07-02 Heikki Tauriainen <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* 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<Operator>::UnaryFormula): Likewise.
(BinaryFormula<Operator>::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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* 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<GraphEdgeContainer>::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<BuchiProduct> and Product<StateSpaceProduct>.
(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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* src/Graph.h.in (Graph<EdgeContainer>::Edge) Fix return
type of targetNode() and the type of the `target_node'
variable to allow compilation with gcc 3.4.0.
(Graph<EdgeContainer>::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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* 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 <opttype,arg>
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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* src/TestOperations.cc (writeFormulaeToFiles): Make the order of
debugging messages (verbosity level 5) more consistent.
2004-02-15 Heikki Tauriainen <heikki.tauriainen@hut.fi>
* src/DispUtil.h (printText): Move function declarations to their
correct place (out of struct StreamFormatting).
2004-02-15 Heikki Tauriainen <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* 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 <heikki.tauriainen@hut.fi>
* doc/texinfo.tex: New upstream version.

120
lbtt/src/ExternalTranslator.h
View file

@ -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<TempFileObject*, /* Stack for storing */
deque<TempFileObject*, /* temporary file */
ALLOC(TempFileObject*) > > /* information. */
stack<TempFsysName*, /* Stack for storing */
deque<TempFsysName*, /* temporary file */
ALLOC(TempFsysName*) > > /* 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

60
lbtt/src/Makefile.am
View file

@ -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@

1061
lbtt/src/ProductAutomaton.cc
View file

File diff suppressed because it is too large Load diff

596
lbtt/src/ProductAutomaton.h
View file

@ -1,596 +0,0 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
*
* 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 <config.h>
#include <deque>
#include <iostream>
#include <vector>
#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<GraphEdgeContainer>
{
private:
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
class ProductState : /* A class for */
public Graph<GraphEdgeContainer>::Node /* representing the */
{ /* states of the product
* automaton.
*/
public:
explicit ProductState /* Constructor. */
(const size_type hash_val = 0);
~ProductState(); /* Destructor. */
/* `edges' inherited from Graph<GraphEdgeContainer>::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<ProductAutomaton::size_type, /* maximal strongly */
ALLOC(ProductAutomaton::size_type) > /* 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<GraphEdgeContainer> */
/* `empty' inherited from Graph<GraphEdgeContainer> */
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<GraphEdgeContainer> */
/* `stats' inherited from Graph<GraphEdgeContainer> */
/* `subgraphStats' inherited from Graph<GraphEdgeContainer> */
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<deque<StateIdPair, ALLOC(StateIdPair) >, /* product automaton. */
deque<StateIdPair,
ALLOC(StateIdPair) > >&
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<ProductState&>(*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<ProductState&>(Graph<GraphEdgeContainer>::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<GraphEdgeContainer>::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 */

752
lbtt/src/SccIterator.h
View file

@ -1,752 +0,0 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
*
* 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 <config.h>
#include <deque>
#include <set>
#include <stack>
#include <vector>
#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<EdgeContainer>.
*
* 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<EdgeContainer>::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<EdgeContainer>::size_type s)
* [inserts an element into the
* container]
*
* If the container class is left unspecified,
* it defaults to
* set<Graph<EdgeContainer>::size_type,
* less<Graph<EdgeContainer>::size_type>,
* ALLOC(Graph<EdgeContainer>::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<EdgeContainer>::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<EdgeContainer>
* class, which does not restrict the set of
* nodes in any way.
*
*****************************************************************************/
template<class EdgeContainer>
class NullSccFilter;
template<class EdgeContainer,
class SccContainer
= set<typename Graph<EdgeContainer>::size_type,
less<typename Graph<EdgeContainer>::size_type>,
ALLOC(typename Graph<EdgeContainer>::size_type) >,
class Filter = NullSccFilter<EdgeContainer> >
class SccIterator
{
public:
SccIterator(const Graph<EdgeContainer>& g); /* Constructor. */
/* default copy constructor */
~SccIterator(); /* Destructor. */
/* default assignment operator */
bool operator== /* Equality test for */
(const SccIterator<EdgeContainer, /* two iterators. */
SccContainer,
Filter>& it) const;
bool operator!= /* Inequality test for */
(const SccIterator<EdgeContainer, /* two iterators. */
SccContainer,
Filter>& it) const;
bool operator< /* `Less than' relation */
(const SccIterator<EdgeContainer, /* between two */
SccContainer, /* iterators. */
Filter>& it) const;
bool operator<= /* `Less than or equal' */
(const SccIterator<EdgeContainer, /* relation between two */
SccContainer, /* iterators. */
Filter>& it) const;
bool operator> /* `Greater than' */
(const SccIterator<EdgeContainer, /* relation between two */
SccContainer, /* iterators. */
Filter>& it) const;
bool operator>= /* `Greater than or */
(const SccIterator<EdgeContainer, /* equal' relation */
SccContainer, /* between two */
Filter>& 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<EdgeContainer>& graph; /* Reference to the graph
* with which the iterator
* is associated.
*/
typename Graph<EdgeContainer>::size_type /* Number of graph */
dfs_number; /* nodes processed by
* the iterator.
*/
vector<typename Graph<EdgeContainer>::size_type, /* dfs_ordering[i] */
ALLOC(typename Graph<EdgeContainer> /* 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<typename Graph<EdgeContainer>::size_type, /* lowlink[i] indicates */
ALLOC(typename Graph<EdgeContainer> /* 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<typename Graph<EdgeContainer>::size_type,
typename EdgeContainer::const_iterator>
NodeStackElement;
stack<NodeStackElement, /* Depth-first search */
deque<NodeStackElement, /* backtracking stack. */
ALLOC(NodeStackElement) > >
node_stack;
typename Graph<EdgeContainer>::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<typename Graph<EdgeContainer>::size_type, /* Stack used for */
deque<typename Graph<EdgeContainer> /* collecting the nodes */
::size_type, /* in a strongly */
ALLOC(typename Graph<EdgeContainer> /* 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 EdgeContainer>
class NullSccFilter
{
public:
bool operator()(const typename Graph<EdgeContainer>::Node*) const;
};
/******************************************************************************
*
* Inline function definitions for template class
* SccIterator<EdgeContainer, SccContainer, Filter>.
*
*****************************************************************************/
/* ========================================================================= */
template<class EdgeContainer, class SccContainer, class Filter>
inline SccIterator<EdgeContainer, SccContainer, Filter>::SccIterator
(const Graph<EdgeContainer>& g) :
graph(g), dfs_ordering(graph.size()), lowlink(graph.size())
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class
* SccIterator<EdgeContainer, SccContainer, Filter>.
* 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<EdgeContainer> object).
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
reset();
computeNextScc();
}
/* ========================================================================= */
template<class EdgeContainer, class SccContainer, class Filter>
inline SccIterator<EdgeContainer, SccContainer, Filter>::~SccIterator()
/* ----------------------------------------------------------------------------
*
* Description: Destructor for class
* SccIterator<EdgeContainer, SccContainer, Filter>.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
template<class EdgeContainer, class SccContainer, class Filter>
inline bool SccIterator<EdgeContainer, SccContainer, Filter>::operator==
(const SccIterator<EdgeContainer, SccContainer, Filter>& 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<class EdgeContainer, class SccContainer, class Filter>
inline bool SccIterator<EdgeContainer, SccContainer, Filter>::operator!=
(const SccIterator<EdgeContainer, SccContainer, Filter>& 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<class EdgeContainer, class SccContainer, class Filter>
inline bool SccIterator<EdgeContainer, SccContainer, Filter>::operator<
(const SccIterator<EdgeContainer, SccContainer, Filter>& 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<class EdgeContainer, class SccContainer, class Filter>
inline bool SccIterator<EdgeContainer, SccContainer, Filter>::operator<=
(const SccIterator<EdgeContainer, SccContainer, Filter>& 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<class EdgeContainer, class SccContainer, class Filter>
inline bool SccIterator<EdgeContainer, SccContainer, Filter>::operator>
(const SccIterator<EdgeContainer, SccContainer, Filter>& 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<class EdgeContainer, class SccContainer, class Filter>
inline bool SccIterator<EdgeContainer, SccContainer, Filter>::operator>=
(const SccIterator<EdgeContainer, SccContainer, Filter>& 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<class EdgeContainer, class SccContainer, class Filter>
inline const SccContainer&
SccIterator<EdgeContainer, SccContainer, Filter>::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<class EdgeContainer, class SccContainer, class Filter>
inline const SccContainer*
SccIterator<EdgeContainer, SccContainer, Filter>::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<class EdgeContainer, class SccContainer, class Filter>
inline const SccContainer&
SccIterator<EdgeContainer, SccContainer, Filter>::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<class EdgeContainer, class SccContainer, class Filter>
inline const SccContainer
SccIterator<EdgeContainer, SccContainer, Filter>::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<class EdgeContainer, class SccContainer, class Filter>
inline bool SccIterator<EdgeContainer, SccContainer, Filter>::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<EdgeContainer, SccContainer, Filter>.
*
*****************************************************************************/
/* ========================================================================= */
template<class EdgeContainer, class SccContainer, class Filter>
void SccIterator<EdgeContainer, SccContainer, Filter>::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<typename Graph<EdgeContainer>::size_type,
ALLOC(typename Graph<EdgeContainer>::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<class EdgeContainer, class SccContainer, class Filter>
void SccIterator<EdgeContainer, SccContainer, Filter>::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<typename Graph<EdgeContainer>::size_type,
ALLOC(typename Graph<EdgeContainer>::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<EdgeContainer>::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<EdgeContainer>::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<EdgeContainer>.
*
*****************************************************************************/
/* ========================================================================= */
template<class EdgeContainer>
inline bool NullSccFilter<EdgeContainer>::operator()
(const typename Graph<EdgeContainer>::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<EdgeContainer>::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 */

75
lbtt/src/translate.cc
View file

@ -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<struct sigaction*>(0));
raise(signal_number);
}
/******************************************************************************
*
* Function for installing signal handlers.
*
*****************************************************************************/
static void installSignalHandler(int signum)
{
struct sigaction s;
sigaction(signum, static_cast<struct sigaction*>(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<struct sigaction*>(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);