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

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



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:

Attachment: lookup3d.summary
Description: Binary data

Attachment: lookup3d.pvs
Description: Binary data


Best Regards,
Ben Hocking



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,