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

fix status of lbtt's subtree. Apparently it was messed up during the cvsimport

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2008-02-23 00:17:42 +01:00
parent 17f76e371f
commit 91df6cab77
77 changed files with 16272 additions and 6019 deletions
Download patch file Download diff file Expand all files Collapse all files

2
lbtt/AUTHORS
View file

@ -1 +1 @@
lbtt was written by Heikki Tauriainen <heikki.tauriainen@hut.fi>
Heikki Tauriainen <heikki.tauriainen@tkk.fi>

26
lbtt/ChangeLog
View file

@ -16,13 +16,13 @@
Update description of the --formulafile command line option.
(Configuration::print): Do not display a file name when reading
formulas from standard input.
* src/SpotWrapper.h, src/SpotWrapper.cc: Merge files from
Spot 0.2 (contributed by Alexandre Duret-Lutz); remove #pragma
definitions.
* src/ExternalTranslator.h, src/Makefile.in, src/translate.cc:
Merge changes from Spot 0.2 (contributed by Alexandre Duret-Lutz).
* doc/lbtt.texi: Fix typo in URL of the FormulaOptions block
generator. Update version, add documentation and references about
support for Spot. Describe the new semantics of the --formulafile
@ -124,7 +124,7 @@
log file.
* configure.ac: Add test for the setsid library function.
2004-07-31 Heikki Tauriainen <heikki.tauriainen@hut.fi>
* src/Product.h (ProductEdge::edge_1, ProductEdge::edge_2):
@ -178,7 +178,7 @@
* 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
@ -257,13 +257,13 @@
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.
@ -337,7 +337,7 @@
(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.
@ -365,7 +365,7 @@
* 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
@ -475,7 +475,7 @@
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.
@ -505,7 +505,7 @@
* 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)
@ -513,7 +513,7 @@
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.
@ -858,7 +858,7 @@
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.
@ -926,7 +926,7 @@
Reformat the automata file format section to avoid overfull lines
in dvi generation.
Fix description of the Algorithm block used with lbtt-translate.
* doc/testprocedure.txt, doc/intersectioncheck.txt: Add initial
newlines.

180
lbtt/NEWS
View file

@ -1,5 +1,5 @@
lbtt NEWS -- history of user-visible changes. 01 Oct 2002
Copyright (C) 2002 Heikki Tauriainen
lbtt NEWS -- history of user-visible changes. 30 Aug 2005
Copyright (C) 2005 Heikki Tauriainen
Permission is granted to anyone to make or distribute verbatim copies
of this document as received, in any medium, provided that the
@ -10,7 +10,181 @@ Copyright (C) 2002 Heikki Tauriainen
provided also that they carry prominent notices stating who last
changed them.
Please send bug reports to <heikki.tauriainen@hut.fi>.
Please send bug reports to <heikki.tauriainen@tkk.fi>.
Version 1.2.0
* This release adds direct support (contributed by Alexandre Duret-Lutz)
for the LTL-to-Büchi translator distributed with the Spot model
checking library (available at <http://spot.lip6.fr/>).
lbtt 1.2.0 also supports reading input formulas from standard input
(by using the command-line option `--formulafile=-'; when reading input
formulas from an actual file, the filename needs to be different from
"-").
Version 1.1.3
* This release fixes build problems with GCC 4 and more job control
problems.
Version 1.1.2
* Another bug fix release that fixes memory access and job control
problems.
Version 1.1.1
* This release includes fixes to build problems with non-GNU
compilers on GNU libc systems and a few minor bug fixes.
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
and Darwin, and documentation generation in dvi format. A problem
with reading user commands from a source that is not a terminal was
also fixed. Many thanks to Alexandre Duret-Lutz for patches and
useful suggestions.
Version 1.0.2
* Bug fix release.
* The official WWW home page of the tool is now located at
<http://www.tcs.hut.fi/Software/lbtt/>. From there you can also
access the FormulaOptions block generator for lbtt configuration
files. The generator has limited support for specifying relative
(instead of absolute) priorities for the LTL operators.
Version 1.0.1

22
lbtt/README
View file

@ -1,24 +1,24 @@
lbtt version 1.0.1
lbtt version 1.2.0
------------------
lbtt is a tool for testing programs which translate formulas
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üchi 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/%7Ehtauriai/lbtt/>.
<http://www.tcs.hut.fi/Software/lbtt/>.
lbtt is free software, you may change and redistribute it under
the terms of the GNU General Public License. lbtt comes with
NO WARRANTY. See the file COPYING for details.
Quick installation instructions:
Brief installation instructions:
--------------------------------
The basic procedure to build lbtt, the associated tools
@ -82,4 +82,4 @@ Documentation:
The documentation is also available in various formats
at the program's home page at
<http://www.tcs.hut.fi/%7Ehtauriai/lbtt/>.
<http://www.tcs.hut.fi/Software/lbtt/>.

52
lbtt/configure.ac
View file

@ -1,8 +1,8 @@
# Process this file with autoconf to produce a configure script.
AC_PREREQ([2.59])
AC_INIT([lbtt], [1.1.1], [heikki.tauriainen@hut.fi])
AC_REVISION([Revision: 1.5])
AC_INIT([lbtt], [1.2.0], [heikki.tauriainen@tkk.fi])
AC_REVISION([Revision: 1.8])
AC_CONFIG_SRCDIR([src/main.cc])
AC_CONFIG_HEADERS([config.h])
AM_INIT_AUTOMAKE
@ -124,52 +124,6 @@ AC_CHECK_HEADERS(
# Checks for typedefs, structures, and compiler characteristics.
# Check for the availability of the slist header (an extension to the C++
# Standard Template Library). (In GCC 3.x the header is in the ext/
# subdirectory of the directory containing the standard C++ headers.)
AC_MSG_CHECKING([for slist])
for slist_header in slist ext/slist no; do
if test "${slist_header}" != no; then
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 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_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_SUBST([INCLUDE_SLIST_HEADER], ["#include <${slist_header}>"])
else
slist_header=no
fi
fi
if test "${slist_header}" = no; then
AC_MSG_RESULT([no])
fi
AC_LANG(C)
AC_CHECK_TYPES(
@ -191,7 +145,7 @@ AC_C_INLINE
# Checks for library functions.
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],
[strchr strtod strtol strtoul strerror mkdir mkstemp open read write close popen pclose pipe fork execvp getpgrp setpgid tcgetpgrp tcsetpgrp 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])

1
lbtt/doc/intersectioncheck.txt
View file

@ -1,3 +1,4 @@
,,,,,,,,,,,,,,,,,,, ,,,,,,,,,,,,,,,,,,,,,,,,,,,,
: LTL formula `f' :_____ : Negated LTL formula `!f' :
'''''''T''''''T'''' \ ___'''''''T'''''''''''T''''''''

1268
lbtt/doc/lbtt.texi
View file

File diff suppressed because it is too large Load diff

1
lbtt/doc/testprocedure.txt
View file

@ -1,3 +1,4 @@
,,,,,,,,,,,,,,,
: State space :
'''''''''''''''

7482
lbtt/doc/texinfo.tex Normal file
View file

File diff suppressed because it is too large Load diff

10
lbtt/src/BitArray.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -17,10 +17,6 @@
* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*/
#ifdef __GNUC__
#pragma implementation
#endif /* __GNUC__ */
#include <config.h>
#ifdef HAVE_SSTREAM
#include <sstream>
@ -378,7 +374,7 @@ unsigned long int BitArray::find(const unsigned long int max_count) const
for (i = 0; i < bsize && bits[i] == 0; ++i)
;
if (i == max_count)
if (i == bsize)
return max_count;
unsigned char c = bits[i];

18
lbtt/src/BitArray.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -20,10 +20,6 @@
#ifndef BITARRAY_H
#define BITARRAY_H
#ifdef __GNUC__
#pragma interface
#endif /* __GNUC__ */
#include <config.h>
#include <cstring>
#include <string>
@ -363,7 +359,10 @@ inline void BitArray::set(const unsigned long int bit_count)
*
* ------------------------------------------------------------------------- */
{
memset(static_cast<void*>(bits), 0xFF, (bit_count + 7) >> 3);
unsigned long int bsize = bit_count >> 3;
memset(static_cast<void*>(bits), 0xFF, bsize);
if ((bit_count & 0x07) != 0)
bits[bsize] |= (1 << (bit_count & 7)) - 1;
}
/* ========================================================================= */
@ -394,7 +393,10 @@ inline void BitArray::clear(const unsigned long int bit_count)
*
* ------------------------------------------------------------------------- */
{
memset(static_cast<void*>(bits), 0, (bit_count + 7) >> 3);
unsigned long int bsize = bit_count >> 3;
memset(static_cast<void*>(bits), 0, bsize);
if ((bit_count & 0x07) != 0)
bits[bsize] &= ~((1 << (bit_count & 7)) - 1);
}
/* ========================================================================= */

4
lbtt/src/Bitset.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License

621
lbtt/src/BuchiAutomaton.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -17,10 +17,6 @@
* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*/
#ifdef __GNUC__
#pragma implementation
#endif /* __GNUC__ */
#include <config.h>
#include <deque>
#include <stack>
@ -96,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);
@ -133,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);
@ -194,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.
*
@ -316,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
@ -345,27 +288,20 @@ void BuchiAutomaton::read(istream& input_stream)
* to the interval [0...(number of states - 1)].
*/
map<long int, size_type, less<long int>, ALLOC(size_type) >
state_number_map;
map<long int, size_type> state_number_map;
pair<long int, size_type> state_mapping(0, 0);
pair<map<long int, size_type, less<long int>, ALLOC(size_type) >
::const_iterator,
bool>
state_finder;
pair<map<long int, size_type>::const_iterator, bool> state_finder;
/*
* Also the acceptance set numbers will be mapped to the interval
* [0...(number of acceptance sets - 1)].
*/
map<long int, unsigned long int, less<long int>, ALLOC(unsigned long int) >
acceptance_set_map;
map<long int, unsigned long int> acceptance_set_map;
pair<long int, unsigned long int> acceptance_set_mapping(0, 0);
pair<map<long int, unsigned long int, less<long int>,
ALLOC(unsigned long int) >::const_iterator,
bool>
pair<map<long int, unsigned long int>::const_iterator, bool>
acceptance_set_finder;
/*
@ -450,36 +386,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.
*/
@ -505,6 +446,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);
@ -520,7 +497,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);
@ -548,297 +525,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
@ -880,7 +566,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
@ -941,7 +627,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";
}
}
@ -964,16 +651,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.
*
* ------------------------------------------------------------------------- */
@ -981,11 +675,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));
@ -1006,9 +698,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();
}
@ -1073,7 +789,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";

200
lbtt/src/BuchiAutomaton.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -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);
}
/******************************************************************************

10
lbtt/src/BuchiProduct.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -28,8 +28,7 @@ namespace Graph
*
*****************************************************************************/
map< ::Ltl::LtlFormula*, BuchiProduct::SatisfiabilityMapping,
less< ::Ltl::LtlFormula*>, ALLOC(BuchiProduct::SatisfiabilityMapping) >
map< ::Ltl::LtlFormula*, BuchiProduct::SatisfiabilityMapping>
BuchiProduct::sat_cache;
@ -73,8 +72,7 @@ bool BuchiProduct::synchronizable
guard_1 = swap_guard;
}
map<LtlFormula*, SatisfiabilityMapping, less<LtlFormula*>,
ALLOC(SatisfiabilityMapping) >::iterator
map<LtlFormula*, SatisfiabilityMapping>::iterator
sat_cache_element = sat_cache.find(guard_1);
if (sat_cache_element == sat_cache.end())

16
lbtt/src/BuchiProduct.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -142,18 +142,16 @@ private:
* automata.
*/
typedef map< ::Ltl::LtlFormula*, bool, /* Type definition for */
less< ::Ltl::LtlFormula*>, /* storing information */
ALLOC(bool) > /* about the */
SatisfiabilityMapping; /* satisfiability of the
typedef map< ::Ltl::LtlFormula*, bool> /* Type definition for */
SatisfiabilityMapping; /* storing information
* about the
* satisfiability of the
* guards of product
* transitions.
*/
static map< ::Ltl::LtlFormula*, /* Result cache for */
SatisfiabilityMapping, /* satisfiability tests. */
less< ::Ltl::LtlFormula*>,
ALLOC(SatisfiabilityMapping) >
SatisfiabilityMapping> /* satisfiability tests. */
sat_cache;
};

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

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -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();
}

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

File diff suppressed because it is too large Load diff

1652
lbtt/src/Configuration.cc
View file

File diff suppressed because it is too large Load diff

301
lbtt/src/Configuration.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -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.
@ -63,21 +62,29 @@ public:
struct AlgorithmInformation; /* See below. */
string algorithmString /* Formats the the id */
(vector<AlgorithmInformation, /* of an algorithm and */
ALLOC(AlgorithmInformation) >::size_type/* the name of the */
algorithm_id) const; /* algorithm into a
(vector<AlgorithmInformation>::size_type /* of an algorithm and */
algorithm_id) const; /* the name of the
* algorithm into a
* 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
@ -290,11 +311,12 @@ public:
* LTL formula symbols.
*/
map<int, int, less<int>, ALLOC(int) > /* Priorities for LTL */
symbol_priority; /* formula symbols. */
map<int, int> symbol_priority; /* Priorities for LTL
* formula symbols.
*/
map<int, double, less<int>, ALLOC(double) > /* Expected numbers of */
symbol_distribution; /* occurrence for the
map<int, double> symbol_distribution; /* Expected numbers of
* occurrence for the
* different formula
* operators.
*/
@ -354,12 +376,18 @@ public:
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
vector<AlgorithmInformation, /* A vector containing */
ALLOC(AlgorithmInformation) > algorithms; /* information about the
vector<AlgorithmInformation> algorithms; /* A vector containing
* information about the
* algorithms used in
* the tests.
*/
map<string, unsigned long int> algorithm_names; /* Mapping between
* algorithm names and
* their numeric
* identifiers.
*/
GlobalConfiguration global_options; /* General configuration
* information.
*/
@ -376,15 +404,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 +438,9 @@ public:
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
private:
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
struct IntegerRange /* Data structure for
* representing integer-
* valued ranges of certain
@ -426,11 +448,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 +461,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 +497,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,
@ -492,17 +512,18 @@ private:
OPT_STATESPACEPROPOSITIONS,
OPT_STATESPACESIZE, OPT_TRUTHPROBABILITY};
typedef map<pair<int, int>, double, /* Type definitions for */
less<pair<int, int> >, /* the result cache used */
ALLOC(double) > /* for computing the */
ProbabilityMapElement; /* probability */
typedef map<int, ProbabilityMapElement, /* distribution of LTL */
less<int>, /* formula operators. */
ALLOC(ProbabilityMapElement) >
ProbabilityMap;
typedef map<pair<int, int>, double> /* Type definitions for */
ProbabilityMapElement; /* the result cache used */
/* for computing the */
typedef map<int, ProbabilityMapElement> /* probability */
ProbabilityMap; /* distribution of LTL
* formula operators.
*/
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
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.

12
lbtt/src/DispUtil.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -32,10 +32,10 @@
namespace DispUtil
{
stack<StreamFormatting, /* Stack for storing the */
deque<StreamFormatting, /* previous states of an */
ALLOC(StreamFormatting) > > /* output stream. */
stream_formatting_stack;
stack<StreamFormatting, deque<StreamFormatting> > /* Stack for storing the */
stream_formatting_stack; /* previous states of an
* output stream.
*/
/* ========================================================================= */
void changeStreamFormatting

28
lbtt/src/DispUtil.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -20,10 +20,6 @@
#ifndef DISPUTIL_H
#define DISPUTIL_H
#ifdef __GNUC__
#pragma interface
#endif /* __GNUC__ */
#include <config.h>
#include <iostream>
#include <string>
@ -62,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);
/******************************************************************************
@ -82,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);
};

4
lbtt/src/EdgeContainer.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License

56
lbtt/src/Exception.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -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&()
/* ----------------------------------------------------------------------------

143
lbtt/src/ExternalTranslator.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -18,12 +18,11 @@
*/
#include <config.h>
#include <csignal>
#include <cstdio>
#include <cstdlib>
#include <cstring>
#include <sys/stat.h>
#include <sys/types.h>
#include <sys/wait.h>
#ifdef HAVE_FCNTL_H
#include <fcntl.h>
#endif /* HAVE_FCNTL_H */
@ -64,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();
}
/* ========================================================================= */
@ -101,21 +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);
std::cout << translated_formula << std::endl;
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);
@ -125,106 +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);
int exitcode = system(command_line.c_str());
/*
* system() blocks SIGINT and SIGQUIT. If the child was killed
* by such a signal, forward the signal to the current process.
*/
if (WIFSIGNALED(exitcode) &&
(WTERMSIG(exitcode) == SIGINT || WTERMSIG(exitcode) == SIGQUIT))
raise(WTERMSIG(exitcode));
if (!execSuccess(exitcode))
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);
}

