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

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



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