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

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



There's one other weird behavior I'm seeing. Somehow I've gotten into a state where I cannot load *any* file into PVS from a particular directory. Whatever file I load, even a blank one, leads to a message similar to the one shown in the screen shot below:
That said, I can copy the necessary files into a separate directory (sandbox), including lib_erqmod_lib_smooth_Division, and I am able to prove what I need to prove for this particular case. I've tried deleting pvsbin and lib_erqmod_lib_smooth_Division.prf in case the problem was some old state, but that did not resolve my problem.

Best Regards,
Ben Hocking
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx




On Nov 18, 2014, at 11:43 AM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

Hi Sam,

First, I want to say thanks for all of the help you've provided.

Secondly, I've determined that for the LookupTestWithTheorems case, that's a bug on my side, not yours. (The LookupTest theory was modified in an unexpected manner which meant that the "simple_test" theorem is no longer true.)

The "car" error still persists, however.

Best Regards,
Ben Hocking
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx




On Nov 18, 2014, at 11:35 AM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

The discrepancy was probably in my .prf files. I'm still experiencing the "Error: Attempt to take the car of 256 which is not listp." message on distance2. Here is that file along with its .prf file:
<distance2.prf><distance2.pvs>

I'm no longer getting the "Error: No next method for method" message with LookupTestWithTheorems.pvs, but the (grind) strategy which used to work with simple_test no longer does. Here are those files:
<LookupTest.prf><LookupTest.pvs><LookupTestWithTheorems.prf><LookupTestWithTheorems.pvs>

To be on the safe side, I deleted my old .prf files and pvsbin contents and then checked out my old ones from my git repository.

Best Regards,
Ben Hocking
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx




On Nov 18, 2014, at 11:19 AM, Sam Owre <owre@xxxxxxxxxxx> wrote:

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

<patch-20141114.lisp>

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