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

Re: [PVS-Help] Very slow proveit/PVS proofs



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.":

Attachment: distance2.pvs
Description: Binary data


Here's another pair of theories (LookupTestWithTheorems uses LookupTest), that generates the message "Error: No next method for method":

Attachment: LookupTest.pvs
Description: Binary data

Attachment: LookupTestWithTheorems.pvs
Description: Binary data



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
>>> 
>