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

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



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