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

[PVS-Help] Problems with a bigger lookup table

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.

Attachment: example_map.pvs
Description: Binary data

Best Regards,