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

Re: [PVS-Help] Error in PVS 7 and PVS 6



Thanks Sam!

Best Regards,
Ben Hocking
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx

> On Oct 10, 2016, at 10:07 PM, Sam Owre <owre@xxxxxxxxxxx> wrote:
> 
> Hi Ben,
> 
> This is definitely a bug - anytime you see "Error: No methods applicable
> for generic function" it is a bug, and you can send it immediately to
> pvs-bugs (or open an issue on https://github.com/SRI-CSL/PVS/issues).
> 
> I'm including a fix below, though you don't really need it, as it will
> lead to a typecheck error anyway.  The problem is that the right-hand
> sides of update expressions need to be complete expressions, e.g.,
> instead of 
> 
>      LET v_state2: state_type = p_sys`f_state WITH [`f_cent := `f_cent + 1] IN
>      IF (v_state2`f_cent = 100) THEN
>        LET v_state3: state_type = v_state2 WITH [`f_cent := 0, `f_sec := `f_sec + 1] IN
>        IF (v_state3`f_sec = 60) THEN
>          v_state3 WITH [`f_sec := 0, `f_min := `f_min + 1]
> 
> It should be
> 
>      LET v_state2: state_type = p_sys`f_state WITH [`f_cent := p_sys`f_state`f_cent + 1] IN
>      IF (v_state2`f_cent = 100) THEN
>        LET v_state3: state_type = v_state2 WITH [`f_cent := 0, `f_sec := v_state2`f_sec + 1] IN
>        IF (v_state3`f_sec = 60) THEN
>          v_state3 WITH [`f_sec := 0, `f_min := v_state3`f_min + 1]
> 
> In the future, I may look into modifying the typechecker to allow the
> short form, which does seem natural to me.
> 
> Regards,
> Sam
> 
> -------Add to ~/.pvs.lisp---------
> 
> (defmethod copy-untyped* ((ex fieldex))
>  (with-slots (id actuals dactuals) ex
>    (copy ex
>      'type nil
>      'actuals (copy-untyped* actuals)
>      'dactuals (copy-untyped* dactuals))))
> 
> Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> 
>> Hi all,
>> 
>> I’m trying to work with the following theory:
>> 
>> While still very much a work-in-progress, this is meant to be a PVS
>> representation of the stopwatch model described in Fig. 1 here:
>> http://www.csl.sri.com/users/rushby/papers/sttt07.pdf
>> 
>> However, when I try to prove it in PVS 7, I get the following message:
>> Error: No methods applicable for generic function
>> #<standard-generic-function copy-untyped*> with args (`f_cent)
>> of classes (fieldex)
>> [condition type: program-error]
>> 
>> Restart actions (select using :continue):
>> 0: Try calling it again
>> 1: Return to Top Level (an "abort" restart).
>> 2: Abort entirely from this (lisp) process.
>> 
>> In PVS 6, I get a similar message (though it is harder to see):
>> rec:{Error: No methods applicable for generic function
>> #<standard-generic-function find-supertype> with args (recT) of
>> classes (name-expr)
>> [condition type: program-error]
>> 
>> Restart actions (select using :continue):
>> 0: Try calling it again
>> 1: Return to Top Level (an "abort" restart).
>> 2: Abort entirely from this (lisp) process.
>> 
>> Is this a bug in PVS, or is something wrong with my theory (or both)?
>> 
>> Best Regards,
>> Ben Hocking
>> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>> 
>> 
>