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

[PVS-Help] Very slow proveit/PVS proofs



I’m representing a small 2-d and a small 3-d lookup table in PVS using the following code:

Attachment: ndlookup.pvs
Description: Binary data


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:

Attachment: ndlookup.summary
Description: Binary data


Thank you for any help,
Ben Hocking