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

Import of lbtt 1.1.0

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2004-07-07 16:40:50 +00:00
parent 15618b84ea
commit d7b3d97422
49 changed files with 13388 additions and 5404 deletions
Download patch file Download diff file Expand all files Collapse all files

743
lbtt/ChangeLog
View file

@ -1,3 +1,744 @@
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},
@ -12,6 +753,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.

2
lbtt/INSTALL
View file

@ -1,4 +1,4 @@
Copyright 1994, 1995, 1996, 1999, 2000, 2001, 2002 Free Software
Copyright (C) 1994, 1995, 1996, 1999, 2000, 2001, 2002 Free Software
Foundation, Inc.
This file is free documentation; the Free Software Foundation gives

132
lbtt/NEWS
View file

@ -1,4 +1,4 @@
lbtt NEWS -- history of user-visible changes. 13 Feb 2004
lbtt NEWS -- history of user-visible changes. 7 Jul 2004
Copyright (C) 2004 Heikki Tauriainen
Permission is granted to anyone to make or distribute verbatim copies
@ -12,6 +12,136 @@ Copyright (C) 2004 Heikki Tauriainen
Please send bug reports to <heikki.tauriainen@hut.fi>.
Version 1.1.0
* File formats
- The file format for automata description files has changed to
accommodate automata with acceptance conditions on both states
and transitions. The old format for automata remains supported
with the restriction that each guard formula of a transition
should be followed by a newline (with optional preceding white
space).
- In addition to the prefix format for LTL formulas, the input
files used with the `--formulafile' command line option may now
contain formulas in a variety of other formats, such as in the
infix format used by lbtt for log messages, together with formats
used by some LTL-to-Büchi translator implementations (Spin,
LTL2BA, LTL2AUT, Temporal Massage Parlor, Wring, Spot, LBT).
These formats can also be used for guard formulas in automaton
description files (however, lbtt still uses the prefix format in
the input files for the translators).
Thanks to Alexandre Duret-Lutz for useful suggestions for
enhancements.
* Support for symbolic names of implementations
- Beside the numeric identifiers of implementations, lbtt now
accepts also the symbolic names of implementations (as defined in
a configuration file) as parameters for command line options and
internal commands. Consequently, the names of implementations
defined in the configuration file have to be unique.
- The name `lbtt' is now reserved for lbtt's internal model checking
algorithm and cannot be used as a name for an implementation in
the configuration file.
* User commands
- For consistency, numeric intervals in state or implementation
identifier lists can now be specified using either - or ... as a
separator between the bounds of the interval.
- The user command `formula' now accepts an additional parameter
(`normal' or `nnf') for choosing whether to display a formula in
the form in which it was generated or in negation normal form.
- The internal model checking algorithm is now referred to with the
keyword "lbtt" instead of "p" as was the case with previous
versions of lbtt. The internal model checking algorithm can now be
enabled or disabled similarly to the external translators.
- The `consistencyanalysis' and `buchianalysis' commands now show
more information about the accepting runs of Büchi automata to
help examining the runs. (Because of this change, the runs and
witnesses may be longer than in previous versions of lbtt.)
- The `implementations' and `translators' commands are now recognized
as synonyms of the `algorithms' command.
* Configuration files
- Quotes are no longer required for enclosing string values
containing no white space.
- Numeric intervals in formula or state space sizes can now be
specified using either - or ... as a separator between the bounds
of the interval.
- The keywords "Implementation" and "Translator" are now recognized
as synonyms of the "Algorithm" block identifier.
* User interrupts
Keyboard interrupt handling is now enabled only at explicit request
(if not enabled, lbtt simply aborts on keyboard interrupts). The
interrupt handler is enabled by combining the keyword `onbreak' with
any of the three standard interactivity modes (`always', `never', or
`onerror') in the arguments for the `GlobalOptions.Interactive'
configuration file option or the `--interactive' command line option.
For example, use the command line option
`--interactive=onerror,onbreak' to pause testing in case of an error
or on a user interrupt.
* Command line options
- The `--pause' command line option now works identically to the
`--interactive' option.
- The command-line options `--nopause' and `--pauseonerror' are no
longer supported. Use the `--interactive' or the `--pause'
option instead with an optional argument of a comma-separated list
of interactivity modes (`always', `never', `onerror', `onbreak').
* Timeouts
lbtt now supports specifying a time (in wall-clock time) after
which the execution of a translator is aborted if it has not yet
produced a result. The timeout can be set using either the new
configuration file option `GlobalOptions.TranslatorTimeout' or the
equivalent command line option `--translatortimeout'. Both options
require a parameter of the form [hours]h[minutes]min[seconds]s; for
example, use the command line option `--translatortimeout=1h30min'
to set the timeout at one hour and thirty minutes.
* Reporting
- lbtt now reports test statistics also in verbosity modes 1 and 2.
The output of the user command `results' also reflects the active
verbosity mode more accurately.
- lbtt now exits with status 0 only if no test failures were
detected; otherwise the exit status is either 1 (at least
one failure occurred), 2 (error in program configuration or
command line parameters) or 3 (lbtt exited due to an internal
error).
* Internal changes
Due to the changes in the supported file formats, this version
includes a rewrite of the product computation and emptiness checking
algorithms. As this is a major internal change, any information about
unexpected changes in the stability (*) of the tool is welcomed at the
e-mail address given above.
(*) Unfortunately, the above changes in the source code are known to
cause build problems with GCC 2.95. Therefore, this compiler is no
longer officially supported for building the tool.
---------------------------------------------------------------------------
Version 1.0.3
* This release fixes several compilation issues with GNU libc 2.3.2

14
lbtt/README
View file

@ -1,14 +1,14 @@
lbtt version 1.0.3
lbtt version 1.1.0
------------------
lbtt is a tool for testing programs that translate formulas
expressed in propositional linear temporal logic (LTL) into
Büchi automata. The goal of the tool is to assist in the
correct implementation of LTL-to-Büchi translation algorithms
by providing an automated testing environment for LTL-to-Büchi
translators. Additionally, the testing environment can be used
for very basic profiling of different LTL-to-Büchi translators
to evaluate their performance.
Büchi automata. The goal of the tool is to assist implementing
LTL-to-Büchi translation algorithms correctly by providing an
automated testing environment for LTL-to-B@"uchi translators.
Additionally, the testing environment can be used for very basic
profiling of different LTL-to-Büchi translators to evaluate their
performance.
The latest version of the program is available at
<http://www.tcs.hut.fi/Software/lbtt/>.

220
lbtt/configure.ac
View file

@ -1,11 +1,11 @@
# Process this file with autoconf to produce a configure script.
AC_PREREQ([2.53])
AC_INIT([lbtt], [1.0.3], [heikki.tauriainen@hut.fi])
AC_REVISION([Revision: 1.3])
AC_PREREQ([2.59])
AC_INIT([lbtt], [1.1.0], [heikki.tauriainen@hut.fi])
AC_REVISION([Revision: 1.4])
AC_CONFIG_SRCDIR([src/main.cc])
AC_CONFIG_HEADERS([config.h])
AM_INIT_AUTOMAKE
AM_CONFIG_HEADER([config.h])
@ -18,35 +18,68 @@ AC_PROG_CXXCPP
AM_PROG_LEX
AC_PROG_YACC
YACC="${YACC} -d"
# Check whether the user has explicitly disabled the test for the availability
# of the GNU readline library.
# Check whether the user has explicitly disabled support for the GNU readline
# library.
readline=yes
readline_includedir=
readline_libdir=
AC_ARG_WITH([readline],
[AC_HELP_STRING([--without-readline],
[disable check for the GNU readline library])],
[if test x"${withval}" = xno; then readline=no; fi])
AC_ARG_WITH(
[readline],
[AS_HELP_STRING(
[--without-readline],
[disable support for the GNU readline library (default enable)])],
[if test x"${withval}" = xno; then readline=no; fi])
AC_ARG_WITH(
[readline-prefix],
[AS_HELP_STRING(
[--with-readline-prefix=DIR],
[location where GNU readline is installed (optional)])],
[readline_includedir="${withval}/include"
readline_libdir="${withval}/lib"])
AC_ARG_WITH(
[readline-includes],
[AS_HELP_STRING(
[--with-readline-includes=DIR],
[location where GNU readline headers are installed (optional)])],
[readline_includedir="${withval}"])
AC_ARG_WITH(
[readline-libs],
[AS_HELP_STRING(
[--with-readline-libs=DIR],
[location where GNU readline libraries are installed (optional)])],
[readline_libdir="${withval}"])
old_CPPFLAGS=${CPPFLAGS}
old_LDFLAGS=${LDFLAGS}
if test -n "${readline_includedir}"; then
CPPFLAGS="${CPPFLAGS} -I${readline_includedir}"
fi
if test -n "${readline_libdir}"; then
LDFLAGS="${LDFLAGS} -L${readline_libdir}"
fi
# Check for the availability of headers.
AC_HEADER_STDC
AC_CHECK_HEADERS([fcntl.h])
AC_CHECK_HEADERS([libintl.h fcntl.h sys/times.h])
AC_HEADER_SYS_WAIT
# Check for the availability of the GNU readline headers.
if test "${readline}" = yes; then
rl_history_h="readline/history.h"
rl_readline_h="readline/readline.h"
AC_CHECK_HEADERS([${rl_history_h} ${rl_readline_h}],
[],
[readline=no])
AC_CHECK_HEADERS([${rl_history_h} ${rl_readline_h}], [], [readline=no])
fi
AC_LANG([C++])
@ -55,25 +88,36 @@ AC_LANG([C++])
# version of this header that cannot be compiled using g++; enable a workaround
# if necessary.
AC_CHECK_HEADERS([obstack.h],
[AC_MSG_CHECKING([whether obstack.h compilation workaround is needed])
AC_TRY_COMPILE([#include <obstack.h>],
[#if __GLIBC__ == 2 && __GLIBC_MINOR__ == 3
obstack_alloc(0, 0);
#endif],
[AC_MSG_RESULT([no])],
[AC_MSG_RESULT([yes])
AC_DEFINE([GLIBC_OBSTACK_WORKAROUND],
[1],
[Define to 1 to enable an obstack.h C++ compilation workaround for GNU libc 2.3.])])])
AC_CHECK_HEADERS(
[obstack.h],
[AC_MSG_CHECKING([whether obstack.h compilation workaround is needed])
old_cxxflags=${CXXFLAGS}
CXXFLAGS="${CXXFLAGS} -Werror"
AC_COMPILE_IFELSE(
[AC_LANG_PROGRAM(
[[#include <obstack.h>]],
[[
#ifdef __GLIBC__ == 2 && __GLIBC_MINOR__ = 3
obstack_alloc(0, 0);
#endif
]])],
[AC_MSG_RESULT([no])],
[AC_MSG_RESULT([yes])
AC_DEFINE(
[GLIBC_OBSTACK_WORKAROUND],
[1],
[Define to 1 to enable an obstack.h C++ compilation workaround for GNU libc 2.3.])])
CXXFLAGS=${old_cxxflags}])
# Check for the availablility of the sstream or strstream header.
AC_CHECK_HEADERS([sstream],
[],
[AC_CHECK_HEADERS([strstream],
[],
[AC_MSG_ERROR([missing one or more standard C++ headers])])])
AC_CHECK_HEADERS(
[sstream],
[],
[AC_CHECK_HEADERS(
[strstream],
[],
[AC_MSG_ERROR([missing one or more standard C++ headers])])])
@ -86,30 +130,35 @@ AC_CHECK_HEADERS([sstream],
AC_MSG_CHECKING([for slist])
for slist_header in slist ext/slist no; do
if test "${slist_header}" != no; then
AC_TRY_CPP([#include <${slist_header}>], [break])
AC_PREPROC_IFELSE(
[AC_LANG_SOURCE([[#include <${slist_header}>]])],
[break])
fi
done
# Try to determine the C++ namespace in which the class slist resides.
# (For example, GCC versions 3.1, 3.1.1 and 3.2 put slist into the
# __gnu_cxx namespace.)
# (For example, GCC versions >= 3.1 put slist into the __gnu_cxx namespace.)
if test "${slist_header}" != no; then
for slist_namespace in std __gnu_cxx error; do
if test "${slist_namespace}" != error; then
AC_TRY_LINK([#include <${slist_header}>],
[${slist_namespace}::slist<int> s;],
[break])
AC_COMPILE_IFELSE(
[AC_LANG_PROGRAM(
[[#include <${slist_header}>]],
[[${slist_namespace}::slist<int> s;]])],
[break])
fi
done
if test "${slist_namespace}" != error; then
AC_MSG_RESULT([header <${slist_header}>, typename ${slist_namespace}::slist])
AC_DEFINE([HAVE_SLIST],
[1],
[Define to 1 if you have the <slist> or <ext/slist> header file.])
AC_DEFINE_UNQUOTED([SLIST_NAMESPACE],
[${slist_namespace}],
[Define as the name of the C++ namespace containing slist.])
AC_DEFINE(
[HAVE_SLIST],
[1],
[Define to 1 if you have the <slist> or <ext/slist> header file.])
AC_DEFINE_UNQUOTED(
[SLIST_NAMESPACE],
[${slist_namespace}],
[Define as the name of the C++ namespace containing slist.])
AC_SUBST([INCLUDE_SLIST_HEADER], ["#include <${slist_header}>"])
else
slist_header=no
@ -119,26 +168,21 @@ fi
if test "${slist_header}" = no; then
AC_MSG_RESULT([no])
# Check for the availability of the single_client_alloc memory allocator
# available in some compilers supporting the SGI extensions to the Standard
# template library (for example, pre-3.0 versions of gcc). This check is not
# needed if no suitable slist header was found above, since in that case the
# compiler does not support the SGI extensions.
else
AC_MSG_CHECKING([for single_client_alloc])
AC_TRY_LINK([#include <${slist_header}>],
[using namespace std;
${slist_namespace}::slist<int, single_client_alloc> s;],
[AC_MSG_RESULT([yes])
AC_DEFINE([HAVE_SINGLE_CLIENT_ALLOC],
[1],
[Define if your C++ compiler supports the single_client_allocator memory allocator.])],
[AC_MSG_RESULT([no])])
fi
AC_LANG(C)
AC_CHECK_TYPES(
[unsigned long long int],
[AC_DEFINE(
[BIGUINT],
[unsigned long long int],
[Define to an unsigned integer type supported by your compiler.])],
[AC_DEFINE(
[BIGUINT],
[unsigned long int],
[Define to an unsigned integer type supported by your compiler.])])
AC_C_CONST
AC_C_INLINE
@ -146,12 +190,14 @@ AC_C_INLINE
# Checks for library functions.
AC_TYPE_SIGNAL
AC_CHECK_FUNCS([mkdir strchr strtod strtol strtoul getopt_long isatty])
AC_CHECK_FUNCS(
[strchr strtod strtol strtoul strerror mkdir mkstemp open read write close popen pclose pipe fork execvp getpid waitpid alarm sigaction sigprocmask sigemptyset sigaddset times sysconf],
[],
[AC_MSG_ERROR([missing one of the library functions required for compilation])])
AC_CHECK_FUNCS([strsignal isatty getopt_long])
if test x"${ac_cv_func_getopt_long}" = xno; then
AC_LIBOBJ([getopt])
AC_LIBOBJ([getopt1])
AC_CHECK_HEADERS([libintl.h])
AC_CHECK_FUNCS([memset])
fi
@ -163,42 +209,56 @@ if test "${readline}" = yes; then
for READLINELIBS in "-lreadline" "-lreadline -lcurses" "-lreadline -ltermcap" error; do
if test "${READLINELIBS}" != error; then
LIBS="${oldlibs} ${READLINELIBS}"
AC_TRY_LINK([#include <stdio.h>
#include <${rl_history_h}>
#include <${rl_readline_h}>],
[using_history(); readline(""); add_history("");],
[break])
AC_LINK_IFELSE(
[AC_LANG_PROGRAM(
[[
#include <stdio.h>
#include <${rl_history_h}>
#include <${rl_readline_h}>
]],
[[using_history(); readline(""); add_history("");]])],
[break])
fi
done
LIBS=${oldlibs}
if test "${READLINELIBS}" != error; then
AC_DEFINE([HAVE_READLINE],
[1],
[Define if you have the GNU readline library.])
AC_DEFINE(
[HAVE_READLINE],
[1],
[Define if you have the GNU readline library.])
AC_SUBST([READLINELIBS])
AC_MSG_RESULT([${READLINELIBS}])
else
AC_MSG_RESULT([no suitable libraries found, readline support disabled])
READLINELIBS=""
readline=no
fi
fi
if test "${readline}" = no; then
CPPFLAGS=${old_CPPFLAGS}
LDFLAGS=${old_LDFLAGS}
fi
# Check for the availability of the `rand48' family of random number
# generation functions.
have_rand48=yes
AC_CHECK_FUNCS([srand48 lrand48 seed48],
[],
[have_rand48=no
AC_CHECK_FUNCS([rand srand],
[],
[AC_MSG_ERROR([missing library functions for random number generation])])])
AC_CHECK_FUNCS(
[srand48 lrand48 seed48],
[],
[have_rand48=no
AC_CHECK_FUNCS(
[rand srand],
[],
[AC_MSG_ERROR([missing library functions for random number generation])])])
if test "${have_rand48}" = yes; then
AC_DEFINE([HAVE_RAND48],
[1],
[Define if you have the `rand48' family of random number generation functions.])
AC_DEFINE(
[HAVE_RAND48],
[1],
[Define if you have the `rand48' family of random number generation functions.])
fi

1217
lbtt/doc/lbtt.texi
View file

File diff suppressed because it is too large Load diff

598
lbtt/src/BuchiAutomaton.cc
View file

@ -92,7 +92,9 @@ BuchiAutomaton::BuchiAutomaton(const BuchiAutomaton& automaton) :
++transition)
connect(state,
static_cast<const BuchiTransition*>(*transition)->targetNode(),
static_cast<const BuchiTransition*>(*transition)->guard());
static_cast<const BuchiTransition*>(*transition)->guard(),
static_cast<const BuchiTransition*>(*transition)
->acceptanceSets());
operator[](state).acceptanceSets().copy(automaton[state].acceptanceSets(),
number_of_acceptance_sets);
@ -129,7 +131,9 @@ BuchiAutomaton& BuchiAutomaton::operator=(const BuchiAutomaton& automaton)
++transition)
connect(state,
static_cast<const BuchiTransition*>(*transition)->targetNode(),
static_cast<const BuchiTransition*>(*transition)->guard());
static_cast<const BuchiTransition*>(*transition)->guard(),
static_cast<const BuchiTransition*>(*transition)
->acceptanceSets());
operator[](state).acceptanceSets().copy
(automaton[state].acceptanceSets(), number_of_acceptance_sets);
@ -190,113 +194,13 @@ BuchiAutomaton::size_type BuchiAutomaton::expand(size_type node_count)
return nodes.size() - 1;
}
/* ========================================================================= */
BuchiAutomaton* BuchiAutomaton::regularize() const
/* ----------------------------------------------------------------------------
*
* Description: Converts a generalized Büchi automaton (i.e., an automaton
* with any number of accepting state sets) into an automaton
* with only one set of accepting states.
*
* Arguments: None.
*
* Returns: A pointer to an equivalent BuchiAutomaton with exactly one
* set of accepting states.
*
* ------------------------------------------------------------------------- */
{
/*
* If `this' automaton already has exactly one set of accepting states,
* return a copy of `this' automaton.
*/
if (number_of_acceptance_sets == 1)
return new BuchiAutomaton(*this);
/*
* Otherwise construct the result using a depth-first search in `this'
* automaton.
*/
typedef pair<size_type, unsigned long int> ExpandedState;
BuchiAutomaton* result_automaton = new BuchiAutomaton(0, 0, 1);
if (empty())
return result_automaton;
stack<ExpandedState, deque<ExpandedState, ALLOC(ExpandedState) > >
states_to_process;
map<ExpandedState, size_type, less<ExpandedState>, ALLOC(size_type) >
state_mapping;
const GraphEdgeContainer* transitions;
size_type result_source_state, result_target_state;
map<ExpandedState, size_type, less<ExpandedState>, ALLOC(size_type) >
::const_iterator check_state;
ExpandedState state = make_pair(initial_state, 0);
states_to_process.push(state);
state_mapping[state] = result_automaton->expand();
while (!states_to_process.empty())
{
state = states_to_process.top();
states_to_process.pop();
result_source_state = state_mapping[state];
transitions = &operator[](state.first).edges();
if (number_of_acceptance_sets == 0
|| operator[](state.first).acceptanceSets().test(state.second))
{
if (state.second == 0)
(*result_automaton)[result_source_state].acceptanceSets().setBit(0);
if (number_of_acceptance_sets > 0)
{
++state.second;
state.second %= number_of_acceptance_sets;
}
}
for (GraphEdgeContainer::const_iterator transition = transitions->begin();
transition != transitions->end();
++transition)
{
state.first = (*transition)->targetNode();
check_state = state_mapping.find(state);
if (check_state == state_mapping.end())
{
result_target_state = result_automaton->expand();
state_mapping[state] = result_target_state;
states_to_process.push(state);
}
else
result_target_state = check_state->second;
result_automaton->connect(result_source_state, result_target_state,
static_cast<const BuchiTransition*>
(*transition)->guard());
}
}
return result_automaton;
}
/* ========================================================================= */
void BuchiAutomaton::read(istream& input_stream)
/* ----------------------------------------------------------------------------
*
* Description: Reads an automaton description (which may represent a
* generalized Büchi automaton) from a stream and stores it
* into the automaton object, converting it to a regular
* Büchi automaton if necessary.
* into the automaton object.
*
* Argument: input_stream -- A reference to an input stream.
*
@ -312,20 +216,63 @@ void BuchiAutomaton::read(istream& input_stream)
try
{
/*
* Read in the number of states in the generalized Büchi automaton.
*/
/* Read the number of states in the generalized Büchi automaton. */
einput_stream >> number_of_states;
/*
* If the automaton is empty, do nothing.
*/
/* If the automaton is empty, do nothing. */
if (number_of_states == 0)
return;
einput_stream >> number_of_acceptance_sets;
/*
* Determine the number and placement of acceptance sets.
* (Acceptance sets are described using strings described by the regular
* expression [0-9]+(s|S|t|T)*, where the [0-9]+ part corresponds to the
* number of the sets, and the (s|S|t|T)* part corresponds to the
* placement of the sets -- s or S for states, t or T for transitions.
* To retain compatibility with lbtt 1.0.x, the acceptance set placement
* defaults to acceptance sets on states if is not given explicitly.)
*/
bool acceptance_sets_on_states = false;
bool acceptance_sets_on_transitions = false;
string tok;
einput_stream >> tok;
string::size_type s_pos = string::npos;
string::size_type t_pos = string::npos;
string::size_type pos = tok.find_first_not_of("0123456789");
if (pos == 0)
throw AutomatonParseException
("invalid specification for acceptance sets");
number_of_acceptance_sets = strtoul(tok.substr(0, pos).c_str(), 0, 10);
for ( ; pos < tok.length(); ++pos)
{
if (tok[pos] == 's' || tok[pos] == 'S')
{
s_pos = pos;
acceptance_sets_on_states = true;
}
else if (tok[pos] == 't' || tok[pos] == 'T')
{
t_pos = pos;
acceptance_sets_on_transitions = true;
}
else
throw AutomatonParseException
("invalid specification for acceptance sets");
}
if (s_pos == string::npos && t_pos == string::npos)
{
acceptance_sets_on_states = true;
acceptance_sets_on_transitions = false;
}
BitArray acc_sets(number_of_acceptance_sets);
/*
* Allocate space for the regular Büchi automaton that will be constructed
@ -446,36 +393,41 @@ void BuchiAutomaton::read(istream& input_stream)
operator[](current_state).acceptanceSets().clear
(number_of_acceptance_sets);
while (1)
if (acceptance_sets_on_states)
{
einput_stream >> acceptance_set_mapping.first;
if (acceptance_set_mapping.first == -1)
break;
acceptance_set_finder =
acceptance_set_map.insert(acceptance_set_mapping);
if (!acceptance_set_finder.second)
acceptance_set = (acceptance_set_finder.first)->second;
else
while (1)
{
if (acceptance_set_mapping.second >= number_of_acceptance_sets)
throw AutomatonParseException("number of acceptance sets "
"does not match automaton state "
"definitions");
einput_stream >> acceptance_set_mapping.first;
acceptance_set = acceptance_set_mapping.second;
++acceptance_set_mapping.second;
}
if (acceptance_set_mapping.first == -1)
break;
operator[](current_state).acceptanceSets().setBit(acceptance_set);
acceptance_set_finder =
acceptance_set_map.insert(acceptance_set_mapping);
if (!acceptance_set_finder.second)
acceptance_set = (acceptance_set_finder.first)->second;
else
{
if (acceptance_set_mapping.second >= number_of_acceptance_sets)
throw AutomatonParseException("number of acceptance sets "
"does not match automaton state "
"definitions");
acceptance_set = acceptance_set_mapping.second;
++acceptance_set_mapping.second;
}
operator[](current_state).acceptanceSets().setBit(acceptance_set);
}
}
/*
* Process the transitions from the state to other states. Read a
* target state id and add a mapping for it in the translation table if
* necessary. Then, read the propositional formula guarding the
* necessary. If the automaton is allowed to have acceptance sets
* associated with transitions, read an additional list of acceptance
* sets. Finally, read the propositional formula guarding the
* transition and connect the current state to the target using the
* guard formula.
*/
@ -501,6 +453,42 @@ void BuchiAutomaton::read(istream& input_stream)
state_mapping.second++;
}
acc_sets.clear(number_of_acceptance_sets);
/*
* If automata with acceptance sets on transitions are accepted, read
* the acceptance sets associated with the transition.
*/
if (acceptance_sets_on_transitions)
{
while (1)
{
einput_stream >> acceptance_set_mapping.first;
if (acceptance_set_mapping.first == -1)
break;
acceptance_set_finder =
acceptance_set_map.insert(acceptance_set_mapping);
if (!acceptance_set_finder.second)
acceptance_set = (acceptance_set_finder.first)->second;
else
{
if (acceptance_set_mapping.second >= number_of_acceptance_sets)
throw AutomatonParseException("number of acceptance sets "
"does not match automaton state "
"definitions");
acceptance_set = acceptance_set_mapping.second;
++acceptance_set_mapping.second;
}
acc_sets.setBit(acceptance_set);
}
}
try
{
guard = ::Ltl::LtlFormula::read(input_stream);
@ -516,7 +504,7 @@ void BuchiAutomaton::read(istream& input_stream)
throw AutomatonParseException("illegal operators in guard formula");
}
connect(current_state, neighbor_state, guard);
connect(current_state, neighbor_state, guard, acc_sets);
}
processed_states.setBit(current_state);
@ -544,297 +532,6 @@ void BuchiAutomaton::read(istream& input_stream)
}
}
/* ========================================================================= */
BuchiAutomaton* BuchiAutomaton::intersect
(const BuchiAutomaton& a1, const BuchiAutomaton& a2,
map<size_type, StateIdPair, less<size_type>, ALLOC(StateIdPair) >*
intersection_state_mapping)
/* ----------------------------------------------------------------------------
*
* Description: Computes the intersection of two Büchi automata and returns
* a pointer to the intersection of the two automata.
*
* Arguments: a1, a2 -- References to two constant
* Büchi automata.
* intersection_state_mapping -- An (optional) pointer to a
* map which can be used to find
* out the state identifiers of
* the original automata to
* which a particular state in
* the intersection corresponds.
*
* Returns: A newly allocated BuchiAutomaton representing the
* intersection of the two automata.
*
* ------------------------------------------------------------------------- */
{
if (intersection_state_mapping != 0)
intersection_state_mapping->clear();
/*
* If either of the original automata is empty, the intersection is also
* empty.
*/
if (a1.empty() || a2.empty())
return new BuchiAutomaton(0, 0, 0);
BuchiAutomaton* automaton;
/*
* Determine the number of acceptance sets in the intersection.
*/
const bool a1_has_no_acceptance_sets = (a1.number_of_acceptance_sets == 0);
const bool a2_has_no_acceptance_sets = (a2.number_of_acceptance_sets == 0);
unsigned long int number_of_intersection_acceptance_sets;
if (a1_has_no_acceptance_sets && a2_has_no_acceptance_sets)
number_of_intersection_acceptance_sets = 0;
else
number_of_intersection_acceptance_sets = a1.number_of_acceptance_sets
+ a2.number_of_acceptance_sets;
automaton = new BuchiAutomaton(1, 0, number_of_intersection_acceptance_sets);
/*
* A stack for processing pairs of states of the original automata.
*/
stack<const StateIdPair*, deque<const StateIdPair*,
ALLOC(const StateIdPair*) > >
unprocessed_states;
/*
* `state_mapping' maps pairs of states of the original automata to the
* states of the new automaton.
*/
map<StateIdPair, size_type, less<StateIdPair>, ALLOC(size_type) >
state_mapping;
size_type first_free_id = 1; /* First free identifier for a
* new state in the intersection
* automaton.
*/
const StateIdPair* state_pair; /* Pointer to pair of two state
* identifiers of the original
* automata.
*/
size_type intersect_state; /* `Current' state in the
* intersection automaton.
*/
bool intersect_state_valid; /* True if the current state has
* been determined by using the
* mapping.
*/
BitArray* intersect_acceptance_sets; /* Pointers for accessing the */
const BitArray* acceptance_sets; /* acceptance sets of the new
* and the original automata.
*/
const GraphEdgeContainer* transitions1; /* Pointers for accessing the */
const GraphEdgeContainer* transitions2; /* transitions of the two
* original automata.
*/
::Ltl::LtlFormula* guard1; /* Pointers for accessing the */
::Ltl::LtlFormula* guard2; /* guard formulas of the */
::Ltl::LtlFormula* new_guard; /* transitions of the
* automata.
*/
/*
* Insert the initial state into the state mapping.
*/
state_mapping.insert(make_pair(make_pair(a1.initial_state, a2.initial_state),
0));
unprocessed_states.push(&(state_mapping.begin()->first));
/*
* Adjust the acceptance sets of the initial state of the intersection.
*/
intersect_acceptance_sets = &((*automaton)[0].acceptanceSets());
if (!a1_has_no_acceptance_sets)
{
acceptance_sets = &(a1[a1.initial_state].acceptanceSets());
for (unsigned long int accept_set = 0;
accept_set < a1.number_of_acceptance_sets;
accept_set++)
{
if (acceptance_sets->test(accept_set))
intersect_acceptance_sets->setBit(accept_set);
}
}
if (!a2_has_no_acceptance_sets)
{
acceptance_sets = &(a2[a2.initial_state].acceptanceSets());
for (unsigned long int accept_set = 0;
accept_set < a2.number_of_acceptance_sets;
accept_set++)
{
if (acceptance_sets->test(accept_set))
intersect_acceptance_sets->setBit(a1.number_of_acceptance_sets
+ accept_set);
}
}
/*
* Pop pairs of states of the two original automata until all states have
* been processed.
*/
try
{
while (!unprocessed_states.empty())
{
if (::user_break)
throw UserBreakException();
intersect_state_valid = false;
state_pair = unprocessed_states.top();
unprocessed_states.pop();
/*
* Loop through the transitions of the two original automata. If the
* conjunction of the guard formulae of any two transitions is
* satisfiable, insert a new transition into the intersection automaton.
* Create new states in the intersection automaton if necessary.
*/
transitions1 = &a1[state_pair->first].edges();
transitions2 = &a2[state_pair->second].edges();
for (GraphEdgeContainer::const_iterator tr1 = transitions1->begin();
tr1 != transitions1->end();
++tr1)
{
guard1 = &(static_cast<BuchiTransition*>(*tr1)->guard());
for (GraphEdgeContainer::const_iterator tr2 = transitions2->begin();
tr2 != transitions2->end();
++tr2)
{
guard2 = &(static_cast<BuchiTransition*>(*tr2)->guard());
new_guard = &Ltl::And::construct(*guard1, *guard2);
if (new_guard->satisfiable())
{
/*
* Determine the `current' state of the intersection automaton.
*/
if (!intersect_state_valid)
{
intersect_state = state_mapping[*state_pair];
intersect_state_valid = true;
}
/*
* Test whether the state pair pointed to by the two transitions
* is already in the intersection.
*/
pair<map<StateIdPair, size_type, less<StateIdPair>,
ALLOC(size_type) >::iterator, bool>
check_state;
check_state
= state_mapping.insert(make_pair(make_pair((*tr1)->targetNode(),
(*tr2)->targetNode()),
first_free_id));
if (check_state.second) /* insertion occurred? */
{
automaton->expand();
/*
* Determine the acceptance sets to which the new state in the
* intersection automaton belongs.
*/
intersect_acceptance_sets
= &((*automaton)[first_free_id].acceptanceSets());
if (!a1_has_no_acceptance_sets)
{
acceptance_sets = &(a1[check_state.first->first.first].
acceptanceSets());
for (unsigned long int accept_set = 0;
accept_set < a1.number_of_acceptance_sets;
accept_set++)
{
if (acceptance_sets->test(accept_set))
intersect_acceptance_sets->setBit(accept_set);
}
}
if (!a2_has_no_acceptance_sets)
{
acceptance_sets = &(a2[check_state.first->first.second].
acceptanceSets());
for (unsigned long int accept_set = 0;
accept_set < a2.number_of_acceptance_sets;
accept_set++)
{
if (acceptance_sets->test(accept_set))
intersect_acceptance_sets->setBit
(a1.number_of_acceptance_sets + accept_set);
}
}
/*
* Connect the `current' state of the intersection automaton to
* the new state.
*/
automaton->connect(intersect_state, first_free_id, new_guard);
first_free_id++;
unprocessed_states.push(&(check_state.first->first));
}
else
automaton->connect(intersect_state, check_state.first->second,
new_guard);
}
else
::Ltl::LtlFormula::destruct(new_guard);
}
}
}
if (intersection_state_mapping != 0)
{
for (map<StateIdPair, size_type, less<StateIdPair>, ALLOC(size_type) >
::const_iterator mapping = state_mapping.begin();
mapping != state_mapping.end();
++mapping)
intersection_state_mapping->insert(make_pair(mapping->second,
mapping->first));
}
}
catch (...)
{
delete automaton;
throw;
}
return automaton;
}
/* ========================================================================= */
void BuchiAutomaton::print
(ostream& stream, const int indent, const GraphOutputFormat fmt) const
@ -876,7 +573,7 @@ void BuchiAutomaton::print
<< " transitions.\n" + string(indent, ' ')
+ "The automaton has "
<< number_of_acceptance_sets
<< " sets of accepting states.\n" + string(indent, ' ')
<< " acceptance sets.\n" + string(indent, ' ')
+ "The reachable part of the automaton contains\n"
+ string(indent + 4, ' ')
<< reachable_part_statistics.first
@ -937,7 +634,8 @@ void BuchiAutomaton::print
++transition)
{
estream << string(indent + 2, ' ') + 'n' << state;
(*transition)->print(stream, indent, fmt);
static_cast<const BuchiTransition*>(*transition)
->print(stream, indent, fmt, number_of_acceptance_sets);
estream << ";\n";
}
}
@ -960,16 +658,23 @@ void BuchiAutomaton::print
/* ========================================================================= */
void BuchiAutomaton::BuchiTransition::print
(ostream& stream, const int indent, const GraphOutputFormat fmt) const
(ostream& stream, const int indent, const GraphOutputFormat fmt,
const unsigned long int number_of_acceptance_sets) const
/* ----------------------------------------------------------------------------
*
* Description: Writes information about a transition between two states of
* a Büchi automaton.
*
* Arguments: stream -- A reference to an output stream.
* indent -- Number of spaces to leave to the left of output.
* fmt -- Determines the format of output.
*
* Arguments: stream -- A reference to an output
* stream.
* indent -- Number of spaces to leave to
* the left of output.
* fmt -- Determines the format of
* output.
* number_of_acceptance_sets -- Number of acceptance sets in
* the automaton to which the
* transition belongs.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
@ -977,11 +682,9 @@ void BuchiAutomaton::BuchiTransition::print
Exceptional_ostream estream(&stream, ios::failbit | ios::badbit);
if (fmt == NORMAL)
{
estream << string(indent, ' ') + "Transition to state "
<< targetNode()
<< " [ guard: " << *guard_formula << " ]\n";
}
<< " [ acc.: ";
else if (fmt == DOT)
{
string formula(StringUtil::toString(*guard_formula));
@ -1002,9 +705,33 @@ void BuchiAutomaton::BuchiTransition::print
else
estream << formula[i];
}
estream << "\",fontsize=10,fontname=\"Courier-Bold\"]";
estream << "\\n";
}
estream << '{';
bool first_printed = false;
for (unsigned long int accept_set = 0;
accept_set < number_of_acceptance_sets;
++accept_set)
{
if (acceptance_sets[accept_set])
{
if (first_printed)
estream << ", ";
else
first_printed = true;
estream << accept_set;
}
}
estream << '}';
if (fmt == NORMAL)
estream << ", guard: " << *guard_formula << " ]\n";
else if (fmt == DOT)
estream << "\",fontsize=10,fontname=\"Courier-Bold\"]";
estream.flush();
}
@ -1069,7 +796,8 @@ void BuchiAutomaton::BuchiState::print
GraphEdgeContainer::const_iterator edge;
for (edge = edges().begin(); edge != edges().end(); ++edge)
(*edge)->print(stream, indent);
static_cast<const BuchiAutomaton::BuchiTransition*>(*edge)
->print(stream, indent, fmt, number_of_acceptance_sets);
} else
estream << string(indent, ' ') + "No transitions to other states.\n";

196
lbtt/src/BuchiAutomaton.h
View file

@ -21,6 +21,7 @@
#define BUCHIAUTOMATON_H
#include <config.h>
#include <cstdlib>
#include <iostream>
#include <map>
#include <string>
@ -38,8 +39,7 @@ namespace Graph
/******************************************************************************
*
* A class for representing Büchi automata with a single set of accepting
* states.
* A class for representing generalized Büchi automata.
*
*****************************************************************************/
@ -139,15 +139,19 @@ public:
void connect /* Connects two states */
(const size_type father, /* of the automaton with */
const size_type child); /* an unguarded
* transition.
* transition with no
* associated acceptance
* sets.
*/
void connect /* Connects two states */
(const size_type father, const size_type child, /* of the automaton with */
::Ltl::LtlFormula& guard); /* a transition guarded */
void connect /* by a propositional */
(const size_type father, const size_type child, /* formula. */
::Ltl::LtlFormula* guard);
::Ltl::LtlFormula& guard, /* a transition guarded */
const BitArray& acc_sets); /* by a propositional */
void connect /* formula. */
(const size_type father, const size_type child,
::Ltl::LtlFormula* guard,
const BitArray& acc_sets);
/* `disconnect' inherited from Graph<GraphEdgeContainer> */
@ -167,12 +171,6 @@ public:
* automaton.
*/
BuchiAutomaton* regularize() const; /* Converts a generalized
* automaton to an
* automaton with one set
* of accepting states.
*/
void read(istream& input_stream); /* Reads the automaton
* from a stream.
*/
@ -181,17 +179,10 @@ public:
(ostream& stream = cout, /* about the automaton */
const int indent = 0, /* to a stream in */
const GraphOutputFormat fmt = NORMAL) const; /* various formats
* (determined by the
* `fmt' argument).
* (determined by the
* `fmt' argument).
*/
static BuchiAutomaton* intersect /* Computes the */
(const BuchiAutomaton& a1, /* intersection of two */
const BuchiAutomaton& a2, /* Büchi automata. */
map<size_type, StateIdPair,
less<size_type>, ALLOC(StateIdPair) >*
intersection_state_mapping = 0);
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
class AutomatonParseException; /* Class for reporting
@ -227,14 +218,12 @@ class BuchiAutomaton::BuchiTransition : public Graph<GraphEdgeContainer>::Edge
public:
BuchiTransition /* Constructor. */
(const size_type target,
::Ltl::LtlFormula* formula);
::Ltl::LtlFormula* formula,
const BitArray& acc_sets,
unsigned long int num_acc_sets);
~BuchiTransition(); /* Destructor. */
private:
public:
/* `targetNode' inherited from Graph<GraphEdgeContainer>::Edge */
bool enabled /* These functions test */
@ -249,14 +238,24 @@ public:
* propositional formula
* guarding the transition.
*/
BitArray& acceptanceSets(); /* Returns the */
const BitArray& acceptanceSets() const; /* acceptance sets
* associated with the
* the transition.
*/
void print /* Writes information */
(ostream& stream, /* about the transition */
const int indent, /* (as a plain graph */
const GraphOutputFormat fmt) const; /* edge) to a stream. */
void print /* Writes information */
(ostream& stream = cout, /* about the transition */
const int indent = 0, /* to a stream in */
const GraphOutputFormat fmt = NORMAL) const; /* various formats
* (determined by the
* `fmt' argument).
*/
(ostream& stream, /* about the transition */
const int indent, /* to a stream in */
const GraphOutputFormat fmt, /* various formats */
const unsigned long int /* (determined by the */
number_of_acceptance_sets) const; /* `fmt' argument). */
private:
BuchiTransition(const BuchiTransition&); /* Prevent copying and */
@ -281,6 +280,11 @@ private:
* formula guarding the
* transition.
*/
BitArray acceptance_sets; /* Acceptance sets
* associated with the
* transition.
*/
};
@ -372,7 +376,8 @@ inline void BuchiAutomaton::connect
*
* Description: Connects two states of a BuchiAutomaton to each other with an
* unguarded transition (actually, a transition with a guard
* that is always true).
* that is always true) with an empty set of acceptance
* conditions.
*
* Arguments: father -- Source state identifier.
* child -- Target state identifier.
@ -381,50 +386,59 @@ inline void BuchiAutomaton::connect
*
* ------------------------------------------------------------------------- */
{
connect(father, child, &(::Ltl::True::construct()));
BitArray acc_sets(number_of_acceptance_sets);
acc_sets.clear(number_of_acceptance_sets);
connect(father, child, &(::Ltl::True::construct()), acc_sets);
}
/* ========================================================================= */
inline void BuchiAutomaton::connect
(const size_type father, const size_type child, ::Ltl::LtlFormula& guard)
(const size_type father, const size_type child, ::Ltl::LtlFormula& guard,
const BitArray& acc_sets)
/* ----------------------------------------------------------------------------
*
* Description: Connects two states of a BuchiAutomaton to each other, using
* a LtlFormula (which is actually a propositional formula) to
* guard the transition between the states.
*
* Arguments: father -- Source state.
* child -- Target state.
* guard -- A reference to an LtlFormula (a propositional
* formula) guarding the transition.
* Arguments: father -- Source state.
* child -- Target state.
* guard -- A reference to an LtlFormula (a propositional
* formula) guarding the transition.
* acc_sets -- A reference to a BitArray giving the
* acceptance sets associated with the transition.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
connect(father, child, guard.clone());
connect(father, child, guard.clone(), acc_sets);
}
/* ========================================================================= */
inline void BuchiAutomaton::connect
(const size_type father, const size_type child, ::Ltl::LtlFormula* guard)
(const size_type father, const size_type child, ::Ltl::LtlFormula* guard,
const BitArray& acc_sets)
/* ----------------------------------------------------------------------------
*
* Description: Connects two states of a BuchiAutomaton to each other, using
* a LtlFormula (which is actually a propositional formula) to
* guard the transition between the states.
*
* Arguments: father -- Source state.
* child -- Target state.
* guard -- A pointer to an LtlFormula (a propositional
* formula) guarding the transition. The transition
* will "own" the guard formula.
* Arguments: father -- Source state.
* child -- Target state.
* guard -- A pointer to an LtlFormula (a propositional
* formula) guarding the transition. The
* transition will "own" the guard formula.
* acc_sets -- A reference to a BitArray giving the acceptance
* sets associated with the transition.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
BuchiTransition* new_buchi_transition = new BuchiTransition(child, guard);
BuchiTransition* new_buchi_transition
= new BuchiTransition(child, guard, acc_sets, number_of_acceptance_sets);
try
{
@ -512,39 +526,28 @@ inline istream& operator>>(istream& stream, BuchiAutomaton& automaton)
/* ========================================================================= */
inline BuchiAutomaton::BuchiTransition::BuchiTransition
(const size_type target, ::Ltl::LtlFormula* formula) :
Edge(target), guard_formula(formula)
(const size_type target, ::Ltl::LtlFormula* formula,
const BitArray& acc_sets, unsigned long int num_acc_sets) :
Edge(target), guard_formula(formula), acceptance_sets(num_acc_sets)
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class BuchiAutomaton::BuchiTransition.
* Initializes a new transition to a BuchiState, guarded by an
* LtlFormula (which is actually a propositional formula).
*
* Arguments: target -- Identifier of the target state of the automaton.
* formula -- A pointer to a propositional formula guarding
* the transition.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline BuchiAutomaton::BuchiTransition::BuchiTransition
(const BuchiTransition& transition) :
Edge(transition), guard_formula(transition.guard_formula->clone())
/* ----------------------------------------------------------------------------
*
* Description: Copy constructor for class BuchiAutomaton::BuchiTransition.
* Creates a copy of a BuchiTransition object.
*
* Arguments: transition -- BuchiTransition to be copied.
* Arguments: target -- Identifier of the target state of the
* automaton.
* formula -- A pointer to a propositional formula guarding
* the transition.
* acc_sets -- A reference to a constant BitArray containing
* the acceptance sets associated with the
* transition.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
acceptance_sets.copy(acc_sets, num_acc_sets);
}
/* ========================================================================= */
@ -688,6 +691,59 @@ inline ::Ltl::LtlFormula& BuchiAutomaton::BuchiTransition::guard() const
return *guard_formula;
}
/* ========================================================================= */
inline BitArray& BuchiAutomaton::BuchiTransition::acceptanceSets()
/* ----------------------------------------------------------------------------
*
* Description: Returns the acceptance sets associated with a
* BuchiTransition.
*
* Arguments: None.
*
* Returns: A reference to the BitArray storing the acceptance sets
* associated with the transition.
*
* ------------------------------------------------------------------------- */
{
return acceptance_sets;
}
/* ========================================================================= */
inline const BitArray& BuchiAutomaton::BuchiTransition::acceptanceSets() const
/* ----------------------------------------------------------------------------
*
* Description: Returns the acceptance sets associated with a
* BuchiTransition.
*
* Arguments: None.
*
* Returns: A constant reference to the BitArray storing the acceptance
* sets associated with the transition.
*
* ------------------------------------------------------------------------- */
{
return acceptance_sets;
}
/* ========================================================================= */
inline void BuchiAutomaton::BuchiTransition::print
(ostream& stream, const int indent, const GraphOutputFormat fmt) const
/* ----------------------------------------------------------------------------
*
* Description: Writes information about a transition (as a plain graph edge
* without any associated information) to a stream.
*
* Arguments: stream -- A reference to an output stream.
* indent -- Number of spaces to leave to the left of output.
* fmt -- Determines the output format of the transition.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
Graph<GraphEdgeContainer>::Edge::print(stream, indent, fmt);
}
/******************************************************************************

98
lbtt/src/BuchiProduct.cc Normal file
View file

@ -0,0 +1,98 @@
/*
* 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.
*/
#include "BuchiProduct.h"
namespace Graph
{
/******************************************************************************
*
* Static member definitions for class BuchiProduct.
*
*****************************************************************************/
map< ::Ltl::LtlFormula*, BuchiProduct::SatisfiabilityMapping,
less< ::Ltl::LtlFormula*>, ALLOC(BuchiProduct::SatisfiabilityMapping) >
BuchiProduct::sat_cache;
/******************************************************************************
*
* Function definitions for class BuchiProduct.
*
*****************************************************************************/
/* ========================================================================= */
bool BuchiProduct::synchronizable
(const Graph<GraphEdgeContainer>::Edge& transition_1,
const Graph<GraphEdgeContainer>::Edge& transition_2)
/* ----------------------------------------------------------------------------
*
* Description: Tests whether two transitions of two Büchi automata are
* synchronizable by checking whether the conjunction of their
* guard formulas is satisfiable.
*
* Arguments: transition_1, -- Constant references to the transitions.
* transition_2
*
* Returns: true iff the transitions are synchronizable. The result is
* also stored into `this->sat_cache' for later reference.
*
* ------------------------------------------------------------------------- */
{
using ::Ltl::LtlFormula;
using ::Ltl::And;
LtlFormula* guard_1 = &static_cast<const BuchiAutomaton::BuchiTransition&>
(transition_1).guard();
LtlFormula* guard_2 = &static_cast<const BuchiAutomaton::BuchiTransition&>
(transition_2).guard();
if (guard_2 > guard_1)
{
LtlFormula* swap_guard = guard_2;
guard_2 = guard_1;
guard_1 = swap_guard;
}
map<LtlFormula*, SatisfiabilityMapping, less<LtlFormula*>,
ALLOC(SatisfiabilityMapping) >::iterator
sat_cache_element = sat_cache.find(guard_1);
if (sat_cache_element == sat_cache.end())
sat_cache_element = sat_cache.insert
(make_pair(guard_1, SatisfiabilityMapping())).first;
else
{
SatisfiabilityMapping::const_iterator sat_result
= sat_cache_element->second.find(guard_2);
if (sat_result != sat_cache_element->second.end())
return sat_result->second;
}
LtlFormula* f = &And::construct(*guard_1, *guard_2);
const bool result = f->satisfiable();
LtlFormula::destruct(f);
sat_cache_element->second.insert(make_pair(guard_2, result));
return result;
}
}

