Commit graph

40 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
3793454864 [lbtt] Fix issues reported by Clang++ 3.1.
* src/Graph.h.in (PathElement::hasEdge): Check the correct
pointer, not the address of some member function.
* src/BuchiAutomaton.cc, src/Configuration.cc,
src/TestOperations.cc, src/TestOperations.h: Recode these files in
utf-8.
2012-07-02 17:35:22 +02:00
Alexandre Duret-Lutz
e9e132dd29 [lbtt] Adjust parsers to accommodate old and new versions of Automake.
* src/Config-parse.yy, src/Ltl-parse.yy, src/NeverClaim-parse.yy:
Rename these as..
* src/Config-parse.y, src/Ltl-parse.y, src/NeverClaim-parse.y:
... these.
* src/Config-parse_.cc, src/Ltl-parse_.cc,
src/NeverClaim-parse_.cc: New files to hack around
incompatibilities between Automake 1.12 and Automake 1.11.
* src/Makefile.am: Adjust.
* NEWS: Mention this change.
2012-06-19 17:34:28 +02:00
Alexandre Duret-Lutz
a8fd9e8b14 [lbtt] Make it clearer this is not LBTT 1.2.1.
* configure.ac: Bump the version number to 1.2.1a.
* NEWS: Summarize all changes since 1.2.1.
* README: Warn this is not 1.2.1, and add pointers to NEWS and
ChangeLog.
2012-05-21 15:37:42 +02:00
Tomáš Babiak
f2b188d9ec [lbtt] Count deterministic automata and deterministic states.
* src/BuchiAutomaton.h, src/BuchiAutomaton.cc
(BuchiState::isDeterministic, BuchiAutomaton::isDeterministic,
BuchiAutomaton::nondeterminismIndex): New methods.
* src/TestOperations.cc (generateBuchiAutomaton): Collect
nondeterminism indices, and count deterministic automata.
* src/TestStatistics.cc, src/TestStatistics.h: Add storage
for these statistics.
* src/StatDisplay.cc (printBuchiAutomatonStats,
printCollectiveStats): Display these statistics.
2012-05-21 14:39:27 +02:00
Alexandre Duret-Lutz
8aa653e010 [lbtt] Fix make pdf.
* doc/gpl.texi: Fix make pdf for newer texinfo.tex.
2012-04-27 22:47:54 +02:00
Alexandre Duret-Lutz
907ba16bfa [lbtt] Remove a useless configure check.
* configure.ac: Do not check for mkstemp(), it is not used.
2012-04-27 15:40:54 +02:00
Alexandre Duret-Lutz
35a57c6dff [lbtt] Accept W and M in lbtt-translate --spot.
* src/SpotWrapper.cc: Translate W and M operators.
2010-04-12 16:39:57 +02:00
Alexandre Duret-Lutz
9cbaae7b66 [lbtt]
Let "make dvi" work on Ubuntu.

* doc/lbtt.texi (The formula generation algorithm): Use op^\prime
instead of op', because etex on Ubuntu hangs (an infinite loop?)
on the later when texi2dvi tries to compile a dvi.
2010-01-22 13:14:48 +01:00
Alexandre Duret-Lutz
a6b9583628 [lbtt]
Kill some warnings on Ubuntu.

* src/UserCommandReader.cc (UserCommandInterface): Explicitly
ignore the return code of system() to kill a warning.
* src/TestOperations.cc (generateBuchiAutomaton): Explicitly
ignore the return code of write() to kill a warning.
2010-01-21 15:58:18 +01:00
Guillaume Sadegh
1f19198d2d [LBTT] Add a missing include.
* src/translate.cc: exit(2) requires cstdlib.
2010-01-17 02:15:08 +01:00
Alexandre Duret-Lutz
3cbd681c6d [lbtt]
Fix generation of random formulae on 64bits systems.

