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

lbtt 1.0.2

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2003-07-29 12:12:15 +00:00
parent 8128d92b36
commit 06226f3227
65 changed files with 222 additions and 138 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@hut.fi>

32
lbtt/ChangeLog
View file

@ -1,3 +1,35 @@
2003-07-18 Heikki Tauriainen <heikki.tauriainen@hut.fi>
* UserCommands.cc (printAutomatonAnalysisResults): Ensure that
the states in a witness for the nonemptiness of two Bûchi
automata are distinct to prevent the truth valuation for the
atomic propositions from being defined multiple times in any
state of the witness.
* Version 1.0.2 released.
2003-07-17 Heikki Tauriainen <heikki.tauriainen@hut.fi>
* NeverClaimAutomaton.cc (ParseErrorException::ParseErrorException):
Fix a string buffer overflow.
* ProductAutomaton.cc (findAcceptingExecution): Concatenate
fragments of an accepting cycle in the correct order. (Thanks to
Joachim Klein for pointing out an example uncovering the bug
in previous releases.)
2002-11-04 Heikki Tauriainen <heikki.tauriainen@hut.fi>
* StatDisplay.cc (printCollectiveStats): If using more than five
formula operators (but the total number of operators is not
a multiple of 5), insert an empty line in the output before the
last row of the operator distribution table.
2002-10-21 Heikki Tauriainen <heikki.tauriainen@hut.fi>
* BitArray.cc (BitArray::find): Fix bug in testing whether
all accessed bytes were zero.
2002-10-01 Heikki Tauriainen <heikki.tauriainen@hut.fi> 2002-10-01 Heikki Tauriainen <heikki.tauriainen@hut.fi>
* Version 1.0.1 released. * Version 1.0.1 released.

14
lbtt/NEWS
View file

@ -1,5 +1,5 @@
lbtt NEWS -- history of user-visible changes. 01 Oct 2002 lbtt NEWS -- history of user-visible changes. 18 Jul 2003
Copyright (C) 2002 Heikki Tauriainen Copyright (C) 2003 Heikki Tauriainen
Permission is granted to anyone to make or distribute verbatim copies Permission is granted to anyone to make or distribute verbatim copies
of this document as received, in any medium, provided that the of this document as received, in any medium, provided that the
@ -12,6 +12,16 @@ Copyright (C) 2002 Heikki Tauriainen
Please send bug reports to <heikki.tauriainen@hut.fi>. Please send bug reports to <heikki.tauriainen@hut.fi>.
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 Version 1.0.1
* This release does not add new functionality to the program apart from * This release does not add new functionality to the program apart from

8
lbtt/README
View file

@ -1,7 +1,7 @@
lbtt version 1.0.1 lbtt version 1.0.2
------------------ ------------------
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 expressed in propositional linear temporal logic (LTL) into
Büchi automata. The goal of the tool is to assist in the Büchi automata. The goal of the tool is to assist in the
correct implementation of LTL-to-Büchi translation algorithms correct implementation of LTL-to-Büchi translation algorithms
@ -11,7 +11,7 @@ for very basic profiling of different LTL-to-B
to evaluate their performance. to evaluate their performance.
The latest version of the program is available at 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 lbtt is free software, you may change and redistribute it under
the terms of the GNU General Public License. lbtt comes with the terms of the GNU General Public License. lbtt comes with
@ -82,4 +82,4 @@ Documentation:
The documentation is also available in various formats The documentation is also available in various formats
at the program's home page at at the program's home page at
<http://www.tcs.hut.fi/%7Ehtauriai/lbtt/>. <http://www.tcs.hut.fi/Software/lbtt/>.

4
lbtt/configure.ac
View file

@ -1,8 +1,8 @@
# Process this file with autoconf to produce a configure script. # Process this file with autoconf to produce a configure script.
AC_PREREQ([2.53]) AC_PREREQ([2.53])
AC_INIT([lbtt], [1.0.1], [heikki.tauriainen@hut.fi]) AC_INIT([lbtt], [1.0.2], [heikki.tauriainen@hut.fi])
AC_REVISION([Revision: 1.1]) AC_REVISION([Revision: 1.2])
AC_CONFIG_SRCDIR([src/main.cc]) AC_CONFIG_SRCDIR([src/main.cc])
AM_INIT_AUTOMAKE AM_INIT_AUTOMAKE
AM_CONFIG_HEADER([config.h]) AM_CONFIG_HEADER([config.h])

41
lbtt/doc/lbtt.texi
View file

