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

Re: [PVS-Help] Unit composition in PVS



Hi Sam,

I’m still doing some regression tests, but that definitely solves the current problem. I noticed that I had to remove my previous patch (that fixed an issue with lookup table modeling) in order to make it work. Do you know if those fixes are included in this patch?

Best Regards,
Ben Hocking
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx




> On May 6, 2015, at 3:08 AM, Sam Owre <owre@xxxxxxxxxxx> wrote:
> 
> Hi Ben,
> 
> Both of these problems are bugs.  The infinite loop is due to a bug
> that was triggered by the subtype-tcc strategy on certain kinds of
> arithmetic formulas.
> 
> The second bug was due to the code that tries to typecheck only as much of
> the theory as necessary; I think I've fixed it, but this is harder to
> test.
> 
> Could you try out the following patch file, and see if it helps?
> Just create a "pvs-patches" subdirectory in your PVS installation if there
> isn't one there already, and put it in there.  It should load the next
> time you start PVS.
> 
> Thanks,
> Sam
> 
> <patch-20150430.lisp>
> 
> Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> 
>> 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:
>> 
>> 
>> 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
>>>>>>> 
>>>> 
>>> 
>>