512
lbtt/src/BuchiProduct.h Normal file
View file

@ -0,0 +1,512 @@
/*
* 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 BUCHIPRODUCT_H
#define BUCHIPRODUCT_H
#include <config.h>
#include <deque>
#include <iostream>
#include <map>
#include <string>
#include <vector>
#include "BitArray.h"
#include "BuchiAutomaton.h"
#include "EdgeContainer.h"
#include "Graph.h"
#include "LtlFormula.h"
using namespace std;
namespace Graph
{
/******************************************************************************
*
* A class with operations for checking the intersection of two Büchi automata
* (represented as two BuchiAutomaton objects) for emptiness.
*
*****************************************************************************/
class BuchiProduct
{
public:
BuchiProduct /* Constructor. */
(const Graph<GraphEdgeContainer>& a1,
const Graph<GraphEdgeContainer>& a2);
/* default copy constructor */
~BuchiProduct(); /* Destructor. */
/* default assignment operator */
bool empty() const; /* Tells whether the
* intersection of the
* Büchi automata
* associated with the
* product object is
* (trivially) empty.
*/
unsigned long int numberOfAcceptanceSets() const; /* Tells the number of
* acceptance sets in the
* intersection of the
* automata associated with
* the object.
*/
const BuchiAutomaton::BuchiState& firstComponent /* Mappings between an */
(const Graph<GraphEdgeContainer>::size_type /* intersection state */
state_id) const; /* identifier and states */
const BuchiAutomaton::BuchiState& secondComponent /* of the underlying */
(const Graph<GraphEdgeContainer>::size_type /* automata. */
state_id) const;
void mergeAcceptanceInformation /* Merges the acceptance */
(const Graph<GraphEdgeContainer>::Node& state1, /* sets associated with */
const Graph<GraphEdgeContainer>::Node& state2, /* a pair of states into */
BitArray& acceptance_sets) const; /* a collection of sets. */
void mergeAcceptanceInformation /* Merges the acceptance */
(const Graph<GraphEdgeContainer>::Edge& /* sets associated with */
transition1, /* a pair of */
const Graph<GraphEdgeContainer>::Edge& /* transitions into a */
transition2, /* collection of sets. */
BitArray& acceptance_sets) const;
void validateEdgeIterators /* Ensures that a pair */
(const Graph<GraphEdgeContainer>::Node& /* of transition */
state_1, /* iterators points to a */
const Graph<GraphEdgeContainer>::Node& /* transition beginning */
state_2, /* from a given state in */
GraphEdgeContainer::const_iterator& /* the intersection of */
transition_1, /* two Büchi automata. */
GraphEdgeContainer::const_iterator&
transition_2);
void incrementEdgeIterators /* Updates a pair of */
(const Graph<GraphEdgeContainer>::Node& /* transition iterators */
state_1, /* to make them point to */
const Graph<GraphEdgeContainer>::Node& /* the "next" transition */
state_2, /* starting from a given */
GraphEdgeContainer::const_iterator& /* state in the */
transition_1, /* intersection of two */
GraphEdgeContainer::const_iterator& /* Büchi automata. */
transition_2);
static void clearSatisfiabilityCache(); /* Clears information about
* the satisfiability of
* the guards of product
* transitions.
*/
private:
void mergeAcceptanceInformation /* Bitwise or between */
(const BitArray& sets1, const BitArray& sets2, /* two "component" */
BitArray& result) const; /* acceptance set
* vectors and a result
* vector.
*/
bool synchronizable /* Tests whether a pair */
(const Graph<GraphEdgeContainer>::Edge& /* of transitions of two */
transition_1, /* Büchi automata is */
const Graph<GraphEdgeContainer>::Edge& /* synchronizable. */
transition_2);
const BuchiAutomaton& automaton_1; /* Automata associated */
const BuchiAutomaton& automaton_2; /* with the BuchiProduct */
/* object. */
const unsigned long int /* Number of acceptance */
number_of_acceptance_sets; /* sets in the
* intersection of the
* automata.
*/
typedef map< ::Ltl::LtlFormula*, bool, /* Type definition for */
less< ::Ltl::LtlFormula*>, /* storing information */
ALLOC(bool) > /* about the */
SatisfiabilityMapping; /* satisfiability of the
* guards of product
* transitions.
*/
static map< ::Ltl::LtlFormula*, /* Result cache for */
SatisfiabilityMapping, /* satisfiability tests. */
less< ::Ltl::LtlFormula*>,
ALLOC(SatisfiabilityMapping) >
sat_cache;
};
/******************************************************************************
*
* Inline function definitions for class BuchiProduct.
*
*****************************************************************************/
/* ========================================================================= */
inline BuchiProduct::BuchiProduct
(const Graph<GraphEdgeContainer>& a1, const Graph<GraphEdgeContainer>& a2) :
automaton_1(static_cast<const BuchiAutomaton&>(a1)),
automaton_2(static_cast<const BuchiAutomaton&>(a2)),
number_of_acceptance_sets(static_cast<const BuchiAutomaton&>(a1)
.numberOfAcceptanceSets()
+ static_cast<const BuchiAutomaton&>(a2)
.numberOfAcceptanceSets())
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class BuchiProduct. Initializes a new object
* with operations for checking the emptiness of two Büchi
* automata.
*
* Arguments: a1, a2 -- Constant references to two
* Graph<GraphEdgeContainer> objects, assumed to be
* BüchiAutomaton objects to which to apply the
* operations.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline BuchiProduct::~BuchiProduct()
/* ----------------------------------------------------------------------------
*
* Description: Destructor for class BuchiProduct.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline bool BuchiProduct::empty() const
/* ----------------------------------------------------------------------------
*
* Description: Tells whether the intersection of the Büchi automata
* associated with a BuchiProduct object is (trivially) empty.
*
* Arguments: None.
*
* Returns: true iff either of the automata associated with the
* BuchiProduct object is (trivially) empty (i.e., whether
* either of the automata has no states).
*
* ------------------------------------------------------------------------- */
{
return (automaton_1.empty() || automaton_2.empty());
}
/* ========================================================================= */
inline unsigned long int BuchiProduct::numberOfAcceptanceSets() const
/* ----------------------------------------------------------------------------
*
* Description: Tells the number of acceptance sets in the intersection of
* the two Büchi automata associated with a BuchiProduct object.
*
* Arguments: None.
*
* Returns: The number of acceptance sets in the intersection.
*
* ------------------------------------------------------------------------- */
{
return number_of_acceptance_sets;
}
/* ========================================================================= */
inline const BuchiAutomaton::BuchiState& BuchiProduct::firstComponent
(const Graph<GraphEdgeContainer>::size_type state_id) const
/* ----------------------------------------------------------------------------
*
* Description: Function for accessing states of the "first" component
* automaton in the intersection of two Büchi automata.
*
* Argument: state_id -- Identifier of a state in the component
* automaton.
*
* Returns: A constant reference to a state in the component automaton.
*
* ------------------------------------------------------------------------- */
{
return automaton_1[state_id];
}
/* ========================================================================= */
inline const BuchiAutomaton::BuchiState& BuchiProduct::secondComponent
(const Graph<GraphEdgeContainer>::size_type state_id) const
/* ----------------------------------------------------------------------------
*
* Description: Function for accessing states of the "second" component
* automaton in the intersection of two Büchi automata.
*
* Argument: state_id -- Identifier of a state in the component
* automaton.
*
* Returns: A constant reference to a state in the component automaton.
*
* ------------------------------------------------------------------------- */
{
return automaton_2[state_id];
}
/* ========================================================================= */
inline void BuchiProduct::mergeAcceptanceInformation
(const Graph<GraphEdgeContainer>::Node& state1,
const Graph<GraphEdgeContainer>::Node& state2,
BitArray& acceptance_sets) const
/* ----------------------------------------------------------------------------
*
* Description: Merges the acceptance sets associated with a pair of states
* of two Büchi automata into a collection of sets.
*
* Arguments: state1, state2 -- Constant references to the states of the
* automata.
* acceptance_sets -- A reference to a BitArray for storing
* the result. The BitArray is assumed to
* have capacity for
* `this->number_of_acceptance_sets' bits.
*
* Returns: Nothing. Let n=`this->automaton_1.numberOfAcceptanceSets()';
* after the operation, `acceptance_sets[i] = true' holds if
* either
* 0 <= i < n and
* `state1.acceptanceSets().test(i) == true'
* or 0 <= i - n < `this->automaton_2.numberOfAcceptanceSets()'
* and `state2.acceptanceSets().test(i - n) == true'.
*
* ------------------------------------------------------------------------- */
{
mergeAcceptanceInformation
(static_cast<const BuchiAutomaton::BuchiState&>(state1).acceptanceSets(),
static_cast<const BuchiAutomaton::BuchiState&>(state2).acceptanceSets(),
acceptance_sets);
}
/* ========================================================================= */
inline void BuchiProduct::mergeAcceptanceInformation
(const Graph<GraphEdgeContainer>::Edge& transition1,
const Graph<GraphEdgeContainer>::Edge& transition2,
BitArray& acceptance_sets) const
/* ----------------------------------------------------------------------------
*
* Description: Merges the acceptance sets associated with a pair of
* transitions of two Büchi automata into a collection of
* acceptance sets.
*
* Arguments: transition1, -- Constant references to the transitions
* transition2 of the automata.
* acceptance_sets -- A reference to a BitArray for storing
* the result. The BitArray is assumed to
* have capacity for
* `this->number_of_acceptance_sets' bits.
*
* Returns: Nothing. Let n=`this->automaton_1.numberOfAcceptanceSets()';
* after the operation, `acceptance_sets[i] = true' holds if
* either
* 0 <= i < n and
* `transition1.acceptanceSets().test(i) == true'
* or 0 <= i - n < `this->automaton_2.numberOfAcceptanceSets()'
* and `transition2.acceptanceSets().test(i - n) == true'.
*
* ------------------------------------------------------------------------- */
{
mergeAcceptanceInformation
(static_cast<const BuchiAutomaton::BuchiTransition&>(transition1)
.acceptanceSets(),
static_cast<const BuchiAutomaton::BuchiTransition&>(transition2)
.acceptanceSets(),
acceptance_sets);
}
/* ========================================================================= */
inline void BuchiProduct::mergeAcceptanceInformation
(const BitArray& sets1, const BitArray& sets2, BitArray& result) const
/* ----------------------------------------------------------------------------
*
* Description: Bitwise or between two acceptance set vectors and a result
* vector.
*
* Arguments: sets1, -- Constant references to two BitArrays having (at
* sets2 least) capacities
* `automaton_1.numberOfAcceptanceSets()' and
* `automaton_2.numberOfAcceptanceSets()',
* respectively.
* result -- A BitArray for storing the result, assumed to
* have room for at least
* `this->number_of_acceptance_sets' bits.
*
* Returns: Nothing. Let n=`this->automaton_1.numberOfAcceptanceSets()';
* after the operation, `result[i] = true' holds if
* either
* 0 <= i < n and `sets1[i] == true'
* or 0 <= i - n < `this->automaton_2.numberOfAcceptanceSets()'
* and `sets2[i - n] == true'.
*
* ------------------------------------------------------------------------- */
{
const unsigned long int shift
= automaton_1.numberOfAcceptanceSets();
unsigned long int acceptance_set;
for (acceptance_set = 0; acceptance_set < shift; ++acceptance_set)
{
if (sets1[acceptance_set])
result.setBit(acceptance_set);
}
for ( ; acceptance_set < number_of_acceptance_sets; ++acceptance_set)
{
if (sets2[acceptance_set - shift])
result.setBit(acceptance_set);
}
}
/* ========================================================================= */
inline void BuchiProduct::validateEdgeIterators
(const Graph<GraphEdgeContainer>::Node& state_1,
const Graph<GraphEdgeContainer>::Node& state_2,
GraphEdgeContainer::const_iterator& transition_1,
GraphEdgeContainer::const_iterator& transition_2)
/* ----------------------------------------------------------------------------
*
* Description: Checks whether a pair of transition iterators corresponds to
* a transition beginning from a state in the intersection of
* two Büchi automata; if this is not the case, increments the
* iterators to make them point to a valid transition beginning
* from the state in the intersection (or to the "end" of the
* collection of transitions beginning from the state if no
* valid transition can be found by incrementing the iterators).
*
* Arguments: state_1, -- These variables determine the state in
* state_2 the intersection automaton; `state_1' and
* `state_2' should both be references to
* BuchiAutomaton::BuchiState objects.
* transition_1, -- References to the transition iterators.
* transition_2 Initially, `transition_1' and
* `transition_2' should point to two
* transitions starting from `state_1' and
* `state_2', respectively.
*
* Returns: Nothing. Upon return, `transition_1' and `transition_2' will
* either equal `state_1.edges().end()' and
* `state_2.edges().end()', respectively, or they will point to
* a pair of transitions beginning from `state_1' and `state_2'
* such that this pair of transitions corresponds to a
* transition starting from the intersection state determined by
* `state_1' and `state_2'.
*
* ------------------------------------------------------------------------- */
{
const GraphEdgeContainer& transitions_1 = state_1.edges();
const GraphEdgeContainer& transitions_2 = state_2.edges();
if (transition_1 == transitions_1.end())
{
transition_2 = transitions_2.end();
return;
}
if (transition_2 == transitions_2.end())
{
transition_1 = transitions_1.end();
return;
}
if (!synchronizable(**transition_1, **transition_2))
incrementEdgeIterators(state_1, state_2, transition_1, transition_2);
}
/* ========================================================================= */
inline void BuchiProduct::incrementEdgeIterators
(const Graph<GraphEdgeContainer>::Node& state_1,
const Graph<GraphEdgeContainer>::Node& state_2,
GraphEdgeContainer::const_iterator& transition_1,
GraphEdgeContainer::const_iterator& transition_2)
/* ----------------------------------------------------------------------------
*
* Description: Increments a pair of transition iterators to point to the
* "next" transition beginning from a state in the intersection
* of two Büchi automata. If no "next" transition exists, makes
* the iterators point to the "end" of the collection of
* transitions beginning from the state.
*
* Arguments: state_1, -- These variables determine the state in
* state_2 the intersection automaton; `state_1' and
* `state_2' should both be references to
* BuchiAutomaton::BuchiState objects.
* transition_1, -- References to the transition iterators.
* transition_2 Initially, `transition_1' and
* `transition_2' should point to two
* transitions starting from `state_1' and
* `state_2', respectively.
*
* Returns: Nothing. Upon return, `transition_1' and `transition_2' will
* either equal `state_1.edges().end()' and
* `state_2.edges().end()', respectively, or they will point to
* a pair of transitions beginning from `state_1' and `state_2'
* such that this pair of transitions corresponds to a
* transition starting from the intersection state determined by
* `state_1' and `state_2'.
*
* ------------------------------------------------------------------------- */
{
const GraphEdgeContainer& transitions_1 = state_1.edges();
const GraphEdgeContainer& transitions_2 = state_2.edges();
do
{
++transition_2;
if (transition_2 == transitions_2.end())
{
++transition_1;
if (transition_1 == transitions_1.end())
return;
transition_2 = transitions_2.begin();
}
}
while (!synchronizable(**transition_1, **transition_2));
}
/* ========================================================================= */
inline void BuchiProduct::clearSatisfiabilityCache()
/* ----------------------------------------------------------------------------
*
* Description: Clears information about the satisfiability of the guard
* formulas of product transitions.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
sat_cache.clear();
}
}
#endif /* !BUCHIPRODUCT_H */