@ -14,12 +14,14 @@
This file documents how to use the LTL-to-B@"uchi This file documents how to use the LTL-to-B@"uchi
translator testbench @command{lbtt}. translator testbench @command{lbtt}.
Copyright @copyright{} 2001 Heikki Tauriainen Copyright @copyright{} 2003 Heikki Tauriainen
@ifinfo @ifinfo
@email{heikki.tauriainen@@hut.fi} @email{heikki.tauriainen@@hut.fi}
@end ifinfo @end ifinfo
@ifnotinfo @ifnotinfo
@ifnothtml
<@email{heikki.tauriainen@@hut.fi}> <@email{heikki.tauriainen@@hut.fi}>
@end ifnothtml
@end ifnotinfo @end ifnotinfo
@ifhtml @ifhtml
@ -66,11 +68,11 @@ under the above conditions for modified versions.
@author Heikki Tauriainen <@email{heikki.tauriainen@@hut.fi}> @author Heikki Tauriainen <@email{heikki.tauriainen@@hut.fi}>
@page @page
@vskip 0pt plus 1filll @vskip 0pt plus 1filll
Copyright @copyright{} 2001 Heikki Tauriainen Copyright @copyright{} 2003 Heikki Tauriainen
<@email{heikki.tauriainen@@hut.fi}> <@email{heikki.tauriainen@@hut.fi}>
The latest version of this manual can be obtained from@* The latest version of this manual can be obtained from@*
<@url{http://www.tcs.hut.fi/%7Ehtauriai/lbtt/}>. <@url{http://www.tcs.hut.fi/Software/lbtt/}>.
Permission is granted to make and distribute verbatim Permission is granted to make and distribute verbatim
copies of this manual provided the copyright notice and copies of this manual provided the copyright notice and
@ -101,7 +103,7 @@ under the above conditions for modified versions.
for translating propositional linear temporal logic formulas into for translating propositional linear temporal logic formulas into
B@"uchi automata. B@"uchi automata.
This is edition 1.0.0 of the @command{lbtt} documentation. This edition This is edition 1.0.1 of the @command{lbtt} documentation. This edition
applies to @command{lbtt} versions 1.0.x. applies to @command{lbtt} versions 1.0.x.
@command{lbtt} is free software, you may change and redistribute it @command{lbtt} is free software, you may change and redistribute it
@ -203,12 +205,12 @@ formulas as input and then performing simple consistency checks on the
resulting automata to test whether the translators seem to operate correctly resulting automata to test whether the translators seem to operate correctly
in practice. (See in practice. (See
@ifnottex @ifnottex
@ref{[Tau00]} @ref{[TH02]}
@end ifnottex @end ifnottex
@iftex @iftex
[Tau00] [TH02]
@end iftex @end iftex
for a description of the theory behind the testing methods.) If the tests for more information on the theory behind the testing methods.) If the tests
suggest an implementation suggest an implementation
error in a translator, @command{lbtt} can generate sample data which causes error in a translator, @command{lbtt} can generate sample data which causes
a test failure and which may also be useful for debugging the a test failure and which may also be useful for debugging the
@ -240,6 +242,13 @@ together with the outline of @command{lbtt}'s testing procedure. However, the
chapter is not intended to be a thorough introduction to the theoretical chapter is not intended to be a thorough introduction to the theoretical
background of the different tests; see, for example, background of the different tests; see, for example,
@ifnottex @ifnottex
@ref{[TH02]}
@end ifnottex
@iftex
[TH02]
@end iftex
or
@ifnottex
@ref{[Tau00]} @ref{[Tau00]}
@end ifnottex @end ifnottex
@iftex @iftex
@ -3821,10 +3830,10 @@ originally based on the algorithm presented in
@end iftex @end iftex
See See
@ifinfo @ifinfo
@url{http://netlib.bell-labs.com/netlib/spin/whatispin.html} @url{http://spinroot.com/spin/whatispin.html}
@end ifinfo @end ifinfo
@ifnotinfo @ifnotinfo
<@uref{http://netlib.bell-labs.com/netlib/spin/whatispin.html}> <@uref{http://spinroot.com/spin/whatispin.html}>
@end ifnotinfo @end ifnotinfo
for more information. for more information.
@ -3947,19 +3956,25 @@ pages 247---263. Springer-Verlag, 2000.
@item @anchor{[Tau00]} [Tau00] @item @anchor{[Tau00]} [Tau00]
H. Tauriainen. Automated testing of B@"uchi automata translators H. Tauriainen. Automated testing of B@"uchi automata translators
for linear temporal logic. Technical report A66, Laboratory for Theoretical for linear temporal logic. Research report A66, Laboratory for Theoretical
Computer Science, Helsinki University of Technology, Espoo, Finland, Computer Science, Helsinki University of Technology, Espoo, Finland,
2000. Available on the WWW at 2000. Available on the WWW at
@ifinfo @ifinfo
@url{http://www.tcs.hut.fi/Publications/reports/A66abstract.html} @url{http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A66.shtml}
@end ifinfo @end ifinfo
@ifhtml @ifhtml
<@uref{http://www.tcs.hut.fi/Publications/reports/A66abstract.html}>. <@uref{http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A66.shtml}>.
@end ifhtml @end ifhtml
@iftex @iftex
<@url{http://www.tcs.hut.fi/Publications/reports/ A66abstract.html}>. <@url{http://www.tcs.hut.fi/Publications/info/ bibdb.HUT-TCS-A66.shtml}>.
@end iftex @end iftex
@item @anchor{[TH02]} [TH02]
H. Tauriainen and K. Heljanko. Testing LTL formula translation into B@"uchi
automata.
@i{International Journal on Software Tools for Technology Transfer (STTT)}
4(1):57---70, 2002.
@item @anchor{[Var96]} [Var96] @item @anchor{[Var96]} [Var96]
M.@: Y.@: Vardi. An automata-theoretic approach to linear temporal logic. M.@: Y.@: Vardi. An automata-theoretic approach to linear temporal logic.
In @i{Logics for Concurrency: Structure versus Automata}, volume 1043 of In @i{Logics for Concurrency: Structure versus Automata}, volume 1043 of

2
lbtt/src/Alloc.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

4
lbtt/src/BitArray.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
@ -378,7 +378,7 @@ unsigned long int BitArray::find(const unsigned long int max_count) const
for (i = 0; i < bsize && bits[i] == 0; ++i) for (i = 0; i < bsize && bits[i] == 0; ++i)
; ;
if (i == max_count) if (i == bsize)
return max_count; return max_count;
unsigned char c = bits[i]; unsigned char c = bits[i];

2
lbtt/src/BitArray.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/Bitset.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/BuchiAutomaton.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/BuchiAutomaton.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

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

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

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

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/Configuration.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/Configuration.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/DispUtil.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/DispUtil.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/EdgeContainer.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/Exception.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/ExternalTranslator.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/ExternalTranslator.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/FormulaRandomizer.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/FormulaRandomizer.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/FormulaWriter.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

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

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/LbtWrapper.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/LtlFormula.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/LtlFormula.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

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

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

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

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

4
lbtt/src/NeverClaimAutomaton.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
@ -312,7 +312,7 @@ ParseErrorException::ParseErrorException
else else
{ {
string space_string(msg.substr(0, error_pos)); 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') if (space_string[c] != ' ' && space_string[c] != '\t')
space_string[c] = ' '; space_string[c] = ' ';

2
lbtt/src/NeverClaimAutomaton.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/PathEvaluator.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/PathEvaluator.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/PathIterator.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/PathIterator.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

16
lbtt/src/ProductAutomaton.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
@ -864,12 +864,15 @@ void ProductAutomaton::findAcceptingExecution
all_acceptance_sets_on_path = false; all_acceptance_sets_on_path = false;
} }
deque<StateIdPair, ALLOC(StateIdPair) > cycle_fragment;
while (state != bfs_root) while (state != bfs_root)
{ {
cycle.push_back(make_pair(buchiState(state), cycle_fragment.push_back(make_pair(buchiState(state),
systemState(state))); systemState(state)));
state = shortest_path_predecessor[state]; state = shortest_path_predecessor[state];
} }
cycle.insert(cycle.begin(), cycle_fragment.begin(),
cycle_fragment.end());
bfs_root = (*predecessor)->targetNode(); bfs_root = (*predecessor)->targetNode();
visited.clear(nodes.size()); visited.clear(nodes.size());
@ -887,13 +890,16 @@ void ProductAutomaton::findAcceptingExecution
backward_search_queue.pop_front(); backward_search_queue.pop_front();
} }
deque<StateIdPair, ALLOC(StateIdPair) > cycle_fragment;
while (state != bfs_root) while (state != bfs_root)
{ {
cycle.push_back(make_pair(buchiState(state), cycle_fragment.push_back(make_pair(buchiState(state),
systemState(state))); systemState(state)));
state = shortest_path_predecessor[state]; state = shortest_path_predecessor[state];
} }
cycle.insert(cycle.begin(), cycle_fragment.begin(),
cycle_fragment.end());
cycle.push_back(make_pair(buchiState(search_start_state), cycle.push_back(make_pair(buchiState(search_start_state),
systemState(search_start_state))); systemState(search_start_state)));

2
lbtt/src/ProductAutomaton.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/Random.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/SccIterator.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/SharedTestData.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/SpinWrapper.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/SpinWrapper.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

4
lbtt/src/StatDisplay.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
@ -912,6 +912,8 @@ void printCollectiveStats(ostream& stream, int indent)
if (number_of_symbols_printed % 5 != 0) if (number_of_symbols_printed % 5 != 0)
{ {
if (number_of_symbols_printed > 5)
estream << '\n';
estream << ind + " operator " + symbol_name_string + '\n' estream << ind + " operator " + symbol_name_string + '\n'
+ ind + " # " + symbol_number_string + '\n' + ind + " # " + symbol_number_string + '\n'
+ ind + " #/formula " + symbol_distribution_string + ind + " #/formula " + symbol_distribution_string

2
lbtt/src/StatDisplay.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/StateSpace.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/StateSpace.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/StateSpaceRandomizer.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/StateSpaceRandomizer.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/StringUtil.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/StringUtil.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/TestOperations.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/TestOperations.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/TestRoundInfo.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/TestStatistics.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/TestStatistics.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/TranslatorInterface.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/UserCommandReader.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/UserCommandReader.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

123
lbtt/src/UserCommands.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or
@ -965,53 +965,73 @@ void printAutomatonAnalysisResults
* intersection automaton from the result. * intersection automaton from the result.
*/ */
deque<BuchiAutomaton::size_type, ALLOC(BuchiAutomaton::size_type) > prefix;
deque<BuchiAutomaton::size_type, ALLOC(BuchiAutomaton::size_type) > cycle;
vector<StateSpace::size_type, ALLOC(StateSpace::size_type) > path; vector<StateSpace::size_type, ALLOC(StateSpace::size_type) > path;
while (!execution.first.empty()) for (deque<BuchiAutomaton::StateIdPair,
{ ALLOC(BuchiAutomaton::StateIdPair) >::const_iterator
prefix.push_back(execution.first.front().first); state = execution.first.begin();
path.push_back(execution.first.front().first); state != execution.first.end();
execution.first.pop_front(); ++state)
} path.push_back(state->first);
while (!execution.second.empty()) const vector<StateSpace::size_type, ALLOC(StateSpace::size_type) >
{ ::size_type loop_pos = path.size();
cycle.push_back(execution.second.front().first);
path.push_back(execution.second.front().first); for (deque<BuchiAutomaton::StateIdPair,
execution.second.pop_front(); ALLOC(BuchiAutomaton::StateIdPair) >::const_iterator
} state = execution.second.begin();
state != execution.second.end();
++state)
path.push_back(state->first);
/* /*
* Construct an execution accepted by both of the automata. This is done * Construct an execution accepted by both of the automata. This is done
* by giving suitable truth assignments for the atomic propositions in * by giving suitable truth assignments for the atomic propositions in
* selected states of the state space to which the intersection automaton * 'path.size()' states, where `path' corresponds to an accepting run of
* was converted. * the intersection automaton. (The state space representing the
* intersection automaton is reused for this purpose, since it is not
* needed any longer.) In addition, `prefix' and `cycle' (required for
* displaying the execution) are built to refer to the reused states.
*/ */
GraphEdgeContainer::const_iterator transition; deque<StateSpace::size_type, ALLOC(StateSpace::size_type) > prefix, cycle;
path.push_back(cycle.front()); /*
* Ensure that the state space is large enough to contain the execution
* (the execution may pass several times through a state in the
* intersection automaton).
*/
if (automaton_as_statespace.size() < path.size())
automaton_as_statespace.expand
(path.size() - automaton_as_statespace.size());
path.push_back(path[loop_pos]); /* use the first state of the cycle as a
* temporary sentinel element
*/
for (vector<StateSpace::size_type, ALLOC(StateSpace::size_type) > for (vector<StateSpace::size_type, ALLOC(StateSpace::size_type) >
::size_type state = 0; ::size_type state = 0;
state + 1 < path.size(); state + 1 < path.size();
state++) ++state)
{ {
GraphEdgeContainer::const_iterator transition;
for (transition = (*a)[path[state]].edges().begin(); for (transition = (*a)[path[state]].edges().begin();
(*transition)->targetNode() != path[state + 1]; (*transition)->targetNode() != path[state + 1];
++transition) ++transition)
; ;
automaton_as_statespace[path[state]].positiveAtoms() automaton_as_statespace[state].positiveAtoms()
= static_cast<BuchiAutomaton::BuchiTransition*>(*transition) = static_cast<BuchiAutomaton::BuchiTransition*>(*transition)
->guard().findPropositionalModel ->guard().findPropositionalModel
(configuration.formula_options.formula_generator. (configuration.formula_options.formula_generator.
number_of_available_variables); number_of_available_variables);
(state < loop_pos ? prefix : cycle).push_back(state);
} }
path.pop_back(); path.pop_back(); /* remove the sentinel element */
delete a; delete a;
a = 0; a = 0;
@ -1038,40 +1058,25 @@ void printAutomatonAnalysisResults
deque<BuchiAutomaton::size_type, ALLOC(BuchiAutomaton::size_type) > deque<BuchiAutomaton::size_type, ALLOC(BuchiAutomaton::size_type) >
aut_cycle; aut_cycle;
const deque<BuchiAutomaton::size_type, ALLOC(BuchiAutomaton::size_type) >*
original_execution_states;
deque<BuchiAutomaton::size_type, ALLOC(BuchiAutomaton::size_type) >*
new_execution_states;
for (int i = 0; i < 2; i++) for (int i = 0; i < 2; i++)
{ {
aut_prefix.clear(); aut_prefix.clear();
aut_cycle.clear(); aut_cycle.clear();
for (int j = 0; j < 2; j++) deque<BuchiAutomaton::size_type, ALLOC(BuchiAutomaton::size_type) >*
{ new_execution_states = &aut_prefix;
if (j == 0)
{
original_execution_states = &prefix;
new_execution_states = &aut_prefix;
}
else
{
original_execution_states = &cycle;
new_execution_states = &aut_cycle;
}
for (deque<BuchiAutomaton::size_type, for (vector<StateSpace::size_type, ALLOC(StateSpace::size_type) >
ALLOC(BuchiAutomaton::size_type) >::const_iterator ::size_type state_id = 0;
execution_state = original_execution_states->begin(); state_id < path.size();
execution_state != original_execution_states->end(); ++state_id)
++execution_state) {
{ if (state_id == loop_pos)
new_execution_states->push_back new_execution_states = &aut_cycle;
(i == 0 new_execution_states->push_back
? intersection_state_mapping[*execution_state].first (i == 0
: intersection_state_mapping[*execution_state].second); ? intersection_state_mapping[path[state_id]].first
} : intersection_state_mapping[path[state_id]].second);
} }
synchronizePrefixAndCycle(aut_prefix, aut_cycle); synchronizePrefixAndCycle(aut_prefix, aut_cycle);
@ -1083,13 +1088,27 @@ void printAutomatonAnalysisResults
automaton_stats[i].buchi_automaton)); automaton_stats[i].buchi_automaton));
} }
/*
* Normalize the state identifiers in `path' to refer to the states that
* give the valuations for atomic propositions along the execution.
*/
for (vector<StateSpace::size_type, ALLOC(StateSpace::size_type) >
::size_type state = 0;
state < path.size();
++state)
path[state] = state;
/*
* Display a proof or a refutation for the formula in the execution.
*/
estream << string(indent + 2, ' ') estream << string(indent + 2, ' ')
+ "Analysis of the positive formula in the execution M:\n"; + "Analysis of the positive formula in the execution M:\n";
Ltl::PathEvaluator path_evaluator; Ltl::PathEvaluator path_evaluator;
bool result = path_evaluator.evaluate bool result = path_evaluator.evaluate
(*round_info.formulae[formula], automaton_as_statespace, path, (*round_info.formulae[formula], automaton_as_statespace, path, loop_pos);
prefix.size());
path_evaluator.print(stream, indent + 4); path_evaluator.print(stream, indent + 4);

2
lbtt/src/UserCommands.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/main.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/translate.cc
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or

2
lbtt/src/translate.h
View file

@ -1,5 +1,5 @@
/* /*
* Copyright (C) 1999, 2000, 2001, 2002 * Copyright (C) 1999, 2000, 2001, 2002, 2003
* Heikki Tauriainen <Heikki.Tauriainen@hut.fi> * Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
* *
* This program is free software; you can redistribute it and/or * This program is free software; you can redistribute it and/or