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

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



Thanks, Sam, you're incredible!

Best Regards,
Ben Hocking
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx




> On Nov 14, 2014, at 7:06 PM, Sam Owre <owre@xxxxxxxxxxx> wrote:
> 
> Hi Ben,
> I'm looking into this - it looks like the typechecker is doing too much
> work computing the judgement types.  I have the start of a fix for this, I
> should have it ready tomorrow and I'll send it to you.
> Regards,
> Sam
> 
> 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:
>> 
>> 
>> 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:
>> 
>> 
>> Thank you for any help,
>> Ben Hocking
>> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>>