290
lbtt/src/Config-lex.ll
View file

@ -19,11 +19,6 @@
%{
#include <config.h>
#include <cmath>
#include <climits>
#include <cstdlib>
#include <cstring>
#include <string>
#include "Configuration.h"
#include "Config-parse.h"
@ -34,225 +29,102 @@ extern int config_file_line_number;
%option case-insensitive
%option never-interactive
%option noyywrap
%option nounput
%x ATTR EQ VAL
SQSTR [^\'\n]*
DQSTR ([^\"\\\n]|\\.)*
UQC [^\'\"\\ \t\n]
UQSTR ({UQC}+|\\.)({UQC}*|\\.)*
OKVAL \'{SQSTR}\'|\"{DQSTR}\"|{UQSTR}
%%
[ \t]* { /* Skip whitespace. */ }
"#"[^\n]* { /* Skip comments. */ }
<*>[ \t]* { /* Skip whitespace everywhere. */ }
<*>"#".*$ { /* Skip comments everywhere. */ }
"\n" { /* Skip newlines, but update the line number. */
<INITIAL,ATTR>"\n" { /* Skip newlines, but update the line number. */
config_file_line_number++;
}
"{" { return CFG_LBRACE; }
"}" { return CFG_RBRACE; }
"=" { return CFG_EQUALS; }
algorithm { return CFG_ALGORITHM; }
enabled { return CFG_ENABLED; }
name { return CFG_NAME; }
parameters { return CFG_PARAMETERS; }
path { return CFG_PROGRAMPATH; }
"{" { BEGIN(ATTR); return CFG_LBRACE; }
algorithm|implementation|translator { return CFG_ALGORITHM; }
globaloptions { return CFG_GLOBALOPTIONS; }
comparisoncheck { return CFG_COMPARISONTEST; }
comparisontest { return CFG_COMPARISONTEST; }
consistencycheck { return CFG_CONSISTENCYTEST; }
consistencytest { return CFG_CONSISTENCYTEST; }
interactive { return CFG_INTERACTIVE; }
intersectioncheck { return CFG_INTERSECTIONTEST; }
intersectiontest { return CFG_INTERSECTIONTEST; }
modelcheck { return CFG_MODELCHECK; }
rounds { return CFG_ROUNDS; }
verbosity { return CFG_VERBOSITY; }
statespaceoptions { return CFG_STATESPACEOPTIONS; }
edgeprobability { return CFG_EDGEPROBABILITY; }
propositions { return CFG_PROPOSITIONS; }
size { return CFG_SIZE; }
truthprobability { return CFG_TRUTHPROBABILITY; }
changeinterval { return CFG_CHANGEINTERVAL; }
randomseed { return CFG_RANDOMSEED; }
formulaoptions { return CFG_FORMULAOPTIONS; }
abbreviatedoperators { return CFG_ABBREVIATEDOPERATORS; }
andpriority { return CFG_ANDPRIORITY; }
beforepriority { return CFG_BEFOREPRIORITY; }
defaultoperatorpriority { return CFG_DEFAULTOPERATORPRIORITY; }
equivalencepriority { return CFG_EQUIVALENCEPRIORITY; }
falsepriority { return CFG_FALSEPRIORITY; }
finallypriority { return CFG_FINALLYPRIORITY; }
generatemode { return CFG_GENERATEMODE; }
globallypriority { return CFG_GLOBALLYPRIORITY; }
implicationpriority { return CFG_IMPLICATIONPRIORITY; }
nextpriority { return CFG_NEXTPRIORITY; }
notpriority { return CFG_NOTPRIORITY; }
orpriority { return CFG_ORPRIORITY; }
outputmode { return CFG_OUTPUTMODE; }
propositionpriority { return CFG_PROPOSITIONPRIORITY; }
releasepriority { return CFG_RELEASEPRIORITY; }
strongreleasepriority { return CFG_STRONGRELEASEPRIORITY; }
truepriority { return CFG_TRUEPRIORITY; }
untilpriority { return CFG_UNTILPRIORITY; }
weakuntilpriority { return CFG_WEAKUNTILPRIORITY; }
xorpriority { return CFG_XORPRIORITY; }
true|yes {
yylval.truth_value = true;
return CFG_TRUTH_VALUE;
[^ \t\n]+ { return CFG_UNKNOWN; }
<ATTR>enabled { BEGIN(EQ); return CFG_ENABLED; }
<ATTR>name { BEGIN(EQ); return CFG_NAME; }
<ATTR>parameters { BEGIN(EQ); return CFG_PARAMETERS; }
<ATTR>path { BEGIN(EQ); return CFG_PROGRAMPATH; }
<ATTR>comparisoncheck { BEGIN(EQ); return CFG_COMPARISONTEST; }
<ATTR>comparisontest { BEGIN(EQ); return CFG_COMPARISONTEST; }
<ATTR>consistencycheck { BEGIN(EQ); return CFG_CONSISTENCYTEST; }
<ATTR>consistencytest { BEGIN(EQ); return CFG_CONSISTENCYTEST; }
<ATTR>interactive { BEGIN(EQ); return CFG_INTERACTIVE; }
<ATTR>intersectioncheck { BEGIN(EQ); return CFG_INTERSECTIONTEST; }
<ATTR>intersectiontest { BEGIN(EQ); return CFG_INTERSECTIONTEST; }
<ATTR>modelcheck { BEGIN(EQ); return CFG_MODELCHECK; }
<ATTR>rounds { BEGIN(EQ); return CFG_ROUNDS; }
<ATTR>translatortimeout { BEGIN(EQ); return CFG_TRANSLATORTIMEOUT; }
<ATTR>verbosity { BEGIN(EQ); return CFG_VERBOSITY; }
<ATTR>edgeprobability { BEGIN(EQ); return CFG_EDGEPROBABILITY; }
<ATTR>propositions { BEGIN(EQ); return CFG_PROPOSITIONS; }
<ATTR>size { BEGIN(EQ); return CFG_SIZE; }
<ATTR>truthprobability { BEGIN(EQ); return CFG_TRUTHPROBABILITY; }
<ATTR>changeinterval { BEGIN(EQ); return CFG_CHANGEINTERVAL; }
<ATTR>randomseed { BEGIN(EQ); return CFG_RANDOMSEED; }
<ATTR>abbreviatedoperators { BEGIN(EQ); return CFG_ABBREVIATEDOPERATORS; }
<ATTR>andpriority { BEGIN(EQ); return CFG_ANDPRIORITY; }
<ATTR>beforepriority { BEGIN(EQ); return CFG_BEFOREPRIORITY; }
<ATTR>defaultoperatorpriority {
BEGIN(EQ); return CFG_DEFAULTOPERATORPRIORITY;
}
<ATTR>equivalencepriority { BEGIN(EQ); return CFG_EQUIVALENCEPRIORITY; }
<ATTR>falsepriority { BEGIN(EQ); return CFG_FALSEPRIORITY; }
<ATTR>finallypriority { BEGIN(EQ); return CFG_FINALLYPRIORITY; }
<ATTR>generatemode { BEGIN(EQ); return CFG_GENERATEMODE; }
<ATTR>globallypriority { BEGIN(EQ); return CFG_GLOBALLYPRIORITY; }
<ATTR>implicationpriority { BEGIN(EQ); return CFG_IMPLICATIONPRIORITY; }
<ATTR>nextpriority { BEGIN(EQ); return CFG_NEXTPRIORITY; }
<ATTR>notpriority { BEGIN(EQ); return CFG_NOTPRIORITY; }
<ATTR>orpriority { BEGIN(EQ); return CFG_ORPRIORITY; }
<ATTR>outputmode { BEGIN(EQ); return CFG_OUTPUTMODE; }
<ATTR>propositionpriority { BEGIN(EQ); return CFG_PROPOSITIONPRIORITY; }
<ATTR>releasepriority { BEGIN(EQ); return CFG_RELEASEPRIORITY; }
<ATTR>strongreleasepriority { BEGIN(EQ); return CFG_STRONGRELEASEPRIORITY; }
<ATTR>truepriority { BEGIN(EQ); return CFG_TRUEPRIORITY; }
<ATTR>untilpriority { BEGIN(EQ); return CFG_UNTILPRIORITY; }
<ATTR>weakuntilpriority { BEGIN(EQ); return CFG_WEAKUNTILPRIORITY; }
<ATTR>xorpriority { BEGIN(EQ); return CFG_XORPRIORITY; }
<ATTR>"}" { BEGIN(INITIAL); return CFG_RBRACE; }
<ATTR>"="?[^= \t\n]* { return CFG_UNKNOWN; }
<EQ>"=" { BEGIN(VAL); return CFG_EQUALS; }
<EQ>. { return CFG_UNKNOWN; }
<VAL>\\|{OKVAL}+(\\)? {
yylval.value = yytext;
BEGIN(ATTR);
return CFG_VALUE;
}
false|no {
yylval.truth_value = false;
return CFG_TRUTH_VALUE;
}
always {
yylval.interactivity_value =
Configuration::ALWAYS;
return CFG_INTERACTIVITY_VALUE;
}
never {
yylval.interactivity_value =
Configuration::NEVER;
return CFG_INTERACTIVITY_VALUE;
}
onerror {
yylval.interactivity_value =
Configuration::ONERROR;
return CFG_INTERACTIVITY_VALUE;
}
normal {
yylval.formula_mode_value =
Configuration::NORMAL;
return CFG_FORMULA_MODE_VALUE;
}
nnf {
yylval.formula_mode_value = Configuration::NNF;
return CFG_FORMULA_MODE_VALUE;
}
local {
yylval.product_type_value = Configuration::LOCAL;
return CFG_PRODUCT_TYPE_VALUE;
}
global {
yylval.product_type_value =
Configuration::GLOBAL;
return CFG_PRODUCT_TYPE_VALUE;
}
randomgraph {
yylval.statespace_mode_value
= Configuration::RANDOMGRAPH;
return CFG_STATESPACE_MODE_VALUE;
}
randomconnectedgraph {
yylval.statespace_mode_value
= Configuration::RANDOMCONNECTEDGRAPH;
return CFG_STATESPACE_MODE_VALUE;
}
randompath {
yylval.statespace_mode_value
= Configuration::RANDOMPATH;
return CFG_STATESPACE_MODE_VALUE;
}
enumeratedpath {
yylval.statespace_mode_value
= Configuration::ENUMERATEDPATH;
return CFG_STATESPACE_MODE_VALUE;
}
"-"?[0-9]+"...""-"?[0-9]+ {
char* dot_ptr;
yylval.integer_interval.min
= strtol(yytext, &dot_ptr, 10);
if (yylval.integer_interval.min == LONG_MIN
|| yylval.integer_interval.min == LONG_MAX)
throw Configuration::ConfigurationException
(config_file_line_number,
"integer out of range");
dot_ptr += 3;
yylval.integer_interval.max
= strtol(dot_ptr, 0, 10);
if (yylval.integer_interval.max == LONG_MIN
|| yylval.integer_interval.max == LONG_MAX)
throw Configuration::ConfigurationException
(config_file_line_number,
"integer out of range");
return CFG_INTEGER_INTERVAL;
}
"-"?[0-9]+ {
yylval.integer = strtol(yytext, 0, 10);
if (yylval.integer == LONG_MIN
|| yylval.integer == LONG_MAX)
throw Configuration::ConfigurationException
(config_file_line_number,
"integer out of range");
return CFG_INTEGER;
}
"-"?[0-9]*"."[0-9]+ {
yylval.real = strtod(yytext, 0);
if (yylval.real == HUGE_VAL
|| yylval.real == -HUGE_VAL)
throw Configuration::ConfigurationException
(config_file_line_number,
"real number out of range");
return CFG_REAL;
}
\"([^\n\"\\]*(\\[^\n])?)*\" {
unsigned long int len = strlen(yytext);
bool escape = false;
yylval.str = new string;
for (unsigned long int i = 1; i < len - 1; i++)
{
if (!escape && yytext[i] == '\\')
escape = true;
else
{
escape = false;
(*yylval.str) += yytext[i];
}
}
return CFG_STRING_CONSTANT;
}
. {
return CFG_UNKNOWN;
<VAL>{OKVAL}*(\'{SQSTR}|\"{DQSTR})(\\)? {
throw Configuration::ConfigurationException
(config_file_line_number,
"unmatched quotes");
}
<EQ,VAL>"\n" { return CFG_UNKNOWN; }
%%
/* ========================================================================= */
int getCharacter()
/* ----------------------------------------------------------------------------
*
* Description: Reads the next character from the lexer input stream.
*
* Arguments: None.
*
* Returns: The next character in the lexer input stream or EOF if there
* are no more characters to read.
*
* ------------------------------------------------------------------------- */
{
return yyinput();
}

1300
lbtt/src/Config-parse.yy
View file

File diff suppressed because it is too large Load diff

1610
lbtt/src/Configuration.cc
View file

File diff suppressed because it is too large Load diff

263
lbtt/src/Configuration.h
View file

@ -21,6 +21,7 @@
#define CONFIGURATION_H
#include <config.h>
#include <cstdio>
#include <iostream>
#include <map>
#include <set>
@ -35,8 +36,6 @@
using namespace std;
/******************************************************************************
*
* A class for storing program configuration information.
@ -69,15 +68,23 @@ public:
* string.
*/
bool isInternalAlgorithm(unsigned long int id) /* Tests whether a given */
const; /* algorithm identifier
* refers to lbtt's
* internal model
* checking algorithm.
*/
static void showCommandLineHelp /* Prints the list of */
(const char* program_name); /* command line options. */
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
enum InteractionMode {NEVER, ALWAYS, ONERROR}; /* Enumeration constants
* affecting the behaviour
* of the program as
* regards user control.
enum InteractionMode {NEVER, ALWAYS, ONERROR, /* Enumeration constants */
ONBREAK}; /* affecting the
* behavior of the
* program as regards
* user control.
*/
enum FormulaMode {NORMAL, NNF}; /* Enumeration constants
@ -109,19 +116,23 @@ public:
* parameters).
*/
{
string* name; /* Name of the algorithm.
string name; /* Name of the algorithm.
*/
string* path_to_program; /* Path to the executable
char** parameters; /* Command-line parameters
* required for running
* the algorithm.
*/
string* extra_parameters; /* Additional command-line
* parameters required for
* running the executable.
* the executable. See
* the documentation for
* the registerAlgorithm
* function (in
* Configuration.cc) for
* more information.
*/
vector<string>::size_type num_parameters; /* Number of command-line
* parameters.
*/
bool enabled; /* Determines whether the
* algorithm is enabled
* (whether it will be used
@ -169,6 +180,12 @@ public:
* commands.
*/
bool handle_breaks; /* If true, pause testing
* also on interrupt
* signals instead of
* simply aborting.
*/
unsigned long int number_of_rounds; /* Number of test rounds.
*/
@ -278,6 +295,10 @@ public:
* formula generation
* algorithms.
*/
unsigned int translator_timeout; /* Timeout (in seconds) for
* translators.
*/
};
struct FormulaConfiguration /* A structure for storing
@ -360,6 +381,12 @@ public:
* the tests.
*/
map<string, unsigned long int, less<string>, /* Mapping between */
ALLOC(unsigned long int) > /* algorithm names and */
algorithm_names; /* their numeric
* identifiers.
*/
GlobalConfiguration global_options; /* General configuration
* information.
*/
@ -376,15 +403,6 @@ public:
* algorithms.
*/
typedef pair<int, int> IntPair;
set<IntPair, less<IntPair>, ALLOC(IntPair) > /* Configuration options */
locked_options; /* the values of which
* should not be
* initialized from the
* configuration file.
*/
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
class ConfigurationException : public Exception /* A class for reporting
@ -419,6 +437,9 @@ public:
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
private:
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
struct IntegerRange /* Data structure for
* representing integer-
* valued ranges of certain
@ -426,11 +447,11 @@ public:
* options.
*/
{
long int min; /* Lower bound. */
unsigned long int min; /* Lower bound. */
long int max; /* Upper bound. */
unsigned long int max; /* Upper bound. */
char* error_message; /* Error message to be
const char* error_message; /* Error message to be
* displayed if the value
* is not within the
* specified range.
@ -439,31 +460,30 @@ public:
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
/*
* Ranges for certain integer-valued configuration options.
*/
/* Ranges for certain integer-valued configuration options. */
static const struct IntegerRange
VERBOSITY_RANGE, ROUND_COUNT_RANGE, GENERATION_RANGE, PRIORITY_RANGE,
PROPOSITION_COUNT_RANGE, FORMULA_SIZE_RANGE, FORMULA_MAX_SIZE_RANGE,
STATESPACE_SIZE_RANGE, STATESPACE_MAX_SIZE_RANGE;
DEFAULT_RANGE, VERBOSITY_RANGE,
ROUND_COUNT_RANGE, RANDOM_SEED_RANGE,
ATOMIC_PRIORITY_RANGE, OPERATOR_PRIORITY_RANGE;
private:
enum CommandLineOptionType /* Command line options. */
{OPT_COMPARISONTEST = 10000, OPT_CONFIGFILE,
/* Command line options. */
enum CommandLineOptionType
{OPT_HELP = 'h', OPT_VERSION = 'V',
OPT_COMPARISONTEST = 10000, OPT_CONFIGFILE,
OPT_CONSISTENCYTEST, OPT_DISABLE, OPT_ENABLE,
OPT_FORMULACHANGEINTERVAL, OPT_FORMULAFILE,
OPT_FORMULARANDOMSEED, OPT_HELP = 'h',
OPT_GLOBALPRODUCT = 20000, OPT_INTERACTIVE,
OPT_FORMULACHANGEINTERVAL,
OPT_FORMULAFILE, OPT_FORMULARANDOMSEED,
OPT_GLOBALPRODUCT, OPT_INTERACTIVE,
OPT_INTERSECTIONTEST, OPT_LOGFILE,
OPT_MODELCHECK, OPT_NOCOMPARISONTEST,
OPT_NOCONSISTENCYTEST, OPT_NOINTERSECTIONTEST,
OPT_NOPAUSE, OPT_PAUSE, OPT_PAUSEONERROR,
OPT_PROFILE, OPT_QUIET, OPT_ROUNDS,
OPT_SHOWCONFIG, OPT_SHOWOPERATORDISTRIBUTION,
OPT_SKIP, OPT_STATESPACECHANGEINTERVAL,
OPT_STATESPACERANDOMSEED, OPT_VERBOSITY,
OPT_VERSION,
OPT_MODELCHECK, OPT_PROFILE, OPT_QUIET,
OPT_ROUNDS, OPT_SHOWCONFIG,
OPT_SHOWOPERATORDISTRIBUTION, OPT_SKIP,
OPT_STATESPACECHANGEINTERVAL,
OPT_STATESPACERANDOMSEED,
OPT_TRANSLATORTIMEOUT, OPT_VERBOSITY,
OPT_LOCALPRODUCT,
@ -476,7 +496,6 @@ private:
OPT_FORMULAPROPOSITIONS, OPT_FORMULASIZE,
OPT_GENERATENNF, OPT_GLOBALLYPRIORITY,
OPT_IMPLICATIONPRIORITY, OPT_NEXTPRIORITY,
OPT_NOABBREVIATEDOPERATORS,
OPT_NOGENERATENNF, OPT_NOOUTPUTNNF,
OPT_NOTPRIORITY, OPT_ORPRIORITY,
OPT_OUTPUTNNF, OPT_PROPOSITIONPRIORITY,
@ -503,6 +522,8 @@ private:
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
friend int yyparse();
Configuration(const Configuration& cfg); /* Prevent copying and */
Configuration& operator= /* assignment of */
(const Configuration& cfg); /* Configuration
@ -514,10 +535,59 @@ private:
* to default values.
*/
long int parseCommandLineInteger /* Converts an integer */
(const string& option, const string& value) /* to a string with */
const; /* some additional
* validity checks.
void registerAlgorithm /* Adds a new algorithm */
(const string& name, const string& path, /* to the configuration. */
const string& parameters, bool enabled,
const int block_begin_line);
template<typename T> /* Reads an integer, */
void readInteger /* checks that it is */
(T& target, const string& value, /* within given bounds */
const IntegerRange& range = DEFAULT_RANGE); /* and stores it into
* an unsigned integer
* type variable.
*/
void readProbability /* Reads a probability */
(double& target, const string& value); /* and stores it into
* a given variable of
* type double.
*/
void readSize(int valtype, const string& value); /* Initializes formula or
* state space size
* ranges from a given
* string.
*/
void readTruthValue /* Interprets a symbolic */
(bool& target, const string& value); /* truth value. */
void readInteractivity(const string& value); /* Interprets a symbolic
* interactivity mode.
*/
void readProductType(const string& value); /* Interprets a symbolic
* model checking mode.
*/
void readFormulaMode /* Interprets a symbolic */
(FormulaMode& target, const string& mode); /* formula mode.
*/
void readStateSpaceMode(const string& mode); /* Initializes
* `global_options.
* statespace_generation
* _mode' from a
* symbolic mode
* identifier.
*/
void readTranslatorTimeout(const string& value); /* Initializes
* `global_options.
* translator_timeout'
* from a symbolic time
* specification.
*/
double operatorProbability /* Computes the */
@ -532,6 +602,97 @@ private:
/******************************************************************************
*
* Declarations for functions and variables provided by the parser.
*
*****************************************************************************/
extern int config_file_line_number; /* Number of the current
* line in the
* configuration file.
*/
extern int parseConfiguration /* Parser interface. */
(FILE*, Configuration&);
/******************************************************************************
*
* Inline function definitions for class Configuration.
*
*****************************************************************************/
/* ========================================================================= */
inline bool Configuration::isInternalAlgorithm(unsigned long int id) const
/* ----------------------------------------------------------------------------
*
* Description: Tests whether a given algorithm identifier refers to lbtt's
* internal model checking algorithm.
*
* Argument: id -- Identifier to test.
*
* Returns: True if `id' is the identifier of lbtt's internal model
* checking algorithm.
*
* ------------------------------------------------------------------------- */
{
return ((global_options.statespace_generation_mode & Configuration::PATH)
&& id == algorithms.size() - 1);
}
/******************************************************************************
*
* Template function definitions for class Configuration.
*
*****************************************************************************/
/* ========================================================================= */
template<typename T>
void Configuration::readInteger
(T& target, const string& value, const IntegerRange& range)
/* ----------------------------------------------------------------------------
*
* Description: Reads an integer and stores it into `target'.
*
* Arguments: target -- A reference to an unsigned integer type variable
* for storing the result.
* value -- The integer as a string.
* range -- A reference to a constant IntegerRange object
* giving the bounds for the value.
*
* Returns: Nothing; the result is stored into `target'. The function
* throws a ConfigurationException if `value' is not a valid
* integer within the bounds specified by `range'.
*
* ------------------------------------------------------------------------- */
{
string error;
unsigned long int val;
try
{
val = ::StringUtil::parseNumber(value);
}
catch (const ::StringUtil::NotANumberException&)
{
error = "`" + value + "' is not a valid nonnegative integer";
}
if (error.empty() && (val < range.min || val > range.max))
error = range.error_message;
if (!error.empty())
throw ConfigurationException(config_file_line_number, error);
target = val;
}
/******************************************************************************
*
* Inline function definitions for class Configuration::ConfigurationException.

20
lbtt/src/DispUtil.h
View file

@ -58,6 +58,16 @@ void printTextBlock /* Writes an indented */
* a stream.
*/
bool printText /* "Verbosity-aware" */
(const char* text, /* functions for writing */
const int verbosity_threshold, /* text to standard */
const int indent); /* output. */
bool printText
(const string& text,
const int verbosity_threshold,
const int indent);
/******************************************************************************
@ -78,16 +88,6 @@ struct StreamFormatting
* e.g. the justification
* of output.
*/
bool printText /* "Verbosity-aware" */
(const char* text, /* functions for writing */
const int verbosity_threshold, /* text to standard */
const int indent); /* output. */
bool printText
(const string& text,
const int verbosity_threshold,
const int indent);
};

52
lbtt/src/Exception.h
View file

@ -23,6 +23,7 @@
#include <config.h>
#include <string>
#include <exception>
#include <istream>
#include <iostream>
using namespace std;
@ -299,6 +300,16 @@ public:
template<class T> /* Operator for reading */
Exceptional_istream &operator>>(T &t); /* from the stream. */
Exceptional_istream& get(istream::char_type& C); /* Reads a character from
* the stream.
*/
Exceptional_istream& read /* Reads a given number */
(istream::char_type* buffer, streamsize count); /* of characters from
* the stream into a
* buffer.
*/
operator istream&(); /* Casts the exception-
* aware input stream into
* a regular input stream.
@ -992,6 +1003,47 @@ inline Exceptional_istream::~Exceptional_istream()
{
}
/* ========================================================================= */
inline Exceptional_istream& Exceptional_istream::get(istream::char_type& c)
/* ----------------------------------------------------------------------------
*
* Description: Reads a character from the input stream.
*
* Argument: c -- A reference to a character to extract.
*
* Returns: A reference to the stream.
*
* ------------------------------------------------------------------------- */
{
stream->get(c);
if (stream->rdstate() & exception_mask)
throw IOException("error reading from stream");
return *this;
}
/* ========================================================================= */
inline Exceptional_istream& Exceptional_istream::read
(istream::char_type* buffer, streamsize count)
/* ----------------------------------------------------------------------------
*
* Description: Reads a given number of characters from the stream into a
* buffer.
*
* Arguments: buffer -- A pointer to the buffer.
* count -- Number of characters to read.
*
* Returns: A reference to the stream.
*
* ------------------------------------------------------------------------- */
{
stream->read(buffer, count);
if (stream->rdstate() & exception_mask)
throw IOException("error reading from stream");
return *this;
}
/* ========================================================================= */
inline Exceptional_istream::operator istream&()
/* ----------------------------------------------------------------------------

123
lbtt/src/ExternalTranslator.cc
View file

@ -20,6 +20,7 @@
#include <config.h>
#include <cstdio>
#include <cstdlib>
#include <cstring>
#include <sys/stat.h>
#include <sys/types.h>
#ifdef HAVE_FCNTL_H
@ -62,25 +63,30 @@ ExternalTranslator::~ExternalTranslator()
}
/* ========================================================================= */
ExternalTranslator::TempFileObject&
ExternalTranslator::registerTempFileObject
(const string& filename, TempFileObject::Type type)
const char* ExternalTranslator::registerTempFileObject
(const string& filename, const TempFsysName::NameType type,
const bool literal)
/* ----------------------------------------------------------------------------
*
* Description: Registers a temporary file or directory such that it will be
* automatically deleted when the ExternalTranslator object is
* destroyed.
*
* Arguments: filename -- Name of the temporary file or directory.
* Arguments: filename -- Name of the temporary file or directory. If
* empty, a new name will be created.
* type -- Type of the object (TempFileObject::FILE or
* TempFileObject::DIRECTORY).
* literal -- Tells whether the file name should be
* interpreted literally.
*
* Returns: A reference to the file object.
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
temporary_file_objects.push(new TempFileObject(filename, type));
return *temporary_file_objects.top();
TempFsysName* name = new TempFsysName;
name->allocate(filename.c_str(), type, literal);
temporary_file_objects.push(name);
return name->get();
}
/* ========================================================================= */
@ -99,19 +105,19 @@ void ExternalTranslator::translate
*
* ------------------------------------------------------------------------- */
{
TempFileObject& external_program_input_file = registerTempFileObject();
const char* external_program_input_file
= registerTempFileObject("lbtt-translate");
TempFileObject& external_program_output_file = registerTempFileObject();
const char* external_program_output_file
= registerTempFileObject("lbtt-translate");
string translated_formula;
translateFormula(formula, translated_formula);
ofstream input_file;
input_file.open(external_program_input_file.getName().c_str(),
ios::out | ios::trunc);
input_file.open(external_program_input_file, ios::out | ios::trunc);
if (!input_file.good())
throw FileCreationException(string("`")
+ external_program_input_file.getName()
throw FileCreationException(string("`") + external_program_input_file
+ "'");
Exceptional_ostream einput_file(&input_file, ios::failbit | ios::badbit);
@ -121,96 +127,11 @@ void ExternalTranslator::translate
input_file.close();
string command_line = string(command_line_arguments[2])
+ commandLine(external_program_input_file.getName(),
external_program_output_file.getName());
+ commandLine(external_program_input_file,
external_program_output_file);
if (!execSuccess(system(command_line.c_str())))
throw ExecFailedException(command_line_arguments[2]);
parseAutomaton(external_program_output_file.getName(), filename);
}
/******************************************************************************
*
* Function definitions for class ExternalTranslator::TempFileObject.
*
*****************************************************************************/
/* ========================================================================= */
ExternalTranslator::TempFileObject::TempFileObject
(const string& filename, Type t)
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class TempFileObject. Creates a temporary
* file or a directory and tests whether it can really be
* written to (if not, a FileCreationException is thrown).
*
* Arguments: filename -- Name of the temporary file or directory.
* If the filename is an empty string, the
* filename is obtained by a call to tmpnam(3).
* t -- Type of the object (TempFileObject::FILE or
* TempFileObject::DIRECTORY).
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
if (filename.empty())
{
char tempname[L_tmpnam + 1];
if (tmpnam(tempname) == 0)
throw FileCreationException("a temporary file");
name = tempname;
}
else
name = filename;
if (t == FILE)
{
ofstream tempfile;
tempfile.open(name.c_str(), ios::out | ios::trunc);
if (!tempfile.good())
throw FileCreationException("a temporary file");
tempfile.close();
}
else
{
if (mkdir(name.c_str(), 0700) != 0)
throw FileCreationException("a temporary directory");
}
type = t;
}
/* ========================================================================= */
ExternalTranslator::TempFileObject::~TempFileObject()
/* ----------------------------------------------------------------------------
*
* Description: Destructor for class TempFileObject. Deletes the file or
* the directory associated with the object (displays a warning
* if this fails).
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
if (remove(name.c_str()) != 0)
{
string msg("error removing temporary ");
if (type == TempFileObject::FILE)
msg += "file";
else
msg += "directory";
msg += " `" + name + "'";
printWarning(msg);
}
parseAutomaton(external_program_output_file, filename);
}

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,17 +174,12 @@ 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 WringWrapper;
friend class SpinWrapper; /* Friend declarations. */
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
@ -316,46 +280,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

1
lbtt/src/FormulaRandomizer.h
View file

@ -21,6 +21,7 @@
#define FORMULARANDOMIZER_H
#include <config.h>
#include <map>
#include <vector>
#include <utility>
#include "LbttAlloc.h"

4
lbtt/src/FormulaWriter.h
View file

@ -21,13 +21,11 @@
#define FORMULAWRITER_H
#include "Exception.h"
#include "LtlFormula.h"
namespace Ltl
{
class LtlFormula;
class Atom;
/******************************************************************************
*
* A function template class for writing the formula to a stream.

198
lbtt/src/Graph.h.in
View file

@ -186,6 +186,10 @@ public:
* graph nodes.
*/
class PathElement; /* A class for representing
* (node, edge) pairs
*/
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
protected:
@ -205,6 +209,14 @@ public:
* the graph nodes.
*/
typedef EdgeContainer EdgeContainerType; /* Type definition for
* containers of graph
* edges.
*/
typedef deque<PathElement, ALLOC(PathElement) > /* Type definition for */
Path; /* paths in a graph. */
typedef pair<size_type, size_type> StateIdPair; /* Type definition for a
* pair of state
* identifiers in a graph.
@ -323,8 +335,8 @@ public:
/* default assignment operator */
Graph<EdgeContainer>::size_type targetNode() /* Returns the index of */
const; /* the target node of
size_type targetNode() const; /* Returns the index of */
/* the target node of
* the directed edge.
*/
@ -353,7 +365,7 @@ protected:
*/
private:
Graph<EdgeContainer>::size_type target_node; /* Identifier of the edge's
size_type target_node; /* Identifier of the edge's
* target node.
*/
};
@ -404,6 +416,62 @@ protected:
/******************************************************************************
*
* A template class for representing (node identifier, edge) pairs in a graph.
*
*****************************************************************************/
template <class EdgeContainer>
class Graph<EdgeContainer>::PathElement
{
public:
explicit PathElement /* Constructors. */
(const typename Graph<EdgeContainer>::size_type
n,
const typename Graph<EdgeContainer>::Edge*
e = 0);
PathElement
(const typename Graph<EdgeContainer>::size_type
n,
const typename Graph<EdgeContainer>::Edge& e);
/* default copy constructor */
~PathElement(); /* Destructor. */
/* default assignment operator */
size_type node() const; /* Returns the identifier
* of the node associated
* with the path element.
*/
bool hasEdge() const; /* Tells whether there is
* an edge associated with
* the path element.
*/
const Edge& edge() const; /* Returns the edge
* associated with the
* path element.
*/
private:
typename Graph<EdgeContainer>::size_type node_id; /* Identifier of the node
* associated with the path
* element.
*/
const typename Graph<EdgeContainer>::Edge* /* Pointer to the edge */
edge_pointer; /* associated with the
* path element.
*/
};
/******************************************************************************
*
* An exception class for reporting errors when indexing graph nodes.
@ -924,7 +992,7 @@ Graph<EdgeContainer>::stats() const
*
* ------------------------------------------------------------------------- */
{
pair<Graph<EdgeContainer>::size_type, unsigned long int> result;
pair<size_type, unsigned long int> result;
result.first = nodes.size();
result.second = 0;
@ -1468,6 +1536,128 @@ void Graph<EdgeContainer>::Node::print
/******************************************************************************
*
* Inline function definitions for template class
* Graph<EdgeContainer>::PathElement.
*
*****************************************************************************/
/* ========================================================================= */
template <class EdgeContainer>
inline Graph<EdgeContainer>::PathElement::PathElement
(const typename Graph<EdgeContainer>::size_type n,
const typename Graph<EdgeContainer>::Edge* e) :
node_id(n), edge_pointer(e)
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class Graph<EdgeContainer>::PathElement.
* Creates a (node identifier, edge) pair from a node identifier
* and a pointer to an edge.
*
* Arguments: n -- Numeric identifier of a graph node.
* e -- A constant pointer to a graph edge.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
template <class EdgeContainer>
inline Graph<EdgeContainer>::PathElement::PathElement
(const typename Graph<EdgeContainer>::size_type n,
const typename Graph<EdgeContainer>::Edge& e) :
node_id(n), edge_pointer(&e)
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class Graph<EdgeContainer>::PathElement.
* Creates a (node identifier, edge) pair from a node identifier
* and an edge.
*
* Arguments: n -- Numeric identifier of a graph node.
* e -- A constant reference to a graph edge.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
template <class EdgeContainer>
inline Graph<EdgeContainer>::PathElement::~PathElement()
/* ----------------------------------------------------------------------------
*
* Description: Destructor for class Graph<EdgeContainer>::PathElement.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
template <class EdgeContainer>
inline typename Graph<EdgeContainer>::size_type
Graph<EdgeContainer>::PathElement::node() const
/* ----------------------------------------------------------------------------
*
* Description: Returns the identifier of the node associated with a
* Graph<EdgeContainer>::PathElement object.
*
* Arguments: None.
*
* Returns: Identifier of the node associated with the object.
*
* ------------------------------------------------------------------------- */
{
return node_id;
}
/* ========================================================================= */
template <class EdgeContainer>
inline bool Graph<EdgeContainer>::PathElement::hasEdge() const
/* ----------------------------------------------------------------------------
*
* Description: Tells whether there is an edge associated with a
* Graph<EdgeContainer>::PathElement object.
*
* Arguments: None.
*
* Returns: true iff there is an edge associated with the object.
*
* ------------------------------------------------------------------------- */
{
return (edge != 0);
}
/* ========================================================================= */
template <class EdgeContainer>
inline const typename Graph<EdgeContainer>::Edge&
Graph<EdgeContainer>::PathElement::edge() const
/* ----------------------------------------------------------------------------
*
* Description: Returns the edge associated with a
* Graph<EdgeContainer>::PathElement object. The function
* assumes that there is such an edge; it is an error to call
* this function for a PathElement object `element' for which
* `element.hasEdge() == false'.
*
* Arguments: None.
*
* Returns: The edge associated with the object.
*
* ------------------------------------------------------------------------- */
{
return *edge_pointer;
}
/******************************************************************************
*
* Inline function definitions for class NodeIndexException.

187
lbtt/src/IntervalList.cc Normal file
View file

@ -0,0 +1,187 @@
/*
* Copyright (C) 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.
*/
#include "IntervalList.h"
#include "StringUtil.h"
/******************************************************************************
*
* Function definitions for class IntervalList.
*
*****************************************************************************/
/* ========================================================================= */
void IntervalList::merge(unsigned long int min, unsigned long int max)
/* ----------------------------------------------------------------------------
*
* Description: Merges a new interval with a list of intervals.
*
* Arguments: min, max -- Upper and lower bound of the new interval.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
if (min > max)
return;
list<Interval, ALLOC(Interval) >::iterator interval;
for (interval = intervals.begin();
interval != intervals.end() && interval->second + 1 < min;
++interval)
;
if (interval == intervals.end())
{
intervals.insert(interval, make_pair(min, max));
return;
}
if (interval->first <= min && max <= interval->second)
return;
if (max + 1 < interval->first)
{
intervals.insert(interval, make_pair(min, max));
return;
}
if (min < interval->first)
interval->first = min;
if (interval->second < max)
{
interval->second = max;
list<Interval, ALLOC(Interval) >::iterator interval2 = interval;
++interval2;
while (interval2 != intervals.end()
&& interval2->first <= interval->second + 1)
{
if (interval->second < interval2->second)
interval->second = interval2->second;
list<Interval, ALLOC(Interval) >::iterator interval_to_erase = interval2;
++interval2;
intervals.erase(interval_to_erase);
}
}
}
/* ========================================================================= */
void IntervalList::remove(unsigned long int min, unsigned long int max)
/* ----------------------------------------------------------------------------
*
* Description: Removes a closed interval from an interval list.
*
* Arguments: min, max -- Bounds for the interval to remove.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
if (min > max)
return;
list<Interval, ALLOC(Interval) >::iterator interval;
for (interval = intervals.begin();
interval != intervals.end() && interval->second < min;
++interval)
;
while (interval != intervals.end())
{
if (max < interval->first) /* min <= max < imin <= imax */
return;
if (interval->first < min)
{
if (max < interval->second) /* imin < min <= max < imax */
{
intervals.insert(interval, make_pair(interval->first, min - 1));
interval->first = max + 1;
return;
}
interval->second = min - 1; /* imin < min <= imax <= max */
++interval;
}
else if (max < interval->second) /* min <= imin <= max < imax */
{
interval->first = max + 1;
return;
}
else /* min <= imin <= imax <= max */
{
list<Interval, ALLOC(Interval) >::iterator interval_to_erase = interval;
++interval;
intervals.erase(interval_to_erase);
}
}
}
/* ========================================================================= */
bool IntervalList::covers(unsigned long int min, unsigned long int max) const
/* ----------------------------------------------------------------------------
*
* Description: Test whether an interval list covers a given interval.
*
* Arguments: min, max -- Upper and lower bound for the interval to test.
*
* Returns: True if the IntervalList covers the given interval.
*
* ------------------------------------------------------------------------- */
{
if (min > max)
return true; /* empty interval is always covered */
list<Interval, ALLOC(Interval) >::const_iterator interval;
for (interval = intervals.begin();
interval != intervals.end() && min > interval->second;
++interval)
;
if (interval == intervals.end())
return false;
return (min >= interval->first && max <= interval->second);
}
/* ========================================================================= */
string IntervalList::toString() const
/* ----------------------------------------------------------------------------
*
* Description: Converts the interval list to a string.
*
* Arguments: None.
*
* Returns: A string listing the intervals in the interval list.
*
* ------------------------------------------------------------------------- */
{
string s;
for (list<Interval, ALLOC(Interval) >::const_iterator
interval = intervals.begin();
interval != intervals.end();
++interval)
{
if (interval != intervals.begin())
s += ',';
s += StringUtil::toString(interval->first) + "..."
+ StringUtil::toString(interval->second);
}
return s;
}

499
lbtt/src/IntervalList.h Normal file
View file

@ -0,0 +1,499 @@
/*
* Copyright (C) 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 INTERVALLIST_H
#define INTERVALLIST_H
#include <config.h>
#include <list>
#include <string>
#include <utility>
#include "LbttAlloc.h"
using namespace std;
/******************************************************************************
*
* The IntervalList class represents a list of disjoint closed intervals
* formed from pairs of unsigned long integers. The class supports merging
* a new interval with a list of intervals, removing an interval from a list
* of intervals and checking whether the interval list covers a given element
* (or a given interval). The elements of the intervals can also be accessed
* in increasing order via IntervalList::const_iterator.
*
*****************************************************************************/
class IntervalList
{
private:
typedef pair<unsigned long int,
unsigned long int>
Interval;
public:
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
class const_iterator /* A class for iterating */
{ /* over the elements of */
/* an IntervalList. */
public:
const_iterator(); /* Constructor. */
/* default copy constructor */
~const_iterator(); /* Destructor. */
/* default assignment operator */
bool operator==(const const_iterator& it) /* Comparison operators. */
const;
bool operator!=(const const_iterator& it)
const;
unsigned long int operator*() const; /* Dereference operator. */
unsigned long int operator++(); /* Prefix increment. */
unsigned long int operator++(int); /* Postfix increment. */
private:
const list<Interval, ALLOC(Interval) >* /* The interval list */
interval_list; /* associated with the */
/* iterator. */
list<Interval, ALLOC(Interval) > /* An iterator pointing */
::const_iterator interval; /* at the current */
/* interval list. */
unsigned long int element; /* Element currently
* pointed to by the
* iterator.
*/
friend class IntervalList;
};
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
IntervalList(); /* Constructor. */
~IntervalList(); /* Destructor. */
/* default copy constructor */
/* default assignment operator */
void merge(unsigned long int element); /* Merges a point interval
* with the list of
* intervals.
*/
void merge /* Merges a new interval */
(unsigned long int min, unsigned long int max); /* with the list of
* intervals.
*/
void remove(unsigned long int element); /* Removes an element from
* the list of intervals.
*/
void remove /* Removes an interval */
(unsigned long int min, unsigned long int max); /* from the list of
* intervals.
*/
bool covers(unsigned long int element) const; /* Tests whether the
* interval list covers an
* element.
*/
bool covers /* Tests whether the */
(unsigned long int min, unsigned long int max) /* interval list covers */
const; /* an interval. */
const_iterator begin() const; /* Returns an iterator to
* the beginning of the
* interval list.
*/
const_iterator end() const; /* Returns an iterator to
* the end of the interval
* list.
*/
typedef const_iterator iterator; /* The interval list
* cannot be modified with
* iterators.
*/
typedef list<Interval, ALLOC(Interval) > /* Size type. */
::size_type size_type;
size_type size() const; /* Tell the number of
* disjoint intervals in
* the interval list.
*/
size_type max_size() const; /* Tell the maximum
* allowable number of
* disjoint intervals in
* the interval list.
*/
bool empty() const; /* Tell whether the
* interval list is empty.
*/
void clear(); /* Makes the interval list
* empty.
*/
string toString() const; /* Converts the interval
* list to a string.
*/
private:
list<Interval, ALLOC(Interval) > intervals; /* List of intervals. */
friend class const_iterator;
};
/******************************************************************************
*
* Inline function definitions for class IntervalList.
*
*****************************************************************************/
/* ========================================================================= */
inline IntervalList::IntervalList()
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class IntervalList. Creates an empty list of
* intervals.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline IntervalList::~IntervalList()
/* ----------------------------------------------------------------------------
*
* Description: Destructor for class IntervalList.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline void IntervalList::merge(unsigned long int element)
/* ----------------------------------------------------------------------------
*
* Description: Merges an element (a point interval) with an IntervalList.
*
* Arguments: element -- Element to merge.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
merge(element, element);
}
/* ========================================================================= */
inline bool IntervalList::covers(unsigned long int element) const
/* ----------------------------------------------------------------------------
*
* Description: Tests whether an interval list covers an element.
*
* Arguments: element -- Element to test.
*
* Returns: True if the IntervalList covers the element.
*
* ------------------------------------------------------------------------- */
{
return covers(element, element);
}
/* ========================================================================= */
inline IntervalList::size_type IntervalList::size() const
/* ----------------------------------------------------------------------------
*
* Description: Tells the number of disjoint intervals in an IntervalList.
*
* Arguments: None.
*
* Returns: Number of disjoint intervals in the IntervalList.
*
* ------------------------------------------------------------------------- */
{
return intervals.size();
}
/* ========================================================================= */
inline IntervalList::size_type IntervalList::max_size() const
/* ----------------------------------------------------------------------------
*
* Description: Tells the maximum allowable number of disjoint intervals in
* an IntervalList.
*
* Arguments: None.
*
* Returns: Maximum allowable number of disjoint intervals in the
* IntervalList.
*
* ------------------------------------------------------------------------- */
{
return intervals.max_size();
}
/* ========================================================================= */
inline bool IntervalList::empty() const
/* ----------------------------------------------------------------------------
*
* Description: Tells whether an IntervalList is empty.
*
* Arguments: None.
*
* Returns: True if the IntervalList is empty.
*
* ------------------------------------------------------------------------- */
{
return intervals.empty();
}
/* ========================================================================= */
inline void IntervalList::clear()
/* ----------------------------------------------------------------------------
*
* Description: Makes an IntervalList empty.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
intervals.clear();
}
/* ========================================================================= */
inline IntervalList::const_iterator IntervalList::begin() const
/* ----------------------------------------------------------------------------
*
* Description: Returns an IntervalList::const_iterator pointing to the
* beginning of an IntervalList.
*
* Arguments: None.
*
* Returns: An IntervalList::const_iterator pointing to the beginning of
* the IntervalList.
*
* ------------------------------------------------------------------------- */
{
const_iterator it;
it.interval_list = &this->intervals;
it.interval = intervals.begin();
if (it.interval != intervals.end())
it.element = it.interval->first;
else
it.element = 0;
return it;
}
/* ========================================================================= */
inline IntervalList::const_iterator IntervalList::end() const
/* ----------------------------------------------------------------------------
*
* Description: Returns an IntervalList::const_iterator pointing to the end
* of an IntervalList.
*
* Arguments: None.
*
* Returns: An IntervalList::const_iterator pointing to the end of the
* IntervalList.
*
* ------------------------------------------------------------------------- */
{
const_iterator it;
it.interval_list = &this->intervals;
it.interval = intervals.end();
it.element = 0;
return it;
}
/******************************************************************************
*
* Inline function definitions for class IntervalList::const_iterator.
*
*****************************************************************************/
/* ========================================================================= */
inline IntervalList::const_iterator::const_iterator()
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class IntervalList::const_iterator.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline IntervalList::const_iterator::~const_iterator()
/* ----------------------------------------------------------------------------
*
* Description: Destructor for class IntervalList::const_iterator.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline bool IntervalList::const_iterator::operator==
(const const_iterator& it) const
/* ----------------------------------------------------------------------------
*
* Description: Equality test for two IntervalList::const_iterators. Two
* IntervalList::const_iterators are equal if and only if they
* point to the same interval of an interval list and the same
* element in the interval.
*
* Argument: it -- A constant reference to another
* IntervalList::const_iterator.
*
* Returns: Result of the equality test (a truth value).
*
* ------------------------------------------------------------------------- */
{
return (interval_list == it.interval_list && interval == it.interval
&& element == it.element);
}
/* ========================================================================= */
inline bool IntervalList::const_iterator::operator!=
(const const_iterator& it) const
/* ----------------------------------------------------------------------------
*
* Description: Inequality test for two IntervalList::const_iterators. Two
* IntervalList::const_iterators are not equal if and only if
* they point to different intervals of an interval list or to
* different elements of the same interval in the list.
*
* Argument: it -- A constant reference to another
* IntervalList::const_iterator.
*
* Returns: Result of the inequality test (a truth value).
*
* ------------------------------------------------------------------------- */
{
return (interval_list != it.interval_list || interval != it.interval
|| element != it.element);
}
/* ========================================================================= */
inline unsigned long int IntervalList::const_iterator::operator*() const
/* ----------------------------------------------------------------------------
*
* Description: Dereferencing operator for IntervalList::const_iterator.
*
* Arguments: None.
*
* Returns: The element currently pointed to by the iterator.
*
* ------------------------------------------------------------------------- */
{
return element;
}
/* ========================================================================= */
inline unsigned long int IntervalList::const_iterator::operator++()
/* ----------------------------------------------------------------------------
*
* Description: Prefix increment operator for IntervalList::const_iterator.
*
* Arguments: None.
*
* Returns: The element following the "current" element in the interval
* list.
*
* ------------------------------------------------------------------------- */
{
if (element == interval->second)
{
++interval;
if (interval != interval_list->end())
element = interval->first;
else
element = 0;
}
else
++element;
return element;
}
/* ========================================================================= */
inline unsigned long int IntervalList::const_iterator::operator++(int)
/* ----------------------------------------------------------------------------
*
* Description: Postfix increment operator for IntervalList::const_iterator.
*
* Arguments: None.
*
* Returns: The "current" element in the interval list.
*
* ------------------------------------------------------------------------- */
{
unsigned long int current_element = element;
if (element == interval->second)
{
++interval;
if (interval != interval_list->end())
element = interval->first;
else
element = 0;
}
else
++element;
return current_element;
}
#endif /* INTERVALLIST_H */

4
lbtt/src/LbttAlloc.h
View file

@ -22,11 +22,7 @@
#include <config.h>
#ifdef HAVE_SINGLE_CLIENT_ALLOC
#define ALLOC(typename) single_client_alloc
#else
#define ALLOC(typename) allocator<typename>
#endif /* HAVE_SINGLE_CLIENT_ALLOC */
#ifdef HAVE_OBSTACK_H

610
lbtt/src/Ltl-parse.yy Normal file
View file

@ -0,0 +1,610 @@
/*
* Copyright (C) 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.
*/
%{
#include <config.h>
#include <cctype>
#include <climits>
#include <cstring>
#include <istream>
#include <set>
#include "Exception.h"
#include "LbttAlloc.h"
#include "LtlFormula.h"
using namespace Ltl;
/******************************************************************************
*
* Variables and functions used for parsing an LTL formula.
*
*****************************************************************************/
static Exceptional_istream* estream; /* Pointer to input stream.
*/
static LtlFormula* result; /* This variable stores the
* result after a call to
* ltl_parse.
*/
static std::set<LtlFormula*, less<LtlFormula*>, /* Intermediate results. */
ALLOC(LtlFormula*) > /* (This set is used */
intermediate_results; /* for keeping track of
* the subformulas of a
* partially constructed
* formula in case the
* memory allocated for
* the subformulas needs
* to be freed because
* of a parse error.)
*/
static int ltl_lex(); /* The lexical scanner. */
/******************************************************************************
*
* Function for reporting parse errors.
*
*****************************************************************************/
static void ltl_error(const char*)
{
throw LtlFormula::ParseErrorException("error parsing LTL formula");
}
/******************************************************************************
*
* Function for updating the set of intermediate results.
*
*****************************************************************************/
inline LtlFormula* newFormula(LtlFormula& f)
{
intermediate_results.insert(&f);
return &f;
}
%}
%name-prefix="ltl_"
/******************************************************************************
*
* Declarations for terminal and nonterminal symbols used in the grammar rules
* below.
*
*****************************************************************************/
%union {
class LtlFormula* formula;
}
/* Uninterpreted symbols. */
%token LTLPARSE_LPAR LTLPARSE_RPAR LTLPARSE_FALSE LTLPARSE_TRUE
LTLPARSE_UNKNOWN
/* Atomic propositions. */
%token <formula> LTLPARSE_ATOM
/* Operators. */
%nonassoc LTLPARSE_UNTIL LTLPARSE_RELEASE LTLPARSE_WEAK_UNTIL
LTLPARSE_STRONG_RELEASE LTLPARSE_BEFORE
%left LTLPARSE_IMPLY LTLPARSE_EQUIV LTLPARSE_XOR
%left LTLPARSE_OR
%left LTLPARSE_AND
%nonassoc LTLPARSE_NOT LTLPARSE_NEXT LTLPARSE_FINALLY LTLPARSE_GLOBALLY
%nonassoc LTLPARSE_EQUALS
/* Compound formulas. */
%type <formula> formula atomic_formula unary_formula prefix_op_formula
binary_formula prefix_b_formula infix_b_formula
/******************************************************************************
*
* Grammar rule definitions.
*
*****************************************************************************/
%%
ltl_formula: formula
{ result = $1; }
;
formula: atomic_formula
{ $$ = $1; }
| unary_formula
{ $$ = $1; }
| binary_formula
{ $$ = $1; }
| LTLPARSE_LPAR formula LTLPARSE_RPAR
{ $$ = $2; }
;
atomic_formula: LTLPARSE_ATOM
{ $$ = $1; }
| LTLPARSE_ATOM LTLPARSE_EQUALS LTLPARSE_FALSE
{
intermediate_results.erase($1);
$$ = newFormula(Not::construct($1));
}
| LTLPARSE_ATOM LTLPARSE_EQUALS LTLPARSE_TRUE
{ $$ = $1; }
| LTLPARSE_FALSE
{ $$ = newFormula(False::construct()); }
| LTLPARSE_TRUE
{ $$ = newFormula(True::construct()); }
;
unary_formula: LTLPARSE_NOT formula
{
intermediate_results.erase($2);
$$ = newFormula(Not::construct($2));
}
| LTLPARSE_NEXT formula
{
intermediate_results.erase($2);
$$ = newFormula(Next::construct($2));
}
| LTLPARSE_FINALLY formula
{
intermediate_results.erase($2);
$$ = newFormula(Finally::construct($2));
}
| LTLPARSE_GLOBALLY formula
{
intermediate_results.erase($2);
$$ = newFormula(Globally::construct($2));
}
;
prefix_op_formula: atomic_formula
{ $$ = $1; }
| unary_formula
{ $$ = $1; }
| prefix_b_formula
{ $$ = $1; }
| LTLPARSE_LPAR formula LTLPARSE_RPAR
{ $$ = $2; }
;
binary_formula: prefix_b_formula
{ $$ = $1; }
| infix_b_formula
{ $$ = $1; }
;
prefix_b_formula: LTLPARSE_AND prefix_op_formula prefix_op_formula
{
intermediate_results.erase($2);
intermediate_results.erase($3);
$$ = newFormula(And::construct($2, $3));
}
| LTLPARSE_OR prefix_op_formula prefix_op_formula
{
intermediate_results.erase($2);
intermediate_results.erase($3);
$$ = newFormula(Or::construct($2, $3));
}
| LTLPARSE_IMPLY prefix_op_formula prefix_op_formula
{
intermediate_results.erase($2);
intermediate_results.erase($3);
$$ = newFormula(Imply::construct($2, $3));
}
| LTLPARSE_EQUIV prefix_op_formula prefix_op_formula
{
intermediate_results.erase($2);
intermediate_results.erase($3);
$$ = newFormula(Equiv::construct($2, $3));
}
| LTLPARSE_XOR prefix_op_formula prefix_op_formula
{
intermediate_results.erase($2);
intermediate_results.erase($3);
$$ = newFormula(Xor::construct($2, $3));
}
| LTLPARSE_UNTIL prefix_op_formula prefix_op_formula
{
intermediate_results.erase($2);
intermediate_results.erase($3);
$$ = newFormula(Until::construct($2, $3));
}
| LTLPARSE_RELEASE prefix_op_formula prefix_op_formula
{
intermediate_results.erase($2);
intermediate_results.erase($3);
$$ = newFormula(V::construct($2, $3));
}
| LTLPARSE_WEAK_UNTIL prefix_op_formula prefix_op_formula
{
intermediate_results.erase($2);
intermediate_results.erase($3);
$$ = newFormula(WeakUntil::construct($2, $3));
}
| LTLPARSE_STRONG_RELEASE prefix_op_formula
prefix_op_formula
{
intermediate_results.erase($2);
intermediate_results.erase($3);
$$ = newFormula(StrongRelease::construct($2, $3));
}
| LTLPARSE_BEFORE prefix_op_formula prefix_op_formula
{
intermediate_results.erase($2);
intermediate_results.erase($3);
$$ = newFormula(Before::construct($2, $3));
}
;
infix_b_formula: formula LTLPARSE_AND formula
{
intermediate_results.erase($1);
intermediate_results.erase($3);
$$ = newFormula(And::construct($1, $3));
}
| formula LTLPARSE_OR formula
{
intermediate_results.erase($1);
intermediate_results.erase($3);
$$ = newFormula(Or::construct($1, $3));
}
| formula LTLPARSE_IMPLY formula
{
intermediate_results.erase($1);
intermediate_results.erase($3);
$$ = newFormula(Imply::construct($1, $3));
}
| formula LTLPARSE_EQUIV formula
{
intermediate_results.erase($1);
intermediate_results.erase($3);
$$ = newFormula(Equiv::construct($1, $3));
}
| formula LTLPARSE_XOR formula
{
intermediate_results.erase($1);
intermediate_results.erase($3);
$$ = newFormula(Xor::construct($1, $3));
}
| formula LTLPARSE_UNTIL formula
{
intermediate_results.erase($1);
intermediate_results.erase($3);
$$ = newFormula(Until::construct($1, $3));
}
| formula LTLPARSE_RELEASE formula
{
intermediate_results.erase($1);
intermediate_results.erase($3);
$$ = newFormula(V::construct($1, $3));
}
| formula LTLPARSE_WEAK_UNTIL formula
{
intermediate_results.erase($1);
intermediate_results.erase($3);
$$ = newFormula(WeakUntil::construct($1, $3));
}
| formula LTLPARSE_STRONG_RELEASE formula
{
intermediate_results.erase($1);
intermediate_results.erase($3);
$$ = newFormula(StrongRelease::construct($1, $3));
}
| formula LTLPARSE_BEFORE formula
{
intermediate_results.erase($1);
intermediate_results.erase($3);
$$ = newFormula(Before::construct($1, $3));
}
;
%%
/******************************************************************************
*
* Helper function for reading lexical tokens from a stream.
*
*****************************************************************************/
static inline size_t matchCharactersFromStream
(istream& stream, char* chars)
{
size_t num_matched;
for (num_matched = 0; *chars != '\0' && stream.peek() == *chars; ++chars)
{
stream.ignore(1);
++num_matched;
}
return num_matched;
}
/******************************************************************************
*
* Main interface to the parser.
*
*****************************************************************************/
namespace Ltl
{
/* ========================================================================= */
LtlFormula* parseFormula(istream& stream)
/* ----------------------------------------------------------------------------
*
* Description: Parses an LTL formula from a stream. The formula should be
* in one of the formats used by the tools lbtt 1.0.x (both
* prefix and infix form), Spin/Temporal Massage Parlor/LTL2BA,
* LTL2AUT or Wring 1.1.0 (actually, the grammar is basically
* a combination of the grammars of the above tools with the
* exception that propositions should always be written in the
* form `pN' for some integer N; in principle, it is possible to
* use a mixed syntax for the formula). The input should be
* terminated with a newline.
*
* Argument: stream -- A reference to the input stream.
*
* Returns: A pointer to the formula. The function throws an
* LtlFormula::ParseErrorException if the syntax is incorrect,
* or an IOException in case of an end-of-file or another I/O
* error.
*
* ------------------------------------------------------------------------- */
{
Exceptional_istream es(&stream, ios::badbit | ios::failbit | ios::eofbit);
estream = &es;
intermediate_results.clear();
try
{
ltl_parse();
}
catch (...)
{
for (std::set<LtlFormula*, less<LtlFormula*>, ALLOC(LtlFormula*) >
::const_iterator f = intermediate_results.begin();
f != intermediate_results.end();
++f)
LtlFormula::destruct(*f);
throw;
}
return result;
}
}
/******************************************************************************
*
* The lexical scanner.
*
*****************************************************************************/
static int ltl_lex()
{
char c;
std::istream& stream = static_cast<istream&>(*estream);
do
{
estream->get(c);
}
while (isspace(c) && c != '\n');
switch (c)
{
case '\n' : return 0;
case '(' :
return (matchCharactersFromStream(stream, ")") == 1
? LTLPARSE_NEXT
: LTLPARSE_LPAR);
case ')' : return LTLPARSE_RPAR;
case 'f' :
switch (matchCharactersFromStream(stream, "alse"))
{
case 0 : case 4 :
return LTLPARSE_FALSE;
default:
break;
}
return LTLPARSE_UNKNOWN;
case '0' : return LTLPARSE_FALSE;
case 't' :
switch (matchCharactersFromStream(stream, "rue"))
{
case 0 : case 3 :
return LTLPARSE_TRUE;
default :
return LTLPARSE_UNKNOWN;
}
case 'T' :
return (matchCharactersFromStream(stream, "RUE") == 3
? LTLPARSE_TRUE
: LTLPARSE_UNKNOWN);
case '1' : return LTLPARSE_TRUE;
case '!' : case '~' : return LTLPARSE_NOT;
case '&' :
matchCharactersFromStream(stream, "&");
return LTLPARSE_AND;
case '/' :
return (matchCharactersFromStream(stream, "\\") == 1
? LTLPARSE_AND
: LTLPARSE_UNKNOWN);
case '*' : return LTLPARSE_AND;
case '|' :
matchCharactersFromStream(stream, "|");
return LTLPARSE_OR;
case '\\' :
return (matchCharactersFromStream(stream, "/") == 1
? LTLPARSE_OR
: LTLPARSE_UNKNOWN);
case '+' : return LTLPARSE_OR;
case '=' :
return (matchCharactersFromStream(stream, ">") == 1
? LTLPARSE_IMPLY
: LTLPARSE_EQUALS);
case '-' :
return (matchCharactersFromStream(stream, ">") == 1
? LTLPARSE_IMPLY
: LTLPARSE_UNKNOWN);
case 'i' : return LTLPARSE_IMPLY;
case '<' :
if (matchCharactersFromStream(stream, ">") == 1)
return LTLPARSE_FINALLY;
return (matchCharactersFromStream(stream, "->") == 2
|| matchCharactersFromStream(stream, "=>") == 2
? LTLPARSE_EQUIV
: LTLPARSE_UNKNOWN);
case 'e' : return LTLPARSE_EQUIV;
case 'x' :
return (matchCharactersFromStream(stream, "or") == 2
? LTLPARSE_XOR
: LTLPARSE_UNKNOWN);
case '^' : return LTLPARSE_XOR;
case 'X' : return LTLPARSE_NEXT;
case 'U' : return LTLPARSE_UNTIL;
case 'V' : case 'R' : return LTLPARSE_RELEASE;
case 'W' : return LTLPARSE_WEAK_UNTIL;
case 'M' : return LTLPARSE_STRONG_RELEASE;
case 'B' : return LTLPARSE_BEFORE;
case 'F' :
switch (matchCharactersFromStream(stream, "ALSE"))
{
case 0 :
return LTLPARSE_FINALLY;
case 4 :
return LTLPARSE_FALSE;
default :
return LTLPARSE_UNKNOWN;
}
case '[' :
return (matchCharactersFromStream(stream, "]") == 1
? LTLPARSE_GLOBALLY
: LTLPARSE_UNKNOWN);
case 'G' : return LTLPARSE_GLOBALLY;
case 'p' :
{
long int id = 0;
bool id_ok = false;
int ch = stream.peek();
while (ch >= '0' && ch <= '9')
{
id_ok = true;
estream->get(c);
if (LONG_MAX / 10 < id)
throw LtlFormula::ParseErrorException
("error parsing LTL formula (proposition identifier out of "
"range)");
id *= 10;
id += (c - '0');
ch = stream.peek();
}
if (id_ok)
{
ltl_lval.formula = newFormula(Atom::construct(id));
return LTLPARSE_ATOM;
}
return LTLPARSE_UNKNOWN;
}
default : return LTLPARSE_UNKNOWN;
}
}

194
lbtt/src/LtlFormula.cc
View file

@ -24,9 +24,8 @@
namespace Ltl
{
map<LtlFormula*, unsigned long int, /* Shared storage for */
LtlFormula::ptr_less, /* LTL formulae. */
ALLOC(unsigned long int) >
set<LtlFormula*, LtlFormula::ptr_less, /* Shared storage for */
ALLOC(LtlFormula*) > /* LTL formulae. */
LtlFormula::formula_storage;
unsigned long int /* Upper limit for the */
@ -38,8 +37,6 @@ unsigned long int /* Upper limit for the */
* truth assignment).
*/
/******************************************************************************
*
* Function for obtaining the infix symbol associated with a given
@ -875,193 +872,6 @@ Bitset LtlFormula::findPropositionalModel(long int max_atom) const
return model;
}
/* ========================================================================= */
LtlFormula* LtlFormula::read(Exceptional_istream& stream)
/* ----------------------------------------------------------------------------
*
* Description: Recursively constructs an LtlFormula by parsing input from an
* exception-aware input stream.
*
* Argument: stream -- A reference to an exception-aware input stream.
*
* Returns: The constructed LtlFormula.
*
* ------------------------------------------------------------------------- */
{
string token;
LtlFormula* formula;
try
{
stream >> token;
}
catch (const IOException&)
{
if (static_cast<istream&>(stream).eof())
throw ParseErrorException("error parsing LTL formula (unexpected end of "
"input)");
else
throw ParseErrorException("error parsing LTL formula (I/O error)");
}
if (token[0] == 'p')
{
if (token.length() == 1)
throw ParseErrorException("error parsing LTL formula (unrecognized "
"token: `" + token + "')");
long int id;
char* endptr;
id = strtol(token.c_str() + 1, &endptr, 10);
if (*endptr != '\0' || id < 0 || id == LONG_MIN || id == LONG_MAX)
throw ParseErrorException("error parsing LTL formula (unrecognized "
"token: `" + token + "')");
formula = &Atom::construct(id);
}
else
{
if (token.length() > 1)
throw ParseErrorException("error parsing LTL formula (unrecognized "
"token: `" + token + "')");
switch (token[0])
{
case LTL_TRUE :
formula = &True::construct();
break;
case LTL_FALSE :
formula = &False::construct();
break;
case LTL_NEGATION :
case LTL_NEXT :
case LTL_FINALLY :
case LTL_GLOBALLY :
{
LtlFormula* g = read(stream);
try
{
switch (token[0])
{
case LTL_NEGATION :
formula = &Not::construct(g);
break;
case LTL_NEXT :
formula = &Next::construct(g);
break;
case LTL_FINALLY :
formula = &Finally::construct(g);
break;
default : /* LTL_GLOBALLY */
formula = &Globally::construct(g);
break;
}
}
catch (...)
{
LtlFormula::destruct(g);
throw;
}
break;
}
case LTL_CONJUNCTION :
case LTL_DISJUNCTION :
case LTL_IMPLICATION :
case LTL_EQUIVALENCE :
case LTL_XOR :
case LTL_UNTIL :
case LTL_V :
case LTL_WEAK_UNTIL :
case LTL_STRONG_RELEASE :
case LTL_BEFORE :
{
LtlFormula* g = read(stream);
LtlFormula* h;
try
{
h = read(stream);
}
catch (...)
{
LtlFormula::destruct(g);
throw;
}
try
{
switch (token[0])
{
case LTL_CONJUNCTION :
formula = &And::construct(g, h);
break;
case LTL_DISJUNCTION :
formula = &Or::construct(g, h);
break;
case LTL_IMPLICATION :
formula = &Imply::construct(g, h);
break;
case LTL_EQUIVALENCE :
formula = &Equiv::construct(g, h);
break;
case LTL_XOR :
formula = &Xor::construct(g, h);
break;
case LTL_UNTIL :
formula = &Until::construct(g, h);
break;
case LTL_V :
formula = &V::construct(g, h);
break;
case LTL_WEAK_UNTIL :
formula = &WeakUntil::construct(g, h);
break;
case LTL_STRONG_RELEASE :
formula = &StrongRelease::construct(g, h);
break;
default : /* LTL_BEFORE */
formula = &Before::construct(g, h);
break;
}
}
catch (...)
{
LtlFormula::destruct(g);
LtlFormula::destruct(h);
throw;
}
break;
}
default :
throw ParseErrorException("error parsing LTL formula (unrecognized "
"token: `" + token + "')");
}
}
return formula;
}
/* ========================================================================= */
void LtlFormula::print(Exceptional_ostream& estream, OutputMode mode) const
/* ----------------------------------------------------------------------------

70
lbtt/src/LtlFormula.h
View file

@ -23,7 +23,7 @@
#include <config.h>
#include <deque>
#include <iostream>
#include <map>
#include <set>
#include <stack>
#include <string>
#include "LbttAlloc.h"
@ -188,13 +188,6 @@ public:
* input stream.
*/
static LtlFormula* read /* Constructs an */
(Exceptional_istream& stream); /* LtlFormula by parsing
* input from an
* exception-aware input
* stream.
*/
void print /* Writes the formula to */
(ostream& stream = cout, /* an output stream. */
OutputMode mode = LTL_INFIX) const;
@ -250,6 +243,10 @@ protected:
unsigned int is_constant : 1; /* operators and atomic */
} info_flags; /* propositions. */
unsigned long int refcount; /* Number of references to
* `this' LtlFormula.
*/
static LtlFormula& /* Updates the shared */
insertToStorage(LtlFormula* f); /* formula storage with
* a new formula.
@ -288,8 +285,8 @@ private:
* formula.
*/
static map<LtlFormula*, unsigned long int, /* Shared storage for */
ptr_less, ALLOC(unsigned long int) > /* LTL formulae. */
static set<LtlFormula*, ptr_less, /* Shared storage for */
ALLOC(LtlFormula*) > /* LTL formulae. */
formula_storage;
static unsigned long int /* Upper limit for the */
@ -330,6 +327,16 @@ private:
/******************************************************************************
*
* Interface to the formula parser.
*
*****************************************************************************/
extern LtlFormula* parseFormula(istream& stream);
/******************************************************************************
*
* A class for atomic propositions.
@ -474,7 +481,7 @@ private:
* to satisfy the
* LtlFormula member
* function interface.
*/
*/
};
@ -1076,7 +1083,7 @@ typedef BinaryFormula<LtlBefore> Before;
*****************************************************************************/
/* ========================================================================= */
inline LtlFormula::LtlFormula()
inline LtlFormula::LtlFormula() : refcount(1)
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class LtlFormula. Initializes the attributes
@ -1088,8 +1095,6 @@ inline LtlFormula::LtlFormula()
*
* --------------------------------------------------------------------------*/
{
info_flags.is_propositional = 0;
info_flags.is_constant = 0;
}
/* ========================================================================= */
@ -1122,14 +1127,9 @@ inline void LtlFormula::destruct(LtlFormula* f)
*
* ------------------------------------------------------------------------- */
{
map<LtlFormula*, unsigned long int, LtlFormula::ptr_less,
ALLOC(unsigned long int) >::iterator
deleter;
deleter = formula_storage.find(f);
if (--deleter->second == 0)
if (--f->refcount == 0)
{
formula_storage.erase(deleter);
formula_storage.erase(f);
delete f;
}
}
@ -1147,7 +1147,7 @@ inline LtlFormula* LtlFormula::clone()
*
* ------------------------------------------------------------------------- */
{
formula_storage.find(this)->second++;
++refcount;
return this;
}
@ -1241,8 +1241,7 @@ inline LtlFormula* LtlFormula::read(istream& stream)
*
* ------------------------------------------------------------------------- */
{
Exceptional_istream estream(&stream, ios::badbit | ios::failbit);
return read(estream);
return parseFormula(stream);
}
/* ========================================================================= */
@ -1303,8 +1302,6 @@ inline Exceptional_ostream& operator<<
return stream;
}
/* ========================================================================= */
inline LtlFormula& LtlFormula::insertToStorage(LtlFormula* f)
/* ----------------------------------------------------------------------------
@ -1317,19 +1314,16 @@ inline LtlFormula& LtlFormula::insertToStorage(LtlFormula* f)
*
* ------------------------------------------------------------------------- */
{
map<LtlFormula*, unsigned long int, LtlFormula::ptr_less,
ALLOC(unsigned long int) >::iterator
inserter;
inserter = formula_storage.find(f);
set<LtlFormula*, ptr_less, ALLOC(LtlFormula*) >::iterator inserter
= formula_storage.find(f);
if (inserter != formula_storage.end())
{
delete f;
inserter->second++;
return *(inserter->first);
++(*inserter)->refcount;
return **inserter;
}
formula_storage.insert(make_pair(f, 1));
formula_storage.insert(f);
return *f;
}
@ -1571,8 +1565,7 @@ inline Atom& Atom::construct(long int a)
}
/* ========================================================================= */
inline Atom::Atom(long int a) :
LtlFormula(), atom(a)
inline Atom::Atom(long int a) : atom(a)
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class Atom. Creates a new propositional atom.
@ -1886,8 +1879,7 @@ inline UnaryFormula<Operator>& UnaryFormula<Operator>::construct(LtlFormula& f)
/* ========================================================================= */
template<class Operator>
inline UnaryFormula<Operator>::UnaryFormula(LtlFormula* f) :
LtlFormula(), subformula(f)
inline UnaryFormula<Operator>::UnaryFormula(LtlFormula* f) : subformula(f)
/* ----------------------------------------------------------------------------
*
* Description: Constructs an LTL formula with a unary operator.
@ -2189,7 +2181,7 @@ BinaryFormula<Operator>::construct(LtlFormula& f1, LtlFormula* f2)
/* ========================================================================= */
template<class Operator>
inline BinaryFormula<Operator>::BinaryFormula(LtlFormula* f1, LtlFormula* f2) :
LtlFormula(), subformula1(f1), subformula2(f2)
subformula1(f1), subformula2(f2)
/* ----------------------------------------------------------------------------
*
* Description: Constructs a binary LTL formula.

104
lbtt/src/Makefile.am
View file

@ -1,22 +1,90 @@
BUILT_SOURCES = Config-parse.h NeverClaim-parse.h
AM_YFLAGS = -d
bin_PROGRAMS = lbtt lbtt-translate
lbtt_SOURCES = BitArray.h Bitset.h BitArray.cc BuchiAutomaton.h \
BuchiAutomaton.cc Config-parse.yy Config-lex.ll Configuration.h \
Configuration.cc DispUtil.h DispUtil.cc EdgeContainer.h Exception.h \
FormulaRandomizer.h FormulaRandomizer.cc FormulaWriter.h LbttAlloc.h \
LtlFormula.h LtlFormula.cc main.cc PathEvaluator.h PathEvaluator.cc \
PathIterator.h PathIterator.cc ProductAutomaton.h ProductAutomaton.cc \
Random.h SccIterator.h SharedTestData.h StatDisplay.h StatDisplay.cc \
StateSpace.h StateSpace.cc StateSpaceRandomizer.h StateSpaceRandomizer.cc \
StringUtil.h StringUtil.cc TestOperations.h TestOperations.cc TestRoundInfo.h \
TestStatistics.h TestStatistics.cc UserCommandReader.h UserCommandReader.cc \
UserCommands.h UserCommands.cc
EXTRA_lbtt_SOURCES = gnu-getopt.h Config-parse.h
lbtt_SOURCES = \
BitArray.h \
Bitset.h \
BitArray.cc \
BuchiAutomaton.h \
BuchiAutomaton.cc \
BuchiProduct.h \
BuchiProduct.cc \
Config-parse.yy \
Config-lex.ll \
Configuration.h \
Configuration.cc \
DispUtil.h \
DispUtil.cc \
EdgeContainer.h \
Exception.h \
FormulaRandomizer.h \
FormulaRandomizer.cc \
FormulaWriter.h \
IntervalList.h \
IntervalList.cc \
LbttAlloc.h \
LtlFormula.h \
LtlFormula.cc \
Ltl-parse.yy \
main.cc \
PathEvaluator.h \
PathEvaluator.cc \
PathIterator.h \
PathIterator.cc \
Product.h \
Random.h \
SccCollection.h \
SharedTestData.h \
StatDisplay.h \
StatDisplay.cc \
StateSpace.h \
StateSpace.cc \
StateSpaceProduct.h \
StateSpaceRandomizer.h \
StateSpaceRandomizer.cc \
StringUtil.h \
StringUtil.cc \
TempFsysName.h \
TempFsysName.cc \
TestOperations.h \
TestOperations.cc \
TestRoundInfo.h \
TestStatistics.h \
TestStatistics.cc \
UserCommandReader.h \
UserCommandReader.cc \
UserCommands.h \
UserCommands.cc
EXTRA_lbtt_SOURCES = gnu-getopt.h
lbtt_LDADD = @LIBOBJS@ @READLINELIBS@
lbtt_translate_SOURCES = BitArray.h BitArray.cc Exception.h \
ExternalTranslator.h ExternalTranslator.cc FormulaWriter.h LbttAlloc.h \
LbtWrapper.h LtlFormula.h LtlFormula.cc NeverClaim-parse.yy NeverClaim-lex.ll \
NeverClaimAutomaton.h NeverClaimAutomaton.cc SpinWrapper.h SpinWrapper.cc \
StringUtil.h StringUtil.cc translate.h translate.cc TranslatorInterface.h
EXTRA_lbtt_translate_SOURCES = gnu-getopt.h NeverClaim-parse.h
lbtt_translate_SOURCES = \
BitArray.h \
BitArray.cc \
Exception.h \
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 \
NeverClaimAutomaton.cc \
SpinWrapper.h \
SpinWrapper.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@

1
lbtt/src/NeverClaim-lex.ll
View file

@ -30,6 +30,7 @@ extern int current_neverclaim_line_number;
%option never-interactive
%option noyywrap
%option nounput
%%

47
lbtt/src/PathEvaluator.cc
View file

@ -61,26 +61,25 @@ void PathEvaluator::reset()
/* ========================================================================= */
bool PathEvaluator::evaluate
(const LtlFormula& formula, const StateSpace& statespace,
const vector<StateSpace::size_type, ALLOC(StateSpace::size_type) >&
states_on_path,
StateSpace::size_type loop_state)
(const LtlFormula& formula, const StateSpace::Path& prefix,
const StateSpace::Path& cycle, const StateSpace& statespace)
/* ----------------------------------------------------------------------------
*
* Description: Evaluates an LTL formula in a state space in which the states
* are connected into a non-branching sequence that ends in a
* loop.
* Description: Evaluates an LTL formula in a path formed from a prefix and
* an infinitely repeating cycle of states in a state space.
*
* Arguments: formula -- Formula to be evaluated.
* statespace -- State space from which the path is
* extracted.
* states_on_path -- Mapping between states in the path and
* the states in `statespace' such that
* `statespace[states_on_path[i]]'
* corresponds to the ith state of the path.
* loop_state -- Number of the state in the path to which
* the ``last'' state of the path is
* connected.
* Arguments: formula -- Formula to be evaluated.
* prefix -- A StateSpace::Path object corresponding to
* the prefix of the path. Only the state
* identifiers in the path elements are used;
* the function will not require `prefix' to
* actually represent a path in `statespace'.
* cycle -- A StateSpace::Path object corresponding to
* the infinitely repeating cycle. Only the
* state identifiers in the path elements are
* relevant.
* statespace -- State space to which the state identifiers in
* `path' and `cycle' refer.
*
* Returns: `true' if and only if the LTL formula holds in the path.
*
@ -88,13 +87,21 @@ bool PathEvaluator::evaluate
{
reset();
if (states_on_path.empty() || loop_state >= states_on_path.size())
if (cycle.empty())
return false;
current_formula = &formula;
current_path = &statespace;
current_loop_state = loop_state;
path_states = states_on_path;
current_loop_state = prefix.size();
path_states.reserve(prefix.size() + cycle.size());
for (StateSpace::Path::const_iterator state = prefix.begin();
state != prefix.end();
++state)
path_states.push_back(state->node());
for (StateSpace::Path::const_iterator state = cycle.begin();
state != cycle.end();
++state)
path_states.push_back(state->node());
return eval();
}

10
lbtt/src/PathEvaluator.h
View file

@ -54,11 +54,11 @@ public:
bool evaluate /* Tests whether an */
(const LtlFormula& formula, /* LtlFormula holds in a */
const StateSpace& statespace, /* state space. */
const vector<StateSpace::size_type,
ALLOC(StateSpace::size_type) >&
states_on_path,
StateSpace::size_type loop_state);
const StateSpace::Path& prefix, /* path described by a */
const StateSpace::Path& cycle, /* prefix and a cycle of */
const StateSpace& statespace); /* states from a state
* space.
*/
bool evaluate /* Same as above. */
(const LtlFormula& formula,

2936
lbtt/src/Product.h Normal file
View file

File diff suppressed because it is too large Load diff

1174
lbtt/src/SccCollection.h Normal file
View file

File diff suppressed because it is too large Load diff

550
lbtt/src/StatDisplay.cc
View file

@ -21,6 +21,7 @@
#include <string>
#include "DispUtil.h"
#include "Exception.h"
#include "IntervalList.h"
#include "SharedTestData.h"
#include "StatDisplay.h"
#include "StringUtil.h"
@ -33,6 +34,47 @@ using namespace ::DispUtil;
using namespace ::SharedTestData;
using namespace ::StringUtil;
/* ========================================================================= */
void printStatTableHeader(ostream& stream, int indent)
/* ----------------------------------------------------------------------------
*
* Description: Displays a table header for test statistics (used in
* verbosity mode 2).
*
* Arguments: stream -- A reference to the output stream to which the
* header should be written.
* indent -- Number of spaces to leave on the left of the
* output.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
Exceptional_ostream estream(&stream, ios::failbit | ios::badbit);
int num_dashes = 39;
estream << string(indent, ' ') + " # F Elapsed Büchi Büchi Acc.";
if (configuration.global_options.do_cons_test
|| configuration.global_options.do_comp_test)
{
num_dashes += 31;
estream << " Product Product Acc.";
if (configuration.global_options.do_cons_test)
{
num_dashes += 3;
estream << " CC";
}
}
estream << '\n' + string(indent + 10, ' ')
+ "time states trans. sets";
if (configuration.global_options.do_cons_test
|| configuration.global_options.do_comp_test)
estream << " states trans. cycles";
estream << "\n" + string(indent, ' ') + string(num_dashes, '-') + '\n';
estream.flush();
}
/* ========================================================================= */
void printBuchiAutomatonStats
(ostream& stream, int indent,
@ -48,7 +90,7 @@ void printBuchiAutomatonStats
* Arguments: stream -- A reference to the output stream to which the
* information should be written.
* indent -- Number of spaces to leave on the left of the
* output.
* output in verbosity modes >= 3.
* algorithm -- Identifier of the algorithm used for
* generating the automaton.
* result_id -- Selects between the automata constructed from
@ -63,35 +105,68 @@ void printBuchiAutomatonStats
const AutomatonStats& automaton_stats =
test_results[algorithm].automaton_stats[result_id];
estream << string(indent, ' ');
if (!automaton_stats.buchiAutomatonComputed())
estream << "not computed";
if (configuration.global_options.verbosity <= 2)
{
if (!automaton_stats.buchiAutomatonComputed())
estream << " N/A N/A N/A N/A";
else
{
if (automaton_stats.buchi_generation_time >= 0.0)
{
changeStreamFormatting(stream, 9, 2, ios::fixed | ios::right);
estream << automaton_stats.buchi_generation_time;
restoreStreamFormatting(stream);
}
else
estream << " N/A";
estream << ' ';
changeStreamFormatting(stream, 9, 0, ios::right);
estream << automaton_stats.number_of_buchi_states;
restoreStreamFormatting(stream);
estream << ' ';
changeStreamFormatting(stream, 9, 0, ios::right);
estream << automaton_stats.number_of_buchi_transitions;
restoreStreamFormatting(stream);
estream << ' ';
changeStreamFormatting(stream, 4, 0, ios::right);
estream << automaton_stats.number_of_acceptance_sets;
restoreStreamFormatting(stream);
}
estream << ' ';
}
else
{
estream << "number of states:" + string(6, ' ')
+ toString(automaton_stats.number_of_buchi_states)
+ '\n' + string(indent, ' ') + "number of transitions: "
+ toString(automaton_stats.number_of_buchi_transitions)
+ '\n' + string(indent, ' ') + "acceptance sets:"
+ string(7, ' ')
+ toString(automaton_stats.number_of_acceptance_sets)
+ '\n' + string(indent, ' ') + "computation time:"
+ string(6, ' ');
if (automaton_stats.buchi_generation_time != -1.0)
{
changeStreamFormatting(stream, 9, 2, ios::fixed | ios::left);
estream << automaton_stats.buchi_generation_time;
restoreStreamFormatting(stream);
estream << string(indent, ' ');
estream << " seconds (user time)";
}
if (!automaton_stats.buchiAutomatonComputed())
estream << "not computed";
else
estream << "N/A";
{
estream << "number of states:" + string(6, ' ')
+ toString(automaton_stats.number_of_buchi_states)
+ '\n' + string(indent, ' ') + "number of transitions: "
+ toString(automaton_stats.number_of_buchi_transitions)
+ '\n' + string(indent, ' ') + "acceptance sets:"
+ string(7, ' ')
+ toString(automaton_stats.number_of_acceptance_sets)
+ '\n' + string(indent, ' ') + "computation time:"
+ string(6, ' ');
if (automaton_stats.buchi_generation_time != -1.0)
{
changeStreamFormatting(stream, 9, 2, ios::fixed | ios::left);
estream << automaton_stats.buchi_generation_time;
restoreStreamFormatting(stream);
estream << " seconds (user time)";
}
else
estream << "N/A";
}
estream << '\n';
}
estream << '\n';
estream.flush();
}
@ -110,7 +185,7 @@ void printProductAutomatonStats
* Arguments: stream -- A reference to the output stream to which the
* information should be written.
* indent -- Number of spaces to leave on the left of the
* output.
* output in verbosity modes >= 3.
* algorithm -- Identifier of the algorithm used for
* generating the product automaton.
* result_id -- Selects between the automata constructed from
@ -125,43 +200,64 @@ void printProductAutomatonStats
const AutomatonStats& automaton_stats =
test_results[algorithm].automaton_stats[result_id];
estream << string(indent, ' ');
if (!automaton_stats.productAutomatonComputed())
estream << "not computed";
if (configuration.global_options.verbosity <= 2)
{
if (!automaton_stats.productAutomatonComputed())
estream << " N/A N/A";
else
{
changeStreamFormatting(stream, 11, 0, ios::right);
estream << automaton_stats.number_of_product_states;
restoreStreamFormatting(stream);
estream << ' ';
changeStreamFormatting(stream, 11, 0, ios::right);
estream << automaton_stats.number_of_product_transitions;
restoreStreamFormatting(stream);
}
estream << ' ';
}
else
{
estream << "number of states:" + string(6, ' ');
estream << string(indent, ' ');
changeStreamFormatting(stream, 9, 0, ios::left);
estream << automaton_stats.number_of_product_states;
restoreStreamFormatting(stream);
estream << " [";
if (automaton_stats.number_of_product_states != 0)
if (!automaton_stats.productAutomatonComputed())
estream << "not computed";
else
{
changeStreamFormatting(stream, 0, 2, ios::fixed);
estream << static_cast<double>
(automaton_stats.number_of_product_states)
/ static_cast<double>(automaton_stats.number_of_buchi_states)
/ static_cast<double>(round_info.statespace->size())
* 100.0;
estream << "number of states:" + string(6, ' ');
changeStreamFormatting(stream, 9, 0, ios::left);
estream << automaton_stats.number_of_product_states;
restoreStreamFormatting(stream);
estream << "% of worst case ("
<< automaton_stats.number_of_buchi_states
* round_info.statespace->size()
<< ')';
}
else
estream << "empty automaton";
estream << " [";
estream << "]\n" + string(indent, ' ') + "number of transitions: "
+ toString(automaton_stats.number_of_product_transitions);
if (automaton_stats.number_of_product_states != 0)
{
changeStreamFormatting(stream, 0, 2, ios::fixed);
estream << static_cast<double>
(automaton_stats.number_of_product_states)
/ static_cast<double>
(automaton_stats.number_of_buchi_states)
/ static_cast<double>(round_info.statespace->size())
* 100.0;
restoreStreamFormatting(stream);
estream << "% of worst case ("
<< automaton_stats.number_of_buchi_states
* round_info.statespace->size()
<< ')';
}
else
estream << "empty automaton";
estream << "]\n" + string(indent, ' ') + "number of transitions: "
+ toString(automaton_stats.number_of_product_transitions);
}
estream << '\n';
}
estream << '\n';
estream.flush();
}
@ -181,7 +277,7 @@ void printAcceptanceCycleStats
* Arguments: stream -- A reference to the output stream to which the
* information should be written.
* indent -- Number of spaces to leave on the left of the
* output.
* output in verbosity mode >= 3.
* algorithm -- Identifier of the algorithm used for
* computing the Büchi automaton whose accepting
* cycles are to be considered.
@ -197,41 +293,57 @@ void printAcceptanceCycleStats
const AutomatonStats& automaton_stats =
test_results[algorithm].automaton_stats[result_id];
estream << string(indent, ' ');
if (!automaton_stats.emptiness_check_performed)
estream << "not computed";
else if (configuration.global_options.product_mode == Configuration::LOCAL)
if (configuration.global_options.verbosity <= 2)
{
estream << string("cycle ");
if (automaton_stats.emptiness_check_result[0])
estream << "reachable ";
if (!automaton_stats.emptiness_check_performed)
estream << " N/A";
else
estream << "not reachable";
estream << " (from the initial state)";
{
changeStreamFormatting(stream, 6, 0, ios::right);
estream << automaton_stats.emptiness_check_result.count();
restoreStreamFormatting(stream);
}
estream << ' ';
}
else
{
estream << "cycle reachable from ";
estream << string(indent, ' ');
changeStreamFormatting(stream, 9, 0, ios::left);
estream << automaton_stats.emptiness_check_result.count();
restoreStreamFormatting(stream);
if (!automaton_stats.emptiness_check_performed)
estream << "not computed";
else if (configuration.global_options.product_mode == Configuration::LOCAL)
{
estream << string("cycle ");
estream << " states\n" + string(indent, ' ')
+ "not reachable from ";
if (automaton_stats.emptiness_check_result[0])
estream << "reachable ";
else
estream << "not reachable";
changeStreamFormatting(stream, 9, 0, ios::left);
estream << (round_info.real_emptiness_check_size
- automaton_stats.emptiness_check_result.count());
restoreStreamFormatting(stream);
estream << " (from the initial state)";
}
else
{
estream << "cycle reachable from ";
estream << " states";
changeStreamFormatting(stream, 9, 0, ios::left);
estream << automaton_stats.emptiness_check_result.count();
restoreStreamFormatting(stream);
estream << " states\n" + string(indent, ' ')
+ "not reachable from ";
changeStreamFormatting(stream, 9, 0, ios::left);
estream << (round_info.real_emptiness_check_size
- automaton_stats.emptiness_check_result.count());
restoreStreamFormatting(stream);
estream << " states";
}
estream << '\n';
}
estream << '\n';
estream.flush();
}
@ -249,7 +361,7 @@ void printConsistencyCheckStats
* Arguments: stream -- A reference to an output stream to which the
* information should be written.
* indent -- Number of spaces to leave on the left of the
* output.
* output in verbosity mode >= 3.
* algorithm -- Identifier of the algorithm whose consistency
* check result should be displayed.
*
@ -260,100 +372,114 @@ void printConsistencyCheckStats
Exceptional_ostream estream(&stream, ios::failbit | ios::badbit);
const AlgorithmTestResults& test_result = test_results[algorithm];
estream << string(indent, ' ');
if (configuration.global_options.verbosity <= 2)
{
switch (test_result.consistency_check_result)
{
case -1 :
estream << "NA";
break;
if (test_result.consistency_check_result == -1)
estream << "not performed";
case 0 :
estream << " F";
break;
default:
estream << " P";
break;
}
}
else
{
estream << "result:" + string(18, ' ');
estream << string(indent, ' ');
if (test_result.consistency_check_result == 0)
{
estream << "failed ["
+ toString(test_result.failed_consistency_check_comparisons)
+ " (";
changeStreamFormatting(stream, 0, 2, ios::fixed);
estream << ((test_result.consistency_check_comparisons == 0)
? 0.0
: static_cast<double>
(test_result.failed_consistency_check_comparisons)
/ test_result.consistency_check_comparisons * 100.0);
restoreStreamFormatting(stream);
estream << "%) of "
+ toString(test_result.consistency_check_comparisons)
+ " test cases]";
}
if (test_result.consistency_check_result == -1)
estream << "not performed";
else
estream << "passed";
{
estream << "result:" + string(18, ' ');
if (test_result.consistency_check_result == 0)
{
estream << "failed ["
+ toString(test_result.failed_consistency_check_comparisons)
+ " (";
changeStreamFormatting(stream, 0, 2, ios::fixed);
estream << ((test_result.consistency_check_comparisons == 0)
? 0.0
: static_cast<double>
(test_result.failed_consistency_check_comparisons)
/ test_result.consistency_check_comparisons * 100.0);
restoreStreamFormatting(stream);
estream << "%) of "
+ toString(test_result.consistency_check_comparisons)
+ " test cases]";
}
else
estream << "passed";
}
estream << '\n';
}
estream << '\n';
estream.flush();
}
/* ========================================================================= */
void printCrossComparisonStats
(ostream& stream, int indent,
vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type
algorithm)
(ostream& stream, int indent, const IntervalList& algorithms)
/* ----------------------------------------------------------------------------
*
* Description: Displays information about the model checking result cross-
* comparison check, extracting the information from a vector of
* TestStatistics structures stored in the UserInterface object.
*
* Arguments: stream -- A reference to an output stream to which the
* information should be written.
* indent -- Number of spaces to leave on the left of the
* output.
* algorithm -- If less than the number of algorithms, show
* only the results for the algorithm with this
* identifier.
* Arguments: stream -- A reference to an output stream to which the
* information should be written.
* indent -- Number of spaces to leave on the left of the
* output.
* algorithms -- A reference to a constant IntervalList
* storing the numeric identifiers of the
* algorithms for which the statistics should
* be shown.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
Exceptional_ostream estream(&stream, ios::failbit | ios::badbit);
bool no_errors_to_report = true;
if (algorithm < configuration.algorithms.size()
&& !configuration.algorithms[algorithm].enabled)
{
estream << string(indent, ' ') + "not performed\n\n";
estream.flush();
return;
}
estream << string(indent, ' ') + "result:";
bool no_errors_to_report = true, nothing_to_report = true;
const AutomatonStats* alg_1_pos_results;
const AutomatonStats* alg_1_neg_results;
for (vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type
alg_1 = 0;
alg_1 < test_results.size();
alg_1++)
for (IntervalList::const_iterator alg_1 = algorithms.begin();
alg_1 != algorithms.end();
++alg_1)
{
alg_1_pos_results = &test_results[alg_1].automaton_stats[0];
alg_1_neg_results = &test_results[alg_1].automaton_stats[1];
alg_1_pos_results = &test_results[*alg_1].automaton_stats[0];
alg_1_neg_results = &test_results[*alg_1].automaton_stats[1];
for (vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type
alg_2 = alg_1 + 1;
alg_2 < test_results.size();
alg_2 = 0;
alg_2 < round_info.number_of_translators;
alg_2++)
{
if ((algorithm >= configuration.algorithms.size()
|| alg_1 == algorithm
|| alg_2 == algorithm)
&& configuration.algorithms[alg_1].enabled
if (*alg_1 != alg_2
&& (alg_2 > *alg_1 || !algorithms.covers(alg_2))
&& configuration.algorithms[*alg_1].enabled
&& configuration.algorithms[alg_2].enabled)
{
bool pos_test, neg_test;
if (nothing_to_report)
{
nothing_to_report = false;
estream << string(indent, ' ') + "result:";
}
for (int counter = 0; counter < 2; counter++)
{
if (counter == 0)
@ -381,89 +507,76 @@ void printCrossComparisonStats
else
estream << "-) ";
estream << ' ';
if (alg_1 == round_info.number_of_translators)
estream << "lbtt";
else
estream << configuration.algorithmString(alg_1);
estream << ", ";
if (alg_2 == round_info.number_of_translators)
estream << "lbtt";
else
estream << configuration.algorithmString(alg_2);
estream << " " + configuration.algorithmString(*alg_1) + ", "
+ configuration.algorithmString(alg_2);
}
}
}
}
}
if (no_errors_to_report)
if (nothing_to_report)
estream << string(indent, ' ') + "not performed";
else if (no_errors_to_report)
estream << string(20, ' ') + "no failures detected";
estream << "\n\n";
estream.flush();
}
/* ========================================================================= */
void printBuchiIntersectionCheckStats
(ostream& stream, int indent,
vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type
algorithm)
(ostream& stream, int indent, const IntervalList& algorithms)
/* ----------------------------------------------------------------------------
*
* Description: Displays information about the Büchi automaton intersection
* emptiness check results, extracting the information from a
* TestStatistics structure stored in the UserInterface object.
*
* Arguments: stream -- A reference to an output stream to which the
* information should be written.
* indent -- Number of spaces to leave on the left of the
* output.
* algorithm -- If less than the number of algorithms, show
* only the results for the algorithm with this
* identifier.
* Arguments: stream -- A reference to an output stream to which the
* information should be written.
* indent -- Number of spaces to leave on the left of the
* output.
* algorithms -- A reference to a constant IntervalList
* storing the numeric identifiers of the
* algorithms for which the statistics should
* be shown.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
Exceptional_ostream estream(&stream, ios::failbit | ios::badbit);
bool no_errors_to_report = true;
if (algorithm < round_info.number_of_translators
&& !configuration.algorithms[algorithm].enabled)
{
estream << string(indent, ' ') + "not performed\n\n";
estream.flush();
return;
}
estream << string(indent, ' ') + "result:";
bool no_errors_to_report = true, nothing_to_report = true;
const AutomatonStats* alg_1_pos_results;
const AutomatonStats* alg_1_neg_results;
for (vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type
alg_1 = 0;
alg_1 < round_info.number_of_translators;
alg_1++)
for (IntervalList::const_iterator alg_1 = algorithms.begin();
alg_1 != algorithms.end();
++alg_1)
{
alg_1_pos_results = &test_results[alg_1].automaton_stats[0];
alg_1_neg_results = &test_results[alg_1].automaton_stats[1];
alg_1_pos_results = &test_results[*alg_1].automaton_stats[0];
alg_1_neg_results = &test_results[*alg_1].automaton_stats[1];
for (vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type
alg_2 = alg_1;
alg_2 = 0;
alg_2 < round_info.number_of_translators;
alg_2++)
{
if ((algorithm >= round_info.number_of_translators
|| alg_1 == algorithm
|| alg_2 == algorithm)
&& configuration.algorithms[alg_1].enabled
&& configuration.algorithms[alg_2].enabled)
if (configuration.algorithms[*alg_1].enabled
&& configuration.algorithms[alg_2].enabled
&& (alg_2 >= *alg_1 || !algorithms.covers(alg_2))
&& !configuration.isInternalAlgorithm(*alg_1)
&& !configuration.isInternalAlgorithm(alg_2))
{
bool pos_test, neg_test;
if (nothing_to_report)
{
nothing_to_report = false;
estream << string(indent, ' ') + "result:";
}
for (int counter = -1; counter < 1; counter++)
{
pos_test = (alg_1_pos_results->buchi_intersection_check_stats[alg_2]
@ -478,7 +591,7 @@ void printBuchiIntersectionCheckStats
estream << string(counter == -1 ? "N/A " : "failed") + ' ';
if (alg_1 != alg_2)
if (*alg_1 != alg_2)
{
estream << '(';
if (pos_test)
@ -489,9 +602,9 @@ void printBuchiIntersectionCheckStats
else
estream << " ";
estream << ' ' + configuration.algorithmString(alg_1);
estream << ' ' + configuration.algorithmString(*alg_1);
if (alg_1 != alg_2)
if (*alg_1 != alg_2)
{
estream << ", (";
if (pos_test)
@ -507,10 +620,11 @@ void printBuchiIntersectionCheckStats
}
}
if (no_errors_to_report)
if (nothing_to_report)
estream << string(indent, ' ') + "not performed";
else if (no_errors_to_report)
estream << string(20, ' ') + "no failures detected";
estream << "\n\n";
estream << "\n";
estream.flush();
}
@ -537,30 +651,46 @@ void printAllStats
{
Exceptional_ostream estream(&stream, ios::failbit | ios::badbit);
estream << string(indent, ' ') + configuration.algorithmString(algorithm)
+ '\n';
estream.flush();
if (configuration.global_options.verbosity >= 3)
estream << string(indent, ' ') + configuration.algorithmString(algorithm)
+ '\n';
for (int counter = 0; counter < 2; counter++)
{
estream << string(indent + 2, ' ')
+ (counter == 0 ? "Positive" : "Negated") + " formula:\n"
+ string(indent + 4, ' ') + "Büchi automaton:\n";
if (configuration.global_options.verbosity <= 2)
{
if (counter == 1)
estream << '\n';
estream << string(indent, ' ');
changeStreamFormatting(stream, 2, 0, ios::right);
estream << algorithm << ' ';
restoreStreamFormatting(stream);
estream << (counter == 0 ? '+' : '-') << ' ';
}
else
{
estream << string(indent + 2, ' ')
+ (counter == 0 ? "Positive" : "Negated") + " formula:\n"
+ string(indent + 4, ' ') + "Büchi automaton:\n";
}
printBuchiAutomatonStats(stream, indent + 6, algorithm, counter);
if (configuration.global_options.do_comp_test
|| configuration.global_options.do_cons_test)
{
estream << string(indent + 4, ' ') + "Product automaton:\n";
if (configuration.global_options.verbosity >= 3)
estream << string(indent + 4, ' ') + "Product automaton:\n";
printProductAutomatonStats(stream, indent + 6, algorithm, counter);
estream << string(indent + 4, ' ') + "Accepting cycles:\n";
if (configuration.global_options.verbosity >= 3)
estream << string(indent + 4, ' ') + "Accepting cycles:\n";
printAcceptanceCycleStats(stream, indent + 6, algorithm, counter);
}
}
if (configuration.global_options.do_cons_test)
{
estream << string(indent + 2, ' ') + "Result consistency check:\n";
if (configuration.global_options.verbosity >= 3)
estream << string(indent + 2, ' ') + "Result consistency check:\n";
printConsistencyCheckStats(stream, indent + 4, algorithm);
}
@ -626,10 +756,8 @@ void printCollectiveCrossComparisonStats
break;
default :
if (configuration.global_options.statespace_generation_mode
& Configuration::PATH
&& (algorithm_x == round_info.number_of_translators
|| algorithm_y == round_info.number_of_translators))
if (configuration.isInternalAlgorithm(algorithm_x)
|| configuration.isInternalAlgorithm(algorithm_y))
{
estream << string(21, ' ');
return;
@ -951,8 +1079,11 @@ void printCollectiveStats(ostream& stream, int indent)
algorithm < round_info.number_of_translators;
++algorithm)
{
if (configuration.isInternalAlgorithm(algorithm))
continue;
estream << '\n' + string((i > 0 ? 4 : 2) + indent, ' ')
+ *(configuration.algorithms[algorithm].name) + '\n';
+ configuration.algorithms[algorithm].name + '\n';
switch (i)
{
@ -965,14 +1096,14 @@ void printCollectiveStats(ostream& stream, int indent)
unsigned long int failures_to_compute_automaton;
unsigned long int automaton_count;
unsigned long int number_of_successful_instances;
unsigned long int total_number_of_states;
unsigned long int total_number_of_transitions;
BIGUINT total_number_of_states;
BIGUINT total_number_of_transitions;
const TestStatistics& stats = final_statistics[algorithm];
estream << string(2 + indent, ' ')
+ string(configuration.algorithms[algorithm].name
->length(), '=');
+ string(configuration.algorithms[algorithm].name.
length(), '=');
for (int k = 0; k < 2; k++)
{
@ -1117,7 +1248,7 @@ void printCollectiveStats(ostream& stream, int indent)
if (k == 0)
{
unsigned long int total_number_of_acceptance_sets;
BIGUINT total_number_of_acceptance_sets;
double buchi_generation_time;
estream << '\n' + string(22 + indent, ' ')
@ -1350,7 +1481,7 @@ void printCollectiveStats(ostream& stream, int indent)
if (algorithm_x + i < number_of_algorithms)
{
algorithm_name =
(*(configuration.algorithms[algorithm_x + i].name)).substr(0, 20);
configuration.algorithms[algorithm_x + i].name.substr(0, 20);
estream << "| " + algorithm_name
+ string(21 - algorithm_name.length(), ' ');
}
@ -1360,6 +1491,9 @@ void printCollectiveStats(ostream& stream, int indent)
for (algorithm_y = 0; algorithm_y < number_of_algorithms;
algorithm_y++)
{
if (configuration.isInternalAlgorithm(algorithm_y))
continue;
estream << "\n " + ind + string(26, '-');
for (int i = 0; i < 2; ++i)
@ -1370,7 +1504,7 @@ void printCollectiveStats(ostream& stream, int indent)
estream << '+';
algorithm_name
= (*(configuration.algorithms[algorithm_y].name)).substr(0, 20);
= configuration.algorithms[algorithm_y].name.substr(0, 20);
bool algorithm_name_printed = false;
legend = 1;

19
lbtt/src/StatDisplay.h
View file

@ -42,6 +42,11 @@ extern Configuration configuration;
namespace StatDisplay
{
void printStatTableHeader /* Displays a table */
(ostream& stream, int indent); /* header for test
* statistics.
*/
void printBuchiAutomatonStats /* Displays information */
(ostream& stream, /* about a Büchi */
int indent, /* automaton. */
@ -74,17 +79,15 @@ void printConsistencyCheckStats /* Displays the result */
algorithm);
void printCrossComparisonStats /* Displays information */
(ostream& stream, /* about the model */
int indent, /* checking result */
vector<AlgorithmTestResults, /* cross-comparison */
ALLOC(AlgorithmTestResults) >::size_type /* check. */
algorithm);
(ostream& stream, int indent, /* about the model */
const IntervalList& algorithms); /* checking result */
/* cross-comparison */
/* check. */
void printBuchiIntersectionCheckStats /* Displays the results */
(ostream& stream, int indent, /* of the Büchi automata */
vector<AlgorithmTestResults, /* intersection */
ALLOC(AlgorithmTestResults) >::size_type /* emptiness checks. */
algorithm);
const IntervalList& algorithms); /* intersection */
/* emptiness checks. */
void printAllStats /* A shorthand for */
(ostream& stream, /* showing all the */

430
lbtt/src/StateSpaceProduct.h Normal file
View file

@ -0,0 +1,430 @@
/*
* 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 STATESPACEPRODUCT_H
#define STATESPACEPRODUCT_H
#include <config.h>
#include "BitArray.h"
#include "BuchiAutomaton.h"
#include "EdgeContainer.h"
#include "Graph.h"
#include "StateSpace.h"
using namespace std;
namespace Graph
{
/******************************************************************************
*
* A class with operations for checking the product of a Büchi automaton and
* a state space for emptiness.
*
*****************************************************************************/
class StateSpaceProduct
{
public:
StateSpaceProduct /* Constructor. */
(const Graph<GraphEdgeContainer>& a,
const Graph<GraphEdgeContainer>& s);
/* default copy constructor */
~StateSpaceProduct(); /* Destructor. */
/* default assignment operator */
bool empty() const; /* Tells whether the
* product of a Büchi
* automaton and a state
* space is (trivially)
* empty.
*/
unsigned long int numberOfAcceptanceSets() const; /* Tells the number of
* acceptance sets in a
* Büchi automaton in its
* product with a state
* space.
*/
const BuchiAutomaton::BuchiState& firstComponent /* Mappings between a */
(const Graph<GraphEdgeContainer>::size_type /* product state */
state_id) const; /* identifier and */
const StateSpace::State& secondComponent /* states of the Büchi */
(const Graph<GraphEdgeContainer>::size_type /* automaton and the */
state_id) const; /* state space forming
* the product.
*/
void mergeAcceptanceInformation /* Merges the acceptance */
(const Graph<GraphEdgeContainer>::Node& state, /* sets associated with */
const Graph<GraphEdgeContainer>::Node&, /* a state in the Büchi */
BitArray& acceptance_sets) const; /* automaton into a
* collection of sets.
*/
void mergeAcceptanceInformation /* Merges the acceptance */
(const Graph<GraphEdgeContainer>::Edge& /* sets associated with */
buchi_transition, /* a transition in the */
const Graph<GraphEdgeContainer>::Edge&, /* Büchi automaton into */
BitArray& acceptance_sets) const; /* a collection of sets. */
void validateEdgeIterators /* Ensures that a pair */
(const Graph<GraphEdgeContainer>::Node& /* of transition */
buchi_state, /* iterators points to a */
const Graph<GraphEdgeContainer>::Node& /* transition beginning */
system_state, /* from a given state in */
GraphEdgeContainer::const_iterator& /* the product of a */
buchi_transition, /* Büchi automaton and */
GraphEdgeContainer::const_iterator& /* a state space. */
system_transition) const;
void incrementEdgeIterators /* Updates a pair of */
(const Graph<GraphEdgeContainer>::Node& /* transition iterators */
buchi_state, /* to make them point to */
const Graph<GraphEdgeContainer>::Node& /* the "next" transition */
system_state, /* starting from a given */
GraphEdgeContainer::const_iterator& /* state in the product */
buchi_transition, /* of a Büchi automaton */
GraphEdgeContainer::const_iterator& /* and a state space. */
system_transition) const;
private:
const BuchiAutomaton& buchi_automaton; /* Büchi automaton
* associated with the
* product.
*/
const StateSpace& statespace; /* State space associated
* with the product.
*/
};
/******************************************************************************
*
* Inline function definitions for class StateSpaceProduct.
*
*****************************************************************************/
/* ========================================================================= */
inline StateSpaceProduct::StateSpaceProduct
(const Graph<GraphEdgeContainer>& a, const Graph<GraphEdgeContainer>& s) :
buchi_automaton(static_cast<const BuchiAutomaton&>(a)),
statespace(static_cast<const StateSpace&>(s))
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class StateSpaceProduct. Initializes a new
* object with operations for checking the emptiness of the
* product of a Büchi automaton and a state space.
*
* Arguments: a -- A constant reference to a Graph<GraphEdgeContainer>
* object, assumed to be a BuchiAutomaton.
* s -- A constant reference to a Graph<GraphEdgeContainer>
* object, assumed to be a StateSpace.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline StateSpaceProduct::~StateSpaceProduct()
/* ----------------------------------------------------------------------------
*
* Description: Destructor for class StateSpaceProduct.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline bool StateSpaceProduct::empty() const
/* ----------------------------------------------------------------------------
*
* Description: Tells whether the product of `this->buchi_automaton' and
* `this->statespace' is (trivially) empty.
*
* Arguments: None.
*
* Returns: true iff either the Büchi automaton or the state space has
* no states.
*
* ------------------------------------------------------------------------- */
{
return (buchi_automaton.empty() || statespace.empty());
}
/* ========================================================================= */
inline unsigned long int StateSpaceProduct::numberOfAcceptanceSets() const
/* ----------------------------------------------------------------------------
*
* Description: Tells the number of acceptance sets in the Büchi automaton
* associated with a StateSpaceProduct object.
*
* Arguments: None.
*
* Returns: The number of acceptance sets in the automaton.
*
* ------------------------------------------------------------------------- */
{
return buchi_automaton.numberOfAcceptanceSets();
}
/* ========================================================================= */
inline const BuchiAutomaton::BuchiState& StateSpaceProduct::firstComponent
(const Graph<GraphEdgeContainer>::size_type state_id) const
/* ----------------------------------------------------------------------------
*
* Description: Function for accessing states in the Büchi automaton
* associated with a StateSpaceProduct object.
*
* Argument: state_id -- Identifier of a state in the automaton.
*
* Returns: A constant reference to a state in the automaton.
*
* ------------------------------------------------------------------------- */
{
return buchi_automaton[state_id];
}
/* ========================================================================= */
inline const StateSpace::State& StateSpaceProduct::secondComponent
(const Graph<GraphEdgeContainer>::size_type state_id) const
/* ----------------------------------------------------------------------------
*
* Description: Function for accessing states in the state space associated
* with a StateSpaceProduct object.
*
* Argument: state_id -- Identifier of a state in the state space.
*
* Returns: A constant reference to a state in the state space.
*
* ------------------------------------------------------------------------- */
{
return statespace[state_id];
}
/* ========================================================================= */
inline void StateSpaceProduct::mergeAcceptanceInformation
(const Graph<GraphEdgeContainer>::Node& state,
const Graph<GraphEdgeContainer>::Node&, BitArray& acceptance_sets) const
/* ----------------------------------------------------------------------------
*
* Description: Merges the acceptance sets associated with a state of a Büchi
* automaton into a collection of sets.
*
* Arguments: state -- A constant reference to a state in the
* automaton.
* acceptance_sets -- A reference to a BitArray for storing
* the result. The BitArray should have
* capacity for (at least)
* `this->buchi_automaton
* .numberOfAcceptanceSets()' bits.
* (The second argument is needed to allow the class
* StateSpaceProduct to be used for instantiating the Product
* template; see file Product.h.)
*
* Returns: Nothing. After the operation, `acceptance_sets[i] == true'
* holds if `state.acceptanceSets().test(i) == true' for all
* 0 <= i < `this->buchi_automaton.numberOfAcceptanceSets()'.
*
* ------------------------------------------------------------------------- */
{
acceptance_sets.bitwiseOr
(static_cast<const BuchiAutomaton::BuchiState&>(state).acceptanceSets(),
numberOfAcceptanceSets());
}
/* ========================================================================= */
inline void StateSpaceProduct::mergeAcceptanceInformation
(const Graph<GraphEdgeContainer>::Edge& buchi_transition,
const Graph<GraphEdgeContainer>::Edge&, BitArray& acceptance_sets) const
/* ----------------------------------------------------------------------------
*
* Description: Merges the acceptance sets associated with a transition of a
* Büchi automaton into a collection of sets.
*
* Arguments: transition -- A constant reference to a transition in
* the automaton.
* acceptance_sets -- A reference to a BitArray for storing
* the result. The BitArray should have
* capacity for (at least)
* `this->buchi_automaton
* .numberOfAcceptanceSets()' bits.
* (The second argument is needed to allow the class
* StateSpaceProduct to be used for instantiating the Product
* template; see file Product.h.)
*
* Returns: Nothing. After the operation, `acceptance_sets[i] == true'
* holds if `transition.acceptanceSets().test(i) == true' for
* all
* 0 <= i < `this->buchi_automaton.numberOfAcceptanceSets()'.
*
* ------------------------------------------------------------------------- */
{
acceptance_sets.bitwiseOr
(static_cast<const BuchiAutomaton::BuchiTransition&>(buchi_transition)
.acceptanceSets(),
numberOfAcceptanceSets());
}
/* ========================================================================= */
inline void StateSpaceProduct::validateEdgeIterators
(const Graph<GraphEdgeContainer>::Node& buchi_state,
const Graph<GraphEdgeContainer>::Node& system_state,
GraphEdgeContainer::const_iterator& buchi_transition,
GraphEdgeContainer::const_iterator& system_transition) const
/* ----------------------------------------------------------------------------
*
* Description: Checks whether a pair of transition iterators corresponds to
* a transition beginning from a state in the product of a Büchi
* automaton and a state space; if this is not the case, makes
* the iterators point to a valid transition beginning from the
* product state (or to the "end" of the collection of
* transitions beginning from the product state if no valid
* transition can be found by incrementing the iterators).
*
* Arguments: buchi_state, -- These variables determine the state
* system_state, in the product; `buchi_state' and
* `system_state' should be references to
* states in `this->buchi_automaton' and
* `this->statespace', respectively.
* buchi_transition, -- References to the transition
* system_transition iterators. It is assumed that
* `buchi_transition' and
* `system_transition' initially point to
* two transitions starting from
* `buchi_state' and `system_state',
* respectively.
*
* Returns: Nothing. Upon return, `buchi_transition' and
* `system_transition' will either equal
* `buchi_state.edges().end()' and `system_state.edges().end()',
* respectively, or they will point to a pair of transitions
* beginning from `buchi_state' and `system_state' such that
* this pair of transitions corresponds to a transition starting
* from the product state determined by `buchi_state' and
* `system_state'.
*
* ------------------------------------------------------------------------- */
{
const GraphEdgeContainer& buchi_transitions = buchi_state.edges();
const GraphEdgeContainer& system_transitions = system_state.edges();
if (buchi_transition == buchi_transitions.end())
{
system_transition = system_transitions.end();
return;
}
if (system_transition == system_transitions.end())
{
buchi_transition = buchi_transitions.end();
return;
}
while (!static_cast<const BuchiAutomaton::BuchiTransition*>
(*buchi_transition)->enabled
(static_cast<const StateSpace::State&>(system_state)
.positiveAtoms(),
statespace.numberOfPropositions()))
{
++buchi_transition;
if (buchi_transition == buchi_transitions.end())
{
system_transition = system_transitions.end();
return;
}
}
system_transition = system_transitions.begin();
}
/* ========================================================================= */
inline void StateSpaceProduct::incrementEdgeIterators
(const Graph<GraphEdgeContainer>::Node& buchi_state,
const Graph<GraphEdgeContainer>::Node& system_state,
GraphEdgeContainer::const_iterator& buchi_transition,
GraphEdgeContainer::const_iterator& system_transition) const
/* ----------------------------------------------------------------------------
*
* Description: Increments a pair of transition iterators to point to the
* "next" transition beginning from a state in the product of a
* Büchi automaton and a state space. If no "next" transition
* exists, makes the iterators point to the "end" of the
* collection of transitions beginning from the product state.
*
* Arguments: buchi_state, -- These variables determine the state
* system_state, in the product; `buchi_state' and
* `system_state' should be references to
* states in `this->buchi_automaton' and
* `this->statespace', respectively.
* buchi_transition, -- References to the transition
* system_transition iterators. It is assumed that
* `buchi_transition' and
* `system_transition' initially point to
* two transitions starting from
* `buchi_state' and `system_state',
* respectively.
*
* Returns: Nothing. Upon return, `buchi_transition' and
* `system_transition' will either equal
* `buchi_state.edges().end()' and `system_state.edges().end()',
* respectively, or they will point to a pair of transitions
* beginning from `buchi_state' and `system_state' such that
* this pair of transitions corresponds to a transition starting
* from the product state determined by `buchi_state' and
* `system_state'.
*
* ------------------------------------------------------------------------- */
{
const GraphEdgeContainer& buchi_transitions = buchi_state.edges();
const GraphEdgeContainer& system_transitions = system_state.edges();
++system_transition;
if (system_transition == system_transitions.end())
{
do
{
++buchi_transition;
if (buchi_transition == buchi_transitions.end())
return;
}
while (!static_cast<const BuchiAutomaton::BuchiTransition*>
(*buchi_transition)->enabled
(static_cast<const StateSpace::State&>(system_state)
.positiveAtoms(),
statespace.numberOfPropositions()));
system_transition = system_transitions.begin();
}
}
}
#endif /* !STATESPACEPRODUCT_H */

