Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 444


Synopsis:        PVS2.2 vs PVS2.3 (problem report)
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Sun Feb 27 20:00:01 2000
Originator:      Jason Wu
Organization:    mcmaster.ca
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  
  Dear John Rushby
  
  I defined a PVS theory file (Clock.pvs) and tried to prove the proposition
  called clock_induction. A couple of months ago I used PVS2.2 and have done
  most steps of proof(although it is not proved completely). Then I am
  re-working on the unfinished part using PVS2.3 (patch level 1.2.2.36) and
  the whole proving stops at the very beginning. Below is the error message I
  got. 
  
  Rule? (Lemma "wf_induction[clock, <]")
  Error: No methods applicable for generic function .... 
  
  
  I am wondering if why the different versions give me different results even
  though the file and proof are the same. Is this a bug for the new version.
  
  Moreover, I am working on the this PVS file for a bit long time and
  haven't got the successful result. I wonder if you can take a look this
  file and give me some help. Just want to make sure I am on the right
  track.
  
  Thanks and have a good day
  
  Jason WU
  McMaster University
  
  
  ---1463811327-1167394081-951703874=:2172
  Content-Type: TEXT/PLAIN; CHARSET=US-ASCII; NAME="clock.dmp"
  Content-Transfer-Encoding: BASE64
  Content-ID: <Pine.LNX.4.10.10002272111140.2172@phred.DES>
  Content-Description: 
  Content-Disposition: ATTACHMENT; FILENAME="clock.dmp"
  
  DQokJCRDbG9ja3MucHZzDQoNCkNsb2Nrc1sgSzogcG9zcmVhbCBdOiBUSEVP
  UlkNCg0KQkVHSU4NCg0Kbm9uX25lZzogVFlQRSA9IHsgeDogcmVhbCB8IHg+
  PTAgfSBDT05UQUlOSU5HIDANCg0KdGltZTogVFlQRSA9IG5vbl9uZWcNCg0K
  dDogVkFSIHRpbWUNCg0KY2xvY2s6IFRZUEUgPSB7IHQ6IHRpbWUgfCBFWElT
  VFMobjogbmF0KTogdD1uKksgfSBDT05UQUlOSU5HIDANCg0KeDogVkFSIGNs
  b2NrDQoNCmluaXQoeCk6IGJvb2wgPSAoeD0wKQ0KDQpub25pbml0X2VsZW06
  IFRZUEUgPXsgeCB8IG5vdCBpbml0KHgpIH0NCg0KeTogVkFSIG5vbmluaXRf
  ZWxlbQ0KDQpwcmUoeSk6IGNsb2NrID0geSAtIEsNCg0KbmV4dCh4KTogbm9u
  aW5pdF9lbGVtID0geCArIEsNCg0KcmFuayh4KTogbmF0ID0geC9LDQoNCmx0
  OiB2YXIgKHdlbGxfZm91bmRlZD9bY2xvY2tdKQ0KDQpjbG9ja19pbmR1Y3Rp
  b246IFBST1BPU0lUSU9ODQogIEZPUkFMTCAoUDogcHJlZFtjbG9ja10pOg0K
  ICAgIChGT1JBTEwgKHQ6IGNsb2NrKTogaW5pdCh0KQ0KICAgICAgSU1QTElF
  UyBQKHQpKSBBTkQNCiAgICAoRk9SQUxMICh0OiBub25pbml0X2VsZW0pOiBQ
  KHByZSh0KSkNCiAgICAgIElNUExJRVMgUCh0KSkNCiAgICAgIElNUExJRVMg
  KEZPUkFMTCAodDogY2xvY2spOiBQKHQpKQ0KDQpFTkQgQ2xvY2tzDQoNCiQk
  JENsb2Nrcy5wcmYNCih8Q2xvY2tzfCAofGNsb2NrX1RDQzF8ICIiIChTVUJU
  WVBFLVRDQykgTklMIE5JTCkNCiAofHByZV9UQ0MxfCAiIiAoU0tPTEVNLVRZ
  UEVQUkVEKQ0KICAoKCIiIChTS09MRU0tVFlQRVBSRUQpDQogICAgKCgiIiAo
  U1BMSVQpDQogICAgICAoKCIxIiAoR1JJTkQpDQogICAgICAgICgoIjEiIChE
  RUxFVEUgLTMpDQogICAgICAgICAgKCgiMSIgKENBU0UgIm4hMT4wIikNCiAg
  ICAgICAgICAgICgoIjEiIChBU1NFUlQpDQogICAgICAgICAgICAgICgoIjEi
  IChMRU1NQSAiYm90aF9zaWRlc190aW1lc19wb3NfZ2UxIikNCiAgICAgICAg
  ICAgICAgICAoKCIxIiAoSU5TVCAtMSAiSyIgIm4hMS0xIiAiMCIpDQogICAg
  ICAgICAgICAgICAgICAoKCIxIiAoU0lNUExJRlkpICgoIjEiIChQUk9QQVgp
  IE5JTCBOSUwpKSBOSUwpKSBOSUwpKQ0KICAgICAgICAgICAgICAgIE5JTCkp
  DQogICAgICAgICAgICAgIE5JTCkNCiAgICAgICAgICAgICAoIjIiIChBU1NF
  UlQpIE5JTCBOSUwpKQ0KICAgICAgICAgICAgTklMKSkNCiAgICAgICAgICBO
  SUwpKQ0KICAgICAgICBOSUwpDQogICAgICAgKCIyIiAoSU5TVCAxICJuITEt
  MSIpDQogICAgICAgICgoIjEiIChBU1NFUlQpIE5JTCBOSUwpDQogICAgICAg
  ICAoIjIiIChFWFBBTkQgImluaXQiKSAoKCIyIiAoQVNTRVJUKSBOSUwgTklM
  KSkgTklMKSkNCiAgICAgICAgTklMKSkNCiAgICAgIE5JTCkpDQogICAgTklM
  KSkNCiAgTklMKQ0KICh8bmV4dF9UQ0MxfCAiIiAoU0tPTEVNLVRZUEVQUkVE
  KQ0KICAoKCIiIChTUExJVCkNCiAgICAoKCIxIiAoU0tPTEVNLVRZUEVQUkVE
  KQ0KICAgICAgKCgiMSIgKElOU1QgMSAibiExKzEiKSAoKCIxIiAoR1JJTkQp
  IE5JTCBOSUwpKSBOSUwpKSBOSUwpDQogICAgICgiMiIgKFNLT0xFTS1UWVBF
  UFJFRCkgKCgiMiIgKEdSSU5EKSBOSUwgTklMKSkgTklMKSkNCiAgICBOSUwp
  KQ0KICBOSUwpDQogKHxyYW5rX1RDQzF8ICIiIChTVUJUWVBFLVRDQykgTklM
  IE5JTCkNCiAofGNsb2NrX2luZHVjdGlvbnwgIiIgKFNLT0xFTSEpDQogICgo
  IiIgKExFTU1BICJ3Zl9pbmR1Y3Rpb25bY2xvY2ssIDwgXSIpDQogICAgKCgi
  MSIgKElOU1QgLTEgIlAhMSIpDQogICAgICAoKCIxIiAoU1BMSVQgLTEpDQog
  ICAgICAgICgoIjEiIChGTEFUVEVOIDEpIE5JTCBOSUwpDQogICAgICAgICAo
  IjIiIChTS09TSU1QIDIpDQogICAgICAgICAgKCgiMiIgKFNLT0xFTSAxICJ0
  ITEiKQ0KICAgICAgICAgICAgKCgiMiIgKEZMQVRURU4gMSkNCiAgICAgICAg
  ICAgICAgKCgiMiIgKElOU1QgLTEgInByZSh0ITEpIikNCiAgICAgICAgICAg
  ICAgICAoKCIxIiAoU1BMSVQgLTEpDQogICAgICAgICAgICAgICAgICAoKCIx
  IiAoSU5TVCAtMyAidCExIikNCiAgICAgICAgICAgICAgICAgICAgKCgiMSIg
  KFNQTElUIC0zKQ0KICAgICAgICAgICAgICAgICAgICAgICgoIjEiIChQUk9Q
  QVgpIE5JTCBOSUwpICgiMiIgKFBST1BBWCkgTklMIE5JTCkpDQogICAgICAg
  ICAgICAgICAgICAgICAgTklMKQ0KICAgICAgICAgICAgICAgICAgICAgKCIy
  IiAoSU5TVCAtMyAidCExIikNCiAgICAgICAgICAgICAgICAgICAgICAoKCIy
  IiAoU1BMSVQgLTMpDQogICAgICAgICAgICAgICAgICAgICAgICAoKCIxIiAo
  UFJPUEFYKSBOSUwgTklMKSAoIjIiIChQUk9QQVgpIE5JTCBOSUwpKQ0KICAg
  ICAgICAgICAgICAgICAgICAgICAgTklMKSkNCiAgICAgICAgICAgICAgICAg
  ICAgICBOSUwpKQ0KICAgICAgICAgICAgICAgICAgICBOSUwpDQogICAgICAg
  ICAgICAgICAgICAgKCIyIiAoSU5TVCAtMiAidCExIikNCiAgICAgICAgICAg
  ICAgICAgICAgKCgiMSIgKFNQTElUIC0yKQ0KICAgICAgICAgICAgICAgICAg
  ICAgICgoIjEiIChQUk9QQVgpIE5JTCBOSUwpDQogICAgICAgICAgICAgICAg
  ICAgICAgICgiMiIgKElOU1QgLTEgInQhMSIpDQogICAgICAgICAgICAgICAg
  ICAgICAgICAoKCIyIiAoU1BMSVQgLTEpDQogICAgICAgICAgICAgICAgICAg
  ICAgICAgICgoIjEiIChQUk9QQVgpIE5JTCBOSUwpDQogICAgICAgICAgICAg
  ICAgICAgICAgICAgICAoIjIiIChTS09MRU0hKSAoKCIyIiAoR1JJTkQpIE5J
  TCBOSUwpKSBOSUwpKQ0KICAgICAgICAgICAgICAgICAgICAgICAgICBOSUwp
  KQ0KICAgICAgICAgICAgICAgICAgICAgICAgTklMKSkNCiAgICAgICAgICAg
  ICAgICAgICAgICBOSUwpDQogICAgICAgICAgICAgICAgICAgICAoIjIiIChH
  UklORCkgTklMIE5JTCkpDQogICAgICAgICAgICAgICAgICAgIE5JTCkpDQog
  ICAgICAgICAgICAgICAgICBOSUwpDQogICAgICAgICAgICAgICAgICgiMiIg
  KElOU1QgLTIgInQhMSIpDQogICAgICAgICAgICAgICAgICAoKCIyIiAoQkRE
  U0lNUCAtMikNCiAgICAgICAgICAgICAgICAgICAgKCgiMSIgKFBST1BBWCkg
  TklMIE5JTCkgKCIyIiAoUFJPUEFYKSBOSUwgTklMKSkNCiAgICAgICAgICAg
  ICAgICAgICAgTklMKSkNCiAgICAgICAgICAgICAgICAgIE5JTCkpDQogICAg
  ICAgICAgICAgICAgTklMKSkNCiAgICAgICAgICAgICAgTklMKSkNCiAgICAg
  ICAgICAgIE5JTCkpDQogICAgICAgICAgTklMKSkNCiAgICAgICAgTklMKSkN
  CiAgICAgIE5JTCkNCiAgICAgKCIyIiAoRVhQQU5EICJ3ZWxsX2ZvdW5kZWQ/
  IikNCiAgICAgICgoIjIiIChTS09TSU1QKQ0KICAgICAgICAoKCIyIiAoU0tP
  TEVNISArKQ0KICAgICAgICAgICgoIjIiIChJTlNUIC0yICJ0ITEiKQ0KICAg
  ICAgICAgICAgKCgiMiIgKFNQTElUIC0yKQ0KICAgICAgICAgICAgICAoKCIx
  IiAoUFJPUEFYKSBOSUwgTklMKQ0KICAgICAgICAgICAgICAgKCIyIiAoSU5T
  VCAtMiAidCExIikNCiAgICAgICAgICAgICAgICAoKCIyIiAoU1BMSVQgLTIp
  DQogICAgICAgICAgICAgICAgICAoKCIxIiAoUFJPUEFYKSBOSUwgTklMKQ0K
  ICAgICAgICAgICAgICAgICAgICgiMiIgKElOU1QgMyAicHJlKHQhMSkiKQ0K
  ICAgICAgICAgICAgICAgICAgICAoKCIxIiAoU0tPTEVNISAzKQ0KICAgICAg
  ICAgICAgICAgICAgICAgICgoIjEiIChFWFBBTkQgInByZSIpDQogICAgICAg
  ICAgICAgICAgICAgICAgICAoKCIxIiAoR1JPVU5EKSAoKCIxIiAoUE9TVFBP
  TkUpIE5JTCBOSUwpKSBOSUwpKQ0KICAgICAgICAgICAgICAgICAgICAgICAg
  TklMKSkNCiAgICAgICAgICAgICAgICAgICAgICBOSUwpDQogICAgICAgICAg
  ICAgICAgICAgICAoIjIiIChISURFIDEpICgoIjIiIChQT1NUUE9ORSkgTklM
  IE5JTCkpIE5JTCkpDQogICAgICAgICAgICAgICAgICAgIE5JTCkpDQogICAg
  ICAgICAgICAgICAgICBOSUwpKQ0KICAgICAgICAgICAgICAgIE5JTCkpDQog
  ICAgICAgICAgICAgIE5JTCkpDQogICAgICAgICAgICBOSUwpKQ0KICAgICAg
  ICAgIE5JTCkpDQogICAgICAgIE5JTCkpDQogICAgICBOSUwpKQ0KICAgIE5J
  TCkpDQogIE5JTCkpDQoNCg==
  ---1463811327-1167394081-951703874=:2172--

How-To-Repeat: 

Fix: 
The conversion mechanism was assuming the expression used by the prover
was an expression, but in some cases it can be a string.  Fixed
add-conversion-info accordingly.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools