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

*To*: Sam Owre <owre@xxxxxxxxxxx>*Subject*: Re: [PVS-Help] Very slow proveit/PVS proofs*From*: Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>*Date*: Sat, 15 Nov 2014 19:39:01 +0900*Cc*: "John C. Knight" <john.knight@xxxxxxxxxxxxxxxxxxxxxxx>, Michael Anthony Aiello <tony.aiello@xxxxxxxxxxxxxxxxxxxxxxx>, pvs-help@xxxxxxxxxxx*In-reply-to*: <10459.1416047269@ubi>*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>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

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 >>

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

**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

- 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):