Hello Denis,
As far as I know, the decomposition of the quantifications over tuples
is done quite early in the Why3 processing ("eval_match" in the WP calculus)
Using a record structure is probably a good workaround, and I don't
think you need to bother with any "model_projection" labels for that. With
type r = { a:bool; b:bool }
let bar (p "model" : r) : bool
ensures { "model_vc" p.a \/ (not p.b) }
= True
I get (with why3 0.88.3)
$ why3 prove --get-ce -P CVC4,1.5 t.mlw
t.mlw Ex WP_parameter bar : Unknown (other) (0.00s)
Counter-example model:File t.mlw:
Line 5:
p.a = {"type" : "Boolean" , "val" : false }
p.b = {"type" : "Boolean" ,
"val" : true }
Line 6:
p.a = {"type" : "Boolean" , "val" : false }
p.b = {"type" : "Boolean" ,
"val" : true }
- Claude
Le 01/02/2018 à 15:30, Denis Cousineau a écrit :
> Dear list,
> I'm stucked with an apparently simple problem of counter-examples
> printing and I'd appreciate a lot if someone had a clue to help me.
> I have a Why3 formalization that deals with Bool tuples. And I'd like to
> print those tuples values when a counter-example is found.
>
> Here's an example:
>
> ***
> module Ex
> let bla (p "model" : (bool,bool)) : bool
> ensures { "model_vc" let a,b = p in a \/ (not b) }
> = True
> end
>
> ***
>
> This dummy example's only goal is to have cvc4 (or another prover)
> exhibit a counter-example with value (False,True) for "p".
>
> When running why3 (0.87.3) on this example,
> ( why3 prove -P cvc4 --get-ce ex.mlw )
> the smt goal is the following:
>
> ****
> (assert
> ;; WP_parameter_bla
> ;; File "ex_poj_tuple_ce.mlw", line 2, characters 4-7
> (not (forall ((p Bool) (p1 Bool)) (or (= p true) (not (= p1 true))))))
>
> ****
>
> The universal quantification on (bool,bool) is currified and we have now
> two universal quantifications on bool.
>
> Unfortunately it seems that the counter-example mechanism does not
> remember this currification when giving back to the Why3 user the
> interpretation of the cvc4 counter-example model:
>
> ***
> ex.mlw Ex WP_parameter bla : Unknown (0.00s)
> Counter-example model:File ex.mlw:
> Line 2:
> p = true
> Line 3:
> p = true
>
> ***
>
> (If I understand well, that "p" corresponds to the right member of the
> original "p").
>
> To bypass this problem, I have thought of using a record structure with
> two boolean fields instead of a boolean pair and using "model
> projections" to print the counter-examples fields.
>
> Does anyone have a(nother) clue to solve my problem ?
>
> Thanks,
>
> Denis Cousineau
>
>
>
> ---
> *Denis * *Cousineau*, Ph.D
> デニ クズノ
> Researcher
> Formal Methods: Theory, Methodology and Tools
> Information and Network Systems (INS) Team
> Communication & Information Systems (CIS) Division
> *Mitsubishi Electric R&D Centre Europe* (MERCE)
> Tel: +33(0)2 23 45 58 36 Fax: +33 (0)2 23 45 58 59
> http://www.fr.mitsubishielectric-rce.eu
>
>
>
> _______________________________________________
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
--
Claude Marché | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France |
Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex |
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