10
lbtt/src/FormulaRandomizer.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -17,10 +17,6 @@
* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*/
#ifdef __GNUC__
#pragma implementation
#endif /* __GNUC__ */
#include <config.h>
#include "FormulaRandomizer.h"
#include "Random.h"
@ -96,7 +92,7 @@ LtlFormula* FormulaRandomizer::recGenerate(unsigned long int target_size)
*
* ------------------------------------------------------------------------- */
{
vector<IntegerPair, ALLOC(IntegerPair) >::const_iterator symbol_priority;
vector<IntegerPair>::const_iterator symbol_priority;
LtlFormula* formula;
long int x;

56
lbtt/src/FormulaRandomizer.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -21,6 +21,7 @@
#define FORMULARANDOMIZER_H
#include <config.h>
#include <map>
#include <vector>
#include <utility>
#include "LbttAlloc.h"
@ -86,16 +87,16 @@ public:
* `reset'.
*/
const map<unsigned long int, unsigned long int, /* Get the numbers of */
less<unsigned long int>, /* different atomic */
ALLOC(unsigned long int) >& /* propositions */
propositionStatistics() const; /* generated since the
const map<unsigned long int, unsigned long int>& /* Get the numbers of */
propositionStatistics() const; /* different atomic
* propositions
* generated since the
* last call to `reset'.
*/
const map<int, unsigned long int, less<int>, /* Get the numbers of */
ALLOC(unsigned long int) >& /* different symbols */
symbolStatistics() const; /* generated since the
const map<int, unsigned long int>& /* Get the numbers of */
symbolStatistics() const; /* different symbols
* generated since the
* last call to `reset'.
*/
@ -123,21 +124,20 @@ private:
typedef pair<int, int> IntegerPair;
vector<IntegerPair, ALLOC(IntegerPair) > /* Operand symbols and */
vector<IntegerPair> /* Operand symbols and */
propositional_symbol_priorities; /* their priorities in
* random formulae.
*/
vector<IntegerPair, ALLOC(IntegerPair) > /* Operators and their */
short_formula_operators; /* priorities in random
* formulae of size
* two.
vector<IntegerPair> short_formula_operators; /* Operators and their
* priorities in random
* formulae of size two.
*/
vector<IntegerPair, ALLOC(IntegerPair) > /* Operators and their */
long_formula_operators; /* priorities in random
* formulae of size
* greater than two.
vector<IntegerPair> long_formula_operators; /* Operators and their
* priorities in random
* formulae of size greater
* than two.
*/
unsigned long int number_of_generated_formulas; /* Number of generated
@ -145,14 +145,15 @@ private:
* last call to `reset'.
*/
map<unsigned long int, unsigned long int, /* Number of different */
less<unsigned long int>, /* atomic propositions */
ALLOC(unsigned long int) > /* generated since the */
proposition_statistics; /* last call to `reset' */
map<unsigned long int, unsigned long int> /* Number of different */
proposition_statistics; /* atomic propositions
* generated since the
* last call to `reset'
*/
map<int, unsigned long int, less<int>, /* Number of different */
ALLOC(unsigned long int) > /* formula symbols */
symbol_statistics; /* generated since the
map<int, unsigned long int> symbol_statistics; /* Number of different
* formula symbols
* generated since the
* last call to `reset'.
*/
};
@ -288,8 +289,7 @@ inline unsigned long int FormulaRandomizer::numberOfFormulas() const
}
/* ========================================================================= */
inline const map<unsigned long int, unsigned long int, less<unsigned long int>,
ALLOC(unsigned long int) >&
inline const map<unsigned long int, unsigned long int>&
FormulaRandomizer::propositionStatistics() const
/* ----------------------------------------------------------------------------
*
@ -307,7 +307,7 @@ FormulaRandomizer::propositionStatistics() const
}
/* ========================================================================= */
inline const map<int, unsigned long int, less<int>, ALLOC(unsigned long int) >&
inline const map<int, unsigned long int>&
FormulaRandomizer::symbolStatistics() const
/* ----------------------------------------------------------------------------
*

8
lbtt/src/FormulaWriter.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -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.

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

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -186,25 +186,38 @@ public:
* graph nodes.
*/
class PathElement; /* A class for representing
* (node, edge) pairs
*/
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
protected:
vector<Node*, ALLOC(Node*) > nodes; /* Nodes of the graph.
vector<Node*> nodes; /* Nodes of the graph.
* Derived classes can
* access this vector
* directly.
*/
public:
typedef typename /* Type definition for */
vector<Node*, ALLOC(Node*) >::size_type /* the size of the */
size_type; /* graph. The size can
typedef typename vector<Node*>::size_type /* Type definition for */
size_type; /* the size of the
* graph. The size can
* be no greater than
* the maximum size of
* the vector containing
* the graph nodes.
*/
typedef EdgeContainer EdgeContainerType; /* Type definition for
* containers of graph
* edges.
*/
typedef deque<PathElement> Path; /* Type definition for
* paths in a graph.
*/
typedef pair<size_type, size_type> StateIdPair; /* Type definition for a
* pair of state
* identifiers in a graph.
@ -323,8 +336,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 +366,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 +417,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.
@ -434,8 +503,7 @@ public:
*
*****************************************************************************/
class EdgeList : public list<Graph<EdgeList>::Edge*,
ALLOC(Graph<EdgeList>::Edge*) >
class EdgeList : public list<Graph<EdgeList>::Edge*>
{
public:
EdgeList(); /* Constructor. */
@ -450,14 +518,12 @@ public:
* the end of the list.
*/
list<Graph<EdgeList>::Edge*, /* Functions for finding */
ALLOC(Graph<EdgeList>::Edge*) > /* an element in the */
::const_iterator /* list. */
find(const Graph<EdgeList>::Edge* edge) const;
list<Graph<EdgeList>::Edge*,
ALLOC(Graph<EdgeList>::Edge*) >
::iterator
list<Graph<EdgeList>::Edge*>::const_iterator /* Functions for finding */
find(const Graph<EdgeList>::Edge* edge) const; /* an element in the
* list.
*/
list<Graph<EdgeList>::Edge*>::iterator
find(const Graph<EdgeList>::Edge* edge);
};
@ -472,8 +538,7 @@ public:
#ifdef HAVE_SLIST
class EdgeSlist : public slist<Graph<EdgeSlist>::Edge*,
ALLOC(Graph<EdgeSlist>::Edge*) >
class EdgeSlist : public slist<Graph<EdgeSlist>::Edge*>
{
public:
EdgeSlist(); /* Constructor. */
@ -489,14 +554,12 @@ public:
* list.
*/
slist<Graph<EdgeSlist>::Edge*, /* Functions for finding */
ALLOC(Graph<EdgeSlist>::Edge*) > /* an element in the */
::const_iterator /* list. */
find(const Graph<EdgeSlist>::Edge* edge) const;
slist<Graph<EdgeSlist>::Edge*>::const_iterator /* Functions for finding */
find(const Graph<EdgeSlist>::Edge* edge) const; /* an element in the
* list.
*/
slist<Graph<EdgeSlist>::Edge*,
ALLOC(Graph<EdgeSlist>::Edge*) >
::iterator
slist<Graph<EdgeSlist>::Edge*>::iterator
find(const Graph<EdgeSlist>::Edge* edge);
};
@ -510,8 +573,7 @@ public:
*
*****************************************************************************/
class EdgeVector : public vector<Graph<EdgeVector>::Edge*,
ALLOC(Graph<EdgeVector>::Edge*) >
class EdgeVector : public vector<Graph<EdgeVector>::Edge*>
{
public:
EdgeVector(); /* Constructor. */
@ -527,15 +589,11 @@ public:
* to edges.
*/
vector<Graph<EdgeVector>::Edge*, /* Functions for finding */
ALLOC(Graph<EdgeVector>::Edge*) > /* an element in the */
::const_iterator /* container. */
find(const Graph<EdgeVector>::Edge* edge)
const;
vector<Graph<EdgeVector>::Edge*>::const_iterator /* Functions for finding */
find(const Graph<EdgeVector>::Edge* edge) /* an element in the */
const; /* container. */
vector<Graph<EdgeVector>::Edge*,
ALLOC(Graph<EdgeVector>::Edge*) >
::iterator
vector<Graph<EdgeVector>::Edge*>::iterator
find(const Graph<EdgeVector>::Edge* edge);
};
@ -548,8 +606,7 @@ public:
*****************************************************************************/
class EdgeSet : public set<Graph<EdgeSet>::Edge*,
Graph<EdgeSet>::Edge::ptr_less,
ALLOC(Graph<EdgeSet>::Edge*) >
Graph<EdgeSet>::Edge::ptr_less>
{
};
@ -562,8 +619,7 @@ class EdgeSet : public set<Graph<EdgeSet>::Edge*,
*****************************************************************************/
class EdgeMultiSet : public multiset<Graph<EdgeMultiSet>::Edge*,
Graph<EdgeMultiSet>::Edge::ptr_less,
ALLOC(Graph<EdgeMultiSet>::Edge*) >
Graph<EdgeMultiSet>::Edge::ptr_less>
{
};
@ -689,7 +745,7 @@ Graph<EdgeContainer>::Graph(const size_type initial_number_of_nodes) :
{
nodes.reserve(initial_number_of_nodes);
for (typename vector<Node*, ALLOC(Node*) >::iterator node = nodes.begin();
for (typename vector<Node*>::iterator node = nodes.begin();
node != nodes.end();
++node)
*node = new Node();
@ -711,8 +767,7 @@ Graph<EdgeContainer>::Graph(const Graph<EdgeContainer>& graph)
* ------------------------------------------------------------------------- */
{
nodes.reserve(graph.nodes.size());
for (typename vector<Node*, ALLOC(Node*) >::const_iterator
node = graph.nodes.begin();
for (typename vector<Node*>::const_iterator node = graph.nodes.begin();
node != graph.nodes.end(); ++node)
nodes.push_back(new Node(**node));
}
@ -738,8 +793,7 @@ Graph<EdgeContainer>& Graph<EdgeContainer>::operator=
clear();
nodes.reserve(graph.nodes.size());
for (typename vector<Node*, ALLOC(Node*) >::const_iterator
node = graph.nodes.begin();
for (typename vector<Node*>::const_iterator node = graph.nodes.begin();
node != graph.nodes.end();
++node)
nodes.push_back(new Node(**node));
@ -782,8 +836,7 @@ void Graph<EdgeContainer>::clear()
*
* ------------------------------------------------------------------------- */
{
for (typename vector<Node*, ALLOC(Node*) >::reverse_iterator
node = nodes.rbegin();
for (typename vector<Node*>::reverse_iterator node = nodes.rbegin();
node != nodes.rend();
++node)
delete *node;
@ -924,13 +977,12 @@ 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;
for (typename vector<Node*, ALLOC(Node*) >::const_iterator
node = nodes.begin();
for (typename vector<Node*>::const_iterator node = nodes.begin();
node != nodes.end(); ++node)
result.second += (*node)->edges().size();
@ -964,7 +1016,7 @@ Graph<EdgeContainer>::subgraphStats(const size_type index) const
if (index >= s)
throw NodeIndexException();
stack<size_type, deque<size_type, ALLOC(size_type) > > unprocessed_nodes;
stack<size_type, deque<size_type> > unprocessed_nodes;
BitArray visited_nodes(s);
visited_nodes.clear(s);
@ -1468,6 +1520,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.
@ -1574,8 +1748,7 @@ inline void EdgeList::insert(Graph<EdgeList>::Edge* edge)
}
/* ========================================================================= */
inline list<Graph<EdgeList>::Edge*, ALLOC(Graph<EdgeList>::Edge*) >
::const_iterator
inline list<Graph<EdgeList>::Edge*>::const_iterator
EdgeList::find(const Graph<EdgeList>::Edge* edge) const
/* ----------------------------------------------------------------------------
*
@ -1586,9 +1759,9 @@ EdgeList::find(const Graph<EdgeList>::Edge* edge) const
* between the actual values of the edges (not the
* pointers).
*
* Returns: A list<Graph<EdgeList>::Edge*, ALLOC>::const_iterator
* Returns: A list<Graph<EdgeList>::Edge*>::const_iterator
* pointing to the edge in the list or
* list<Graph<EdgeList>::Edge*, ALLOC>::end() if the edge is
* list<Graph<EdgeList>::Edge*>::end() if the edge is
* not found in the list.
*
* ------------------------------------------------------------------------- */
@ -1603,7 +1776,7 @@ EdgeList::find(const Graph<EdgeList>::Edge* edge) const
}
/* ========================================================================= */
inline list<Graph<EdgeList>::Edge*, ALLOC(Graph<EdgeList>::Edge*) >::iterator
inline list<Graph<EdgeList>::Edge*>::iterator
EdgeList::find(const Graph<EdgeList>::Edge* edge)
/* ----------------------------------------------------------------------------
*
@ -1614,9 +1787,9 @@ EdgeList::find(const Graph<EdgeList>::Edge* edge)
* between the actual values of the edges (not the
* pointers).
*
* Returns: A list<Graph<EdgeList>::Edge*, ALLOC>::iterator pointing
* Returns: A list<Graph<EdgeList>::Edge*>::iterator pointing
* to the edge in the list or
* list<Graph<EdgeList>::Edge*, ALLOC>::end() if the edge is
* list<Graph<EdgeList>::Edge*>::end() if the edge is
* not found in the list.
*
* ------------------------------------------------------------------------- */
@ -1685,8 +1858,7 @@ inline void EdgeSlist::insert(Graph<EdgeSlist>::Edge* edge)
}
/* ========================================================================= */
inline slist<Graph<EdgeSlist>::Edge*, ALLOC(Graph<EdgeSlist>::Edge*) >
::const_iterator
inline slist<Graph<EdgeSlist>::Edge*>::const_iterator
EdgeSlist::find(const Graph<EdgeSlist>::Edge* edge) const
/* ----------------------------------------------------------------------------
*
@ -1697,9 +1869,9 @@ EdgeSlist::find(const Graph<EdgeSlist>::Edge* edge) const
* between the actual values of the edges (not the
* pointers).
*
* Returns: A slist<Graph<EdgeSlist>::Edge*, ALLOC>::const_iterator
* Returns: A slist<Graph<EdgeSlist>::Edge*>::const_iterator
* pointing to the edge in the list or
* slist<Graph<EdgeSlist>::Edge*, ALLOC>::end() if the edge
* slist<Graph<EdgeSlist>::Edge*>::end() if the edge
* is not found in the list.
*
* ------------------------------------------------------------------------- */
@ -1714,8 +1886,7 @@ EdgeSlist::find(const Graph<EdgeSlist>::Edge* edge) const
}
/* ========================================================================= */
inline slist<Graph<EdgeSlist>::Edge*, ALLOC(Graph<EdgeSlist>::Edge*) >
::iterator
inline slist<Graph<EdgeSlist>::Edge*>::iterator
EdgeSlist::find(const Graph<EdgeSlist>::Edge* edge)
/* ----------------------------------------------------------------------------
*
@ -1726,9 +1897,9 @@ EdgeSlist::find(const Graph<EdgeSlist>::Edge* edge)
* between the actual values of the edges (not the
* pointers).
*
* Returns: A slist<Graph<EdgeSlist>::Edge*, ALLOC>::iterator
* Returns: A slist<Graph<EdgeSlist>::Edge*>::iterator
* pointing to the edge in the list or
* slist<Graph<EdgeSlist>::Edge*, ALLOC>::end() if the edge
* slist<Graph<EdgeSlist>::Edge*>::end() if the edge
* is not found in the list.
*
* ------------------------------------------------------------------------- */
@ -1797,8 +1968,7 @@ inline void EdgeVector::insert(Graph<EdgeVector>::Edge* edge)
}
/* ========================================================================= */
inline vector<Graph<EdgeVector>::Edge*, ALLOC(Graph<EdgeVector>::Edge*) >
::const_iterator
inline vector<Graph<EdgeVector>::Edge*>::const_iterator
EdgeVector::find(const Graph<EdgeVector>::Edge* edge) const
/* ----------------------------------------------------------------------------
*
@ -1809,9 +1979,9 @@ EdgeVector::find(const Graph<EdgeVector>::Edge* edge) const
* between the actual values of the edges (not the
* pointers).
*
* Returns: A vector<Graph<EdgeVector>::Edge*, ALLOC>::const_iterator
* Returns: A vector<Graph<EdgeVector>::Edge*>::const_iterator
* pointing to the edge in the container or
* vector<Graph<EdgeVector>::Edge*, ALLOC>::end() if the
* vector<Graph<EdgeVector>::Edge*>::end() if the
* edge is not found in the container.
*
* ------------------------------------------------------------------------- */
@ -1826,8 +1996,7 @@ EdgeVector::find(const Graph<EdgeVector>::Edge* edge) const
}
/* ========================================================================= */
inline vector<Graph<EdgeVector>::Edge*, ALLOC(Graph<EdgeVector>::Edge*) >
::iterator
inline vector<Graph<EdgeVector>::Edge*>::iterator
EdgeVector::find(const Graph<EdgeVector>::Edge* edge)
/* ----------------------------------------------------------------------------
*
@ -1838,9 +2007,9 @@ EdgeVector::find(const Graph<EdgeVector>::Edge* edge)
* between the actual values of the edges (not the
* pointers).
*
* Returns: A vector<Graph<EdgeVector>::Edge*, ALLOC>::iterator
* Returns: A vector<Graph<EdgeVector>::Edge*>::iterator
* pointing to the edge in the container or
* vector<Graph<EdgeSlist>::Edge*, ALLOC>::end() if the edge
* vector<Graph<EdgeSlist>::Edge*>::end() if the edge
* is not found in the container.
*
* ------------------------------------------------------------------------- */

19
lbtt/src/IntervalList.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -41,7 +41,7 @@ void IntervalList::merge(unsigned long int min, unsigned long int max)
if (min > max)
return;
list<Interval, ALLOC(Interval) >::iterator interval;
list<Interval>::iterator interval;
for (interval = intervals.begin();
interval != intervals.end() && interval->second + 1 < min;
++interval)
@ -68,14 +68,14 @@ void IntervalList::merge(unsigned long int min, unsigned long int max)
if (interval->second < max)
{
interval->second = max;
list<Interval, ALLOC(Interval) >::iterator interval2 = interval;
list<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;
list<Interval>::iterator interval_to_erase = interval2;
++interval2;
intervals.erase(interval_to_erase);
}
@ -97,7 +97,7 @@ void IntervalList::remove(unsigned long int min, unsigned long int max)
if (min > max)
return;
list<Interval, ALLOC(Interval) >::iterator interval;
list<Interval>::iterator interval;
for (interval = intervals.begin();
interval != intervals.end() && interval->second < min;
++interval)
@ -126,7 +126,7 @@ void IntervalList::remove(unsigned long int min, unsigned long int max)
}
else /* min <= imin <= imax <= max */
{
list<Interval, ALLOC(Interval) >::iterator interval_to_erase = interval;
list<Interval>::iterator interval_to_erase = interval;
++interval;
intervals.erase(interval_to_erase);
}
@ -148,7 +148,7 @@ bool IntervalList::covers(unsigned long int min, unsigned long int max) const
if (min > max)
return true; /* empty interval is always covered */
list<Interval, ALLOC(Interval) >::const_iterator interval;
list<Interval>::const_iterator interval;
for (interval = intervals.begin();
interval != intervals.end() && min > interval->second;
++interval)
@ -173,8 +173,7 @@ string IntervalList::toString() const
* ------------------------------------------------------------------------- */
{
string s;
for (list<Interval, ALLOC(Interval) >::const_iterator
interval = intervals.begin();
for (list<Interval>::const_iterator interval = intervals.begin();
interval != intervals.end();
++interval)
{

23
lbtt/src/IntervalList.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -74,13 +74,15 @@ public:
unsigned long int operator++(int); /* Postfix increment. */
private:
const list<Interval, ALLOC(Interval) >* /* The interval list */
interval_list; /* associated with the */
/* iterator. */
const list<Interval>* interval_list; /* The interval list
* associated with the
* iterator.
*/
list<Interval, ALLOC(Interval) > /* An iterator pointing */
::const_iterator interval; /* at the current */
/* interval list. */
list<Interval>::const_iterator interval; /* An iterator pointing at
* the current intrerval
* list.
*/
unsigned long int element; /* Element currently
* pointed to by the
@ -143,8 +145,7 @@ public:
* iterators.
*/
typedef list<Interval, ALLOC(Interval) > /* Size type. */
::size_type size_type;
typedef list<Interval>::size_type size_type; /* Size type. */
size_type size() const; /* Tell the number of
* disjoint intervals in
@ -170,7 +171,7 @@ public:
*/
private:
list<Interval, ALLOC(Interval) > intervals; /* List of intervals. */
list<Interval> intervals; /* List of intervals. */
friend class const_iterator;
};

4
lbtt/src/LbtWrapper.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License

10
lbtt/src/LbttAlloc.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -22,12 +22,6 @@
#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
/* GNU libc 2.3.2's copy of obstack.h uses a definition of __INT_TO_PTR

14
lbtt/src/Ltl-parse.yy
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -44,9 +44,9 @@ static LtlFormula* result; /* This variable stores the
* ltl_parse.
*/
static std::set<LtlFormula*, less<LtlFormula*>, /* Intermediate results. */
ALLOC(LtlFormula*) > /* (This set is used */
intermediate_results; /* for keeping track of
static std::set<LtlFormula*> intermediate_results; /* Intermediate results.
* (This set is used
* for keeping track of
* the subformulas of a
* partially constructed
* formula in case the
@ -426,8 +426,8 @@ LtlFormula* parseFormula(istream& stream)
}
catch (...)
{
for (std::set<LtlFormula*, less<LtlFormula*>, ALLOC(LtlFormula*) >
::const_iterator f = intermediate_results.begin();
for (std::set<LtlFormula*>::const_iterator
f = intermediate_results.begin();
f != intermediate_results.end();
++f)
LtlFormula::destruct(*f);

223
lbtt/src/LtlFormula.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -17,10 +17,6 @@
* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*/
#ifdef __GNUC__
#pragma implementation
#endif /* __GNUC__ */
#include <config.h>
#include "FormulaWriter.h"
#include "LtlFormula.h"
@ -28,10 +24,8 @@
namespace Ltl
{
map<LtlFormula*, unsigned long int, /* Shared storage for */
LtlFormula::ptr_less, /* LTL formulae. */
ALLOC(unsigned long int) >
LtlFormula::formula_storage;
set<LtlFormula*, LtlFormula::ptr_less> /* Shared storage for */
LtlFormula::formula_storage; /* LTL formulae. */
unsigned long int /* Upper limit for the */
LtlFormula::eval_proposition_id_limit; /* atomic proposition
@ -42,8 +36,6 @@ unsigned long int /* Upper limit for the */
* truth assignment).
*/
/******************************************************************************
*
* Function for obtaining the infix symbol associated with a given
@ -147,12 +139,10 @@ public:
*/
private:
stack<LtlFormula*,
deque<LtlFormula*, ALLOC(LtlFormula*) > >
stack<LtlFormula*, deque<LtlFormula*> >
formula_stack;
stack<bool, deque<bool, ALLOC(bool) > >
negation_stack;
stack<bool, deque<bool> > negation_stack;
NnfConverter(const NnfConverter&); /* Prevent copying and */
NnfConverter& operator=(const NnfConverter&); /* assignment of
@ -203,8 +193,7 @@ class SubformulaCollector
public:
SubformulaCollector /* Constructor. */
(stack<const LtlFormula*,
deque<const LtlFormula*,
ALLOC(const LtlFormula*) > >&
deque<const LtlFormula*> >&
result_stack);
~SubformulaCollector(); /* Destructor. */
@ -216,8 +205,7 @@ public:
private:
stack<const LtlFormula*, /* Stack of subformulae. */
deque<const LtlFormula*,
ALLOC(const LtlFormula*) > >&
deque<const LtlFormula*> >&
subformula_stack;
SubformulaCollector(const SubformulaCollector&); /* Prevent copying and */
@ -389,9 +377,7 @@ inline void FormulaSizeCounter::operator()(const LtlFormula*, int)
/* ========================================================================= */
inline SubformulaCollector::SubformulaCollector
(stack<const LtlFormula*, deque<const LtlFormula*,
ALLOC(const LtlFormula*) > >&
result_stack) :
(stack<const LtlFormula*, deque<const LtlFormula*> >& result_stack) :
subformula_stack(result_stack)
/* ----------------------------------------------------------------------------
*
@ -773,9 +759,7 @@ unsigned long int LtlFormula::size() const
/* ========================================================================= */
void LtlFormula::collectSubformulae
(stack<const LtlFormula*, deque<const LtlFormula*,
ALLOC(const LtlFormula*) > >&
result_stack) const
(stack<const LtlFormula*, deque<const LtlFormula*> >& result_stack) const
/* ----------------------------------------------------------------------------
*
* Description: Collects the subformulae of a LtlFormula into a stack. After
@ -879,193 +863,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
/* ----------------------------------------------------------------------------

85
lbtt/src/LtlFormula.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -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.
@ -264,21 +261,18 @@ private:
void collectSubformulae /* Builds a stack of the */
(stack<const LtlFormula*, /* subformulae of the */
deque<const LtlFormula*, /* formula. */
ALLOC(const LtlFormula*) > >&
deque<const LtlFormula*> >& /* formula. */
result_stack) const;
typedef pair<bool, const LtlFormula*> /* Shorthand type */
FormulaStackElement; /* definitions for the */
typedef stack<FormulaStackElement, /* propositional */
deque<FormulaStackElement, /* satisfiability */
ALLOC(FormulaStackElement) > >/* checking algorithm. */
FormulaStack;
deque<FormulaStackElement> > /* satisfiability */
FormulaStack; /* checking algorithm. */
typedef pair<FormulaStack, Bitset>
TableauStackElement;
typedef stack<TableauStackElement,
deque<TableauStackElement,
ALLOC(TableauStackElement) > >
deque<TableauStackElement> >
TableauStack;
bool sat_eval /* Helper function for */
@ -288,9 +282,8 @@ private:
* formula.
*/
static map<LtlFormula*, unsigned long int, /* Shared storage for */
ptr_less, ALLOC(unsigned long int) > /* LTL formulae. */
formula_storage;
static set<LtlFormula*, ptr_less> /* Shared storage for */
formula_storage; /* LTL formulae. */
static unsigned long int /* Upper limit for the */
eval_proposition_id_limit; /* atomic proposition
@ -330,6 +323,16 @@ private:
/******************************************************************************
*
* Interface to the formula parser.
*
*****************************************************************************/
extern LtlFormula* parseFormula(istream& stream);
/******************************************************************************
*
* A class for atomic propositions.
@ -474,7 +477,7 @@ private:
* to satisfy the
* LtlFormula member
* function interface.
*/
*/
};
@ -1076,7 +1079,7 @@ typedef BinaryFormula<LtlBefore> Before;
*****************************************************************************/
/* ========================================================================= */
inline LtlFormula::LtlFormula()
inline LtlFormula::LtlFormula() : refcount(1)
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class LtlFormula. Initializes the attributes
@ -1088,8 +1091,6 @@ inline LtlFormula::LtlFormula()
*
* --------------------------------------------------------------------------*/
{
info_flags.is_propositional = 0;
info_flags.is_constant = 0;
}
/* ========================================================================= */
@ -1122,14 +1123,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 +1143,7 @@ inline LtlFormula* LtlFormula::clone()
*
* ------------------------------------------------------------------------- */
{
formula_storage.find(this)->second++;
++refcount;
return this;
}
@ -1241,8 +1237,7 @@ inline LtlFormula* LtlFormula::read(istream& stream)
*
* ------------------------------------------------------------------------- */
{
Exceptional_istream estream(&stream, ios::badbit | ios::failbit);
return read(estream);
return parseFormula(stream);
}
/* ========================================================================= */
@ -1303,8 +1298,6 @@ inline Exceptional_ostream& operator<<
return stream;
}
/* ========================================================================= */
inline LtlFormula& LtlFormula::insertToStorage(LtlFormula* f)
/* ----------------------------------------------------------------------------
@ -1317,19 +1310,15 @@ 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>::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 +1560,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 +1874,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 +2176,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.

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

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -30,6 +30,7 @@ extern int current_neverclaim_line_number;
%option never-interactive
%option noyywrap
%option nounput
%%

4
lbtt/src/NeverClaim-parse.yy
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License

20
lbtt/src/NeverClaimAutomaton.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -17,10 +17,6 @@
* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*/
#ifdef __GNUC__
#pragma implementation
#endif /* __GNUC__ */
#include <config.h>
#include <cstdio>
#include <fstream>
@ -66,8 +62,7 @@ void NeverClaimAutomaton::clear()
*
* ------------------------------------------------------------------------- */
{
for (vector<StateInfo*, ALLOC(StateInfo*) >::iterator
state = state_list.begin();
for (vector<StateInfo*>::iterator state = state_list.begin();
state != state_list.end();
++state)
delete (*state);
@ -158,8 +153,7 @@ void NeverClaimAutomaton::write(const char* output_filename)
* `-1'.
*/
for (vector<StateInfo*, ALLOC(StateInfo*) >::const_iterator
state = state_list.begin();
for (vector<StateInfo*>::const_iterator state = state_list.begin();
state != state_list.end();
++state)
{
@ -167,7 +161,7 @@ void NeverClaimAutomaton::write(const char* output_filename)
+ ((*state)->initial() ? "1" : "0") + ' '
+ ((*state)->accepting() ? "0 " : "") + "-1\n";
for (multimap<Cstr, Cstr*, less<Cstr>, ALLOC(Cstr*) >::const_iterator
for (multimap<Cstr, Cstr*>::const_iterator
transition = (*state)->transitions().begin();
transition != (*state)->transitions().end(); ++transition)
{
@ -272,7 +266,7 @@ NeverClaimAutomaton::StateInfo::~StateInfo()
*
* ------------------------------------------------------------------------- */
{
for (multimap<Cstr, Cstr*, less<Cstr>, ALLOC(Cstr*) >::const_iterator
for (multimap<Cstr, Cstr*>::const_iterator
transition = state_transitions.begin();
transition != state_transitions.end();
++transition)
@ -312,7 +306,7 @@ ParseErrorException::ParseErrorException
else
{
string space_string(msg.substr(0, error_pos));
for (string::size_type c = 0; c < msg.length(); c++)
for (string::size_type c = 0; c < space_string.length(); c++)
if (space_string[c] != ' ' && space_string[c] != '\t')
space_string[c] = ' ';

29
lbtt/src/NeverClaimAutomaton.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -93,12 +93,13 @@ public:
*/
private:
vector<StateInfo*, ALLOC(StateInfo*) > /* States of the */
state_list; /* automaton. */
vector<StateInfo*> state_list; /* States of the automaton.
*/
map<string, StateInfo*, less<string>, /* Mapping from state */
ALLOC(StateInfo*) > /* labels to the states */
label_mapping; /* itself. */
map<string, StateInfo*> label_mapping; /* Mapping from state
* labels to the states
* itself.
*/
StateInfo* current_state; /* Pointer to the state
* introduced most recently
@ -142,9 +143,9 @@ public:
/* of the state.
*/
const multimap<Cstr, Cstr*, less<Cstr>, /* Returns the labels of */
ALLOC(Cstr*) >& /* the state's successor */
transitions() const; /* states, including the
const multimap<Cstr, Cstr*>& transitions() const; /* Returns the labels of
* the state's successor
* states, including the
* conditions controlling
* the enabledness of the
* transition.
@ -174,8 +175,8 @@ private:
* accepting state?
*/
multimap<Cstr, Cstr*, less<Cstr>, ALLOC(Cstr*) > /* Labels of the state's */
state_transitions; /* successors, including
multimap<Cstr, Cstr*> state_transitions; /* Labels of the state's
* successors, including
* the guard formulae
* controlling the
* enabledness of the
@ -373,9 +374,7 @@ inline bool& NeverClaimAutomaton::StateInfo::accepting()
}
/* ========================================================================= */
inline const multimap<NeverClaimAutomaton::Cstr, NeverClaimAutomaton::Cstr*,
less<NeverClaimAutomaton::Cstr>,
ALLOC(NeverClaimAutomaton::Cstr*) >&
inline const multimap<NeverClaimAutomaton::Cstr, NeverClaimAutomaton::Cstr*>&
NeverClaimAutomaton::StateInfo::transitions() const
/* ----------------------------------------------------------------------------
*

67
lbtt/src/PathEvaluator.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -17,10 +17,6 @@
* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*/
#ifdef __GNUC__
#pragma implementation
#endif /* __GNUC__ */
#include <config.h>
#include <deque>
#include <stack>
@ -53,9 +49,8 @@ void PathEvaluator::reset()
current_loop_state = 0;
path_states.clear();
for (map<const LtlFormula*, BitArray*, LtlFormula::ptr_less,
ALLOC(BitArray*) >::iterator it
= eval_info.begin();
for (map<const LtlFormula*, BitArray*, LtlFormula::ptr_less>::iterator
it = eval_info.begin();
it != eval_info.end();
++it)
delete it->second;
@ -65,26 +60,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.
*
@ -92,13 +86,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();
}
@ -128,8 +130,7 @@ bool PathEvaluator::evaluate
current_formula = &formula;
current_path = &statespace;
map<StateSpace::size_type, StateSpace::size_type,
less<StateSpace::size_type>, ALLOC(StateSpace::size_type) > ordering;
map<StateSpace::size_type, StateSpace::size_type> ordering;
StateSpace::size_type state = statespace.initialState();
StateSpace::size_type state_count = 0;
@ -173,9 +174,7 @@ bool PathEvaluator::eval()
*
* ------------------------------------------------------------------------- */
{
stack<const LtlFormula*, deque<const LtlFormula*,
ALLOC(const LtlFormula*) > >
subformula_stack;
stack<const LtlFormula*, deque<const LtlFormula*> > subformula_stack;
const LtlFormula* f;
BitArray* val;

22
lbtt/src/PathEvaluator.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -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,
@ -105,15 +105,15 @@ private:
* the current path.
*/
vector<StateSpace::size_type, /* Correspondence */
ALLOC(StateSpace::size_type) > /* between states of the */
path_states; /* path and the states
vector<StateSpace::size_type> path_states; /* Correspondence
* between states of the
* path and the states
* of the current state
* space.
*/
map<const LtlFormula*, BitArray*, /* Information about the */
LtlFormula::ptr_less, ALLOC(BitArray*) > /* truth values of the */
LtlFormula::ptr_less> /* truth values of the */
eval_info; /* subformulae of the
* formula to be
* evaluated.

8
lbtt/src/PathIterator.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -17,10 +17,6 @@
* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*/
#ifdef __GNUC__
#pragma implementation
#endif /* __GNUC__ */
#include <config.h>
#include "BitArray.h"
#include "PathIterator.h"

8
lbtt/src/PathIterator.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -20,10 +20,6 @@
#ifndef PATHITERATOR_H
#define PATHITERATOR_H
#ifdef __GNUC__
#pragma interface
#endif /* __GNUC__ */
#include <config.h>
#include "StateSpace.h"

53
lbtt/src/Product.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -393,8 +393,8 @@ public:
typedef ProductEdgeCollection EdgeContainerType; /* required for making */
/* Product<Operations> */
struct PathElement; /* suitable for */
typedef deque<PathElement, ALLOC(PathElement) > /* instantiating the */
Path; /* SccCollection
typedef deque<PathElement> Path; /* instantiating the
* SccCollection
* template (see
* SccCollection.h).
*/
@ -419,9 +419,7 @@ private:
Graph<GraphEdgeContainer>::Path >& cycle, /* segment of the cycle */
size_type source_state_id, Edge transition, /* in a witness for the */
const size_type root_id, /* nonemptiness of the */
const map<size_type, PathElement, /* product. */
less<size_type>,
ALLOC(PathElement) >&
const map<size_type, PathElement>& /* product. */
predecessor) const;
Operations operations; /* Operations for
@ -524,8 +522,8 @@ public:
*/
private:
const Graph<GraphEdgeContainer>::Edge* edge_1; /* Components of the */
const Graph<GraphEdgeContainer>::Edge* edge_2; /* transition. */
GraphEdgeContainer::const_iterator edge_1; /* Components of the */
GraphEdgeContainer::const_iterator edge_2; /* transition. */
};
@ -655,9 +653,10 @@ protected:
* acceptance sets.
*/
typedef deque<AcceptanceStackElement, /* Stack formed from */
ALLOC(AcceptanceStackElement) > /* the above */
AcceptanceStack; /* associations. */
typedef deque<AcceptanceStackElement> /* Stack formed from */
AcceptanceStack; /* the above
* associations.
*/
AcceptanceStack acceptance_stack; /* Stack for storing the
* dfs numbers of roots
@ -877,9 +876,9 @@ private:
* reachable.
*/
set<size_type, less<size_type>, /* Set of states from */
ALLOC(size_type) > /* which an accepting */
reachability_info; /* component is known to
set<size_type> reachability_info; /* Set of states from
* which an accepting
* component is known to
* be reachable in the
* product.
*/
@ -928,9 +927,9 @@ public:
~AcceptingComponentFinder(); /* Destructor. */
typedef set<size_type, less<size_type>, /* Type definition for */
ALLOC(size_type) > /* the set of product */
SccType; /* state identifiers in
typedef set<size_type> SccType; /* Type definition for
* the set of product
* state identifiers in
* an accepting
* strongly connected
* component.
@ -1369,10 +1368,9 @@ void Product<Operations>::findWitness
unsigned long int number_of_collected_acceptance_sets
= collected_acceptance_sets.count(number_of_acceptance_sets);
deque<size_type, ALLOC(size_type) > search_queue;
set<size_type, less<size_type>, ALLOC(size_type) > visited;
map<size_type, PathElement, less<size_type>, ALLOC(PathElement) >
shortest_path_predecessor;
deque<size_type> search_queue;
set<size_type> visited;
map<size_type, PathElement> shortest_path_predecessor;
size_type bfs_root = search_start_state;
@ -1475,8 +1473,7 @@ void Product<Operations>::addCycleSegment
(pair<Graph<GraphEdgeContainer>::Path, Graph<GraphEdgeContainer>::Path>&
cycle,
size_type source_state_id, Edge transition, const size_type root_id,
const map<size_type, PathElement, less<size_type>, ALLOC(PathElement) >&
predecessor) const
const map<size_type, PathElement>& predecessor) const
/* ----------------------------------------------------------------------------
*
* Description: Helper function for constructing a segment of an accepting
@ -1598,7 +1595,7 @@ template <class Operations>
inline Product<Operations>::ProductEdge::ProductEdge
(const GraphEdgeContainer::const_iterator& e1,
const GraphEdgeContainer::const_iterator& e2)
: edge_1(*e1), edge_2(*e2)
: edge_1(e1), edge_2(e2)
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class Product<Operations>::ProductEdge.
@ -1643,7 +1640,7 @@ Product<Operations>::ProductEdge::firstComponent() const
*
* ------------------------------------------------------------------------- */
{
return *edge_1;
return **edge_1;
}
/* ========================================================================= */
@ -1662,7 +1659,7 @@ Product<Operations>::ProductEdge::secondComponent() const
*
* ------------------------------------------------------------------------- */
{
return *edge_2;
return **edge_2;
}
/* ========================================================================= */
@ -1679,7 +1676,7 @@ Product<Operations>::ProductEdge::targetNode() const
*
* ------------------------------------------------------------------------- */
{
return product->stateId(edge_1->targetNode(), edge_2->targetNode());
return product->stateId((*edge_1)->targetNode(), (*edge_2)->targetNode());
}

1063
lbtt/src/ProductAutomaton.cc Normal file
View file

File diff suppressed because it is too large Load diff

596
lbtt/src/ProductAutomaton.h Normal file
View file

@ -0,0 +1,596 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
* as published by the Free Software Foundation; either version 2
* of the License, or (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program; if not, write to the Free Software
* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*/
#ifndef PRODUCTAUTOMATON_H
#define PRODUCTAUTOMATON_H
#include <config.h>
#include <deque>
#include <iostream>
#include <vector>
#include "LbttAlloc.h"
#include "BitArray.h"
#include "BuchiAutomaton.h"
#include "EdgeContainer.h"
#include "Exception.h"
#include "Graph.h"
#include "StateSpace.h"
using namespace std;
extern bool user_break;
namespace UserCommands
{
extern void printAutomatonAnalysisResults
(ostream&, int, unsigned long int, unsigned long int);
}
namespace Graph
{
/******************************************************************************
*
* A class for representing the synchronous product of a Büchi automaton and
* a state space.
*
*****************************************************************************/
class ProductAutomaton : public Graph<GraphEdgeContainer>
{
private:
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
class ProductState : /* A class for */
public Graph<GraphEdgeContainer>::Node /* representing the */
{ /* states of the product
* automaton.
*/
public:
explicit ProductState /* Constructor. */
(const size_type hash_val = 0);
~ProductState(); /* Destructor. */
/* `edges' inherited from Graph<GraphEdgeContainer>::Node */
size_type hashValue() const; /* Get or set the hash */
size_type& hashValue(); /* value for the product
* state (this value can
* be used to extract
* the identifiers of
* the original state
* space and the Büchi
* automaton with which
* the product state is
* associated).
*/
void print /* Writes information */
(ostream& stream = cout, /* about the product */
const int indent = 0, /* state to a stream. */
const GraphOutputFormat fmt = NORMAL) const;
private:
friend class ProductAutomaton;
ProductState(const ProductState&); /* Prevent copying and */
ProductState& operator=(const ProductState&); /* assignment of
* ProductState objects.
*/
size_type hash_value; /* Hash value for the
* product state (can be
* used to extract the
* identifiers of the
* original state space and
* the Büchi automaton with
* which the product state
* is associated).
*/
Edge* incoming_edge; /* The unique edge pointing
* to `this' ProductState.
*/
};
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
class ProductScc : /* A class for storing */
public vector<ProductAutomaton::size_type, /* maximal strongly */
ALLOC(ProductAutomaton::size_type) > /* connected components */
{ /* of the product.
*/
public:
ProductScc(); /* Constructor. */
/* default copy constructor */
~ProductScc(); /* Destructor. */
/* default assignment operator */
bool fair /* Tests whether the */
(const ProductAutomaton& product_automaton) /* component is fair, */
const; /* i.e. it is a
* nontrivial component
* with a state from
* each acceptance set
* of the Büchi
* automaton used for
* constructing a
* given product.
*/
void insert /* Inserts a state into */
(const ProductAutomaton::size_type /* the container. */
product_state);
};
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
public:
class ProductSizeException; /* An exception class for
* reporting the situation
* where the size of the
* product automaton may
* be too big.
*/
friend class ProductScc;
friend void UserCommands::printAutomatonAnalysisResults
(ostream&, int, unsigned long int, unsigned long int);
ProductAutomaton(); /* Constructor. */
~ProductAutomaton(); /* Destructor. */
ProductState& operator[](const size_type index) /* Indexing operator. No */
const; /* range check is performed
* on the argument.
*/
ProductState& node(const size_type index) const; /* Synonym for the indexing
* operator. This function
* also checks the range of
* the argument.
*/
/* `size' inherited from Graph<GraphEdgeContainer> */
/* `empty' inherited from Graph<GraphEdgeContainer> */
void clear(); /* Makes the automaton
* empty.
*/
void connect /* Connects two states */
(const size_type father, /* of the product */
const size_type child); /* automaton. */
void disconnect /* Disconnects two */
(const size_type father, /* states of the product */
const size_type child); /* automaton. */
/* `connected' inherited from Graph<GraphEdgeContainer> */
/* `stats' inherited from Graph<GraphEdgeContainer> */
/* `subgraphStats' inherited from Graph<GraphEdgeContainer> */
void computeProduct /* Function for */
(const BuchiAutomaton& automaton, /* initializing the */
const StateSpace& statespace, /* product automaton. */
const bool global_product);
StateSpace::size_type systemState /* Returns the */
(const size_type state) const; /* identifier of the
* state of the original
* state space with
* which a given product
* state is associated.
*/
BuchiAutomaton::size_type buchiState /* Returns the */
(const size_type state) const; /* identifier of the
* state of the original
* automaton with which
* a given product state
* is associated.
*/
void emptinessCheck(Bitset& result) const; /* Performs an emptiness
* check on the product.
*/
void findAcceptingExecution /* Extracts an accepting */
(const StateSpace::size_type initial_state, /* execution from the */
pair<deque<StateIdPair, ALLOC(StateIdPair) >, /* product automaton. */
deque<StateIdPair,
ALLOC(StateIdPair) > >&
execution) const;
void print /* Writes information */
(ostream& stream = cout, /* about the product */
const int indent = 0, /* automaton to a */
const GraphOutputFormat fmt = NORMAL) const; /* stream. */
private:
ProductAutomaton(const ProductAutomaton&); /* Prevent copying and */
ProductAutomaton& operator= /* assignment of */
(const ProductAutomaton&); /* ProductAutomaton
* objects.
*/
size_type expand(size_type node_count = 1); /* Inserts states to the
* product automaton.
*/
const BuchiAutomaton* buchi_automaton; /* A pointer to the
* Büchi automaton used for
* constructing the
* product.
*/
StateSpace::size_type statespace_size; /* Size of the state space
* used for constructing
* the product automaton.
*/
#ifdef HAVE_OBSTACK_H /* Storage for product */
ObstackAllocator store; /* states and */
#endif /* HAVE_OBSTACK_H */ /* transitions. */
};
/******************************************************************************
*
* An exception class for reporting the situation where the product may be too
* big to compute.
*
*****************************************************************************/
class ProductAutomaton::ProductSizeException : public Exception
{
public:
ProductSizeException(); /* Constructor. */
/* default copy constructor */
~ProductSizeException() throw(); /* Destructor. */
ProductSizeException& /* Assignment operator. */
operator=(const ProductSizeException& e);
/* `what' inherited from class Exception */
};
/******************************************************************************
*
* Inline function definitions for class ProductAutomaton.
*
*****************************************************************************/
/* ========================================================================= */
inline ProductAutomaton::ProductAutomaton() :
buchi_automaton(0), statespace_size(0)
#ifdef HAVE_OBSTACK_H
, store()
#endif /* HAVE_OBSTACK_H */
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class ProductAutomaton. Initializes a
* new object for storing the product of a Büchi automaton and a
* state space. The product must then be explicitly initialized
* by calling the function `computeProduct' on the object.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline ProductAutomaton::~ProductAutomaton()
/* ----------------------------------------------------------------------------
*
* Description: Destructor for class ProductAutomaton.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
clear();
}
/* ========================================================================= */
inline ProductAutomaton::ProductState&
ProductAutomaton::operator[](const size_type index) const
/* ----------------------------------------------------------------------------
*
* Description: Indexing operator for class ProductAutomaton. Can be used to
* refer to the individual states of the product automaton. No
* range check will be performed on the argument.
*
* Argument: index -- Index of a state of the product automaton.
*
* Returns: A reference to the product state corresponding to the index.
*
* ------------------------------------------------------------------------- */
{
return static_cast<ProductState&>(*nodes[index]);
}
/* ========================================================================= */
inline ProductAutomaton::ProductState&
ProductAutomaton::node(const size_type index) const
/* ----------------------------------------------------------------------------
*
* Description: Function for referring to a single state of a
* ProductAutomaton. This function will also check the range
* argument.
*
* Argument: index -- Index of a state of the product automaton.
*
* Returns: A reference to the corresponding product state.
*
* ------------------------------------------------------------------------- */
{
return static_cast<ProductState&>(Graph<GraphEdgeContainer>::node(index));
}
/* ========================================================================= */
inline StateSpace::size_type ProductAutomaton::systemState
(const size_type state) const
/* ----------------------------------------------------------------------------
*
* Description: Returns the identifier of the system state with which a
* given product state is associated. This function will perform
* no range checks on its argument.
*
* Argument: state -- Identifier of a product state.
*
* Returns: Identifier of a state in a state space.
*
* ------------------------------------------------------------------------- */
{
return operator[](state).hashValue() % statespace_size;
}
/* ========================================================================= */
inline StateSpace::size_type ProductAutomaton::buchiState
(const size_type state) const
/* ----------------------------------------------------------------------------
*
* Description: Returns the identifier of the state of the Büchi automaton
* with which a given product state is associated. This function
* will perform no range checks on its argument.
*
* Argument: state -- Identifier of a product state.
*
* Returns: Identifier of a state in a Büchi automaton.
*
* ------------------------------------------------------------------------- */
{
return operator[](state).hashValue() / statespace_size;
}
/******************************************************************************
*
* Inline function definitions for class ProductAutomaton::ProductState.
*
*****************************************************************************/
/* ========================================================================= */
inline ProductAutomaton::ProductState::ProductState(const size_type hash_val) :
Graph<GraphEdgeContainer>::Node(), hash_value(hash_val), incoming_edge(0)
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class ProductAutomaton::ProductState. Creates
* a new object representing a synchronous product of a state of
* a Büchi automaton with a state of a state space.
*
* Arguments: hash_val -- Hash value for the product state.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline ProductAutomaton::ProductState::~ProductState()
/* ----------------------------------------------------------------------------
*
* Description: Destructor for class ProductAutomaton::ProductState.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
if (incoming_edge != 0)
{
#ifdef HAVE_OBSTACK_H
incoming_edge->~Edge();
#else
delete incoming_edge;
#endif /* HAVE_OBSTACK_H */
}
outgoing_edges.clear();
}
/* ========================================================================= */
inline ProductAutomaton::size_type ProductAutomaton::ProductState::hashValue()
const
/* ----------------------------------------------------------------------------
*
* Description: Returns the product state's hash value by value.
*
* Arguments: None.
*
* Returns: The hash value of the product state.
*
* ------------------------------------------------------------------------- */
{
return hash_value;
}
/* ========================================================================= */
inline ProductAutomaton::size_type& ProductAutomaton::ProductState::hashValue()
/* ----------------------------------------------------------------------------
*
* Description: Returns the product state's hash value by reference. (This
* function can therefore be used to change the value.)
*
* Arguments: None.
*
* Returns: A reference to the hash value of the product state.
*
* ------------------------------------------------------------------------- */
{
return hash_value;
}
/******************************************************************************
*
* Inline function definitions for class ProductAutomaton::ProductScc.
*
*****************************************************************************/
/* ========================================================================= */
inline ProductAutomaton::ProductScc::ProductScc()
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class ProductAutomaton::ProductScc. Creates a
* new container for storing a maximal strongly connected
* component of a ProductAutomaton.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline ProductAutomaton::ProductScc::~ProductScc()
/* ----------------------------------------------------------------------------
*
* Description: Destructor for class ProductAutomaton::ProductScc.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline void ProductAutomaton::ProductScc::insert
(const ProductAutomaton::size_type product_state)
/* ----------------------------------------------------------------------------
*
* Description: Inserts a new product state identifier to the container.
*
* Argument: product_state -- Identifier of a product state.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
push_back(product_state);
}
/******************************************************************************
*
* Inline function definitions for class
* ProductAutomaton::ProductSizeException.
*
*****************************************************************************/
/* ========================================================================= */
inline ProductAutomaton::ProductSizeException::ProductSizeException() :
Exception("product may be too large")
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class ProductAutomaton::ProductSizeException.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline ProductAutomaton::ProductSizeException::~ProductSizeException() throw()
/* ----------------------------------------------------------------------------
*
* Description: Destructor for class ProductAutomaton::ProductSizeException.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
inline ProductAutomaton::ProductSizeException&
ProductAutomaton::ProductSizeException::operator=
(const ProductAutomaton::ProductSizeException& e)
/* ----------------------------------------------------------------------------
*
* Description: Assignment operator for class
* ProductAutomaton::ProductSizeException. Assigns the value of
* another ProductAutomaton::ProductSizeException to `this' one.
*
* Arguments: e -- A reference to a constant
* ProductAutomaton::ProductSizeException.
*
* Returns: A reference to the object whose value was changed.
*
* ------------------------------------------------------------------------- */
{
Exception::operator=(e);
return *this;
}
}
#endif /* !PRODUCTAUTOMATON_H */

