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

*To*: Sam Owre <owre@xxxxxxxxxxx>*Subject*: Re: [PVS-Help] Very slow proveit/PVS proofs*From*: Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>*Date*: Tue, 18 Nov 2014 11:43:53 +0900*Cc*: pvs-help@xxxxxxxxxxx*In-reply-to*: <C6AB3395-9328-4588-8FDE-DF6B71A1C573@dependablecomputing.com>*List-archive*: <http://mls.csl.sri.com/pipermail/pvs-help>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <https://mls.csl.sri.com/cgi-bin/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <https://mls.csl.sri.com/cgi-bin/mailman/options/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <F88D25FC-4E8B-45E6-81AB-07FB2A25A540@dependablecomputing.com> <2D334402-D184-4A32-8DA3-9A31334E5273@dependablecomputing.com> <10459.1416047269@ubi> <53C73402-C56D-4C64-87E9-1C033944DC0A@dependablecomputing.com> <18613B2A-0C1B-409E-BC96-838C4C4A31A9@dependablecomputing.com> <21019.1416277147@ubi> <C6AB3395-9328-4588-8FDE-DF6B71A1C573@dependablecomputing.com>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Hi Sam, First, I want to say thanks for all of the help you've provided. Secondly, I've determined that for the LookupTestWithTheorems case, that's a bug on my side, not yours. (The LookupTest theory was modified in an unexpected manner which meant that the "simple_test" theorem is no longer true.) The "car" error still persists, however. Best Regards, Ben Hocking ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx > On Nov 18, 2014, at 11:35 AM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote: > > The discrepancy was probably in my .prf files. I'm still experiencing the "Error: Attempt to take the car of 256 which is not listp." message on distance2. Here is that file along with its .prf file: > <distance2.prf><distance2.pvs> > > I'm no longer getting the "Error: No next method for method" message with LookupTestWithTheorems.pvs, but the (grind) strategy which used to work with simple_test no longer does. Here are those files: > <LookupTest.prf><LookupTest.pvs><LookupTestWithTheorems.prf><LookupTestWithTheorems.pvs> > > To be on the safe side, I deleted my old .prf files and pvsbin contents and then checked out my old ones from my git repository. > > Best Regards, > Ben Hocking > ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx > > > > >> On Nov 18, 2014, at 11:19 AM, Sam Owre <owre@xxxxxxxxxxx> wrote: >> >> Hi Ben, >> There was a bug in that fix, could you try the following replacement? >> >> By the way,(grind) didn't cause the bug for me, it was (model-check), >> which is your default for TCCs that don't have "int" in their name - I >> don't know if there is a discrepancy between us that I should look into. >> Please let me know if there is. >> >> Thanks, >> Sam >> >> <patch-20141114.lisp> >> >> Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote: >> >>> Hi Sam, >>> >>> It seems that the new patch introduced some problems. I'm now getting errors on many proofs that used to work, usually when I run the (grind) strategy (a personal favorite of mine, I'm afraid). >>> >>> Here's a relatively simple theory that generates the message "Error: Attempt to take the car of 256 which is not listp.": >>> >>> >>> Here's another pair of theories (LookupTestWithTheorems uses LookupTest), that generates the message "Error: No next method for method": >>> >>> >>> >>> I have other theories I can provide that are having these problems, but I believe all of my error messages so far fall into one of those two general camps. >>> >>> Best Regards, >>> Ben Hocking >>> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx >>> >>> >>> >>> >>>> On Nov 15, 2014, at 7:39 PM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote: >>>> >>>> Outstanding, Sam. At least for the test 3d-lookup table it worked quickly: >>>> ~Tools/Simulink2PVS/com.dci.simulink2pvs >>>> ▶ time proveit -is lookup3d.pvs >>>> Processing ./lookup3d.pvs. Writing output to file ./lookup3d.summary >>>> Proving chain of imported theories >>>> Proof summary for theory lookup3d >>>> Theory totals: 3 formulas, 3 attempted, 3 succeeded (6.41 s) >>>> Grand Totals: 3 proofs, 3 attempted, 3 succeeded (6.41 s) >>>> proveit -is lookup3d.pvs 8.71s user 0.29s system 90% cpu 9.896 total >>>> >>>> ~Tools/Simulink2PVS/com.dci.simulink2pvs >>>> ▶ time proveit -is ndlookup_with_theorems.pvs >>>> Processing ./ndlookup_with_theorems.pvs. Writing output to file ./ndlookup_with_theorems.summary >>>> Proving chain of imported theories >>>> Proof summary for theory ndlookup_with_theorems >>>> test1.................................untried [Untried]( n/a s) >>>> Theory totals: 1 formulas, 0 attempted, 0 succeeded (0.00 s) >>>> Proof summary for theory ndlookup >>>> Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.00 s) >>>> Grand Totals: 6 proofs, 5 attempted, 5 succeeded (0.00 s) >>>> proveit -is ndlookup_with_theorems.pvs 0.69s user 0.11s system 92% cpu 0.857 total >>>> >>>> ~Tools/Simulink2PVS/com.dci.simulink2pvs >>>> ▶ pvs ndlookup_with_theorems.pvs >>>> >>>> ~Tools/Simulink2PVS/com.dci.simulink2pvs >>>> ▶ time proveit -is ndlookup_with_theorems.pvs >>>> Processing ./ndlookup_with_theorems.pvs. Writing output to file ./ndlookup_with_theorems.summary >>>> Proving chain of imported theories >>>> Proof summary for theory ndlookup_with_theorems >>>> Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) >>>> Proof summary for theory ndlookup >>>> Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.00 s) >>>> Grand Totals: 6 proofs, 6 attempted, 6 succeeded (0.00 s) >>>> proveit -is ndlookup_with_theorems.pvs 0.73s user 0.09s system 98% cpu 0.828 total >>>> Over the next week I'll have the opportunity to test it with some bigger lookup tables. I'll let you know how that goes. >>>> >>>> Thanks again! >>>> >>>> Best Regards, >>>> Ben Hocking >>>> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx >>>> >>>> >>>> >>>> >>>>> On Nov 15, 2014, at 7:27 PM, Sam Owre <owre@xxxxxxxxxxx> wrote: >>>>> >>>>> Hi Ben, >>>>> >>>>> I haven't tested it thoroughly, but could you try the following patch and >>>>> see if it fixes the problem? Just put the patch file in a >>>>> lib/pvs-patches/ subdirectory of your PVS installation (create it if >>>>> needed). >>>>> >>>>> Let me know what you find. >>>>> Thanks, >>>>> Sam >>>>> >>>>> <patch-20141114.lisp> >>>>> Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote: >>>>> >>>>>> As a follow-up, I’ve tried the following steps: 1) I separated out the 2-d and 3-d lookup tables. The >>>>>> 2-d lookup table has its two TCCs proven in 66 seconds. 2) I tried making the TCC strategy be simply “ >>>>>> (assert)” using: >>>>>> %|- *_TCC* : PROOF >>>>>> %|- (assert) >>>>>> %|- QED >>>>>> >>>>>> Even so, the 3-d lookup table is still running: >>>>>> >>>>>> >>>>>> >>>>>> Best Regards, >>>>>> Ben Hocking >>>>>> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx >>>>>> >>>>>> On Nov 14, 2014, at 9:13 AM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote: >>>>>> >>>>>> I’m representing a small 2-d and a small 3-d lookup table in PVS using the following code: >>>>>> <ndlookup.pvs> >>>>>> >>>>>> As you can see the PVS theory is not extremely complex and is only 224 lines (include blank lines). >>>>>> However, it seems to take forever* just to get PVS to discharge the TCCs. Is there anything I can do >>>>>> to help the process? >>>>>> >>>>>> *For the file I’m attaching here, I started the process at 8:56 AM (Japan Standard Time) and it is >>>>>> now 9:13 AM and the proof is still running. I had started a proof yesterday that took hours before I >>>>>> gave up, but I realized that I had some suggested proof strategies other than the default so I >>>>>> removed all such strategies (and deleted the pvs-bin folder just to be safe) and started again. The >>>>>> last several lines of the still-being-modified ndlookup.summary file look like: >>>>>> Context changed to /Users/Dependable/Tools/Simulink2PVS/com.dci.simulink2pvs/ >>>>>> Parsing ndlookup >>>>>> ndlookup parsed in 0.17 seconds >>>>>> Typechecking ndlookup;;; GC:;;; Finished GC >>>>>> ;;; GC:;;; Finished GC >>>>>> ;;; GC:;;; Finished GC >>>>>> ;;; GC:;;; Finished GC >>>>>> ;;; GC:;;; Finished GC >>>>>> ;;; GC:;;; Finished GC >>>>>> ;;; GC:;;; Finished GC >>>>>> ;;; GC:;;; Finished GC >>>>>> ;;; GC:;;; Finished GC >>>>>> ;;; GC:;;; Finished GC >>>>>> ;;; GC:;;; Finished GC >>>>>> ;;; GC:;;; Finished GC >>>>>> ;;; GC:;;; Finished GC >>>>>> ;;; GC:;;; Finished GC >>>>>> ;;; GC:;;; Finished GC >>>>>> ;;; GC:;;; Finished GC >>>>>> ;;; GC:;;; Finished GC >>>>>> ;;; GC:;;; Finished GC >>>>>> ;;; GC:;;; Finished GC >>>>>> ;;; GC:% >>>>>> >>>>>> I’m attaching that file in its current state as well in case it helps: >>>>>> <ndlookup.summary> >>>>>> >>>>>> Thank you for any help, >>>>>> Ben Hocking >>>>>> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx >>>>>> >>>> >>> >

**Follow-Ups**:**Re: [PVS-Help] Very slow proveit/PVS proofs***From:*Ben Hocking

**References**:**[PVS-Help] Very slow proveit/PVS proofs***From:*Ben Hocking

**Re: [PVS-Help] Very slow proveit/PVS proofs***From:*Ben Hocking

**Re: [PVS-Help] Very slow proveit/PVS proofs***From:*Sam Owre

**Re: [PVS-Help] Very slow proveit/PVS proofs***From:*Ben Hocking

**Re: [PVS-Help] Very slow proveit/PVS proofs***From:*Ben Hocking

**Re: [PVS-Help] Very slow proveit/PVS proofs***From:*Sam Owre

- Prev by Date:
**Re: [PVS-Help] Very slow proveit/PVS proofs** - Next by Date:
**Re: [PVS-Help] Very slow proveit/PVS proofs** - Previous by thread:
**Re: [PVS-Help] Very slow proveit/PVS proofs** - Next by thread:
**Re: [PVS-Help] Very slow proveit/PVS proofs** - Index(es):