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

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



Hi all,

I’m trying to work with the following theory:

Attachment: stopwatch_Controller_vision.pvs
Description: Binary data


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