4
lbtt/src/Random.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License

34
lbtt/src/SccCollection.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -195,10 +195,8 @@ public:
/* default assignment operator */
typedef set<typename GraphType::size_type, /* Type definition for */
less<typename GraphType::size_type>, /* a set of node id's. */
ALLOC(typename GraphType::size_type) >
SccType;
typedef set<typename GraphType::size_type> /* Type definition for */
SccType; /* a set of node id's. */
const SccType& operator()() const; /* Returns the set of node
* identifiers in a
@ -338,10 +336,10 @@ public:
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
typedef map<typename GraphType::size_type, /* Type definition for a */
typename GraphType::size_type, /* mapping between node */
less<typename GraphType::size_type>, /* identifiers and the */
ALLOC(typename GraphType::size_type) >/* order in which they */
DfsOrdering; /* were encountered in
typename GraphType::size_type> /* mapping between node */
DfsOrdering; /* identifiers and the
* order in which they
* were encountered in
* the search for
* strongly connected
* components.
@ -433,18 +431,19 @@ public:
typename GraphType::size_type lowlink;
};
deque<NodeStackElement, /* Depth-first search */
ALLOC(NodeStackElement) > /* backtracking stack. */
node_stack;
deque<NodeStackElement> node_stack; /* Depth-first search
* backtracking stack.
*/
NodeStackElement* current_node; /* Pointer to the top
* element of the
* backtracking stack.
*/
deque<typename GraphType::size_type, /* Stack used for */
ALLOC(typename GraphType::size_type) > /* collecting the nodes */
scc_stack; /* in a strongly
deque<typename GraphType::size_type> scc_stack; /* Stack used for
* collecting the nodes
* in a strongly
* connected component,
* excluding the root
* nodes of the
@ -998,8 +997,7 @@ void SccCollection<GraphType, NodeVisitor>::iterator::getPath
* when exiting from this function).
*/
typename deque<NodeStackElement, ALLOC(NodeStackElement) >::const_iterator
n = node_stack.begin();
typename deque<NodeStackElement>::const_iterator n = node_stack.begin();
if (n != node_stack.end())
{
for (++n; n != node_stack.end(); ++n)

752
lbtt/src/SccIterator.h Normal file
View file

@ -0,0 +1,752 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
* as published by the Free Software Foundation; either version 2
* of the License, or (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program; if not, write to the Free Software
* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*/
#ifndef SCCITERATOR_H
#define SCCITERATOR_H
#include <config.h>
#include <deque>
#include <set>
#include <stack>
#include <vector>
#include "LbttAlloc.h"
#include "Graph.h"
using namespace std;
namespace Graph
{
/******************************************************************************
*
* A template iterator class for computing the maximal strongly connected
* components of a graph represented as an object of class
* Graph<EdgeContainer>.
*
* The iterator class has three template arguments:
* class EdgeContainer -- Container class storing the edges in the
* graph with which the iterator is associated.
*
* class SccContainer -- Container for storing the identifiers of the
* nodes belonging to some maximal strongly
* connected component. The container class
* must be able to store elements of type
* Graph<EdgeContainer>::size_type. The container
* class interface must support the following
* operations:
*
* Default constructor which can be called
* without any arguments
* Copy constructor
* Assignment operator
* clear()
* [makes the container empty]
* insert(Graph<EdgeContainer>::size_type s)
* [inserts an element into the
* container]
*
* If the container class is left unspecified,
* it defaults to
* set<Graph<EdgeContainer>::size_type,
* less<Graph<EdgeContainer>::size_type>,
* ALLOC(Graph<EdgeContainer>::size_type)>.
*
* class Filter -- Class for representing function objects that
* can be used to restrict the iterator
* dereferencing operators to return only
* those nodes of a strongly connected component
* which satisfy a certain condition that can be
* tested using Filter::operator(). This function
* has to accept a single parameter of type
* Graph<EdgeContainer>::Node*. It must return a
* Boolean value. The nodes for which the
* function returns `false' will then not be
* included in the collection of nodes returned
* by the iterator dereferencing operators.
*
* If the Filter class is left unspecified, it
* defaults to the NullSccFilter<EdgeContainer>
* class, which does not restrict the set of
* nodes in any way.
*
*****************************************************************************/
template<class EdgeContainer>
class NullSccFilter;
template<class EdgeContainer,
class SccContainer
= set<typename Graph<EdgeContainer>::size_type,
less<typename Graph<EdgeContainer>::size_type>,
ALLOC(typename Graph<EdgeContainer>::size_type) >,
class Filter = NullSccFilter<EdgeContainer> >
class SccIterator
{
public:
SccIterator(const Graph<EdgeContainer>& g); /* Constructor. */
/* default copy constructor */
~SccIterator(); /* Destructor. */
/* default assignment operator */
bool operator== /* Equality test for */
(const SccIterator<EdgeContainer, /* two iterators. */
SccContainer,
Filter>& it) const;
bool operator!= /* Inequality test for */
(const SccIterator<EdgeContainer, /* two iterators. */
SccContainer,
Filter>& it) const;
bool operator< /* `Less than' relation */
(const SccIterator<EdgeContainer, /* between two */
SccContainer, /* iterators. */
Filter>& it) const;
bool operator<= /* `Less than or equal' */
(const SccIterator<EdgeContainer, /* relation between two */
SccContainer, /* iterators. */
Filter>& it) const;
bool operator> /* `Greater than' */
(const SccIterator<EdgeContainer, /* relation between two */
SccContainer, /* iterators. */
Filter>& it) const;
bool operator>= /* `Greater than or */
(const SccIterator<EdgeContainer, /* equal' relation */
SccContainer, /* between two */
Filter>& it) const; /* iterators. */
const SccContainer& operator*() const; /* Dereferencing */
const SccContainer* operator->() const; /* operators. */
const SccContainer& operator++(); /* Prefix and postfix */
const SccContainer operator++(int); /* increment operators. */
bool atEnd() const; /* Tests whether the
* iterator has scanned
* through all the
* strongly connected
* components of the
* graph.
*/
private:
const Graph<EdgeContainer>& graph; /* Reference to the graph
* with which the iterator
* is associated.
*/
typename Graph<EdgeContainer>::size_type /* Number of graph */
dfs_number; /* nodes processed by
* the iterator.
*/
vector<typename Graph<EdgeContainer>::size_type, /* dfs_ordering[i] */
ALLOC(typename Graph<EdgeContainer> /* indicates the */
::size_type) > /* position of graph */
dfs_ordering; /* node i in the depth-
* first search order.
* (If the node has not
* yet been visited,
* dfs_ordering[i]==0.)
*/
vector<typename Graph<EdgeContainer>::size_type, /* lowlink[i] indicates */
ALLOC(typename Graph<EdgeContainer> /* the least graph node */
::size_type) > /* (in the depth-first */
lowlink; /* search order) that
* is reachable from
* graph node i and
* does not belong to
* any strongly
* connected component
* which has already been
* processed.
*/
typedef pair<typename Graph<EdgeContainer>::size_type,
typename EdgeContainer::const_iterator>
NodeStackElement;
stack<NodeStackElement, /* Depth-first search */
deque<NodeStackElement, /* backtracking stack. */
ALLOC(NodeStackElement) > >
node_stack;
typename Graph<EdgeContainer>::size_type /* Current graph node */
current_node; /* the depth-first
* search.
*/
typename EdgeContainer::const_iterator edge; /* Iterator to scan
* through the successors
* of the current node.
*/
stack<typename Graph<EdgeContainer>::size_type, /* Stack used for */
deque<typename Graph<EdgeContainer> /* collecting the nodes */
::size_type, /* in a strongly */
ALLOC(typename Graph<EdgeContainer> /* connected component. */
::size_type)
>
>
scc_stack;
SccContainer current_scc; /* Container of nodes
* forming the maximal
* strongly connected
* graph component
* currently `pointed to'
* by the iterator.
*/
Filter cond; /* Function object for
* filtering out a subset
* of nodes in the
* strongly connected
* components.
*/
void reset(); /* Initializes the
* iterator to point to
* the first strongly
* connected component of
* the graph.
*/
void computeNextScc(); /* Updates the iterator to
* point to the next
* strongly connected
* component.
*/
};
/******************************************************************************
*
* Default test for collecting the nodes in a strongly connected component.
* (See documentation on class SccIterator for information about the purpose
* of the class.)
*
*****************************************************************************/
template<class EdgeContainer>
class NullSccFilter
{
public:
bool operator()(const typename Graph<EdgeContainer>::Node*) const;
};
/******************************************************************************
*
* Inline function definitions for template class
* SccIterator<EdgeContainer, SccContainer, Filter>.
*
*****************************************************************************/
/* ========================================================================= */
template<class EdgeContainer, class SccContainer, class Filter>
inline SccIterator<EdgeContainer, SccContainer, Filter>::SccIterator
(const Graph<EdgeContainer>& g) :
graph(g), dfs_ordering(graph.size()), lowlink(graph.size())
/* ----------------------------------------------------------------------------
*
* Description: Constructor for class
* SccIterator<EdgeContainer, SccContainer, Filter>.
* Initializes a new iterator for scanning the maximal strongly
* connected components of a graph.
*
* Arguments: g -- The graph with which the iterator is to be associated
* (a Graph<EdgeContainer> object).
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
reset();
computeNextScc();
}
/* ========================================================================= */
template<class EdgeContainer, class SccContainer, class Filter>
inline SccIterator<EdgeContainer, SccContainer, Filter>::~SccIterator()
/* ----------------------------------------------------------------------------
*
* Description: Destructor for class
* SccIterator<EdgeContainer, SccContainer, Filter>.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
}
/* ========================================================================= */
template<class EdgeContainer, class SccContainer, class Filter>
inline bool SccIterator<EdgeContainer, SccContainer, Filter>::operator==
(const SccIterator<EdgeContainer, SccContainer, Filter>& it) const
/* ----------------------------------------------------------------------------
*
* Description: Equality test for two SccIterators. Two SccIterators are
* `equal' if and only if both of them are associated with
* exactly the same graph object in memory and the iterators
* have processed the same amount of graph nodes.
*
* Arguments: it -- A constant reference to another SccIterator.
*
* Returns: A truth value according to the result of the equality test.
*
* ------------------------------------------------------------------------- */
{
return (&graph == &(it.graph) && dfs_number == it.dfs_number);
}
/* ========================================================================= */
template<class EdgeContainer, class SccContainer, class Filter>
inline bool SccIterator<EdgeContainer, SccContainer, Filter>::operator!=
(const SccIterator<EdgeContainer, SccContainer, Filter>& it) const
/* ----------------------------------------------------------------------------
*
* Description: Inequality test for two SccIterators. Two SccIterators are
* not equal if and only if they are associated with different
* graphs or they are associated with the same graph object in
* memory but the iterators have processed a different number of
* graph nodes.
*
* Arguments: it -- A constant reference to another SccIterator.
*
* Returns: A truth value according to the result of the inequality test.
*
* ------------------------------------------------------------------------- */
{
return (&graph != &(it.graph) || dfs_number != it.dfs_number);
}
/* ========================================================================= */
template<class EdgeContainer, class SccContainer, class Filter>
inline bool SccIterator<EdgeContainer, SccContainer, Filter>::operator<
(const SccIterator<EdgeContainer, SccContainer, Filter>& it) const
/* ----------------------------------------------------------------------------
*
* Description: `Less than' relation between two SccIterators. An
* SccIterator is `less than' another if and only if the
* iterators relate to the same graph object in memory and
* the first iterator has processed a smaller number of nodes
* than the second one.
*
* Arguments: it -- A constant reference to another SccIterator.
*
* Returns: A truth value according to the result of the test.
*
* ------------------------------------------------------------------------- */
{
return (&graph == &(it.graph) && dfs_number < it.dfs_number);
}
/* ========================================================================= */
template<class EdgeContainer, class SccContainer, class Filter>
inline bool SccIterator<EdgeContainer, SccContainer, Filter>::operator<=
(const SccIterator<EdgeContainer, SccContainer, Filter>& it) const
/* ----------------------------------------------------------------------------
*
* Description: `Less than or equal' relation between two SccIterators. An
* SccIterator is `less than or equal to' another if and only
* if the iterators relate to the same graph object in memory
* and the first iterator has processed a number of nodes not
* exceeding the number of nodes the second iterator has
* processed.
*
* Arguments: it -- A constant reference to another SccIterator.
*
* Returns: A truth value according to the result of the test.
*
* ------------------------------------------------------------------------- */
{
return (&graph == &(it.graph) && dfs_number <= it.dfs_number);
}
/* ========================================================================= */
template<class EdgeContainer, class SccContainer, class Filter>
inline bool SccIterator<EdgeContainer, SccContainer, Filter>::operator>
(const SccIterator<EdgeContainer, SccContainer, Filter>& it) const
/* ----------------------------------------------------------------------------
*
* Description: `Greater than' relation between two SccIterators. An
* SccIterator is `greater than' another if and only if the
* iterators relate to the same graph object in memory and
* the first iterator has processed a greater number of nodes
* than the second one.
*
* Arguments: it -- A constant reference to another SccIterator.
*
* Returns: A truth value according to the result of the test.
*
* ------------------------------------------------------------------------- */
{
return (&graph == &(it.graph) && dfs_number > it.dfs_number);
}
/* ========================================================================= */
template<class EdgeContainer, class SccContainer, class Filter>
inline bool SccIterator<EdgeContainer, SccContainer, Filter>::operator>=
(const SccIterator<EdgeContainer, SccContainer, Filter>& it) const
/* ----------------------------------------------------------------------------
*
* Description: `Greater than or equal' relation between two SccIterators. An
* SccIterator is `greater than or equal to' another if and
* only if the iterators relate to the same graph object in
* memory and the first iterator has processed at least as many
* nodes as the second iterator has processed.
*
* Arguments: it -- A constant reference to another SccIterator.
*
* Returns: A truth value according to the result of the test.
*
* ------------------------------------------------------------------------- */
{
return (&graph == &(it.graph) && dfs_number >= it.dfs_number);
}
/* ========================================================================= */
template<class EdgeContainer, class SccContainer, class Filter>
inline const SccContainer&
SccIterator<EdgeContainer, SccContainer, Filter>::operator*() const
/* ----------------------------------------------------------------------------
*
* Description: Dereferencing operator for a SccIterator. Returns the
* collection of nodes which belong to the maximal strongly
* connected component that the iterator currently points to.
*
* Arguments: None.
*
* Returns: A collection of nodes representing some maximal strongly
* connected component.
*
* ------------------------------------------------------------------------- */
{
return current_scc;
}
/* ========================================================================= */
template<class EdgeContainer, class SccContainer, class Filter>
inline const SccContainer*
SccIterator<EdgeContainer, SccContainer, Filter>::operator->() const
/* ----------------------------------------------------------------------------
*
* Description: Dereferencing operator for a SccIterator. Returns the
* collection of nodes which belong to the maximal strongly
* connected component that the iterator currently points to.
*
* Arguments: None.
*
* Returns: A collection of nodes representing some maximal strongly
* connected component.
*
* ------------------------------------------------------------------------- */
{
return &current_scc;
}
/* ========================================================================= */
template<class EdgeContainer, class SccContainer, class Filter>
inline const SccContainer&
SccIterator<EdgeContainer, SccContainer, Filter>::operator++()
/* ----------------------------------------------------------------------------
*
* Description: Prefix increment operator for a SccIterator. Computes the
* next maximal strongly connected component of the graph and
* then returns it.
*
* Arguments: None.
*
* Returns: A collection of nodes representing some maximal strongly
* connected component.
*
* ------------------------------------------------------------------------- */
{
computeNextScc();
return current_scc;
}
/* ========================================================================= */
template<class EdgeContainer, class SccContainer, class Filter>
inline const SccContainer
SccIterator<EdgeContainer, SccContainer, Filter>::operator++(int)
/* ----------------------------------------------------------------------------
*
* Description: Postfix increment operator for a SccIterator. Effectively
* returns the maximal strongly connected component of the graph
* currently pointed to by the iterator and then updates the
* iterator to point to the next strongly connected component.
*
* Arguments: None (the `int' is only required to distinguish this operator
* from the prefix increment operator).
*
* Returns: A collection of nodes representing some maximal strongly
* connected component.
*
* ------------------------------------------------------------------------- */
{
SccContainer old_scc = current_scc;
computeNextScc();
return old_scc;
}
/* ========================================================================= */
template<class EdgeContainer, class SccContainer, class Filter>
inline bool SccIterator<EdgeContainer, SccContainer, Filter>::atEnd() const
/* ----------------------------------------------------------------------------
*
* Description: Tells whether there are still more strongly connected
* components in the graph for the iterator to process.
*
* Arguments: None.
*
* Returns: A truth value.
*
* ------------------------------------------------------------------------- */
{
return (current_node == graph.size());
}
/******************************************************************************
*
* Function definitions for template class
* SccIterator<EdgeContainer, SccContainer, Filter>.
*
*****************************************************************************/
/* ========================================================================= */
template<class EdgeContainer, class SccContainer, class Filter>
void SccIterator<EdgeContainer, SccContainer, Filter>::reset()
/* ----------------------------------------------------------------------------
*
* Description: Initializes the iterator to point to the first maximal
* strongly connected component of the graph with which the
* iterator it associated.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
dfs_number = 0;
for (typename vector<typename Graph<EdgeContainer>::size_type,
ALLOC(typename Graph<EdgeContainer>::size_type) >
::iterator node = dfs_ordering.begin();
node != dfs_ordering.end();
++node)
*node = 0;
while (!node_stack.empty())
node_stack.pop();
while (!scc_stack.empty())
scc_stack.pop();
current_scc.clear();
}
/* ========================================================================= */
template<class EdgeContainer, class SccContainer, class Filter>
void SccIterator<EdgeContainer, SccContainer, Filter>::computeNextScc()
/* ----------------------------------------------------------------------------
*
* Description: Updates the state of the iterator to `point to' the next
* maximal strongly connected component of the graph, using the
* algorithm due to Tarjan [R. Tarjan. Depth-first search and
* linear graph algorithms. SIAM Journal on Computing,
* 1(2):146--160, June 1972] for computing the next maximal
* strongly connected component of the graph.
*
* Arguments: None.
*
* Returns: Nothing.
*
* ------------------------------------------------------------------------- */
{
current_scc.clear();
if (scc_stack.empty() && node_stack.empty())
{
/*
* If both `scc_stack' and `node_stack' are empty (this holds if we have
* recently finished processing some component of the graph), try to find
* a graph node that has not yet been visited. If no such node is found,
* all nodes have been visited and there are no more strongly connected
* components to be found in the graph.
*/
current_node = 0;
for (typename vector<typename Graph<EdgeContainer>::size_type,
ALLOC(typename Graph<EdgeContainer>::size_type) >
::const_iterator node = dfs_ordering.begin();
node != dfs_ordering.end() && (*node) != 0;
++node)
++current_node;
if (current_node == graph.size())
return;
/*
* Prepare to continue the depth-first search in the unvisited node.
*/
edge = graph[current_node].edges().begin();
scc_stack.push(current_node);
++dfs_number;
dfs_ordering[current_node] = lowlink[current_node] = dfs_number;
}
typename Graph<EdgeContainer>::size_type child_node;
while (1)
{
/*
* If there are still nodes left in the depth-first search backtracking
* stack, pop a node and its next unprocessed outgoing edge off the stack.
* Before continuing the depth-first search in the popped node, update
* its lowlink value if necessary. (This has to be done if the lowlink of
* the current node---a successor of the popped node---is less than the
* lowlink of the popped node but not equal to zero.)
*/
if (!node_stack.empty())
{
typename Graph<EdgeContainer>::size_type father_node
= node_stack.top().first;
edge = node_stack.top().second;
node_stack.pop();
if (lowlink[current_node] < lowlink[father_node]
&& lowlink[current_node] != 0)
lowlink[father_node] = lowlink[current_node];
current_node = father_node;
}
/*
* Scan through the successors of the current node.
*
* If the current nodes has an unvisited successor node (a successor i
* with dfs_ordering[i] == 0), push the current node and its next
* unprocessed edge onto the backtracking stack and then continue the
* search in the successor node. Push also the successor node onto the
* strongly connected component stack.
*
* Otherwise, update the lowlink of the current node to the lowlink of
* its already visited successor if necessary.
*/
while (edge != graph[current_node].edges().end())
{
child_node = (*edge)->targetNode();
++edge;
if (dfs_ordering[child_node] == 0)
{
node_stack.push(make_pair(current_node, edge));
scc_stack.push(child_node);
++dfs_number;
dfs_ordering[child_node] = lowlink[child_node] = dfs_number;
current_node = child_node;
edge = graph[current_node].edges().begin();
}
else if (lowlink[child_node] < lowlink[current_node]
&& lowlink[child_node] != 0)
lowlink[current_node] = lowlink[child_node];
}
/*
* If the least node in the depth-first search order reachable from the
* current node is the current node itself at the end of the previous
* loop, we have found a maximal strongly connected component of the
* graph. In this case, collect the states satisfying `cond' in the
* strongly connected component stack to form the component and exit.
* (Otherwise, return to the start of the outermost while loop and
* continue by popping a state off the depth-first search backtracking
* stack.)
*/
if (dfs_ordering[current_node] == lowlink[current_node])
{
do
{
child_node = scc_stack.top();
scc_stack.pop();
if (cond(&graph[child_node]))
current_scc.insert(child_node);
lowlink[child_node] = 0;
}
while (child_node != current_node);
break;
}
}
}
/******************************************************************************
*
* Inline function definitions for template class NullSccFilter<EdgeContainer>.
*
*****************************************************************************/
/* ========================================================================= */
template<class EdgeContainer>
inline bool NullSccFilter<EdgeContainer>::operator()
(const typename Graph<EdgeContainer>::Node*) const
/* ----------------------------------------------------------------------------
*
* Description: Default test for filtering the nodes in a strongly connected
* graph component. The default is to simply include all nodes
* in the result.
*
* Arguments: A constant pointer to a Graph<EdgeContainer>::Node (required
* only to satisfy the class interface requirements).
*
* Returns: true, so the test will succeed for every node in the
* component.
*
* ------------------------------------------------------------------------- */
{
return true;
}
}
#endif /* !SCCITERATOR_H */

18
lbtt/src/SharedTestData.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -42,14 +42,14 @@ extern TestRoundInfo round_info; /* Data structure for
* round.
*/
extern vector<AlgorithmTestResults, /* Test results for each */
ALLOC(AlgorithmTestResults) > /* implementation. */
test_results;
extern vector<TestStatistics, /* Overall test */
ALLOC(TestStatistics) > /* statistics for each */
final_statistics; /* implementation. */
extern vector<AlgorithmTestResults> test_results; /* Test results for each
* implementation.
*/
extern vector<TestStatistics> final_statistics; /* Overall test
* statistics for each
* implementation.
*/
}
#endif /* !SHAREDTESTDATA_H */

8
lbtt/src/SpinWrapper.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -17,10 +17,6 @@
* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*/
#ifdef __GNUC__
#pragma implementation
#endif /* __GNUC__ */
#include <config.h>
#ifdef HAVE_SSTREAM
#include <sstream>

8
lbtt/src/SpinWrapper.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -20,10 +20,6 @@
#ifndef SPINWRAPPER_H
#define SPINWRAPPER_H
#ifdef __GNUC__
#pragma interface
#endif /* __GNUC__ */
#include <config.h>
#include <string>
#include "ExternalTranslator.h"

598
lbtt/src/StatDisplay.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -17,14 +17,11 @@
* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*/
#ifdef __GNUC__
#pragma implementation
#endif /* __GNUC__ */
#include <config.h>
#include <string>
#include "DispUtil.h"
#include "Exception.h"
#include "IntervalList.h"
#include "SharedTestData.h"
#include "StatDisplay.h"
#include "StringUtil.h"
@ -37,11 +34,51 @@ 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,
vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type
algorithm,
vector<AlgorithmTestResults>::size_type algorithm,
int result_id)
/* ----------------------------------------------------------------------------
*
@ -52,7 +89,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
@ -67,43 +104,75 @@ 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();
}
/* ========================================================================= */
void printProductAutomatonStats
(ostream& stream, int indent,
vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type
algorithm,
vector<AlgorithmTestResults>::size_type algorithm,
int result_id)
/* ----------------------------------------------------------------------------
*
@ -114,7 +183,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
@ -129,51 +198,71 @@ 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();
}
/* ========================================================================= */
void printAcceptanceCycleStats
(ostream& stream, int indent,
vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type
algorithm,
vector<AlgorithmTestResults>::size_type algorithm,
int result_id)
/* ----------------------------------------------------------------------------
*
@ -185,7 +274,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.
@ -201,49 +290,64 @@ 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();
}
/* ========================================================================= */
void printConsistencyCheckStats
(ostream& stream, int indent,
vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type
algorithm)
vector<AlgorithmTestResults>::size_type algorithm)
/* ----------------------------------------------------------------------------
*
* Description: Displays information about the consistency check result for
@ -253,7 +357,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.
*
@ -264,100 +368,113 @@ 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();
for (vector<AlgorithmTestResults>::size_type 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)
@ -385,89 +502,75 @@ 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;
for (vector<AlgorithmTestResults>::size_type 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]
@ -482,7 +585,7 @@ void printBuchiIntersectionCheckStats
estream << string(counter == -1 ? "N/A " : "failed") + ' ';
if (alg_1 != alg_2)
if (*alg_1 != alg_2)
{
estream << '(';
if (pos_test)
@ -493,9 +596,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)
@ -511,18 +614,18 @@ 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();
}
/* ========================================================================= */
void printAllStats
(ostream& stream, int indent,
vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >::size_type
algorithm)
vector<AlgorithmTestResults>::size_type algorithm)
/* ----------------------------------------------------------------------------
*
* Description: Displays all test information (Büchi automaton and product
@ -541,30 +644,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);
}
@ -575,8 +694,8 @@ void printAllStats
/* ========================================================================= */
void printCollectiveCrossComparisonStats
(ostream& stream,
vector<TestStatistics, ALLOC(TestStatistics) >::size_type algorithm_y,
vector<TestStatistics, ALLOC(TestStatistics) >::size_type algorithm_x,
vector<TestStatistics>::size_type algorithm_y,
vector<TestStatistics>::size_type algorithm_x,
int data_type)
/* ----------------------------------------------------------------------------
*
@ -630,10 +749,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;
@ -768,13 +885,12 @@ void printCollectiveStats(ostream& stream, int indent)
if (round_info.num_processed_formulae > 0
&& configuration.global_options.formula_input_filename.empty())
{
const map<unsigned long int, unsigned long int, less<unsigned long int>,
ALLOC(unsigned long int) >&
const map<unsigned long int, unsigned long int>&
proposition_statistics
= configuration.formula_options.formula_generator.
propositionStatistics();
const map<int, unsigned long int, less<int>, ALLOC(unsigned long int) >
const map<int, unsigned long int>
symbol_statistics
= configuration.formula_options.formula_generator.symbolStatistics();
@ -820,9 +936,8 @@ void printCollectiveStats(ostream& stream, int indent)
number_of_symbols_printed++;
}
for (map<unsigned long int, unsigned long int,
less<unsigned long int>, ALLOC(unsigned long int) >
::const_iterator proposition = proposition_statistics.begin();
for (map<unsigned long int, unsigned long int>::const_iterator
proposition = proposition_statistics.begin();
proposition != proposition_statistics.end();
++proposition)
{
@ -869,8 +984,8 @@ void printCollectiveStats(ostream& stream, int indent)
= "";
number_of_symbols_printed = 0;
for (map<int, unsigned long int, less<int>, ALLOC(unsigned long int) >
::const_iterator op = symbol_statistics.begin();
for (map<int, unsigned long int>::const_iterator
op = symbol_statistics.begin();
op != symbol_statistics.end();
++op)
{
@ -912,6 +1027,8 @@ void printCollectiveStats(ostream& stream, int indent)
if (number_of_symbols_printed % 5 != 0)
{
if (number_of_symbols_printed > 5)
estream << '\n';
estream << ind + " operator " + symbol_name_string + '\n'
+ ind + " # " + symbol_number_string + '\n'
+ ind + " #/formula " + symbol_distribution_string
@ -953,8 +1070,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)
{
@ -967,14 +1087,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++)
{
@ -1119,7 +1239,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, ' ')
@ -1339,8 +1459,7 @@ void printCollectiveStats(ostream& stream, int indent)
estream << ind + " Result inconsistency statistics\n"
+ ind + " " + string(31, '=') + '\n';
vector<TestStatistics, ALLOC(TestStatistics) >::size_type
algorithm_x, algorithm_y;
vector<TestStatistics>::size_type algorithm_x, algorithm_y;
for (algorithm_x = 0; algorithm_x < number_of_algorithms;
algorithm_x += 2)
@ -1352,7 +1471,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(), ' ');
}
@ -1362,6 +1481,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)
@ -1372,7 +1494,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;

49
lbtt/src/StatDisplay.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -42,65 +42,60 @@ 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. */
vector<AlgorithmTestResults,
ALLOC(AlgorithmTestResults) >::size_type
vector<AlgorithmTestResults>::size_type
algorithm,
int result_id);
void printProductAutomatonStats /* Displays information */
(ostream& stream, /* about a product */
int indent, /* automaton. */
vector<AlgorithmTestResults,
ALLOC(AlgorithmTestResults) >::size_type
vector<AlgorithmTestResults>::size_type
algorithm,
int result_id);
void printAcceptanceCycleStats /* Displays information */
(ostream& stream, /* about the acceptance */
int indent, /* cycles of a product */
vector<AlgorithmTestResults, /* automaton. */
ALLOC(AlgorithmTestResults) >::size_type
vector<AlgorithmTestResults>::size_type /* automaton. */
algorithm,
int result_id);
void printConsistencyCheckStats /* Displays the result */
(ostream& stream, /* of the consistency */
int indent, /* check for a given */
vector<AlgorithmTestResults, /* algorithm. */
ALLOC(AlgorithmTestResults) >::size_type
vector<AlgorithmTestResults>::size_type /* algorithm. */
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 */
int indent, /* information displayed */
vector<TestStatistics, /* by the previous five */
ALLOC(TestStatistics)>::size_type /* functions. */
algorithm);
vector<TestStatistics>::size_type algorithm); /* by the previous five
* functions.
*/
void printCollectiveCrossComparisonStats /* Displays a single */
(ostream& stream, /* `cell' of the final */
vector<TestStatistics, /* result cross- */
ALLOC(TestStatistics) >::size_type /* comparison table. */
algorithm_y,
vector<TestStatistics,
ALLOC(TestStatistics) >::size_type
algorithm_x,
vector<TestStatistics>::size_type algorithm_y, /* result cross- */
vector<TestStatistics>::size_type algorithm_x, /* comparison table. */
int data_type);
void printCollectiveStats /* Displays average test */