513
lbtt/src/StringUtil.cc
View file

@ -18,6 +18,8 @@
*/
#include <config.h>
#include <cctype>
#include <climits>
#include <cstdlib>
#include "StringUtil.h"
@ -100,6 +102,211 @@ void sliceString
while (last_non_slicechar_pos != s.npos && last_slicechar_pos != s.npos);
}
/* ========================================================================= */
string toLowerCase(const string& s)
/* ----------------------------------------------------------------------------
*
* Description: Converts a string to lower case.
*
* Argument: s -- String to process.
*
* Returns: The string in lower case.
*
* ------------------------------------------------------------------------- */
{
string result;
for (string::size_type pos = 0; pos < s.length(); ++pos)
result += tolower(s[pos]);
return result;
}
/* ========================================================================= */
bool interpretSpecialCharacters(const char c, bool& escape, char& quotechar)
/* ----------------------------------------------------------------------------
*
* Description: Updates the values of `escape' and `quotechar' based on their
* original values and the value of `c'. Used for scanning
* through a string possibly containing quotes and escaped
* characters.
*
* Arguments: c -- A character.
* escape -- A truth value telling whether `c' was escaped.
* quotechar -- 0 == `c' was read outside of quotes.
* `'' == `c' was read inside single quotes.
* `"' == `c' was read inside double quotes.
*
* Returns: True if `c' had a special meaning (for example, if it was a
* begin/end quote character) in the state determined by the
* original values of `escape' and `quotechar'.
*
* ------------------------------------------------------------------------- */
{
if (escape)
{
escape = false;
return false;
}
switch (c)
{
case '\\' :
if (quotechar != '\'')
{
escape = true;
return true;
}
break;
case '\'' : case '"' :
if (quotechar == 0)
{
quotechar = c;
return true;
}
else if (c == quotechar)
{
quotechar = 0;
return true;
}
break;
default :
break;
}
return false;
}
/* ========================================================================= */
string unquoteString(const string& s)
/* ----------------------------------------------------------------------------
*
* Description: Removes (unescaped) single and double quotes and escape
* characters from a string.
*
* Argument: s -- String to process.
*
* Returns: A string with the quotes and escape characters removed.
*
* ------------------------------------------------------------------------- */
{
string result;
char quotechar = 0;
bool escape = false;
for (string::size_type pos = 0; pos < s.size(); ++pos)
{
if (!interpretSpecialCharacters(s[pos], escape, quotechar))
result += s[pos];
}
return result;
}
/* ========================================================================= */
string::size_type findInQuotedString
(const string& s, const string& chars, QuoteMode type)
/* ----------------------------------------------------------------------------
*
* Description: Finds a character in a string (respecting quotes).
*
* Arguments: s -- String to process.
* chars -- A sting of characters to be searched in `s'.
* type -- The extent of the search.
* GLOBAL - Apply the search to the entire
* string.
* INSIDE_QUOTES - Restrict the search to
* unescaped characters between
* quotes.
* OUTSIDE_QUOTES - Restrict the search to
* unescaped characters outside
* quotes.
*
* Returns: If `s' contains one of the characters in `chars' in a part
* of the string that matches `type', the position of the
* character in `s', and string::npos otherwise.
*
* ------------------------------------------------------------------------- */
{
char quotechar = 0;
bool escape = false;
for (string::size_type pos = 0; pos < s.size(); ++pos)
{
if ((type == GLOBAL || (!escape &&
((type == INSIDE_QUOTES && quotechar != 0)
|| (type == OUTSIDE_QUOTES && quotechar == 0))))
&& chars.find_first_of(s[pos]) != string::npos)
return pos;
interpretSpecialCharacters(s[pos], escape, quotechar);
}
return string::npos;
}
/* ========================================================================= */
string substituteInQuotedString
(const string& s, const string& chars, const string& substitutions,
QuoteMode type)
/* ----------------------------------------------------------------------------
*
* Description: Substitutes characters in a string with other characters.
*
* Arguments: s -- String to process.
* chars -- A string of characters, each of which
* should be substituted in `s' with the
* character at the corresponding
* position of the string `substitutions'.
* substitutions -- Characters to substitute. The length of
* this string should equal the length of
* `chars'.
* type -- The extent of substitution.
* GLOBAL - Apply the substitutions
* globally (the default).
* INSIDE_QUOTES - Apply the substitutions
* to unescaped characters
* only inside quotes that
* have not been escaped
* with a backslash.
* OUTSIDE_QUOTES - Apply the substitutions
* to unescaped characters
* only outside quotes
* that have not been
* escaped with a
* backslash.
* It is not recommended to substitute the
* special characters ', " and \ with other
* characters if they have special meaning in
* `s'.
*
* Returns: A string with the substitutions.
*
* ------------------------------------------------------------------------- */
{
string result;
char quotechar = 0;
bool escape = false;
for (string::size_type pos = 0; pos < s.size(); ++pos)
{
char c = s[pos];
if (type == GLOBAL || (!escape &&
((type == INSIDE_QUOTES && quotechar != 0)
|| (type == OUTSIDE_QUOTES && quotechar == 0))))
{
string::size_type subst_pos = chars.find_first_of(c);
if (subst_pos != string::npos)
c = substitutions[subst_pos];
}
result += c;
interpretSpecialCharacters(s[pos], escape, quotechar);
}
return result;
}
/* ========================================================================= */
unsigned long int parseNumber(const string& number_string)
/* ----------------------------------------------------------------------------
@ -115,9 +322,11 @@ unsigned long int parseNumber(const string& number_string)
* ------------------------------------------------------------------------- */
{
char* endptr;
unsigned long int number = strtoul(number_string.c_str(), &endptr, 10);
if (*endptr != '\0')
if (*endptr != '\0' || number_string.empty()
|| number_string.find_first_of("-") != string::npos)
throw NotANumberException("expected a nonnegative integer, got `"
+ number_string + "'");
@ -125,98 +334,254 @@ unsigned long int parseNumber(const string& number_string)
}
/* ========================================================================= */
void parseInterval
(const string& token,
set<unsigned long int, less<unsigned long int>, ALLOC(unsigned long int) >&
number_set,
unsigned long int min, unsigned long int max)
int parseInterval
(const string& token, unsigned long int& min, unsigned long int& max)
/* ----------------------------------------------------------------------------
*
* Description: Parses a string for a list of number intervals, storing all
* the numbers into a set.
* Description: Reads the lower and upper bound from an "interval string"
* into two unsigned long integer variables.
*
* Arguments: token -- A reference to a constant string containing
* the list of intervals. A legal list of
* intervals has the following syntax:
* Arguments: token -- A reference to a constant "interval string" of
* the format
* <interval string>
* ::= "*" // 0
* | <ulong> // 1
* | <sep><ulong> // 2
* | <ulong><sep> // 3
* | <ulong><sep><ulong> // 4
* where <ulong> is an unsigned long integer (not
* containing a minus sign), and <sep> is either
* "-" or "...". The meaning of the various cases
* is as follows:
* 0 All integers between 0 and ULONG_MAX.
* 1 A point interval consisting of a single
* value.
* 2 An interval from 0 to a given upper
* bound.
* 3 An interval from a given lower bound to
* ULONG_MAX.
* 4 A bounded interval.
* min, max -- References to two unsigned long integers for
* storing the lower and upper bound of the
* interval.
*
* <interval_list>
* ::= <number>
* | '*' // all numbers in the
* // interval
* // [min, max]
* | '-'<number> // all numbers in the
* // interval
* // [min, number]
* | <number>'-' // all numbers in the
* // interval
* // [number, max]
* | <number>'-'<number>
* | <interval_list>','<interval_list>
*
* number_set -- A reference to a set of unsigned long
* integers for storing the result.
* min -- Minimum bound for the numbers.
* max -- Maximum bound for the numbers.
*
* Note: `min' and `max' are only used to determine the limits
* for only partially defined intervals. The check that
* the explicitly specified values in the interval list
* are within these bounds is left to the caller when
* examining the result set.
*
* Returns: Nothing.
* Returns: A value telling the type of the specified interval, which is
* a bitwise or of the values LEFT_BOUNDED and RIGHT_BOUNDED
* depending on which bounds were given explicitly for the
* interval. (The lower and upper bounds of the interval itself
* are stored in the variables `min' and `max', respectively.)
* The function will throw a NotANumberException if the
* interval string is of an invalid format.
*
* ------------------------------------------------------------------------- */
{
vector<string, ALLOC(string) > intervals;
unsigned long int tmp_min = 0;
unsigned long int tmp_max = ULONG_MAX;
int interval_type = UNBOUNDED;
sliceString(token, ",", intervals);
string::size_type dash_pos;
if (token != "*")
{
string::size_type pos(token.find_first_of("-"));
if (pos == string::npos)
pos = token.find("...");
string value(token.substr(0, pos));
number_set.clear();
if (!value.empty())
{
tmp_min = parseNumber(value);
if (pos == string::npos)
tmp_max = tmp_min;
interval_type |= LEFT_BOUNDED;
}
if (pos != string::npos)
value = token.substr(pos + (token[pos] == '-' ? 1 : 3));
if (!value.empty())
{
tmp_max = parseNumber(value);
interval_type |= RIGHT_BOUNDED;
}
else if (!(interval_type & LEFT_BOUNDED))
throw NotANumberException("invalid format for interval");
}
min = tmp_min;
max = tmp_max;
return interval_type;
}
/* ========================================================================= */
void parseIntervalList
(const string& token, IntervalList& intervals, unsigned long int min,
unsigned long int max, vector<string, ALLOC(string) >* extra_tokens)
/* ----------------------------------------------------------------------------
*
* Description: Parses a string of number intervals into an IntervalList.
*
* Arguments: token -- A reference to a constant comma-separated
* list of interval strings (see documentation
* for the parseInterval function).
* intervals -- A reference to an IntervalList to be used
* for storing the result.
* min -- Absolute lower bound for the numbers.
* Numbers lower than this bound will not be
* stored in the result set.
* max -- Absolute upper bound for the numbers.
* Numbers greater than this bound will not be
* stored in the result set.
* extra_tokens -- If not 0, all tokens that cannot be
* recognized as valid interval strings will
* be stored in the vector of strings to which
* this variable points. Otherwise the
* function will throw a NotANumberException.
*
* Returns: Nothing. Throws an IntervalRangeException if any of the
* intervals in the list does not fit in the closed range
* [min,max].
*
* ------------------------------------------------------------------------- */
{
vector<string, ALLOC(string) > interval_strings;
int interval_type;
intervals.clear();
sliceString(token, ",", interval_strings);
for (vector<string, ALLOC(string) >::const_iterator
interval = intervals.begin();
interval != intervals.end();
++interval)
i = interval_strings.begin();
i != interval_strings.end();
++i)
{
if (*interval == "*")
unsigned long int i_start, i_end;
try
{
for (unsigned long int i = min; i <= max; i++)
number_set.insert(i);
break;
interval_type = parseInterval(*i, i_start, i_end);
}
dash_pos = (*interval).find_first_of("-");
if (dash_pos == (*interval).npos)
number_set.insert(parseNumber(*interval));
else
catch (const NotANumberException&)
{
if (dash_pos == 0)
if (extra_tokens != 0)
{
unsigned long int number = parseNumber((*interval).substr(1));
for (unsigned long int i = min; i <= number; i++)
number_set.insert(i);
}
else if (dash_pos == (*interval).length() - 1)
{
unsigned long int number =
parseNumber((*interval).substr(0, (*interval).length() - 1));
for (unsigned long int i = number; i <= max; i++)
number_set.insert(i);
extra_tokens->push_back(*i);
continue;
}
else
{
unsigned long int min_bound =
parseNumber((*interval).substr(0, dash_pos));
unsigned long int max_bound =
parseNumber((*interval).substr(dash_pos + 1));
for (unsigned long int i = min_bound; i <= max_bound; i++)
number_set.insert(i);
}
throw;
}
if (interval_type & LEFT_BOUNDED)
{
if (i_start < min || i_start > max)
throw IntervalRangeException(i_start);
}
else if (i_start < min)
i_start = min;
if (interval_type & RIGHT_BOUNDED)
{
if (i_end < min || i_end > max)
throw IntervalRangeException(i_end);
}
else if (i_end > max)
i_end = max;
intervals.merge(i_start, i_end);
}
}
/* ========================================================================= */
void parseTime
(const string& time_string, unsigned long int& hours,
unsigned long int& minutes, unsigned long int& seconds)
/* ----------------------------------------------------------------------------
*
* Description: Parses a "time string", i.e., a string of the form
* ([0-9]+"h")([0-9]+"min")?([0-9]+"s")?
* | ([0-9]+"min")([0-9]+"s")?
* | ([0-9]+"s")
* (where 'h', 'min' and 's' correspond to hours, minutes and
* seconds, respectively) and stores the numbers into three
* unsigned long integers. The case of the unit symbols is not
* relevant.
*
* Arguments: time_string -- String to process.
* hours -- A reference to an unsigned long integer for
* storing the number of hours.
* minutes -- A reference to an unsigned long integer for
* storing the number of minutes.
* seconds -- A reference to an unsigned long integer for
* storing the number of seconds.
*
* Time components left unspecified in `time_string' will get
* the value 0.
*
* Returns: Nothing. Throws an Exception if the given string is not of
* the correct format.
*
* ------------------------------------------------------------------------- */
{
bool hours_present = false, minutes_present = false, seconds_present = false;
hours = minutes = seconds = 0;
if (time_string.empty())
throw Exception("invalid time format");
string::size_type pos1 = 0;
string s;
while (pos1 < time_string.length())
{
string::size_type pos2 = time_string.find_first_not_of("0123456789", pos1);
if (pos2 >= time_string.length())
throw Exception("invalid time format");
unsigned long int val;
try
{
val = parseNumber(time_string.substr(pos1, pos2 - pos1));
}
catch (const NotANumberException&)
{
throw Exception("invalid time format");
}
switch (tolower(time_string[pos2]))
{
case 'h' :
if (hours_present || minutes_present || seconds_present)
throw Exception("invalid time format");
hours_present = true;
hours = val;
break;
case 'm' :
if (minutes_present
|| seconds_present
|| pos2 + 2 >= time_string.length()
|| tolower(time_string[pos2 + 1]) != 'i'
|| tolower(time_string[pos2 + 2]) != 'n')
throw Exception("invalid time format");
minutes_present = true;
minutes = val;
pos2 += 2;
break;
case 's' :
if (seconds_present)
throw Exception("invalid time format");
seconds_present = true;
seconds = val;
break;
default : /* 's' */
throw Exception("invalid time format");
break;
}
pos1 = pos2 + 1;
}
}

