Hello Claude, thanks a lot for your quick response. After sending the e-mail, I started to implement the workaround with records and, indeed, contrary to what I wrote, "model_projections" labels are useless in that case. I can now post-process the why3 output to print the counter-example model elements the way I want. The only remaining concern could be the possible overhead that results from using records instead of tuples. I'll run tests to check that point on my particular development. Thanks again,
Denis --- 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 ------ Original Message ------ From: "Claude Marché" <claude.mar...@inria.fr> To: "why3-club@lists.gforge.inria.fr" <why3-club@lists.gforge.inria.fr> Sent: 01/02/2018 16:45:49 Subject: Re: [Why3-club] Tuples and counter-examples printing > >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 _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