11
lbtt/src/StateSpace.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -17,10 +17,6 @@
* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*/
#ifdef __GNUC__
#pragma implementation
#endif /* __GNUC__ */
#include <config.h>
#include <map>
#include "DispUtil.h"
@ -148,8 +144,7 @@ void StateSpace::clear()
initial_state = 0;
#ifdef HAVE_OBSTACK_H
for (vector<Node*, ALLOC(Node*) >::iterator state = nodes.begin();
state != nodes.end();
for (vector<Node*>::iterator state = nodes.begin(); state != nodes.end();
++state)
static_cast<State*>(*state)->~State();

4
lbtt/src/StateSpace.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License

4
lbtt/src/StateSpaceProduct.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License

8
lbtt/src/StateSpaceRandomizer.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -174,9 +174,7 @@ StateSpace* StateSpaceRandomizer::generateConnectedGraph() const
StateSpace::size_type first_unreachable_state = 1, random_node;
multimap<long int, StateSpace::size_type, less<long int>,
ALLOC(StateSpace::size_type) >
reachable_but_unprocessed;
multimap<long int, StateSpace::size_type> reachable_but_unprocessed;
reachable_but_unprocessed.insert(make_pair(0, 0));

8
lbtt/src/StateSpaceRandomizer.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -20,10 +20,6 @@
#ifndef STATESPACERANDOMIZER_H
#define STATESPACERANDOMIZER_H
#ifdef __GNUC__
#pragma interface
#endif /* __GNUC__ */
#include <config.h>
#include "Random.h"
#include "StateSpace.h"

525
lbtt/src/StringUtil.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -17,11 +17,9 @@
* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*/
#ifdef __GNUC__
#pragma implementation
#endif /* __GNUC__ */
#include <config.h>
#include <cctype>
#include <climits>
#include <cstdlib>
#include "StringUtil.h"
@ -63,8 +61,7 @@ string toString(const double d, const int precision, const ios::fmtflags flags)
/* ========================================================================= */
void sliceString
(const string& s, const char* slice_chars,
vector<string, ALLOC(string) >& slices)
(const string& s, const char* slice_chars, vector<string>& slices)
/* ----------------------------------------------------------------------------
*
* Description: Slices a string into a vector of strings, using a given set
@ -104,6 +101,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)
/* ----------------------------------------------------------------------------
@ -119,9 +321,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 + "'");
@ -129,98 +333,253 @@ 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;
number_set.clear();
for (vector<string, ALLOC(string) >::const_iterator
interval = intervals.begin();
interval != intervals.end();
++interval)
if (token != "*")
{
if (*interval == "*")
string::size_type pos(token.find_first_of("-"));
if (pos == string::npos)
pos = token.find("...");
string value(token.substr(0, pos));
if (!value.empty())
{
for (unsigned long int i = min; i <= max; i++)
number_set.insert(i);
break;
tmp_min = parseNumber(value);
if (pos == string::npos)
tmp_max = tmp_min;
interval_type |= LEFT_BOUNDED;
}
dash_pos = (*interval).find_first_of("-");
if (pos != string::npos)
value = token.substr(pos + (token[pos] == '-' ? 1 : 3));
if (dash_pos == (*interval).npos)
number_set.insert(parseNumber(*interval));
else
if (!value.empty())
{
if (dash_pos == 0)
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>* 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> interval_strings;
int interval_type;
intervals.clear();
sliceString(token, ",", interval_strings);
for (vector<string>::const_iterator i = interval_strings.begin();
i != interval_strings.end();
++i)
{
unsigned long int i_start, i_end;
try
{
interval_type = parseInterval(*i, i_start, i_end);
}
catch (const NotANumberException&)
{
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;
}
}

176
lbtt/src/StringUtil.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -31,6 +31,7 @@
#include <vector>
#include "LbttAlloc.h"
#include "Exception.h"
#include "IntervalList.h"
using namespace std;
@ -57,22 +58,71 @@ template<typename T> string toString(const T& t); /* Template function for
void sliceString /* Breaks a string into */
(const string& s, const char* slice_chars, /* `slices', using a */
vector<string, ALLOC(string) >& slices); /* given set of
vector<string>& slices); /* given set of
* characters as
* 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>* extra_tokens = 0); /* union of the
* 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 +183,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 +271,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 */

4
lbtt/src/TempFsysName.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License

4
lbtt/src/TempFsysName.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License

1221
lbtt/src/TestOperations.cc
View file

File diff suppressed because it is too large Load diff

38
lbtt/src/TestOperations.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -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 */
@ -90,32 +95,25 @@ void writeFormulaeToFiles(); /* Writes LTL formulas */
void generateBuchiAutomaton /* Generates a Büchi */
(int f, /* automaton from a LTL */
vector<Configuration::AlgorithmInformation, /* formula stored in a */
ALLOC(Configuration::AlgorithmInformation) > /* given file, using a */
::size_type /* given LTL-to-Büchi */
algorithm_id); /* translation algorithm
vector<Configuration::AlgorithmInformation> /* formula stored in a */
::size_type /* given file, using a */
algorithm_id); /* given LTL-to-Büchi
* translation algorithm
* 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. */
ALLOC(Configuration::AlgorithmInformation) >
vector<Configuration::AlgorithmInformation> /* automaton. */
::size_type
algorithm_id);
void performConsistencyCheck /* Performs a */
(vector<Configuration::AlgorithmInformation, /* consistency check on */
ALLOC(Configuration::AlgorithmInformation) > /* the test results */
::size_type /* for a formula and its */
algorithm_id); /* negation. */
(vector<Configuration::AlgorithmInformation> /* consistency check on */
::size_type /* the test results */
algorithm_id); /* for a formula and its
* negation.
*/
void compareResults(); /* Compares the model
* checking results

51
lbtt/src/TestRoundInfo.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -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;
@ -55,7 +55,11 @@ public:
* stream for messages.
*/
ifstream formula_input_file; /* Stream for reading input
istream* formula_input_stream; /* Stream for reading input
* formulae.
*/
ifstream formula_input_file; /* File for reading input
* formulae.
*/
@ -90,6 +94,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 +130,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
@ -150,9 +153,9 @@ public:
* current round.
*/
vector<class ::Ltl::LtlFormula*, /* Formulae used in the */
ALLOC(class ::Ltl::LtlFormula*) > /* current round: */
formulae; /* formulae[0]:
vector<class ::Ltl::LtlFormula*> formulae; /* Formulae used in the
* current round:
* formulae[0]:
* positive formula in
* negation normal
* form
@ -168,7 +171,7 @@ public:
* generated
*/
vector<bool, ALLOC(bool) > formula_in_file; /* The values in this
vector<bool> formula_in_file; /* The values in this
* vector will be set to
* true when the
* corresponding
@ -181,10 +184,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 +209,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 +229,7 @@ inline TestRoundInfo::TestRoundInfo() :
*
* ------------------------------------------------------------------------- */
{
formula_file_name[0] = formula_file_name[1] = 0;
}
/* ========================================================================= */