* src/main.cc (testLoop): Generate random short ints between 0 and
SHRT_MAX, not between 0 and LONG_MAX.  On systems where long ints
are 64bits, LRAND(0,LONG_MAX) was returning a value with the lower
32 bits set to 0, and the latter truncation to short int always
yielded the value 0.  Consequently all generated formulae were
identical...
2009-11-26 15:51:01 +01:00
Alexandre Duret-Lutz
c95eb21ecf [lbtt]
* src/Configuration.cc (registerAlgorithm): Do not complain about
a missing path for disabled algorithms.
2009-11-25 18:07:55 +01:00
Guillaume Sadegh
b3e8797c51 [lbtt] Adjust to support the Intel compiler (icpc).
* configure.ac: Adjust to call...
    * m4/intel.m4: ...this new macro.
    * Makefile.am: Add the directory `m4' as an includedir of
    autoconf's macros.
2009-06-12 16:38:25 +02:00
Alexandre Duret-Lutz
2cc7c253f1 [lbtt] Adjust parser to Bison 2.4.1. 2009-05-31 21:27:47 +02:00
Alexandre Duret-Lutz
6c2bdf4512 Update to LBTT 1.2.1 2008-04-10 10:20:40 +02:00
Alexandre Duret-Lutz
ab1a2ae5d7 * src/main.cc: Include <climits> for LONG_MAX. lbtt won't
compile with g++-4.3 otherwise.
* src/Ltl-parse.yy (matchCharactersFromStream): Declare the chars
as const to kill a g++ warning.
* src/NeverClaim-parse.yy (yyerror): Declare the error
message as const to kill a g++ warning.
2008-03-14 16:59:40 +01:00
Alexandre Duret-Lutz
91df6cab77 fix status of lbtt's subtree. Apparently it was messed up during the cvsimport 2008-02-25 14:30:09 +01:00
Alexandre Duret-Lutz
17f76e371f * lbtt/: Merge lbtt 1.2.0. 2005-08-31 15:30:38 +00:00
Alexandre Duret-Lutz
f3dc612d64 * lbtt/: Merge lbtt 1.1.2. 2004-08-02 09:02:19 +00:00
Alexandre Duret-Lutz
70597c3f51 * lbtt/: Merge lbtt 1.1.1. 2004-07-30 11:50:08 +00:00
Alexandre Duret-Lutz
85d2b7b287 * configure.ac: Call AC_GNU_SOURCE to make glibc's strsignal
definition visible even to non-GNU compilers.
2004-07-16 16:25:38 +00:00
Alexandre Duret-Lutz
e11da2e3af * lbtt/: Merge lbtt 1.1.0.
* src/tgbatest/spotlbtt.test: Adjust config file syntax to
please lbtt 1.1.0.
2004-07-07 17:41:42 +00:00
Alexandre Duret-Lutz
b84e6a6440 * src/Makefile.am (EXTRA_lbtt_SOURCES): Remove Config-parse.h,
it is automatically distributed.
(EXTRA_lbtt_translate_SOURCES): Likewise, remove NeverClaim-parse.h.
2004-03-09 09:49:48 +00:00
Alexandre Duret-Lutz
1d411fa3c1 * configure.ac (YACC): Do not add `-d' here...
* src/Makefile.am (AM_YFLAGS): ... do it here.
(BUILT_SOURCES): New variable.
2004-03-08 17:53:54 +00:00
Alexandre Duret-Lutz
3aec630540 * doc/texinfo.tex: New upstream version. 2004-03-08 17:23:36 +00:00
Alexandre Duret-Lutz
4741dc02bf * lbtt/: Merge lbtt 1.0.3. 2004-02-16 12:09:29 +00:00
Alexandre Duret-Lutz
665216b0c2 * src/ExternalTranslator.cc: Include sys/wait.h. 2004-02-12 14:16:55 +00:00
Alexandre Duret-Lutz
2b7c9ea395 * src/SpotWrapper.cc (SpotWrapper::SPOT_AND, SpotWrapper::SPOT_OR):
Define as && and || as in Spin.
* src/SpotWrapper.hh: Update by email.
2004-02-11 15:20:45 +00:00
Alexandre Duret-Lutz
4b4b640ec4 * src/TestOperations.cc: Include sys/wait.h. 2004-01-16 16:04:04 +00:00
Alexandre Duret-Lutz
7c1ac7bb67 * src/Alloc.h: Rename as ...
* src/ObstackAlloc.h: ... this.  The problem is that alloc.h is a
system header in g++ < 3.0, and Darwin has a case-insensitive
filesystem.  System headers that include alloc.h pick the local
Alloc.h version.
* BuchiAutomaton.h, Configuration.h, DispUtil.cc,
ExternalTranslator.h, FormulaRandomizer.h, Graph.h.in,
LtlFormula.h, Makefile.am, NeverClaimAutomaton.h, PathEvaluator.h,
ProductAutomaton.h, SccIterator.h, SharedTestData.h,
StatDisplay.h, StateSpace.h, StateSpaceRandomizer.cc,
StringUtil.h, TestOperations.h, TestRoundInfo.h, TestStatistics.h,
UserCommandReader.h, UserCommands.h, main.cc: Adjust includes.
2004-01-16 13:30:42 +00:00
Alexandre Duret-Lutz
1b0fe66393 * doc/texinfo.tex: New upstream version. 2003-12-29 10:57:51 +00:00
Alexandre Duret-Lutz
48c03b89b8 * src/TestOperations.cc (generateBuchiAutomaton): Forward SIGINT
and SIGQUIT.
* src/ExternalTranslator.cc (ExternalTranslator::translate): Likewise.
* src/main.cc (main): Do not intercept SIGINT in
non-interactive runs.
2003-07-29 13:06:53 +00:00
Alexandre Duret-Lutz
ea90d2f8be merge changes with lbtt 1.0.2 2003-07-29 12:21:22 +00:00
Alexandre Duret-Lutz
7836595873 * doc/lbtt.texi: Never use @-commands in @node names, recent Texinfo
versions are stricter on this.
2003-07-13 14:45:03 +00:00
Alexandre Duret-Lutz
871f421b5e spacing 2003-07-10 12:46:39 +00:00
Alexandre Duret-Lutz
bbba8ca966 Spot wants ^', not xor'.
* src/SpotWrapper.hh (SpotWrapper::SPOT_XOR): Declare.
* src/SpotWrapper.cc (SpotWrapper::SPOT_XOR): Define.
(SpotWrapper::translateFormula): Use SPOT_XOR.
2003-07-10 08:26:23 +00:00
Alexandre Duret-Lutz
71b7da1437 I want $? = 1 whenever some test fails.
* src/main.cc (testLoop): Return 1 iff an error occured.
(main): Use testLoop's output as exit status.
2003-07-09 15:34:53 +00:00
Alexandre Duret-Lutz
8af9996863 * src/ExternalTranslator.h (class ExternalTranslator):
Declare class SpotWrapper as a friend.
* src/SpotWrapper.h, src/SpotWrapper.cc: New files.
* src/Makefile.am (lbtt_translate_SOURCES): Add SpotWrapper.cc
and SpotWrapper.h.
* src/translate.cc (main): Add the --spot option, and build
a SpotWrapper of required.
2003-07-09 14:11:25 +00:00
Alexandre Duret-Lutz
bca9d83c44 * src/Config-parse.yy: Remove stray `,' in %token arguments.
* src/Alloc.h (__INT_TO_PTR): Redefine to work around glibc 2.3.
* doc/texinfo.tex: New upstream version.
2003-07-04 16:32:14 +00:00
Alexandre Duret-Lutz
ababb9ff93 Initial revision 2002-10-01 14:21:01 +00:00