169
lbtt/src/StringUtil.h
View file

@ -31,6 +31,7 @@
#include <vector>
#include "LbttAlloc.h"
#include "Exception.h"
#include "IntervalList.h"
using namespace std;
@ -62,17 +63,65 @@ void sliceString /* Breaks a string into */
* separators.
*/
string toLowerCase(const string& s); /* Converts a string to
* lower case.
*/
string unquoteString(const string& s); /* Removes unescaped quotes
* from a string and
* interprets escaped
* characters.
*/
enum QuoteMode {GLOBAL, INSIDE_QUOTES, /* Enumeration type used */
OUTSIDE_QUOTES}; /* for controlling the
* behavior of the
* substitute function.
*/
string::size_type findInQuotedString /* Finds a character in */
(const string& s, const string& chars, /* a string (respecting */
QuoteMode type = GLOBAL); /* quotes). */
string substituteInQuotedString /* Replaces characters */
(const string& s, const string& chars, /* in a string with */
const string& substitutions, /* other characters. */
QuoteMode type = GLOBAL);
unsigned long int parseNumber /* Converts a string to */
(const string& number_string); /* an unsigned long
* integer.
*/
void parseInterval /* Converts a string of */
(const string& token, /* number intervals to */
set<unsigned long int, less<unsigned long int>, /* the corresponding set */
ALLOC(unsigned long int) >& number_set, /* of unsigned long */
unsigned long int min, /* integers. */
unsigned long int max);
enum IntervalStringType {UNBOUNDED = 0, /* Type for an interval */
LEFT_BOUNDED = 1, /* string (see the */
RIGHT_BOUNDED = 2}; /* documentation of
* the parseInterval
* function in
* StringUtil.cc).
*/
int parseInterval /* Reads the lower and */
(const string& token, /* upper bounds from a */
unsigned long int& min, /* "number interval */
unsigned long int& max); /* string" into two
* unsigned long integer
* variables.
*/
void parseIntervalList /* Converts a list of */
(const string& token, /* number intervals to */
IntervalList& intervals, /* the set of unsigned */
unsigned long int min, /* long integers */
unsigned long int max, /* corresponding to the */
vector<string, ALLOC(string) >* extra_tokens /* union of the */
= 0); /* intervals. */
void parseTime /* Parses a time string. */
(const string& time_string,
unsigned long int& hours,
unsigned long int& minutes,
unsigned long int& seconds);
@ -133,6 +182,38 @@ public:
/******************************************************************************
*
* A class for reporting "out of range" errors for numbers when parsing
* intervals.
*
*****************************************************************************/
class IntervalRangeException : public Exception
{
public:
IntervalRangeException /* Constructor. */
(const unsigned long int number,
const string& message = "number out of range");
/* default copy constructor */
~IntervalRangeException() throw(); /* Destructor. */
IntervalRangeException& operator= /* Assignment operator. */
(const IntervalRangeException& e);
unsigned long int getNumber() const; /* Returns the number
* associated with the
* exception object.
*/
private:
const unsigned long int invalid_number;
};
/******************************************************************************
*
* Inline function definitions for class NotANumberException.
@ -189,6 +270,82 @@ inline NotANumberException& NotANumberException::operator=
return *this;
}
/******************************************************************************
*
* Inline function definitions for class IntervalRangeException.
*
*****************************************************************************/
/* ========================================================================= */
inline IntervalRangeException::IntervalRangeException
(const unsigned long int number, const string& message) :
Exception(message), invalid_number(number)
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class IntervalRangeException. Creates an
* exception object.
*
* Arguments: number -- A constant unsigned long integer specifying a
* number that does not fit in an interval.
* message -- A reference to a constant string containing an
* error message.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline IntervalRangeException::~IntervalRangeException() throw()
/* ----------------------------------------------------------------------------
*
* Description: Destructor for class IntervalRangeException.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline unsigned long int IntervalRangeException::getNumber() const
/* ----------------------------------------------------------------------------
*
* Description: Returns the number associated with the IntervalRangeException
* object.
*
* Arguments: None.
*
* Returns: The number associated with the object.
*
* ------------------------------------------------------------------------- */
{
return invalid_number;
}
/* ========================================================================= */
inline IntervalRangeException& IntervalRangeException::operator=
(const IntervalRangeException& e)
/* ----------------------------------------------------------------------------
*
* Description: Assignment operator for class IntervalRangeException.
* Copies the contents of an exception object to another.
*
* Arguments: e -- A reference to a constant IntervalRangeException.
*
* Returns: A reference to the object assigned to.
*
* ------------------------------------------------------------------------- */
{
Exception::operator=(e);
return *this;
}
}
#endif /* !STRINGUTIL_H */