13
lbtt/src/TestStatistics.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -17,10 +17,6 @@
* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*/
#ifdef __GNUC__
#pragma implementation
#endif /* __GNUC__ */
#include <config.h>
#include "TestStatistics.h"
@ -54,8 +50,7 @@ void AlgorithmTestResults::emptinessReset()
automaton_stats[i].emptiness_check_result.clear();
automaton_stats[i].emptiness_check_performed = false;
for (vector<AutomatonStats::CrossComparisonStats,
ALLOC(AutomatonStats::CrossComparisonStats) >::iterator it
for (vector<AutomatonStats::CrossComparisonStats>::iterator it
= automaton_stats[i].cross_comparison_stats.begin();
it != automaton_stats[i].cross_comparison_stats.end();
++it)
@ -91,7 +86,7 @@ void AlgorithmTestResults::fullReset()
automaton_stats[i].number_of_msccs = 0;
automaton_stats[i].buchi_generation_time = 0.0;
for (vector<int, ALLOC(int) >::iterator it
for (vector<int>::iterator it
= automaton_stats[i].buchi_intersection_check_stats.begin();
it != automaton_stats[i].buchi_intersection_check_stats.end();
++it)

118
lbtt/src/TestStatistics.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -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;
/******************************************************************************
*
@ -43,9 +43,8 @@ using Graph::ProductAutomaton;
struct AutomatonStats
{
explicit AutomatonStats /* Constructor. */
(vector<Configuration::AlgorithmInformation,
ALLOC(Configuration::AlgorithmInformation) >
::size_type number_of_algorithms,
(vector<Configuration::AlgorithmInformation>
::size_type number_of_algorithms,
StateSpace::size_type max_statespace_size);
/* default copy constructor */
@ -107,7 +106,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
@ -127,9 +126,9 @@ struct AutomatonStats
typedef pair<bool, unsigned long int>
CrossComparisonStats;
vector<CrossComparisonStats, /* Emptiness check */
ALLOC(CrossComparisonStats) > /* cross-comparison */
cross_comparison_stats; /* results. The `first'
vector<CrossComparisonStats> /* Emptiness check */
cross_comparison_stats; /* cross-comparison
* results. The `first'
* element of the pair
* tells whether a cross-
* comparison with a given
@ -142,8 +141,8 @@ struct AutomatonStats
* differ.
*/
vector<int, ALLOC(int) > /* Büchi automaton */
buchi_intersection_check_stats; /* intersection
vector<int> buchi_intersection_check_stats; /* Büchi automaton
* intersection
* emptiness check
* results. The elements
* of the vector tell
@ -173,8 +172,7 @@ struct AutomatonStats
struct AlgorithmTestResults
{
explicit AlgorithmTestResults /* Constructor. */
(vector<Configuration::AlgorithmInformation,
ALLOC(Configuration::AlgorithmInformation) >
(vector<Configuration::AlgorithmInformation>
::size_type
number_of_algorithms,
StateSpace::size_type max_statespace_size);
@ -214,8 +212,8 @@ struct AlgorithmTestResults
* check.
*/
vector<AutomatonStats, ALLOC(AutomatonStats) > /* A two-element vector */
automaton_stats; /* storing test results
vector<AutomatonStats> automaton_stats; /* A two-element vector
* storing test results
* for an algorithm.
*/
};
@ -232,8 +230,7 @@ struct AlgorithmTestResults
struct TestStatistics
{
explicit TestStatistics /* Constructor. */
(vector<TestStatistics,
ALLOC(TestStatistics) >::size_type
(vector<TestStatistics>::size_type
number_of_algorithms);
/* default copy constructor */
@ -270,29 +267,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,36 +289,37 @@ struct TestStatistics
* automata.
*/
unsigned long int /* Total number of */
total_number_of_product_states[2]; /* states in all the
BIGUINT total_number_of_product_states[2]; /* Total number of states
* in all the generated
* product automata.
*/
BIGUINT total_number_of_product_transitions[2]; /* Total number of
* transitions in all the
* generated product
* automata.
*/
unsigned long int /* Total number of */
total_number_of_product_transitions[2]; /* transitions in all the
* generated product
* automata.
vector<unsigned long int> /* Number of failed */
cross_comparison_mismatches; /* result cross-
* comparisons.
*/
vector<unsigned long int, /* Number of failed */
ALLOC(unsigned long int) > /* result cross- */
cross_comparison_mismatches; /* comparisons. */
vector<unsigned long int, /* Number of failed */
ALLOC(unsigned long int) > /* result cross- */
initial_cross_comparison_mismatches; /* comparisons in the
vector<unsigned long int> /* Number of failed */
initial_cross_comparison_mismatches; /* result cross-
* comparisons in the
* initial state of the
* state space.
*/
vector<unsigned long int, /* Number of result */
ALLOC(unsigned long int) > /* cross-comparisons */
cross_comparisons_performed; /* performed. */
vector<unsigned long int> /* Number of result */
cross_comparisons_performed; /* cross-comparisons
* performed.
*/
vector<unsigned long int, /* Number of failed */
ALLOC(unsigned long int) > /* Büchi automaton */
buchi_intersection_check_failures; /* emptiness checks
vector<unsigned long int> /* Number of failed */
buchi_intersection_check_failures; /* Büchi automaton
* emptiness checks
* against the automata
* constructed from the
* negated formula
@ -337,9 +327,9 @@ struct TestStatistics
* algorithms.
*/
vector<unsigned long int, /* Number of Büchi */
ALLOC(unsigned long int) > /* automaton emptiness */
buchi_intersection_checks_performed; /* checks performed
vector<unsigned long int> /* Number of Büchi */
buchi_intersection_checks_performed; /* automaton emptiness
* checks performed
* against the automata
* constructed from the
* negated formula using
@ -357,9 +347,7 @@ struct TestStatistics
/* ========================================================================= */
inline AutomatonStats::AutomatonStats
(vector<Configuration::AlgorithmInformation,
ALLOC(Configuration::AlgorithmInformation) >::size_type
number_of_algorithms,
(vector<Configuration::AlgorithmInformation>::size_type number_of_algorithms,
StateSpace::size_type max_statespace_size) :
buchi_automaton(0), number_of_buchi_states(0),
number_of_buchi_transitions(0), number_of_acceptance_sets(0),
@ -481,9 +469,7 @@ AutomatonStats::buchiIntersectionCheckPerformed(unsigned long int algorithm)
/* ========================================================================= */
inline AlgorithmTestResults::AlgorithmTestResults
(vector<Configuration::AlgorithmInformation,
ALLOC(Configuration::AlgorithmInformation) >::size_type
number_of_algorithms,
(vector<Configuration::AlgorithmInformation>::size_type number_of_algorithms,
StateSpace::size_type max_statespace_size) :
consistency_check_result(-1), consistency_check_comparisons(0),
failed_consistency_check_comparisons(0),
@ -528,8 +514,7 @@ inline AlgorithmTestResults::~AlgorithmTestResults()
/* ========================================================================= */
inline TestStatistics::TestStatistics
(vector<TestStatistics, ALLOC(TestStatistics) >::size_type
number_of_algorithms) :
(vector<TestStatistics>::size_type number_of_algorithms) :
consistency_check_failures(0), consistency_checks_performed(0),
cross_comparison_mismatches(number_of_algorithms, 0),
initial_cross_comparison_mismatches(number_of_algorithms, 0),
@ -556,7 +541,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;

4
lbtt/src/TranslatorInterface.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License

205
lbtt/src/UserCommandReader.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -17,10 +17,6 @@
* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*/
#ifdef __GNUC__
#pragma implementation
#endif /* __GNUC__ */
#include <config.h>
#include <csignal>
#include <cstdio>
@ -32,7 +28,6 @@
#include <strstream>
#endif /* HAVE_SSTREAM */
#include "DispUtil.h"
#include "ProductAutomaton.h"
#include "SharedTestData.h"
#include "StatDisplay.h"
#include "StringUtil.h"
@ -50,6 +45,13 @@
#include <readline/history.h>
#endif /* HAVE_READLINE */
#ifdef HAVE_ISATTY
#ifdef HAVE_UNISTD_H
#include <unistd.h>
#endif /* HAVE_UNISTD_H */
#endif /* HAVE_ISATTY */
/******************************************************************************
*
@ -84,7 +86,7 @@ void executeUserCommands()
* ------------------------------------------------------------------------ */
{
string input_line;
vector<string, ALLOC(string) > input_tokens;
vector<string> input_tokens;
TokenType token;
bool formula_type = true;
@ -115,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)
@ -131,47 +130,86 @@ void executeUserCommands()
input_line = line;
else
{
round_info.cout << '\n';
round_info.cout.flush();
}
#else
round_info.cout << prompt;
round_info.cout.flush();
getline(cin, input_line, '\n');
if (cin.eof())
{
round_info.cout << '\n';
round_info.cout.flush();
cin.clear();
#endif /* HAVE_READLINE */
#ifdef HAVE_ISATTY
/*
* If standard input is not bound to a terminal, act on EOF as if the
* `continue' command had been issued. Otherwise act as if an empty
* line was given as input.
*/
if (!isatty(STDIN_FILENO))
input_line = "continue";
else
{
round_info.cout << '\n';
round_info.cout.flush();
}
#else
input_line = "continue";
round_info.cout << input_line << '\n';
round_info.cout.flush();
#endif /* HAVE_ISATTY */
}
#ifdef HAVE_ISATTY
if (!isatty(STDIN_FILENO))
{
round_info.cout << input_line << '\n';
round_info.cout.flush();
}
#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
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)
@ -192,9 +230,7 @@ void executeUserCommands()
{
bool all_algorithms_disabled = true;
for (vector<Configuration::AlgorithmInformation,
ALLOC(Configuration::AlgorithmInformation) >
::const_iterator
for (vector<Configuration::AlgorithmInformation>::const_iterator
algorithm = configuration.algorithms.begin();
algorithm != configuration.algorithms.end();
++algorithm)
@ -379,8 +415,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";
@ -403,8 +438,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"
@ -431,8 +466,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";
@ -474,8 +508,8 @@ void executeUserCommands()
break;
default :
throw CommandErrorException("Unknown command (`"
+ input_tokens[0] + "').");
throw CommandErrorException("Unknown command (`" + input_tokens[0]
+ "').");
}
if (output_string != 0)
@ -486,21 +520,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();
}
}
@ -533,16 +563,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 (...)
@ -555,7 +575,7 @@ void executeUserCommands()
#endif /* HAVE_READLINE */
signal(SIGPIPE, SIG_DFL);
}
}
/* ========================================================================= */
TokenType parseCommand(const string& token)
@ -570,19 +590,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;
@ -679,8 +686,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' :
@ -760,6 +778,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;
@ -770,19 +793,12 @@ TokenType parseCommand(const string& token)
throw CommandErrorException("Ambiguous command.");
return token_type;
#ifdef __GNUC__
#if __GNUC__ < 3
#undef compare
#endif
#endif
}
/* ========================================================================= */
void verifyArgumentCount
(const vector<string, ALLOC(string) >& command,
vector<string, ALLOC(string) >::size_type min_arg_count,
vector<string, ALLOC(string) >::size_type max_arg_count)
(const vector<string>& command, vector<string>::size_type min_arg_count,
vector<string>::size_type max_arg_count)
/* ----------------------------------------------------------------------------
*
* Description: Verifies that the number of arguments given for a user
@ -805,8 +821,7 @@ void verifyArgumentCount
}
/* ========================================================================= */
pair<string, bool> parseRedirection
(vector<string, ALLOC(string) >& input_tokens)
pair<string, bool> parseRedirection(vector<string>& input_tokens)
/* ----------------------------------------------------------------------------
*
* Description: Tests whether the last argument to a user command specifies
@ -840,13 +855,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();
}
}
@ -855,10 +870,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();
@ -870,7 +884,7 @@ pair<string, bool> parseRedirection
}
/* ========================================================================= */
bool parseFormulaType(vector<string, ALLOC(string) >& input_tokens)
bool parseFormulaType(vector<string>& input_tokens)
/* ----------------------------------------------------------------------------
*
* Description: Tests whether the first argument of a command specifies a
@ -894,8 +908,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());
}

17
lbtt/src/UserCommandReader.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -65,22 +65,19 @@ TokenType parseCommand(const string& token); /* Translates a command
*/
void verifyArgumentCount /* Checks that the */
(const vector<string, ALLOC(string) >& /* number of arguments */
arguments, /* for a command is */
vector<string, ALLOC(string) >::size_type /* within given limits. */
min_arg_count,
vector<string, ALLOC(string) >::size_type
max_arg_count);
(const vector<string>& arguments, /* number of arguments */
vector<string>::size_type min_arg_count, /* for a command is */
vector<string>::size_type max_arg_count); /* within given limits. */
pair<string, bool> parseRedirection /* Checks whether an */
(vector<string, ALLOC(string) >& input_tokens); /* user command given
(vector<string>& input_tokens); /* user command given
* will require
* redirecting its
* output to a file.
*/
bool parseFormulaType /* Checks whether an */
(vector<string, ALLOC(string) >& input_tokens); /* user command
(vector<string>& input_tokens); /* user command
* specified a positive
* or a negative
* formula.

1501
lbtt/src/UserCommands.cc
View file

File diff suppressed because it is too large Load diff

101
lbtt/src/UserCommands.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -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,119 +49,102 @@ 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);
const vector<string>& input_tokens); /* implementations. */
void printConsistencyAnalysisResults /* Analyzes a */
(ostream& stream, int indent, /* contradicition in the */
const vector<string, ALLOC(string) >& /* model checking result */
input_tokens); /* consistency check for
const vector<string>& input_tokens); /* model checking result
* consistency check for
* an implementation.
*/
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>& input_tokens); /* Büchi automata
* 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 */
(ostream& stream, int indent, /* a single automaton */
vector<Configuration::AlgorithmInformation, /* execution. */
ALLOC(Configuration::AlgorithmInformation) >
vector<Configuration::AlgorithmInformation> /* execution. */
::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 */
bool formula_type, /* automaton. */
vector<string, ALLOC(string) >& input_tokens,
vector<string>& input_tokens,
Graph::GraphOutputFormat fmt);
void evaluateFormula /* Displays information */
(ostream& stream, int indent, /* about existence of */
bool formula_type, /* accepting system */
vector<string, ALLOC(string) >& input_tokens); /* executions. */
vector<string>& input_tokens); /* executions. */
void printFormula /* Displays a formula */
(ostream& stream, int indent, /* used for testing. */
bool formula_type);
bool formula_type,
const vector<string>& input_tokens);
void printCommandHelp /* Displays help about */
(ostream& stream, int indent, /* user commands. */
const vector<string, ALLOC(string) >&
input_tokens);
const vector<string>& input_tokens);
void printInconsistencies /* Lists the system */
(ostream& stream, int indent, /* states failing the */
vector<string, ALLOC(string) >& input_tokens); /* consistency check
vector<string>& input_tokens); /* consistency check
* for an algorihm.
*/
void printTestResults /* Displays the test */
(ostream& stream, int indent, /* results of the last */
vector<string, ALLOC(string) >& input_tokens); /* round performed. */
vector<string>& input_tokens); /* round performed. */
void printStateSpace /* Displays information */
(ostream& stream, int indent, /* about a state space. */
vector<string, ALLOC(string) >& input_tokens,
vector<string>& input_tokens,
Graph::GraphOutputFormat fmt);
void changeVerbosity /* Displays or changes */
(const vector<string, ALLOC(string) >& /* the verbosity of */
input_tokens); /* output. */
(const vector<string>& input_tokens); /* the verbosity of
* output.
*/
void changeAlgorithmState /* Enables or disables a */
(vector<string, ALLOC(string) >& input_tokens, /* set of algorithms */
bool enable); /* used in the tests. */
(vector<string>& input_tokens, bool enable); /* set of algorithms
* used in the tests.
*/
}

