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

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



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
>