bug-bison
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Counterexamples timeout


From: Frank Heckenbach
Subject: Counterexamples timeout
Date: Fri, 29 Jul 2022 14:09:35 +0200

Hi,

I don't know if it's something peculiar about my grammars, but it
seems when using "-Wcounterexamples", Bison either finds
counterexamples almost immediately or runs into the timeout.
(Or maybe 6 seconds (see below) are just so eternally long to a
modern CPU that there's not much between that and infinity. ;)

So waiting so long seems pointless, especially when there are a lot
of conflicts (as there often arise at once when experimenting with a
grammar).

RTFS shows me that the timeout can be set with an environment
variable "TIME_LIMIT" which is undocumented (and named a bit too
generic to my taste), but more importantly can't be set via
something like BISON_FLAGS in a Makefile.

The limit is parsed as a double, but checked in whole second
increments due to using difftime which seems a strange function to
me, taking two integers (time_t) and returning their difference as a
double, so that might not be easy to change.

Also, there seems to be an off-by-epsilon error in
"time_passed > time_limit", so the default time_limit = 5.0 actually
results in a timeout of 6.0 seconds, and to get a timeout of 1
second (the minimum possible), one needs "TIME_LIMIT=0" (or some
value < 1 such as 0.9, but apart from looking strange, strtod is
locale-dependent, so one would actually need something like
"LC_ALL= LC_NUMERIC=C TIME_LIMIT=0.9").

So I suggest to change this check to ">=", and to introduce a
command line option that either takes an integer or (if you plan to
actually support split seconds) a double parsed in a
locale-independent way.



reply via email to

[Prev in Thread] Current Thread [Next in Thread]