diff --git a/lbtt/AUTHORS b/lbtt/AUTHORS index 87908cad0..dfd5d7d33 100644 --- a/lbtt/AUTHORS +++ b/lbtt/AUTHORS @@ -1 +1 @@ -lbtt was written by Heikki Tauriainen +Heikki Tauriainen diff --git a/lbtt/ChangeLog b/lbtt/ChangeLog index d15f24ea2..181f75ade 100644 --- a/lbtt/ChangeLog +++ b/lbtt/ChangeLog @@ -1,3 +1,35 @@ +2003-07-18 Heikki Tauriainen + + * 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 + + * 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 + + * 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 + + * BitArray.cc (BitArray::find): Fix bug in testing whether + all accessed bytes were zero. + 2002-10-01 Heikki Tauriainen * Version 1.0.1 released. diff --git a/lbtt/NEWS b/lbtt/NEWS index 1f3705dc8..e8c820d71 100644 --- a/lbtt/NEWS +++ b/lbtt/NEWS @@ -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. 18 Jul 2003 +Copyright (C) 2003 Heikki Tauriainen Permission is granted to anyone to make or distribute verbatim copies 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 . +Version 1.0.2 + +* Bug fix release. + +* The official WWW home page of the tool is now located at + . 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 * This release does not add new functionality to the program apart from diff --git a/lbtt/README b/lbtt/README index fcaf03f9f..3096ee211 100644 --- a/lbtt/README +++ b/lbtt/README @@ -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 Büchi automata. The goal of the tool is to assist in the 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. The latest version of the program is available at -. +. lbtt is free software, you may change and redistribute it under the terms of the GNU General Public License. lbtt comes with @@ -82,4 +82,4 @@ Documentation: The documentation is also available in various formats at the program's home page at - . + . diff --git a/lbtt/configure.ac b/lbtt/configure.ac index 57a31b35f..6dec5b8a0 100644 --- a/lbtt/configure.ac +++ b/lbtt/configure.ac @@ -1,8 +1,8 @@ # Process this file with autoconf to produce a configure script. AC_PREREQ([2.53]) -AC_INIT([lbtt], [1.0.1], [heikki.tauriainen@hut.fi]) -AC_REVISION([Revision: 1.1]) +AC_INIT([lbtt], [1.0.2], [heikki.tauriainen@hut.fi]) +AC_REVISION([Revision: 1.2]) AC_CONFIG_SRCDIR([src/main.cc]) AM_INIT_AUTOMAKE AM_CONFIG_HEADER([config.h]) diff --git a/lbtt/doc/lbtt.texi b/lbtt/doc/lbtt.texi index 167a02439..e70fe4455 100644 --- a/lbtt/doc/lbtt.texi +++ b/lbtt/doc/lbtt.texi @@ -14,12 +14,14 @@ This file documents how to use the LTL-to-B@"uchi translator testbench @command{lbtt}. -Copyright @copyright{} 2001 Heikki Tauriainen +Copyright @copyright{} 2003 Heikki Tauriainen @ifinfo @email{heikki.tauriainen@@hut.fi} @end ifinfo @ifnotinfo +@ifnothtml <@email{heikki.tauriainen@@hut.fi}> +@end ifnothtml @end ifnotinfo @ifhtml @@ -66,11 +68,11 @@ under the above conditions for modified versions. @author Heikki Tauriainen <@email{heikki.tauriainen@@hut.fi}> @page @vskip 0pt plus 1filll -Copyright @copyright{} 2001 Heikki Tauriainen +Copyright @copyright{} 2003 Heikki Tauriainen <@email{heikki.tauriainen@@hut.fi}> 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 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 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. @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 in practice. (See @ifnottex -@ref{[Tau00]} +@ref{[TH02]} @end ifnottex @iftex -[Tau00] +[TH02] @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 error in a translator, @command{lbtt} can generate sample data which causes 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 background of the different tests; see, for example, @ifnottex +@ref{[TH02]} +@end ifnottex +@iftex +[TH02] +@end iftex +or +@ifnottex @ref{[Tau00]} @end ifnottex @iftex @@ -3821,10 +3830,10 @@ originally based on the algorithm presented in @end iftex See @ifinfo -@url{http://netlib.bell-labs.com/netlib/spin/whatispin.html} +@url{http://spinroot.com/spin/whatispin.html} @end ifinfo @ifnotinfo -<@uref{http://netlib.bell-labs.com/netlib/spin/whatispin.html}> +<@uref{http://spinroot.com/spin/whatispin.html}> @end ifnotinfo for more information. @@ -3947,19 +3956,25 @@ pages 247---263. Springer-Verlag, 2000. @item @anchor{[Tau00]} [Tau00] 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, 2000. Available on the WWW at @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 @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 @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 +@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] M.@: Y.@: Vardi. An automata-theoretic approach to linear temporal logic. In @i{Logics for Concurrency: Structure versus Automata}, volume 1043 of diff --git a/lbtt/src/Alloc.h b/lbtt/src/Alloc.h index 73fe13ef0..f264fee63 100644 --- a/lbtt/src/Alloc.h +++ b/lbtt/src/Alloc.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/BitArray.cc b/lbtt/src/BitArray.cc index f2086ab47..1d0342ab7 100644 --- a/lbtt/src/BitArray.cc +++ b/lbtt/src/BitArray.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * 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) ; - if (i == max_count) + if (i == bsize) return max_count; unsigned char c = bits[i]; diff --git a/lbtt/src/BitArray.h b/lbtt/src/BitArray.h index d8ef12b96..0efbac3f0 100644 --- a/lbtt/src/BitArray.h +++ b/lbtt/src/BitArray.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/Bitset.h b/lbtt/src/Bitset.h index 82f87667c..f74da7251 100644 --- a/lbtt/src/Bitset.h +++ b/lbtt/src/Bitset.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/BuchiAutomaton.cc b/lbtt/src/BuchiAutomaton.cc index 7be826c8e..77d0707cf 100644 --- a/lbtt/src/BuchiAutomaton.cc +++ b/lbtt/src/BuchiAutomaton.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/BuchiAutomaton.h b/lbtt/src/BuchiAutomaton.h index 7b58867b3..a9622f82e 100644 --- a/lbtt/src/BuchiAutomaton.h +++ b/lbtt/src/BuchiAutomaton.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/Config-lex.ll b/lbtt/src/Config-lex.ll index e09e51308..96d43b5c4 100644 --- a/lbtt/src/Config-lex.ll +++ b/lbtt/src/Config-lex.ll @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/Config-parse.yy b/lbtt/src/Config-parse.yy index 07fba1c17..fec1407cc 100644 --- a/lbtt/src/Config-parse.yy +++ b/lbtt/src/Config-parse.yy @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/Configuration.cc b/lbtt/src/Configuration.cc index 8392ca33f..f3ac26cb6 100644 --- a/lbtt/src/Configuration.cc +++ b/lbtt/src/Configuration.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/Configuration.h b/lbtt/src/Configuration.h index 99ad8b49a..b58234e45 100644 --- a/lbtt/src/Configuration.h +++ b/lbtt/src/Configuration.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/DispUtil.cc b/lbtt/src/DispUtil.cc index 3c99f0d43..aac917d6a 100644 --- a/lbtt/src/DispUtil.cc +++ b/lbtt/src/DispUtil.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/DispUtil.h b/lbtt/src/DispUtil.h index ff0040c63..4c779aaf3 100644 --- a/lbtt/src/DispUtil.h +++ b/lbtt/src/DispUtil.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/EdgeContainer.h b/lbtt/src/EdgeContainer.h index b0180304d..1d4674e72 100644 --- a/lbtt/src/EdgeContainer.h +++ b/lbtt/src/EdgeContainer.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/Exception.h b/lbtt/src/Exception.h index 274ab3be6..d3c248be4 100644 --- a/lbtt/src/Exception.h +++ b/lbtt/src/Exception.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/ExternalTranslator.cc b/lbtt/src/ExternalTranslator.cc index d73091da7..14a8e42fb 100644 --- a/lbtt/src/ExternalTranslator.cc +++ b/lbtt/src/ExternalTranslator.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/ExternalTranslator.h b/lbtt/src/ExternalTranslator.h index 4835f6ef0..17faaacee 100644 --- a/lbtt/src/ExternalTranslator.h +++ b/lbtt/src/ExternalTranslator.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/FormulaRandomizer.cc b/lbtt/src/FormulaRandomizer.cc index bdd5f87df..10497fac9 100644 --- a/lbtt/src/FormulaRandomizer.cc +++ b/lbtt/src/FormulaRandomizer.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/FormulaRandomizer.h b/lbtt/src/FormulaRandomizer.h index c23348f49..cdeca4422 100644 --- a/lbtt/src/FormulaRandomizer.h +++ b/lbtt/src/FormulaRandomizer.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/FormulaWriter.h b/lbtt/src/FormulaWriter.h index 0df6ecfbf..f2e9cfe77 100644 --- a/lbtt/src/FormulaWriter.h +++ b/lbtt/src/FormulaWriter.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/Graph.h.in b/lbtt/src/Graph.h.in index f701b58a3..22a07ec86 100644 --- a/lbtt/src/Graph.h.in +++ b/lbtt/src/Graph.h.in @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/LbtWrapper.h b/lbtt/src/LbtWrapper.h index 70319c2da..af555df35 100644 --- a/lbtt/src/LbtWrapper.h +++ b/lbtt/src/LbtWrapper.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/LtlFormula.cc b/lbtt/src/LtlFormula.cc index 5d0aa0cef..71a2aa6d0 100644 --- a/lbtt/src/LtlFormula.cc +++ b/lbtt/src/LtlFormula.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/LtlFormula.h b/lbtt/src/LtlFormula.h index fee7e8f60..3b1a0300d 100644 --- a/lbtt/src/LtlFormula.h +++ b/lbtt/src/LtlFormula.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/NeverClaim-lex.ll b/lbtt/src/NeverClaim-lex.ll index 8123ee3a8..d2f6d7bd4 100644 --- a/lbtt/src/NeverClaim-lex.ll +++ b/lbtt/src/NeverClaim-lex.ll @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/NeverClaim-parse.yy b/lbtt/src/NeverClaim-parse.yy index 8688dd00a..ea0ee5703 100644 --- a/lbtt/src/NeverClaim-parse.yy +++ b/lbtt/src/NeverClaim-parse.yy @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/NeverClaimAutomaton.cc b/lbtt/src/NeverClaimAutomaton.cc index 7f6ad3592..341fd36df 100644 --- a/lbtt/src/NeverClaimAutomaton.cc +++ b/lbtt/src/NeverClaimAutomaton.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -312,7 +312,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] = ' '; diff --git a/lbtt/src/NeverClaimAutomaton.h b/lbtt/src/NeverClaimAutomaton.h index 6f93881f0..69759bd7d 100644 --- a/lbtt/src/NeverClaimAutomaton.h +++ b/lbtt/src/NeverClaimAutomaton.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/PathEvaluator.cc b/lbtt/src/PathEvaluator.cc index 84b769974..d42243bcd 100644 --- a/lbtt/src/PathEvaluator.cc +++ b/lbtt/src/PathEvaluator.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/PathEvaluator.h b/lbtt/src/PathEvaluator.h index f8ff84091..cf0c79e0b 100644 --- a/lbtt/src/PathEvaluator.h +++ b/lbtt/src/PathEvaluator.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/PathIterator.cc b/lbtt/src/PathIterator.cc index 3f468940a..740a3a19f 100644 --- a/lbtt/src/PathIterator.cc +++ b/lbtt/src/PathIterator.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/PathIterator.h b/lbtt/src/PathIterator.h index 8c6f914ca..6411692a4 100644 --- a/lbtt/src/PathIterator.h +++ b/lbtt/src/PathIterator.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/ProductAutomaton.cc b/lbtt/src/ProductAutomaton.cc index c0513404a..3e568ea92 100644 --- a/lbtt/src/ProductAutomaton.cc +++ b/lbtt/src/ProductAutomaton.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -864,12 +864,15 @@ void ProductAutomaton::findAcceptingExecution all_acceptance_sets_on_path = false; } + deque cycle_fragment; while (state != bfs_root) { - cycle.push_back(make_pair(buchiState(state), - systemState(state))); + cycle_fragment.push_back(make_pair(buchiState(state), + systemState(state))); state = shortest_path_predecessor[state]; } + cycle.insert(cycle.begin(), cycle_fragment.begin(), + cycle_fragment.end()); bfs_root = (*predecessor)->targetNode(); visited.clear(nodes.size()); @@ -887,13 +890,16 @@ void ProductAutomaton::findAcceptingExecution backward_search_queue.pop_front(); } + deque cycle_fragment; while (state != bfs_root) { - cycle.push_back(make_pair(buchiState(state), - systemState(state))); + cycle_fragment.push_back(make_pair(buchiState(state), + systemState(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), systemState(search_start_state))); diff --git a/lbtt/src/ProductAutomaton.h b/lbtt/src/ProductAutomaton.h index ccd567468..e4c8c33fe 100644 --- a/lbtt/src/ProductAutomaton.h +++ b/lbtt/src/ProductAutomaton.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/Random.h b/lbtt/src/Random.h index 2650599a5..3820b30d3 100644 --- a/lbtt/src/Random.h +++ b/lbtt/src/Random.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/SccIterator.h b/lbtt/src/SccIterator.h index 838008c42..a8547bc13 100644 --- a/lbtt/src/SccIterator.h +++ b/lbtt/src/SccIterator.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/SharedTestData.h b/lbtt/src/SharedTestData.h index ff4cd9209..1a2a9898b 100644 --- a/lbtt/src/SharedTestData.h +++ b/lbtt/src/SharedTestData.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/SpinWrapper.cc b/lbtt/src/SpinWrapper.cc index 1b21aa68c..d66e45571 100644 --- a/lbtt/src/SpinWrapper.cc +++ b/lbtt/src/SpinWrapper.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/SpinWrapper.h b/lbtt/src/SpinWrapper.h index 233d62b06..a43dcc6df 100644 --- a/lbtt/src/SpinWrapper.h +++ b/lbtt/src/SpinWrapper.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/StatDisplay.cc b/lbtt/src/StatDisplay.cc index 6da2df696..2fabdcc47 100644 --- a/lbtt/src/StatDisplay.cc +++ b/lbtt/src/StatDisplay.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * 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) + estream << '\n'; estream << ind + " operator " + symbol_name_string + '\n' + ind + " # " + symbol_number_string + '\n' + ind + " #/formula " + symbol_distribution_string diff --git a/lbtt/src/StatDisplay.h b/lbtt/src/StatDisplay.h index 83469a460..8a6cc1a6a 100644 --- a/lbtt/src/StatDisplay.h +++ b/lbtt/src/StatDisplay.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/StateSpace.cc b/lbtt/src/StateSpace.cc index 90a155f3a..4782846f8 100644 --- a/lbtt/src/StateSpace.cc +++ b/lbtt/src/StateSpace.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/StateSpace.h b/lbtt/src/StateSpace.h index fc356ba1b..9b3328966 100644 --- a/lbtt/src/StateSpace.h +++ b/lbtt/src/StateSpace.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/StateSpaceRandomizer.cc b/lbtt/src/StateSpaceRandomizer.cc index 550f418c4..8cc928d87 100644 --- a/lbtt/src/StateSpaceRandomizer.cc +++ b/lbtt/src/StateSpaceRandomizer.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/StateSpaceRandomizer.h b/lbtt/src/StateSpaceRandomizer.h index 03dd3ee07..44d2b583a 100644 --- a/lbtt/src/StateSpaceRandomizer.h +++ b/lbtt/src/StateSpaceRandomizer.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/StringUtil.cc b/lbtt/src/StringUtil.cc index e60b354fe..bb61e80ea 100644 --- a/lbtt/src/StringUtil.cc +++ b/lbtt/src/StringUtil.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/StringUtil.h b/lbtt/src/StringUtil.h index 8b1623352..dca736e9a 100644 --- a/lbtt/src/StringUtil.h +++ b/lbtt/src/StringUtil.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/TestOperations.cc b/lbtt/src/TestOperations.cc index 790237858..3c7ade3fc 100644 --- a/lbtt/src/TestOperations.cc +++ b/lbtt/src/TestOperations.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/TestOperations.h b/lbtt/src/TestOperations.h index 314690614..b1b012634 100644 --- a/lbtt/src/TestOperations.h +++ b/lbtt/src/TestOperations.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/TestRoundInfo.h b/lbtt/src/TestRoundInfo.h index b77e7f674..1c7c5beb2 100644 --- a/lbtt/src/TestRoundInfo.h +++ b/lbtt/src/TestRoundInfo.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/TestStatistics.cc b/lbtt/src/TestStatistics.cc index b791e27b4..fb04f18d9 100644 --- a/lbtt/src/TestStatistics.cc +++ b/lbtt/src/TestStatistics.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/TestStatistics.h b/lbtt/src/TestStatistics.h index 75a4c7c3f..074f63779 100644 --- a/lbtt/src/TestStatistics.h +++ b/lbtt/src/TestStatistics.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/TranslatorInterface.h b/lbtt/src/TranslatorInterface.h index 8053c5bac..d158d2eee 100644 --- a/lbtt/src/TranslatorInterface.h +++ b/lbtt/src/TranslatorInterface.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/UserCommandReader.cc b/lbtt/src/UserCommandReader.cc index 6365784f3..2f688b51e 100644 --- a/lbtt/src/UserCommandReader.cc +++ b/lbtt/src/UserCommandReader.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/UserCommandReader.h b/lbtt/src/UserCommandReader.h index da087daca..abe22cb77 100644 --- a/lbtt/src/UserCommandReader.h +++ b/lbtt/src/UserCommandReader.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/UserCommands.cc b/lbtt/src/UserCommands.cc index ae5a6630a..c948c85c2 100644 --- a/lbtt/src/UserCommands.cc +++ b/lbtt/src/UserCommands.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -965,53 +965,73 @@ void printAutomatonAnalysisResults * intersection automaton from the result. */ - deque prefix; - deque cycle; vector path; - while (!execution.first.empty()) - { - prefix.push_back(execution.first.front().first); - path.push_back(execution.first.front().first); - execution.first.pop_front(); - } + for (deque::const_iterator + state = execution.first.begin(); + state != execution.first.end(); + ++state) + path.push_back(state->first); - while (!execution.second.empty()) - { - cycle.push_back(execution.second.front().first); - path.push_back(execution.second.front().first); - execution.second.pop_front(); - } + const vector + ::size_type loop_pos = path.size(); + + for (deque::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 * by giving suitable truth assignments for the atomic propositions in - * selected states of the state space to which the intersection automaton - * was converted. + * 'path.size()' states, where `path' corresponds to an accepting run of + * 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 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 ::size_type state = 0; state + 1 < path.size(); - state++) + ++state) { + GraphEdgeContainer::const_iterator transition; + for (transition = (*a)[path[state]].edges().begin(); (*transition)->targetNode() != path[state + 1]; ++transition) ; - automaton_as_statespace[path[state]].positiveAtoms() + automaton_as_statespace[state].positiveAtoms() = static_cast(*transition) ->guard().findPropositionalModel (configuration.formula_options.formula_generator. number_of_available_variables); + + (state < loop_pos ? prefix : cycle).push_back(state); } - path.pop_back(); + path.pop_back(); /* remove the sentinel element */ delete a; a = 0; @@ -1038,40 +1058,25 @@ void printAutomatonAnalysisResults deque aut_cycle; - const deque* - original_execution_states; - deque* - new_execution_states; - for (int i = 0; i < 2; i++) { aut_prefix.clear(); aut_cycle.clear(); - for (int j = 0; j < 2; j++) - { - if (j == 0) - { - original_execution_states = &prefix; - new_execution_states = &aut_prefix; - } - else - { - original_execution_states = &cycle; - new_execution_states = &aut_cycle; - } + deque* + new_execution_states = &aut_prefix; - for (deque::const_iterator - execution_state = original_execution_states->begin(); - execution_state != original_execution_states->end(); - ++execution_state) - { - new_execution_states->push_back - (i == 0 - ? intersection_state_mapping[*execution_state].first - : intersection_state_mapping[*execution_state].second); - } + for (vector + ::size_type state_id = 0; + state_id < path.size(); + ++state_id) + { + if (state_id == loop_pos) + new_execution_states = &aut_cycle; + new_execution_states->push_back + (i == 0 + ? intersection_state_mapping[path[state_id]].first + : intersection_state_mapping[path[state_id]].second); } synchronizePrefixAndCycle(aut_prefix, aut_cycle); @@ -1083,13 +1088,27 @@ void printAutomatonAnalysisResults 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 + ::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, ' ') + "Analysis of the positive formula in the execution M:\n"; Ltl::PathEvaluator path_evaluator; bool result = path_evaluator.evaluate - (*round_info.formulae[formula], automaton_as_statespace, path, - prefix.size()); + (*round_info.formulae[formula], automaton_as_statespace, path, loop_pos); path_evaluator.print(stream, indent + 4); diff --git a/lbtt/src/UserCommands.h b/lbtt/src/UserCommands.h index 02b7a0925..feecf49b8 100644 --- a/lbtt/src/UserCommands.h +++ b/lbtt/src/UserCommands.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/main.cc b/lbtt/src/main.cc index 8cf2c665d..01c7e386d 100644 --- a/lbtt/src/main.cc +++ b/lbtt/src/main.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/translate.cc b/lbtt/src/translate.cc index bf2679c74..6580a4bb1 100644 --- a/lbtt/src/translate.cc +++ b/lbtt/src/translate.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/translate.h b/lbtt/src/translate.h index b0fb7e53f..b25d06caf 100644 --- a/lbtt/src/translate.h +++ b/lbtt/src/translate.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or