125
lbtt/src/TempFsysName.cc Normal file
View file

@ -0,0 +1,125 @@
/*
* Copyright (C) 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.
*/
#include <config.h>
#include <cstdio>
#include <cstdlib>
#include <cstring>
#include <sys/stat.h>
#include <sys/types.h>
#ifdef HAVE_FCNTL_H
#include <fcntl.h>
#endif /* HAVE_FCNTL_H */
#include <string>
#include "Exception.h"
#include "StringUtil.h"
#include "TempFsysName.h"
/******************************************************************************
*
* Number of generated temporary names.
*
*****************************************************************************/
unsigned long int TempFsysName::number_of_allocated_names = 0;
/******************************************************************************
*
* Function definitions for class TempFsysName.
*
*****************************************************************************/
/* ========================================================================= */
const char* TempFsysName::allocate
(const char* prefix, const NameType t, const bool literal)
/* ----------------------------------------------------------------------------
*
* Description: Associates a TempFsysName object with a temporary name. (As
* a side effect, the function actually creates an empty
* temporary file or a directory to reserve the name in the file
* system. The file or directory should never be removed
* explicitly; it is removed automatically when the TempFsysName
* object is destroyed or another call is made to
* `this->allocate'.)
*
* Arguments: prefix -- Pointer to a C-style string containing a prefix
* for the temporary name (empty by default). If
* `literal == true', `prefix' (if nonempty) is
* assumed to contain the full path for the
* temporary file or directory; otherwise the
* function will reserve a temporary name in the
* `P_tmpdir' directory. This name will consist
* of the value of `prefix' (if nonempty), followed
* by the current value of
* `TempFsysName::number_of_allocated_names' and
* the current process id, separated by dots.
* t -- Determines the type of the name (file or a
* directory).
* literal -- See above.
*
* Returns: A pointer to a constant C-style string containing the
* temporary name. The function throws an IOException if the
* name allocation or the file or directory creation fails.
*
* ------------------------------------------------------------------------- */
{
releaseName();
using ::StringUtil::toString;
string tempname;
try
{
if (!literal || strlen(prefix) == 0)
{
tempname = toString(P_tmpdir) + "/";
if (strlen(prefix))
tempname += string(prefix) + ".";
tempname += toString(number_of_allocated_names) + "."
+ toString(getpid());
++number_of_allocated_names;
}
else
tempname = prefix;
name = new char[tempname.length() + 1];
strcpy(name, tempname.c_str());
}
catch (const bad_alloc&)
{
name = 0;
throw IOException
("unable to allocate a temporary name in the file system");
}
type = t;
if (t == FILE)
{
int fd = open(name, O_RDWR | O_CREAT | O_EXCL, S_IREAD | S_IWRITE);
if (fd == -1)
throw IOException("unable to create a temporary file");
close(fd);
}
else if (mkdir(name, S_IRWXU) == -1)
throw IOException("unable to create a temporary directory");
return name;
}

