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

*To*: Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>*Subject*: Re: [PVS-Help] Very slow proveit/PVS proofs*From*: Sam Owre <owre@xxxxxxxxxxx>*Date*: Mon, 17 Nov 2014 18:19:07 -0800*Cc*: Sam Owre <owre@xxxxxxxxxxx>, pvs-help@xxxxxxxxxxx*Comments*: In-reply-to Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> message dated "Mon, 17 Nov 2014 13:25:23 +0900."*In-reply-to*: <18613B2A-0C1B-409E-BC96-838C4C4A31A9@dependablecomputing.com>*List-archive*: <http://mls.csl.sri.com/pipermail/pvs-help>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <https://mls.csl.sri.com/cgi-bin/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <https://mls.csl.sri.com/cgi-bin/mailman/options/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <F88D25FC-4E8B-45E6-81AB-07FB2A25A540@dependablecomputing.com> <2D334402-D184-4A32-8DA3-9A31334E5273@dependablecomputing.com> <10459.1416047269@ubi> <53C73402-C56D-4C64-87E9-1C033944DC0A@dependablecomputing.com> <18613B2A-0C1B-409E-BC96-838C4C4A31A9@dependablecomputing.com>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Hi Ben, There was a bug in that fix, could you try the following replacement? By the way,(grind) didn't cause the bug for me, it was (model-check), which is your default for TCCs that don't have "int" in their name - I don't know if there is a discrepancy between us that I should look into. Please let me know if there is. Thanks, Sam

(in-package :pvs) (defmethod judgement-types* ((ex branch)) (multiple-value-bind (then-types then-jdecls) (judgement-types* (then-part ex)) (multiple-value-bind (else-types else-jdecls) (judgement-types* (else-part ex)) (when (or then-types else-types) (cond ((equal then-types else-types) (values then-types then-jdecls)) ((and (vectorp then-types) (vectorp else-types)) (let ((comp-types (join-compatible-vector-types then-types else-types (type ex)))) (when comp-types (values comp-types (jdecls-union then-jdecls else-jdecls))))) ;; May have to convert a vector, might be better the other way (t (let* ((ttypes (jtypes-to-types then-types (then-part ex))) (etypes (jtypes-to-types else-types (else-part ex))) (comp-types (join-compatible-vector-types ttypes etypes (type ex)))) (when comp-types (values comp-types (jdecls-union then-jdecls else-jdecls)))))))))) (defun join-compatible-vector-types (types1 types2 type) (assert (= (length types1) (length types2))) (let ((ntypes (make-array (length types1) :initial-element nil))) (dotimes (i (length types1)) (let ((t1 (svref types1 i))) (if (and (car t1) (symbolp (car t1))) ;; This is for a record type (let ((t2 (find (car t1) types2 :key #'car)) (fld (find (car t1) (fields type) :key #'id))) (assert t2) (assert fld) (setf (aref ntypes i) (if (tc-eq t1 t2) t1 (cons (car t1) (join-minimal-types (cdr t1) (cdr t2)))))) ;; Else a tuple type (setf (aref ntypes i) (join-compatible-types t1 (svref types2 i) (nth i (types type))))))) ntypes)) ;; types1 and types2 are both minimal types lists, and are compatible ;; result is new list of minimal types. ;; 2 has mintypes (even_int, posint), 3 has (odd_int, posint) ;; the result is (posint), as even_int is not a subtype of anything in ;; Suppose types1 = (a1 b1 c1), so the given ex1 has these minimal types ;; and types2 = (a2 b2 c2), ex2 has these minimal types (defun join-minimal-types (types1 types2 &optional rem min) (if (null types1) (join-minimal-types* types2 min rem) (if (member (car types1) types2 :test #'tc-eq) (join-minimal-types (cdr types1) (remove (car types1) types2 :test #'tc-eq) rem (cons (car types1) min)) (let ((ty2 (find-if #'(lambda (ty2) (strict-subtype-of? (car types1) ty2)) types2))) (if ty2 (join-minimal-types (cdr types1) (remove ty2 types2) rem (cons ty2 min)) (join-minimal-types (cdr types1) types2 (if (null rem) (car types1) (let ((ctype (compatible-type rem (car types1)))) (unless (some #'(lambda (mty) (subtype-of? mty ctype)) min) ctype))) min)))))) (defun join-minimal-types* (types2 min rem) (if (null types2) (if rem (cons rem min) min) (if (and rem (subtype-of? rem (car types2))) (join-minimal-types* (cdr types2) min rem) (join-minimal-types* (cdr types2) min (if (null rem) (car types2) (let ((ctype (compatible-type rem (car types2)))) (unless (some #'(lambda (mty) (subtype-of? mty ctype)) min) ctype)))))))

Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote: > Hi Sam, > > It seems that the new patch introduced some problems. I'm now getting errors on many proofs that used to work, usually when I run the (grind) strategy (a personal favorite of mine, I'm afraid). > > Here's a relatively simple theory that generates the message "Error: Attempt to take the car of 256 which is not listp.": > > > Here's another pair of theories (LookupTestWithTheorems uses LookupTest), that generates the message "Error: No next method for method": > > > > I have other theories I can provide that are having these problems, but I believe all of my error messages so far fall into one of those two general camps. > > Best Regards, > Ben Hocking > ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx > > > > > > On Nov 15, 2014, at 7:39 PM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote: > > > > 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 > >>> > > >

**References**:**[PVS-Help] Very slow proveit/PVS proofs***From:*Ben Hocking

**Re: [PVS-Help] Very slow proveit/PVS proofs***From:*Ben Hocking

**Re: [PVS-Help] Very slow proveit/PVS proofs***From:*Sam Owre

**Re: [PVS-Help] Very slow proveit/PVS proofs***From:*Ben Hocking

**Re: [PVS-Help] Very slow proveit/PVS proofs***From:*Ben Hocking

- Prev by Date:
**Re: [PVS-Help] Very slow proveit/PVS proofs** - Next by Date:
**Re: [PVS-Help] Very slow proveit/PVS proofs** - Previous by thread:
**Re: [PVS-Help] Very slow proveit/PVS proofs** - Next by thread:
**Re: [PVS-Help] Very slow proveit/PVS proofs** - Index(es):