434
lbtt/src/main.cc
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -21,6 +21,9 @@
#include <csignal>
#include <cstdlib>
#include <ctime>
#ifdef HAVE_SYS_TYPES_H
#include <sys/types.h>
#endif /* HAVE_SYS_TYPES_H */
#include <iostream>
#include <vector>
#ifdef HAVE_READLINE
@ -28,6 +31,11 @@
#include <readline/readline.h>
#include <readline/history.h>
#endif /* HAVE_READLINE */
#ifdef HAVE_ISATTY
#ifdef HAVE_UNISTD_H
#include <unistd.h>
#endif /* HAVE_UNISTD_H */
#endif /* HAVE_ISATTY */
#include "LbttAlloc.h"
#include "Configuration.h"
#include "DispUtil.h"
@ -36,6 +44,7 @@
#include "Random.h"
#include "SharedTestData.h"
#include "StatDisplay.h"
#include "TempFsysName.h"
#include "TestOperations.h"
#include "TestRoundInfo.h"
#include "TestStatistics.h"
@ -43,17 +52,6 @@
using namespace std;
/******************************************************************************
*
* Handler for the SIGINT signal.
*
*****************************************************************************/
RETSIGTYPE breakHandler(int)
{
user_break = true;
}
/******************************************************************************
@ -92,12 +90,12 @@ TestRoundInfo round_info; /* Data structure for
* round.
*/
vector<AlgorithmTestResults, /* Test results for each */
ALLOC(AlgorithmTestResults) > /* individual algorithm. */
test_results;
vector<AlgorithmTestResults> test_results; /* Test results for each
* individual algorithm.
*/
vector<TestStatistics, ALLOC(TestStatistics) > /* Overall test */
final_statistics; /* statistics for each
vector<TestStatistics> final_statistics; /* Overall test
* statistics for each
* algorithm.
*/
@ -105,13 +103,124 @@ 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.
*
*****************************************************************************/
pid_t translator_process = 0; /* Process group for translator process */
static void abortHandler(int signum)
{
deallocateTempFilenames();
if (translator_process != 0 && kill(translator_process, 0) == 0)
kill(-translator_process, SIGTERM);
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.
*
*****************************************************************************/
int testLoop()
bool testLoop()
{
using namespace DispUtil;
using namespace SharedTestData;
@ -119,9 +228,6 @@ int testLoop()
using namespace StringUtil;
using namespace TestOperations;
/* Return code. Will be set to 1 if any of the test fails. */
int exit_status = 0;
const Configuration::GlobalConfiguration& global_options
= configuration.global_options;
@ -139,13 +245,6 @@ int 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.
@ -173,9 +272,9 @@ int testLoop()
try
{
round_info.transcript_file << "lbtt " PACKAGE_VERSION
" error log file, created on "
+ string(ctime(&current_time))
+ '\n';
" error log file, created on "
+ string(ctime(&current_time))
+ '\n';
configuration.print(round_info.transcript_file);
}
@ -187,16 +286,24 @@ int testLoop()
/*
* If a formula file name was given in the configuration, open the file for
* reading.
* reading. The special filename "-" refers to the standard input.
*/
try
{
if (!global_options.formula_input_filename.empty())
openFile(global_options.formula_input_filename.c_str(),
round_info.formula_input_file,
ios::in,
0);
{
if (global_options.formula_input_filename == "-")
round_info.formula_input_stream = &cin;
else
{
openFile(global_options.formula_input_filename.c_str(),
round_info.formula_input_file,
ios::in,
0);
round_info.formula_input_stream = &round_info.formula_input_file;
}
}
}
catch (const FileOpenException& e)
{
@ -224,19 +331,6 @@ int 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
@ -265,30 +359,18 @@ int testLoop()
for (round_info.current_round = 1;
!round_info.abort
&& round_info.current_round <= global_options.number_of_rounds;
&& round_info.current_round <= global_options.number_of_rounds;
++round_info.current_round)
{
user_break = false;
round_info.error = false;
round_info.skip
= (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
{
@ -299,7 +381,7 @@ int testLoop()
round_info.fresh_statespace
= ((global_options.do_comp_test || global_options.do_cons_test)
&& round_info.next_round_to_change_statespace
== round_info.current_round);
== round_info.current_round);
if (round_info.fresh_statespace)
{
@ -307,13 +389,13 @@ int testLoop()
seed48(statespace_random_state);
for (int i = 0; i < 3; i++)
statespace_random_state[i] = static_cast<short int>
(LRAND(0, LONG_MAX));
(LRAND(0, LONG_MAX));
#else
SRAND(global_options.statespace_random_seed);
configuration.global_options.statespace_random_seed
= LRAND(0, RAND_MAX);
#endif /* HAVE_RAND48 */
if (global_options.statespace_change_interval == 0)
round_info.next_round_to_change_statespace
= global_options.number_of_rounds + 1;
@ -321,8 +403,7 @@ int testLoop()
round_info.next_round_to_change_statespace
+= global_options.statespace_change_interval;
for (vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >
::iterator it = test_results.begin();
for (vector<AlgorithmTestResults>::iterator it = test_results.begin();
it != test_results.end();
++it)
it->emptinessReset();
@ -352,7 +433,7 @@ int testLoop()
*/
round_info.fresh_formula
= (round_info.next_round_to_change_formula
= (round_info.next_round_to_change_formula
== round_info.current_round);
if (round_info.fresh_formula)
@ -375,8 +456,7 @@ int testLoop()
round_info.formula_in_file[0] = round_info.formula_in_file[1] = false;
for (vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >
::iterator it = test_results.begin();
for (vector<AlgorithmTestResults>::iterator it = test_results.begin();
it != test_results.end();
++it)
it->fullReset();
@ -387,8 +467,8 @@ int testLoop()
{
try
{
generateFormulae(round_info.formula_input_file.is_open()
? &round_info.formula_input_file
generateFormulae(!global_options.formula_input_filename.empty()
? round_info.formula_input_stream
: 0);
}
catch (const FormulaGenerationException&)
@ -402,7 +482,7 @@ int testLoop()
if (user_break)
{
printText("[User break]\n\n", 2, 4);
printText("[User break]\n\n", 1, 4);
throw UserBreakException();
}
@ -417,12 +497,17 @@ int 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;
@ -434,81 +519,61 @@ int 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&)
@ -544,7 +609,13 @@ int 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)
@ -556,10 +627,7 @@ int 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();
}
@ -590,33 +658,22 @@ int testLoop()
round_info.next_round_to_stop = round_info.current_round;
}
if (round_info.error)
exit_status = 1;
/*
* Determine from the program configuration and the error status whether
* 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)
@ -628,8 +685,7 @@ int testLoop()
::Ltl::LtlFormula::destruct(round_info.formulae[f]);
}
for (vector<AlgorithmTestResults, ALLOC(AlgorithmTestResults) >
::iterator it = test_results.begin();
for (vector<AlgorithmTestResults>::iterator it = test_results.begin();
it != test_results.end();
++it)
it->fullReset();
@ -661,19 +717,19 @@ int testLoop()
time(&current_time);
round_info.transcript_file << "lbtt error log closed on "
+ string(ctime(&current_time))
+ string(ctime(&current_time))
<< endl;
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 exit_status;
return round_info.all_tests_successful;
}
@ -686,7 +742,7 @@ int testLoop()
int main(int argc, char* argv[])
{
try
try
{
configuration.read(argc, argv);
}
@ -697,15 +753,35 @@ int main(int argc, char* argv[])
cerr << ":" << configuration.global_options.cfg_filename << ":"
<< e.line_info;
cerr << ": " << e.what() << endl;
exit(-1);
exit(2);
}
#ifdef HAVE_ISATTY
if (configuration.global_options.formula_input_filename == "-"
&& !isatty(STDIN_FILENO))
{
configuration.global_options.interactive = Configuration::NEVER;
configuration.global_options.handle_breaks = false;
}
#endif /* HAVE_ISATTY */
if (configuration.global_options.verbosity >= 3)
configuration.print(cout);
user_break = false;
if (configuration.global_options.interactive != Configuration::NEVER)
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;
@ -715,18 +791,28 @@ int main(int argc, char* argv[])
using_history();
#endif /* HAVE_READLINE */
try
try
{
return 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;
}

10
lbtt/src/translate.cc
View file

@ -180,11 +180,11 @@ int main(int argc, char** argv)
case OPT_VERSION :
cout << "lbtt-translate " PACKAGE_VERSION "\n"
"lbtt-translate is free software; you may change and "
"redistribute it under the\n"
"terms of the GNU General Public License. lbtt-translate "
"comes with NO WARRANTY.\n"
"See the file COPYING for details.\n";
"lbtt-translate is free software; you may change and "
"redistribute it under the\n"
"terms of the GNU General Public License. lbtt-translate "
"comes with NO WARRANTY.\n"
"See the file COPYING for details.\n";
exit(0);
break;

8
lbtt/src/translate.h
View file

@ -1,6 +1,6 @@
/*
* Copyright (C) 1999, 2000, 2001, 2002
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
@ -20,10 +20,6 @@
#ifndef TRANSLATE_H
#define TRANSLATE_H
#ifdef __GNUC__
#pragma interface
#endif /* __GNUC__ */
#include <config.h>
#include <string>