bug-bison
[Top][All Lists]
Advanced

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

Re: Counterexamples timeout


From: Jacob L. Mandelson
Subject: Re: Counterexamples timeout
Date: Thu, 15 Sep 2022 10:02:57 -0700
User-agent: Mutt/1.9.4 (2018-02-28)

On Thu, Sep 15, 2022 at 06:26:12PM +0200, Akim Demaille wrote:
> Hi Frank,
> 
> > Le 29 juil. 2022 à 14:09, Frank Heckenbach <f.heckenbach@fh-soft.de> a 
> > écrit :
> > 
> > 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. ;)
> > [...]
> 
> I agree.  Let's change that.  What do you think about this proposal?

I think the English text needs a few minor edits.


> commit 6a15951030ade757de13159e545394af3cd40205
> Author: Akim Demaille <akim.demaille@gmail.com>
> Date:   Tue Sep 13 08:25:59 2022 +0200
> 
>     cex: provide the user with a means to change the timeout
>     
>     Reported by Frank Heckenbach.
>     https://lists.gnu.org/r/bug-bison/2022-07/msg00011.html
>     
>     * bootstrap.conf: Use c_strtod, so that even in French locales "1.5"
>     is accepted, instead of "1,5".
>     * src/counterexample.c, src/state-item.c: Use xtime_t instead of
>     time_t, so that accuracy goes from seconds to nanoseconds.
>     ( counterexample_init): Depend on cex.timeout rather than
>     $TIME_LIMIT.
>     * doc/bison.texi (%define Summary): Document cex.timeout.
> 
> diff --git a/NEWS b/NEWS
> index f480cb95..32e7361a 100644
> --- a/NEWS
> +++ b/NEWS
> @@ -8,6 +8,10 @@ GNU Bison NEWS
>  
>    The C++ skeletons now expose copy and move operators for symbols.
>  
> +  The `cex.timeout` %define variable allows to control when we give up
> +  finding a unifying counterexample.  For instance `bison -Wcex
> +  -Dcex.timeout=.5 gram.y` to give 1/2s of credit.

Is "credit" used this way elsewhere in the documentation?  It feels like
an unnatural usage to me.  I'd either change it to "limit" (eg, "... to 
limit to 1/2s" or "... for a limit of 1/2s") or rephrase (eg, "... to
stop after 1/2s").

[...]
> +@c ================================================== cex.timeout
> +
> +@deffn Directive {%define cex.timeout} @var{duration}
> +
> +@itemize @bullet
> +@item Language(s): all
> +
> +@item Purpose:
> +Define the time credit allocated to finding unifying counterexamples.

"Define the time limit for finding unifying counterexamples."

[...]
> diff --git a/src/muscle-tab.c b/src/muscle-tab.c
> index 0945d609..40295542 100644
> --- a/src/muscle-tab.c
> +++ b/src/muscle-tab.c
> @@ -127,6 +127,9 @@ muscle_init (void)
>  
>    muscle_table = hash_xinitialize (HT_INITIAL_CAPACITY, NULL, hash_muscle,
>                                     hash_compare_muscles, muscle_entry_free);
> +  /* Avoid warnings if the user defined this variable, but did not
> +     actually called -Wcex.  */

"actually use -Wcex" or "actually call with -Wcex".


Be well,
    -- Jacob



reply via email to

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