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

Re: [PVS-Help] Problems with a bigger lookup table



Hi all,

Although I still have the same problems with the example_map.pvs file I sent you, I have a modified version which meets my needs and works with my current version of PVS:

Attachment: example_map3.pvs
Description: Binary data


Here is its run time (and I've proven the comparable TCC in the theory on which this is based, but not here):
▶ date && time proveit -is example_map3
Tue Dec  9 13:37:47 EST 2014
Processing ./example_map3.pvs. Writing output to file ./example_map3.summary
Proving chain of imported theories
 Proof summary for theory example_map3
    LookupHelper_TCC3.....................unfinished          [shostak](1.58 s)
    Theory totals: 3 formulas, 3 attempted, 2 succeeded (2.01 s)
Grand Totals: 3 proofs, 3 attempted, 2 succeeded (2.01 s)
proveit -is example_map3  7.32s user 0.22s system 96% cpu 7.813 total

In hindsight, I definitely understand why this is so much easier for PVS, so I thought I'd share it with you in case it gives you any inspiration.

By comparison, here is an intermediate version:

Attachment: example_map2.pvs
Description: Binary data


Here is me running proveit on it for a while before giving up:
▶ date && time proveit -is example_map2     
Tue Dec  9 12:01:50 EST 2014
Processing ./example_map2.pvs. Writing output to file ./example_map2.summary
Proving chain of imported theories
^Cproveit -is example_map2  5560.41s user 9.73s system 99% cpu 1:32:54.32 total

Hope this helps.

Best Regards,
Ben Hocking




On Dec 1, 2014, at 10:13 AM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

Hi Sam (et al.),

This latest patch did not seem to resolve my problems. I've also noticed an additional interesting issue (that I think is not caused by the patch, but I have not verified that as it take a while for me to test).

First, here's the exact steps for me recreating the exact problem:
  1. Copy example_map.pvs into its own folder (for me, that's important).
  2. Prove the theory, which has LookupTable_2_D_TCC1 and LookupTable_2_D_TCC2 both proved - complete.
  3. Prove LookupTable_2_D_TCC3, which is initially unfinished.
    1. Do *not* re-run existing proof.
    2. Use (skeep)(skeep)(skeep)(grind).
    3. Get the result:
      Error: `(#<Judgement posrat_div_posrat_is_posrat>)' is not of the
             expected type `array'
        [condition type: type-error]
The other interesting issue is that if I run proveit from within the directory containing only this theory I get the following timing results:
▶ time proveit example_map.pvs
Processing ./example_map.pvs. Writing output to file ./example_map.summary
 Proof summary for theory example_map
    LookupTable_2_D_TCC3...............unfinished          [shostak](1431.93 s)
    Theory totals: 3 formulas, 3 attempted, 2 succeeded (1700.71 s)
Grand Totals: 3 proofs, 3 attempted, 2 succeeded (1700.71 s)
proveit example_map.pvs  1800.82s user 3.48s system 99% cpu 30:06.99 total

If I run proveit from within a directory containing many other (proprietary) theories (73 to be precise, with a total of 61,308 lines, but that includes blank lines), I get this result:
▶ time proveit example_map.pvs
Processing ./example_map.pvs. Writing output to file ./example_map.summary
^C^C^C^C^C^C
^C^C^Cproveit example_map.pvs  43439.69s user 142.36s system 99% cpu 12:07:05.45 total
(I.e., eventually I just give up.)

I get the same results from within PVS, but without being able to conveniently measure timing. Note that in the above example, I deleted .pvscontext and made sure there was no .prf file associated with example_map.pvs, nor any corresponding entry in pvsbin. If there's someething else I should've checked, please let me know, but I also tried this in a brand new directory where I simply copied all of the PVS files into it, so it should've been pristine. I could probably recreate this without proprietary theories, so let me know if you need more to go on.

Best Regards,

On Nov 26, 2014, at 1:28 PM, Sam Owre <owre@xxxxxxxxxxx> wrote:

Hi Ben,

There was another bug exposed by the patch I sent; it took me a while to
make sure there wasn't a deeper problem.  I'm including a replacement
patch below.

More memory won't help with this, as it is hitting an internal error that
would be hard to work around.  I believe if you get more memory, then
Allegro will try to use it, but for me grind finished the proof in
reasonable time (on the other hand, I do have 16G of ram).

Sam

<patch-20141114.lisp>
Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

Is it possible that increasing the available memory to pvs-allegro would help, and if so, what would be
the recommended method for doing so?

Best Regards,
Ben Hocking
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx

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

   Attached is a much larger example of a lookup table. This is the same size as one used for
   proprietary purposes, but with the proprietary information replaced with non-properietary numbers
   that have similar relationships. The purpose of the lookup table is to calculate an efficiency value
   that is between 0 and 1. The theory generates 3 TCCs, the last of which (LookupTable_2_D_TCC3) is
   the important one, namely that the result is indeed between 0 and 1. If I attempt the proof
   strategy (skeep)(skeep)(skeep)(grind), I get the following error:
   Error: `(#<Judgement posrat_div_posrat_is_posrat>)' is not of the
          expected type `array'
     [condition type: type-error]

   Note that I do not get this error if I just try (grind). This uses the patch previously sent to me
   by Sam Owre (patch-20141114.lisp), although I do not know if it is related to that patch, or whether
   the problem would exist without it. While it takes a long time to process with the patch, without
   it, the time required is so long that I have not attempted to ascertain whether it would actually
   complete.

   <example_map.pvs>

   Best Regards,
   Ben Hocking
   ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx