[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Fri, 29 Jul 2022 14:09:35 +0200
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
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
|[Prev in Thread]
||[Next in Thread]|
- Counterexamples timeout,
Frank Heckenbach <=