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

Re: [PVS-Help] Unit composition in PVS



Hi all,

While I have had much success since Sam helped me to understand what I was doing wrong previously, I’m now running into two issues in the attached code:

Attachment: units.tgz
Description: Binary data


First, and easiest to reproduce, is what appears to be some sort of non-ending loop. In the attached example, the theory siso_test as-is can be proven with 15 TCCs. However, if you restore the first line in valve parameters:
  valve_max_flow_rate: posvolume_per_time = 0.1 * m^3 / s
it apparently takes forever to finish. (Possibly not forever, but I’ve seen no evidence that it’s doing anything but garbage collecting.) I’ve tried this in a variety of settings, and the result is fairly consistent. Let me know if you’re unable to recreate.

Secondly, it seems that I’m needing to use “::real” in many places where it should not be necessary, and where adding it in similar places breaks the specification. For example, consider the following line from lengths.pvs:
  length_pred_ax: AXIOM length_pred(0::real) AND length_pred(0 * m) AND length_pred(m)

If I remove the ::real, I get the message:
  Expecting an expression
  No resolution for length_pred with arguments of possible types:
    0 : reals.real

However, if I now add the following line above it:
  f, g:      VAR real
the ::real is not needed in the length_pred_ax line.

In fact, if I add it back, I now get the message:
  Expecting an expression
  No resolution for length_pred with arguments of possible types:
    0:: real : reals.real

Note that these results seem to have a bit of Heisenberg uncertainty involved, so you might have to try some variations on this to see it.

Thank you,
Ben Hocking
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx


> On Apr 28, 2015, at 3:55 PM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> 
> Excellent, thank you very much.
> 
> I had originally attempted to allow complex lengths, but decided to back away from that for now, so just changing number to real works for me.
> 
> Best Regards,
> Ben Hocking
> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
> 
> 
> 
> 
>> On Apr 28, 2015, at 3:52 PM, Sam Owre <owre@xxxxxxxxxxx> wrote:
>> 
>> Hi Ben,
>> 
>> It turns out there are two definitions for length_pred.  One is
>> automatically generated from the declaration
>> 
>> length: NONEMPTY_TYPE FROM real
>> 
>> which generates (run "M-x ppe" to see this)
>> 
>> length_pred: [real -> boolean]
>> 
>> Then you define another one over numbers.  Removing your definition causes
>> problems with the definition
>> 
>> length?(n: number): bool =
>>   number_field_pred(n) and real_pred(n) AND length_pred(n)
>> 
>> but this can be fixed using coercions, i.e., "length_pred(n::real)"
>> 
>> With these changes I had no problem discharging the TCCs.
>> 
>> An alternative may be to define your length_pred over number to be equal
>> to the other length_pred when restricted to real, but you can still see
>> sequents that look like they should be trivial, but require a definition
>> expansion.
>> 
>> I'm going to look into improving show-expanded-sequent so it makes this
>> clearer.
>> 
>> Regards,
>> Sam
>> 
>> Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
>> 
>>> Hi Sam,
>>> 
>>> Got back to this after working on something else for a while, when I used the ‘C-u M-x show-expanded-sequent’ command, I got the following:
>>> ===================================
>>> length_plus_length_is_length :
>>> 
>>> {-1}  length_pred((number_fields.+)(x, y))
>>> |-------
>>> {1}   length_pred((number_fields.+)(x, y))
>>> ===================================
>>> 
>>> As far as I can tell, {-1} should imply {1} fairly cleanly. Neither ‘(assert)’ nor even ‘(grind)’ resolve this, but possibly the output from ‘(grind)’ is useful:
>>> ===================================
>>> The following errors occurred within the strategy:
>>> 
>>> Couldn't find a suitable quantified formula.
>>> 
>>> No suitable (+ve FORALL/-ve EXISTS) quantified expression found.
>>> 
>>> No change on: (grind)
>>> length_plus_length_is_length :
>>> 
>>> [-1]  length_pred(x + y)
>>> |-------
>>> [1]   length_pred(x + y)
>>> ===================================
>>> 
>>> The proof (from show-proof) is simply:
>>> ("" (skeep) (lemma "closed_plus" ("x" "x" "y" "y")) (postpone))
>>> 
>>> Where the judgment being proven is:
>>> length_plus_length_is_length:  JUDGEMENT +(x, y)   HAS_TYPE length
>>> 
>>> And the axiom closed_plus is:
>>> closed_plus:    AXIOM length_pred(x + y) 
>>> 
>>> And the definition for x, y is:
>>> x, y: VAR length
>>> 
>>> Best Regards,
>>> Ben Hocking
>>> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>>> 
>>> 
>>> 
>>> 
>>>> On Apr 23, 2015, at 6:05 PM, Sam Owre <owre@xxxxxxxxxxx> wrote:
>>>> 
>>>> Hi Ben,
>>>> 
>>>> We tried to capture dimensions and units using the PVS type system, and
>>>> failed.  Since then we have started adding it to PVS, then worked on
>>>> adding it to Simulink, and wrote a paper laying out the theory:
>>>> 
>>>> Automatic Dimensional Analysis of Cyber-Physical Systems,
>>>> by Sam Owre, Indranil Saha, and Natarajan Shankar,
>>>> in FM 2012: Formal Methods Lecture Notes in Computer Science pages 356-371.
>>>> 
>>>> We will continue adding it to PVS when there is time available.
>>>> 
>>>> As for your proof, you should try 'C-u M-x show-expanded-sequent'; this
>>>> often shows where mismatches occur.  My guess is you have two different
>>>> '+' operators.
>>>> 
>>>> If you still have problems, please send your specs to me so I can debug
>>>> this.
>>>> 
>>>> Thanks,
>>>> Sam
>>>> 
>>>> 
>>>> Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
>>>> 
>>>>> For lengths, I’ve tried creating a “lengths” theory similar to the reals theory in the PVS
>>>>> prelude, but I’m stuck here:
>>>>> length_plus_length_is_length :
>>>>> 
>>>>> |-------
>>>>> {1}   FORALL (x, y): length_pred(x + y)
>>>>> 
>>>>> Rule? (skeep)
>>>>> Skolemizing and keeping names of the universal formula in (+ -),
>>>>> this simplifies to:
>>>>> length_plus_length_is_length :
>>>>> 
>>>>> |-------
>>>>> {1}   length_pred(x + y)
>>>>> 
>>>>> Rule? (lemma "lengths.closed_plus" ("x" "x" "y" "y"))
>>>>> Applying lengths.closed_plus where
>>>>> x gets x,
>>>>> y gets y,
>>>>> this simplifies to:
>>>>> length_plus_length_is_length :
>>>>> 
>>>>> {-1}  length_pred(x + y)
>>>>> |-------
>>>>> [1]   length_pred(x + y)
>>>>> 
>>>>> Rule?
>>>>> 
>>>>> I’ve tried “assert”, “smash”, “grind”, etc., but nothing seems to resolve this seemingly
>>>>> simple statement…
>>>>> 
>>>>> (Note that length_pred is an undefined function that I’ve attempted to “define” via axioms,
>>>>> such as closed_plus, etc.)
>>>>> 
>>>>> Best Regards,
>>>>> Ben Hocking
>>>>> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>>>>> 
>>>>>  On Apr 22, 2015, at 9:15 AM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
>>>>> 
>>>>>  Alas, it appears that the simplicity comes with a price. I cannot figure out a way to
>>>>>  prevent meters and seconds from being added together, or more importantly of determining
>>>>>  whether a particular measurement is of time, length, or is unitless (as examples).
>>>>> 
>>>>>  Best Regards,
>>>>>  Ben Hocking
>>>>>  ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>>>>> 
>>>>>      On Apr 22, 2015, at 8:01 AM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>
>>>>>      wrote:
>>>>> 
>>>>>      Viorel,
>>>>> 
>>>>>      I really like the idea of using uninterpreted positive real constants. This is far
>>>>>      simpler than the approach I’ve been using.
>>>>> 
>>>>>      Best Regards,
>>>>>      Ben Hocking
>>>>>      ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>>>>> 
>>>>>          On Apr 22, 2015, at 4:51 AM, Viorel Preoteasa <viorel.preoteasa@xxxxxxxx> wrote:
>>>>> 
>>>>>          You can also do something like:
>>>>> 
>>>>>            m: posreal
>>>>>            cm: posreal = m / 100
>>>>>            m_to_cm: lemma 2.5 * m = 250 * cm
>>>>> 
>>>>>          Best regards,
>>>>> 
>>>>>          Viorel Preoteasa
>>>>> 
>>>>>          On 04/22/2015 01:16 AM, Ben Hocking wrote:
>>>>> 
>>>>>              Is anyone familiar with work that has been done on unit composition in
>>>>>              formal specifications within PVS? E.g., verifying that when you multiply
>>>>>              meters by meters you get square meters?
>>>>> 
>>>>>              I have some ideas on what I want to do (and have actually started down that
>>>>>              path), but I don’t want to reinvent the wheel if this has already been done.
>>>>> 
>>>>>              Best Regards,
>>>>>              Ben Hocking
>>>>>              ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>>>>> 
>> 
>