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

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



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