157
lbtt/src/TempFsysName.h Normal file
View file

@ -0,0 +1,157 @@
/*
* Copyright (C) 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 TEMPFSYSNAME_H
#define TEMPFSYSNAME_H
#include <config.h>
#include <cstdio>
#ifdef HAVE_UNISTD_H
#include <unistd.h>
#endif /* HAVE_UNISTD_H */
/******************************************************************************
*
* A class for temporary file system names.
*
*****************************************************************************/
class TempFsysName
{
public:
TempFsysName(); /* Constructor. */
~TempFsysName(); /* Destructor. */
enum NameType { FILE, DIRECTORY }; /* Types of temporary
* file system names.
*/
const char* allocate /* Allocates a name */
(const char* prefix = "", /* in the file system. */
const NameType t = FILE,
const bool literal = false);
const char* get() const; /* Tells the name. */
private:
TempFsysName(const TempFsysName&); /* Prevent copying and */
TempFsysName& operator=(const TempFsysName&); /* assignment of
* TempFsysName objects.
*/
void releaseName(); /* Frees a name in the file
* system.
*/
char* name; /* Temporary name. */
NameType type; /* Tells whether the name
* refers to a file or a
* directory.
*/
static unsigned long int /* Counter for the */
number_of_allocated_names; /* number of generated
* temporary names.
*/
};
/******************************************************************************
*
* Inline function definitions for class TempFsysName.
*
*****************************************************************************/
/* ========================================================================= */
inline TempFsysName::TempFsysName() : name(static_cast<char*>(0))
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class TempFsysName.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline TempFsysName::~TempFsysName()
/* ----------------------------------------------------------------------------
*
* Description: Destructor for class TempFsysName.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
releaseName();
}
/* ========================================================================= */
inline const char* TempFsysName::get() const
/* ----------------------------------------------------------------------------
*
* Description: Tells the name associated with the TempFsysName object.
*
* Arguments: None.
*
* Returns: A pointer to a constant C-style string containing the name
* associated with the TempFsysName object. If the TempFsysName
* object has not yet been (successfully) associated with a file
* using TempFsysName::allocate, this pointer has the value 0.
*
* ------------------------------------------------------------------------- */
{
return name;
}
/* ========================================================================= */
inline void TempFsysName::releaseName()
/* ----------------------------------------------------------------------------
*
* Description: Deallocates the memory reserved for `this->name' and frees
* the name also in the file system by removing the file or
* directory associated with the object. If the name
* is associated with a directory, the directory is assumed to
* be empty.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
if (name == static_cast<char*>(0))
return;
if (type == FILE)
remove(name);
else
rmdir(name);
delete[] name;
name = 0;
}
#endif /* !TEMPFSYSNAME_H */

1082
lbtt/src/TestOperations.cc
View file

File diff suppressed because it is too large Load diff

14
lbtt/src/TestOperations.h
View file

