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

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



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
> 
>