@ -29,6 +29,7 @@
#include "Configuration.h"
#include "Exception.h"
#include "StateSpace.h"
#include "TestStatistics.h"
using namespace std;
@ -53,7 +54,11 @@ void openFile /* Opens a file for */
(const char* filename, ofstream& stream, /* writing. */
ios::openmode mode, int indent = 0);
void removeFile /* Removes a file. */
void openFile /* Opens a file for */
(const char* filename, int& fd, int flags, /* input/output using */
int indent = 0); /* file descriptors. */
void truncateFile /* Truncates a file. */
(const char* filename, int indent = 0);
void printFileContents /* Displays the contents */
@ -97,13 +102,6 @@ void generateBuchiAutomaton /* Generates a B
* for the conversion.
*/
void generateProductAutomaton /* Computes the */
(int f, /* synchronous product */
vector<Configuration::AlgorithmInformation, /* of a Büchi automaton */
ALLOC(Configuration::AlgorithmInformation) > /* and a state space. */
::size_type
algorithm_id);
void performEmptinessCheck /* Performs an emptiness */
(int f, /* check on a product */
vector<Configuration::AlgorithmInformation, /* automaton. */

33
lbtt/src/TestRoundInfo.h
View file

@ -28,9 +28,9 @@
#include "LbttAlloc.h"
#include "Exception.h"
#include "LtlFormula.h"
#include "ProductAutomaton.h"
#include "PathIterator.h"
#include "StateSpace.h"
#include "TempFsysName.h"
using namespace std;
@ -90,6 +90,10 @@ public:
* current round.
*/
bool all_tests_successful; /* True if no errors have
* occurred during testing.
*/
bool skip; /* True if the current
* round is to be skipped.
*/
@ -122,11 +126,6 @@ public:
* paths as state spaces.
*/
const Graph::ProductAutomaton* product_automaton; /* Pointer to the product
* automaton used in the
* current test round.
*/
unsigned long int real_emptiness_check_size; /* Number of states in the
* state space where the
* emptiness check should
@ -181,10 +180,10 @@ public:
* formula.
*/
char formula_file_name[2][L_tmpnam + 1]; /* Storage space for the */
char automaton_file_name[L_tmpnam + 1]; /* names of several */
char cout_capture_file[L_tmpnam + 1]; /* temporary files. */
char cerr_capture_file[L_tmpnam + 1];
TempFsysName* formula_file_name[2]; /* Names for temporary */
TempFsysName* automaton_file_name; /* files. */
TempFsysName* cout_capture_file;
TempFsysName* cerr_capture_file;
private:
TestRoundInfo(const TestRoundInfo& info); /* Prevent copying and */
@ -206,14 +205,15 @@ private:
inline TestRoundInfo::TestRoundInfo() :
cout(&std::cout, ios::failbit | ios::badbit), number_of_translators(0),
current_round(1), next_round_to_run(1), next_round_to_stop(1),
error_report_round(0), error(false), skip(false), abort(false),
num_generated_statespaces(0), total_statespace_states(0),
total_statespace_transitions(0), num_processed_formulae(0),
fresh_statespace(false), statespace(0), path_iterator(0),
product_automaton(0), real_emptiness_check_size(0),
error_report_round(0), error(false), all_tests_successful(true),
skip(false), abort(false), num_generated_statespaces(0),
total_statespace_states(0), total_statespace_transitions(0),
num_processed_formulae(0), fresh_statespace(false), statespace(0),
path_iterator(0), real_emptiness_check_size(0),
next_round_to_change_statespace(1), next_round_to_change_formula(1),
fresh_formula(false), formulae(4, static_cast<class ::Ltl::LtlFormula*>(0)),
formula_in_file(2, false)
formula_in_file(2, false), automaton_file_name(0), cout_capture_file(0),
cerr_capture_file(0)
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class TestRoundInfo. Creates a new
@ -225,6 +225,7 @@ inline TestRoundInfo::TestRoundInfo() :
*
* ------------------------------------------------------------------------- */
{
formula_file_name[0] = formula_file_name[1] = 0;
}
/* ========================================================================= */

44
lbtt/src/TestStatistics.h
View file

@ -23,16 +23,16 @@
#include <config.h>
#include <utility>
#include <vector>
#include "EdgeContainer.h"
#include "Graph.h"
#include "LbttAlloc.h"
#include "BuchiAutomaton.h"
#include "Configuration.h"
#include "ProductAutomaton.h"
#include "StateSpace.h"
using namespace std;
using Graph::BuchiAutomaton;
using Graph::StateSpace;
using Graph::ProductAutomaton;
/******************************************************************************
*
@ -107,7 +107,7 @@ struct AutomatonStats
* Büchi automaton.
*/
ProductAutomaton::size_type /* Number of stats in a */
::Graph::Graph<GraphEdgeContainer>::size_type /* Number of stats in a */
number_of_product_states; /* product automaton. */
unsigned long int number_of_product_transitions; /* Number of transitions in
@ -270,29 +270,21 @@ struct TestStatistics
* checks performed.
*/
unsigned long int /* Total number of */
total_number_of_buchi_states[2]; /* states in all the
* generated Büchi
* automata.
BIGUINT total_number_of_buchi_states[2]; /* Total number of states
* in all the generated
* Büchi automata.
*/
unsigned long int /* Total number of */
total_number_of_buchi_transitions[2]; /* transitions in all
BIGUINT total_number_of_buchi_transitions[2]; /* Total number of
* transitions in all
* the generated Büchi
* automata.
*/
unsigned long int /* Total number of sets */
total_number_of_acceptance_sets[2]; /* of accepting states
* in all the generated
* Büchi automata.
*/
unsigned long int /* Total number of */
total_number_of_msccs[2]; /* maximal strongly
* connected components
* in the generated
* Büchi automata.
BIGUINT total_number_of_acceptance_sets[2]; /* Total number of sets of
* accepting states in all
* the generated Büchi
* automata.
*/
double total_buchi_generation_time[2]; /* Total time used when
@ -300,14 +292,13 @@ struct TestStatistics
* automata.
*/
unsigned long int /* Total number of */
total_number_of_product_states[2]; /* states in all the
* generated product
* automata.
BIGUINT total_number_of_product_states[2]; /* Total number of states
* in all the generated
* product automata.
*/
unsigned long int /* Total number of */
total_number_of_product_transitions[2]; /* transitions in all the
BIGUINT total_number_of_product_transitions[2]; /* Total number of
* transitions in all the
* generated product
* automata.
*/
@ -556,7 +547,6 @@ inline TestStatistics::TestStatistics
total_number_of_buchi_states[i] = 0;
total_number_of_buchi_transitions[i] = 0;
total_number_of_acceptance_sets[i] = 0;
total_number_of_msccs[i] = 0;
total_number_of_product_states[i] = 0;
total_number_of_product_transitions[i] = 0;
total_buchi_generation_time[i] = 0.0;

146
lbtt/src/UserCommandReader.cc
View file

@ -28,7 +28,6 @@
#include <strstream>
#endif /* HAVE_SSTREAM */
#include "DispUtil.h"
#include "ProductAutomaton.h"
#include "SharedTestData.h"
#include "StatDisplay.h"
#include "StringUtil.h"
@ -118,9 +117,6 @@ void executeUserCommands()
{
#endif /* HAVE_READLINE */
ProductAutomaton* product_automaton = 0;
pair<unsigned long int, bool> last_computed_product_automaton;
signal(SIGPIPE, SIG_IGN);
while (1)
@ -170,35 +166,50 @@ void executeUserCommands()
}
#endif /* HAVE_ISATTY */
#ifdef HAVE_READLINE
if (line != static_cast<char*>(0) /* line may be 0 on EOF */
&& input_line.find_first_not_of(" \t") != string::npos)
{
add_history(line);
free(line);
}
#endif /* HAVE_READLINE */
/*
* If the input line contains an unescaped pipe symbol ('|') outside
* quotes, extract an external command from the line.
*/
external_command = "";
string::size_type pipe_pos = input_line.find_first_of('|');
if (pipe_pos != string::npos)
string::size_type pos
= findInQuotedString(input_line, "|", OUTSIDE_QUOTES);
if (pos != string::npos)
{
string::size_type nonspace_pos
= input_line.find_first_not_of(" \t", pipe_pos + 1);
= input_line.find_first_not_of(" \t", pos + 1);
if (nonspace_pos != string::npos)
{
external_command = input_line.substr(nonspace_pos);
input_line = input_line.substr(0, pipe_pos);
input_line = input_line.substr(0, pos);
}
}
sliceString(input_line, " \t", input_tokens);
sliceString(substituteInQuotedString(input_line, " \t", "\n\n",
OUTSIDE_QUOTES),
"\n",
input_tokens);
user_break = false;
if (!input_tokens.empty() || !external_command.empty())
{
round_info.cout << '\n';
round_info.cout.flush();
}
if (!input_tokens.empty())
{
#ifdef HAVE_READLINE
if (line != static_cast<char*>(0)) /* line may be 0 on EOF */
{
add_history(line);
free(line);
}
#endif /* HAVE_READLINE */
round_info.cout << '\n';
round_info.cout.flush();
token = parseCommand(input_tokens[0]);
if (token == CONTINUE || token == SKIP)
@ -406,8 +417,7 @@ void executeUserCommands()
case BUCHIANALYZE :
verifyArgumentCount(input_tokens, 2, 2);
printAutomatonAnalysisResults(*output_stream, indent,
parseNumber(input_tokens[1]),
parseNumber(input_tokens[2]));
input_tokens);
if (output_file != 0)
round_info.cout << " Büchi automaton intersection emptiness "
"check analysis";
@ -430,8 +440,8 @@ void executeUserCommands()
break;
case FORMULA :
verifyArgumentCount(input_tokens, 0, 0);
printFormula(*output_stream, indent, formula_type);
verifyArgumentCount(input_tokens, 0, 1);
printFormula(*output_stream, indent, formula_type, input_tokens);
if (output_file != 0)
round_info.cout << string(" ") + (formula_type
? "Formula"
@ -458,8 +468,7 @@ void executeUserCommands()
case RESULTANALYZE :
verifyArgumentCount(input_tokens, 2, 3);
printCrossComparisonAnalysisResults
(*output_stream, indent, formula_type, input_tokens,
product_automaton, last_computed_product_automaton);
(*output_stream, indent, formula_type, input_tokens);
if (output_file != 0)
round_info.cout << " Model checking result cross-comparison "
"analysis";
@ -501,8 +510,8 @@ void executeUserCommands()
break;
default :
throw CommandErrorException("Unknown command (`"
+ input_tokens[0] + "').");
throw CommandErrorException("Unknown command (`" + input_tokens[0]
+ "').");
}
if (output_string != 0)
@ -513,21 +522,17 @@ void executeUserCommands()
FILE* output_pipe = popen(external_command.c_str(), "w");
if (output_pipe == NULL)
throw ExecFailedException(external_command);
int status = fputs(outstring.c_str(), output_pipe);
if (status != EOF)
fflush(output_pipe);
fputs(outstring.c_str(), output_pipe);
pclose(output_pipe);
round_info.cout << '\n';
round_info.cout.flush();
if (status == EOF)
throw IOException("Error writing to pipe.");
}
else if (output_file != 0)
else
{
round_info.cout << string(redirection_info.second
? " appended"
: " written")
+ " to `" + redirection_info.first + "'.\n\n";
if (output_file != 0)
round_info.cout << string(redirection_info.second
? " appended"
: " written")
+ " to `" + redirection_info.first + "'.\n";
round_info.cout << '\n';
round_info.cout.flush();
}
}
@ -560,16 +565,6 @@ void executeUserCommands()
}
}
if (product_automaton != 0)
{
::DispUtil::printText
("<cleaning up memory allocated for product automaton>", 4, 2);
delete product_automaton;
::DispUtil::printText(" ok\n", 4);
}
#ifdef HAVE_READLINE
}
catch (...)
@ -582,7 +577,7 @@ void executeUserCommands()
#endif /* HAVE_READLINE */
signal(SIGPIPE, SIG_DFL);
}
}
/* ========================================================================= */
TokenType parseCommand(const string& token)
@ -597,19 +592,6 @@ TokenType parseCommand(const string& token)
*
* ------------------------------------------------------------------------- */
{
/*
* gcc versions prior to version 3 do not conform to the C++ standard in their
* support for the string::compare functions. Use a macro to fix this if
* necessary.
*/
#ifdef __GNUC__
#if __GNUC__ < 3
#define compare(start,end,str,dummy) compare(str,start,end)
#endif
#endif
TokenType token_type = UNKNOWN;
string::size_type len = token.length();
bool ambiguous = false;
@ -706,8 +688,19 @@ TokenType parseCommand(const string& token)
break;
case 'i' :
if (token.compare(1, len - 1, "nconsistencies", len - 1) == 0)
token_type = INCONSISTENCIES;
if (len < 2)
ambiguous = true;
else if (token[1] == 'm')
{
if (token.compare(2, len - 2, "plementations", len - 2) == 0)
token_type = ALGORITHMS;
}
else if (token[1] == 'n')
{
if (token.compare(2, len - 2, "consistencies", len - 2) == 0)
token_type = INCONSISTENCIES;
}
break;
case 'q' :
@ -787,6 +780,11 @@ TokenType parseCommand(const string& token)
}
break;
case 't' :
if (token.compare(1, len - 1, "ranslators", len - 1) == 0)
token_type = ALGORITHMS;
break;
case 'v' :
if (token.compare(1, len - 1, "erbosity", len - 1) == 0)
token_type = VERBOSITY;
@ -797,12 +795,6 @@ TokenType parseCommand(const string& token)
throw CommandErrorException("Ambiguous command.");
return token_type;
#ifdef __GNUC__
#if __GNUC__ < 3
#undef compare
#endif
#endif
}
/* ========================================================================= */
@ -867,13 +859,13 @@ pair<string, bool> parseRedirection
if (token.length() > 2)
{
append = true;
filename = token.substr(2);
filename = unquoteString(token.substr(2));
input_tokens.pop_back();
}
}
else
{
filename = token.substr(1);
filename = unquoteString(token.substr(1));
input_tokens.pop_back();
}
}
@ -882,10 +874,9 @@ pair<string, bool> parseRedirection
{
string& token = *(input_tokens.rbegin() + 1);
if (token[0] == '>' && (token.length() == 1
|| (token.length() == 2 && token[1] == '>')))
if (token == ">" || token == ">>")
{
filename = input_tokens.back();
filename = unquoteString(input_tokens.back());
append = (token.length() == 2);
input_tokens.pop_back();
input_tokens.pop_back();
@ -921,8 +912,7 @@ bool parseFormulaType(vector<string, ALLOC(string) >& input_tokens)
{
formula_type = (input_tokens[1] != "-");
if (input_tokens[1].length() == 1
&& (input_tokens[1][0] == '+' || input_tokens[1][0] == '-'))
if (input_tokens[1] == "+" || input_tokens[1] == "-")
input_tokens.erase(input_tokens.begin());
}

1482
lbtt/src/UserCommands.cc
View file

File diff suppressed because it is too large Load diff

67
lbtt/src/UserCommands.h
View file

@ -23,13 +23,17 @@
#include <config.h>
#include <deque>
#include <iostream>
#include <map>
#include <string>
#include <vector>
#include <utility>
#include "LbttAlloc.h"
#include "BuchiAutomaton.h"
#include "Configuration.h"
#include "ProductAutomaton.h"
#include "EdgeContainer.h"
#include "Graph.h"
#include "IntervalList.h"
#include "Product.h"
#include "StateSpace.h"
using namespace std;
@ -45,38 +49,26 @@ extern Configuration configuration;
namespace UserCommands
{
void computeProductAutomaton /* Computes a product */
(ProductAutomaton*& product_automaton, /* automaton. */
const BuchiAutomaton& buchi_automaton,
pair<unsigned long int, bool>& last_automaton,
const pair<unsigned long int, bool>&
new_automaton);
unsigned long int parseAlgorithmId /* Parses an */
(const string& id); /* implementation
* identifier.
*/
void parseAlgorithmId /* Parses a list of */
(const string& ids, IntervalList& algorithms); /* implementation
* identifiers.
*/
void printAlgorithmList /* Displays a list of */
(ostream& stream, int indent); /* algorithms used in
* the tests.
*/
void synchronizePrefixAndCycle /* Synchronizes a prefix */
(deque<Graph::Graph<GraphEdgeContainer> /* with a cycle in a */
::size_type, /* sequence of graph */
ALLOC(Graph::Graph<GraphEdgeContainer> /* state identifiers. */
::size_type) >&
prefix,
deque<Graph::Graph<GraphEdgeContainer>
::size_type,
ALLOC(Graph::Graph<GraphEdgeContainer>
::size_type) >&
cycle);
void printCrossComparisonAnalysisResults /* Analyzes a */
(ostream& stream, int indent, /* contradiction between */
bool formula_type, /* test results of two */
const vector<string, ALLOC(string) >& /* implementations. */
input_tokens,
ProductAutomaton*& product_automaton,
pair<unsigned long int, bool>&
last_product_automaton);
input_tokens);
void printConsistencyAnalysisResults /* Analyzes a */
(ostream& stream, int indent, /* contradicition in the */
@ -87,19 +79,15 @@ void printConsistencyAnalysisResults /* Analyzes a */
void printAutomatonAnalysisResults /* Analyzes a */
(ostream& stream, int indent, /* contradiction in the */
unsigned long int algorithm1, /* Büchi automata */
unsigned long int algorithm2); /* intersection
const vector<string, ALLOC(string) >& /* Büchi automata */
input_tokens); /* intersection
* emptiness check.
*/
void printPath /* Displays information */
(ostream& stream, int indent, /* about a single */
const deque<StateSpace::size_type, /* system execution. */
ALLOC(StateSpace::size_type) >&
prefix,
const deque<StateSpace::size_type,
ALLOC(StateSpace::size_type) >&
cycle,
const StateSpace::Path& prefix, /* system execution. */
const StateSpace::Path& cycle,
const StateSpace& path);
void printAcceptingCycle /* Displays information */
@ -108,13 +96,12 @@ void printAcceptingCycle /* Displays information */
ALLOC(Configuration::AlgorithmInformation) >
::size_type
algorithm_id,
const deque<StateSpace::size_type,
ALLOC(StateSpace::size_type) >&
prefix,
const deque<StateSpace::size_type,
ALLOC(StateSpace::size_type) >&
cycle,
const BuchiAutomaton& automaton);
const BuchiAutomaton::Path& aut_prefix,
const BuchiAutomaton::Path& aut_cycle,
const BuchiAutomaton& automaton,
const StateSpace::Path& path_prefix,
const StateSpace::Path& path_cycle,
const StateSpace& statespace);
void printBuchiAutomaton /* Displays information */
(ostream& stream, int indent, /* about a Büchi */
@ -129,7 +116,9 @@ void evaluateFormula /* Displays information */
void printFormula /* Displays a formula */
(ostream& stream, int indent, /* used for testing. */
bool formula_type);
bool formula_type,
const vector<string, ALLOC(string) >&
input_tokens);
void printCommandHelp /* Displays help about */
(ostream& stream, int indent, /* user commands. */

335
lbtt/src/main.cc
View file

@ -36,6 +36,7 @@
#include "Random.h"
#include "SharedTestData.h"
#include "StatDisplay.h"
#include "TempFsysName.h"
#include "TestOperations.h"
#include "TestRoundInfo.h"
#include "TestStatistics.h"
@ -43,17 +44,6 @@
using namespace std;
/******************************************************************************
*
* Handler for the SIGINT signal.
*
*****************************************************************************/
RETSIGTYPE breakHandler(int)
{
user_break = true;
}
/******************************************************************************
@ -105,13 +95,120 @@ vector<TestStatistics, ALLOC(TestStatistics) > /* Overall test */
/******************************************************************************
*
* Functions for allocating and deallocating temporary file names.
*
*****************************************************************************/
static void allocateTempFilenames()
{
using SharedTestData::round_info;
round_info.formula_file_name[0] = new TempFsysName;
round_info.formula_file_name[0]->allocate("lbtt");
round_info.formula_file_name[1] = new TempFsysName;
round_info.formula_file_name[1]->allocate("lbtt");
round_info.automaton_file_name = new TempFsysName;
round_info.automaton_file_name->allocate("lbtt");
round_info.cout_capture_file = new TempFsysName;
round_info.cout_capture_file->allocate("lbtt");
round_info.cerr_capture_file = new TempFsysName;
round_info.cerr_capture_file->allocate("lbtt");
}
static void deallocateTempFilenames()
{
using SharedTestData::round_info;
if (round_info.formula_file_name[0] != 0)
{
delete round_info.formula_file_name[0];
round_info.formula_file_name[0] = 0;
}
if (round_info.formula_file_name[1] != 0)
{
delete round_info.formula_file_name[1];
round_info.formula_file_name[1] = 0;
}
if (round_info.automaton_file_name != 0)
{
delete round_info.automaton_file_name;
round_info.automaton_file_name = 0;
}
if (round_info.cout_capture_file != 0)
{
delete round_info.cout_capture_file;
round_info.cout_capture_file = 0;
}
if (round_info.cerr_capture_file != 0)
{
delete round_info.cerr_capture_file;
round_info.cerr_capture_file = 0;
}
}
/******************************************************************************
*
* Handler for the SIGINT signal.
*
*****************************************************************************/
static void breakHandler(int)
{
user_break = true;
}
/******************************************************************************
*
* Default handler for signals that terminate the process.
*
*****************************************************************************/
static void abortHandler(int signum)
{
deallocateTempFilenames();
struct sigaction s;
s.sa_handler = SIG_DFL;
sigemptyset(&s.sa_mask);
s.sa_flags = 0;
sigaction(signum, &s, static_cast<struct sigaction*>(0));
raise(signum);
}
/******************************************************************************
*
* Function for installing signal handlers.
*
*****************************************************************************/
static void installSignalHandler(int signum, void (*handler)(int))
{
struct sigaction s;
sigaction(signum, static_cast<struct sigaction*>(0), &s);
if (s.sa_handler != SIG_IGN)
{
s.sa_handler = handler;
sigemptyset(&s.sa_mask);
s.sa_flags = 0;
sigaction(signum, &s, static_cast<struct sigaction*>(0));
}
}
/******************************************************************************
*
* Test loop.
*
*****************************************************************************/
void testLoop()
bool testLoop()
{
using namespace DispUtil;
using namespace SharedTestData;
@ -136,13 +233,6 @@ void testLoop()
? round_info.next_round_to_run
: global_options.number_of_rounds + 1);
if (tmpnam(round_info.formula_file_name[0]) == 0
|| tmpnam(round_info.formula_file_name[1]) == 0
|| tmpnam(round_info.automaton_file_name) == 0
|| tmpnam(round_info.cout_capture_file) == 0
|| tmpnam(round_info.cerr_capture_file) == 0)
throw Exception("unable to allocate names for temporary files");
/*
* If a name for the error log file was given in the configuration, create
* the file.
@ -221,19 +311,6 @@ void testLoop()
formula_random_state[i] = static_cast<short int>(LRAND(0, LONG_MAX));
#endif /* HAVE_RAND48 */
/*
* If using paths as state spaces, include the internal model checking
* algorithm in the set of algorithms.
*/
if (global_options.statespace_generation_mode & Configuration::PATH)
{
Configuration::AlgorithmInformation lbtt_info
= {new string("lbtt"), new string(), new string(), true};
configuration.algorithms.push_back(lbtt_info);
}
/*
* Intialize the vector for storing the test results for each
* implementation and the vector for collecting overall test statistics for
@ -271,21 +348,9 @@ void testLoop()
= (round_info.current_round < round_info.next_round_to_run);
if (!round_info.skip)
{
if (!printText(string("Round ") + toString(round_info.current_round)
+ " of " + toString(global_options.number_of_rounds)
+ "\n\n",
2))
{
if (global_options.verbosity == 1)
{
if (round_info.current_round > 1)
round_info.cout << ' ';
round_info.cout << round_info.current_round;
round_info.cout.flush();
}
}
}
printText(string("Round ") + toString(round_info.current_round)
+ " of " + toString(global_options.number_of_rounds) + "\n\n",
2);
try
{
@ -399,7 +464,7 @@ void testLoop()
if (user_break)
{
printText("[User break]\n\n", 2, 4);
printText("[User break]\n\n", 1, 4);
throw UserBreakException();
}
@ -414,12 +479,17 @@ void testLoop()
if (global_options.statespace_generation_mode & Configuration::PATH
&& (global_options.do_cons_test || global_options.do_comp_test)
&& (!test_results[round_info.number_of_translators].
automaton_stats[0].emptiness_check_performed))
&& (!test_results[round_info.number_of_translators - 1].
automaton_stats[0].emptiness_check_performed)
&& configuration.algorithms[round_info.number_of_translators - 1].
enabled)
verifyFormulaOnPath();
if (!round_info.error)
{
if (global_options.verbosity == 2)
::StatDisplay::printStatTableHeader(round_info.cout, 4);
unsigned long int num_enabled_implementations = 0;
for (unsigned long int algorithm_id = 0;
@ -431,81 +501,61 @@ void testLoop()
num_enabled_implementations++;
if (configuration.isInternalAlgorithm(algorithm_id))
continue;
printText(configuration.algorithmString(algorithm_id) + '\n',
2, 4);
3, 4);
for (int counter = 0; counter < 2; counter++)
{
if (user_break)
{
printText("[User break]\n\n", 2, 4);
printText("[User break]\n\n", 1, 4);
throw UserBreakException();
}
printText(string(counter == 1 ? "Negated" : "Positive")
+ " formula:\n",
2,
6);
if (global_options.verbosity == 1
|| global_options.verbosity == 2)
{
if (counter == 1)
round_info.cout << '\n';
if (global_options.verbosity == 1)
round_info.cout << round_info.current_round << ' ';
else
round_info.cout << string(4, ' ');
changeStreamFormatting(cout, 2, 0, ios::right);
round_info.cout << algorithm_id << ' ';
restoreStreamFormatting(cout);
round_info.cout << (counter == 0 ? '+' : '-') << ' ';
round_info.cout.flush();
}
else
printText(string(counter == 1 ? "Negated" : "Positive")
+ " formula:\n",
3,
6);
try
{
try
{
round_info.product_automaton = 0;
/*
* Generate a Büchi automaton using the current algorithm.
* `counter' determines the formula which is to be
* translated into an automaton; 0 denotes the positive and
* 1 the negated formula.
*/
generateBuchiAutomaton(counter, algorithm_id);
if (global_options.do_cons_test || global_options.do_comp_test)
{
/*
* Generate a Büchi automaton using the current algorithm.
* `counter' determines the formula which is to be
* translated into an automaton; 0 denotes the positive and
* 1 the negated formula.
* Find the system states from which an accepting
* execution cycle can be reached by checking the product
* automaton for emptiness.
*/
generateBuchiAutomaton(counter, algorithm_id);
if (global_options.do_cons_test
|| global_options.do_comp_test)
{
/*
* Compute the product of the Büchi automaton with the
* state space.
*/
generateProductAutomaton(counter, algorithm_id);
/*
* Find the system states from which an accepting
* execution cycle can be reached by checking the product
* automaton for emptiness.
*/
performEmptinessCheck(counter, algorithm_id);
/*
* If a product automaton was computed in this test round
* (it might have not if the emptiness checking result was
* already available), release the memory allocated for
* the product automaton.
*/
if (round_info.product_automaton != 0)
{
printText("<deallocating memory>", 4, 8);
delete round_info.product_automaton;
round_info.product_automaton = 0;
printText(" ok\n", 4);
}
}
}
catch (...)
{
if (round_info.product_automaton != 0)
{
delete round_info.product_automaton;
round_info.product_automaton = 0;
}
throw;
performEmptinessCheck(counter, algorithm_id);
}
}
catch (const BuchiAutomatonGenerationException&)
@ -541,7 +591,13 @@ void testLoop()
emptiness_check_performed)
performConsistencyCheck(algorithm_id);
printText("\n", 2);
printText("\n", 1);
}
if (global_options.verbosity == 2)
{
round_info.cout << '\n';
round_info.cout.flush();
}
if (num_enabled_implementations > 0)
@ -553,10 +609,7 @@ void testLoop()
* results obtained using the different algorithms.
*/
if (num_enabled_implementations >= 2
|| (num_enabled_implementations == 1
&& global_options.statespace_generation_mode
& Configuration::PATH))
if (num_enabled_implementations >= 2)
compareResults();
}
@ -592,25 +645,17 @@ void testLoop()
* the testing should be paused to wait for user commands.
*/
if (round_info.error)
round_info.all_tests_successful = false;
if (round_info.error
&& global_options.interactive == Configuration::ONERROR)
round_info.next_round_to_stop = round_info.current_round;
if (round_info.next_round_to_stop == round_info.current_round)
{
if (global_options.verbosity == 1)
{
round_info.cout << '\n';
round_info.cout.flush();
}
::UserCommandInterface::executeUserCommands();
}
}
for (int i = 0; i < 2; i++)
removeFile(round_info.formula_file_name[i], 2);
if (round_info.path_iterator != 0)
delete round_info.path_iterator;
else if (round_info.statespace != 0)
@ -661,11 +706,13 @@ void testLoop()
round_info.transcript_file.close();
}
if (global_options.verbosity >= 1)
if (global_options.verbosity >= 2)
printCollectiveStats(cout, 0);
if (round_info.formula_input_file.is_open())
round_info.formula_input_file.close();
return round_info.all_tests_successful;
}
@ -688,15 +735,27 @@ int main(int argc, char* argv[])
if (!e.line_info.empty())
cerr << ":" << configuration.global_options.cfg_filename << ":"
<< e.line_info;
cerr << ": " << e.what() << endl;
exit(-1);
cerr << ":" << e.what() << endl;
exit(2);
}
if (configuration.global_options.verbosity >= 3)
configuration.print(cout);
user_break = false;
signal(SIGINT, breakHandler);
installSignalHandler(SIGHUP, abortHandler);
installSignalHandler(SIGINT,
configuration.global_options.handle_breaks
? breakHandler
: abortHandler);
installSignalHandler(SIGQUIT, abortHandler);
installSignalHandler(SIGABRT, abortHandler);
installSignalHandler(SIGPIPE, abortHandler);
installSignalHandler(SIGALRM, abortHandler);
installSignalHandler(SIGTERM, abortHandler);
installSignalHandler(SIGUSR1, abortHandler);
installSignalHandler(SIGUSR2, abortHandler);
#ifdef HAVE_OBSTACK_H
obstack_alloc_failed_handler = &ObstackAllocator::failure;
@ -708,18 +767,26 @@ int main(int argc, char* argv[])
try
{
testLoop();
allocateTempFilenames();
if (!testLoop())
{
deallocateTempFilenames();
return 1;
}
}
catch (const Exception& e)
{
cerr << argv[0] << ": " << e.what() << endl;
exit(-1);
deallocateTempFilenames();
cerr << endl << argv[0] << ": " << e.what() << endl;
exit(3);
}
catch (const bad_alloc&)
{
cerr << argv[0] << ": out of memory" << endl;
exit(-1);
deallocateTempFilenames();
cerr << endl << argv[0] << ": out of memory" << endl;
exit(3);
}
deallocateTempFilenames();
return 0;
}

77
lbtt/src/translate.cc
View file

@ -45,6 +45,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.
@ -60,21 +71,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.
@ -83,7 +119,7 @@ RETSIGTYPE signalHandler(int signal_number)
int main(int argc, char** argv)
{
typedef enum {OPT_HELP = 'h', OPT_LBT, OPT_SPIN, OPT_VERSION = 'v'}
typedef enum {OPT_HELP = 'h', OPT_LBT, OPT_SPIN, OPT_VERSION = 'V'}
OptionType;
static OPTIONSTRUCT command_line_options[] =
@ -100,12 +136,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)
@ -115,8 +149,8 @@ int main(int argc, char** argv)
<< " [translator] [command line for translator] [formula "
"file] [automaton file]\n"
"General options:\n"
" --h, --help Show this help\n"
" --v, --version Show version and exit\n\n"
" -h, --help Show this help\n"
" -V, --version Show version and exit\n\n"
"Translator options:\n"
" --lbt lbt\n"
" --spin Spin\n"
@ -168,16 +202,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);