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

PVS Bug 1062


Synopsis:        error "does not uniquely resolve" with only one candidate
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Wed Jul 21 07:30:01 -0700 2010
Originator:      Hendrik Tews
Release:         PVS 4.2
Organization:    os.inf.tu-dresden.de
Environment: 
 System:          
 Architecture: 

Description: 
  
  --oUNAYqICBS
  Content-Type: text/plain; charset=us-ascii
  Content-Description: message body text
  Content-Transfer-Encoding: 7bit
  
  Hi,
  
  typechecking the appended file gives
  
  bisimulation? does not uniquely resolve - one of:
  
    CacheBisimilarity[ThreeState_adt[number_of_cores].ThreeState,MESIState_adt[
 number_of_cores].MESIState,N1_StateModel.Core].bisimulation? : [[CacheSignatur
 e[ThreeState[number_of_cores], Core],
    CacheSignature[MESIState[number_of_cores], Core]] ->
     [[[Self, Self] -> bool] -> bool]]
  
  
  If there is only one candidate, then it resolves uniquely,
  doesn't it?
  
  There are two Core's: N1_StateModel.Core and
  MESIStateModel_N.Core. In the above message some of the Core's
  are not qualified, so it is not clear what is meant. The second
  candidate might be the one with MESIStateModel_N.Core replacing
  N1_StateModel.Core.
  
  
  Bye,
  
  Hendrik
  
  
  --oUNAYqICBS
  Content-Type: application/octet-stream; name="mesi-bisim-resolve.pvs"
  Content-Disposition: attachment;
  	filename="mesi-bisim-resolve.pvs"
  Content-Transfer-Encoding: base64
  
  VHlwZXNEZWZpbml0aW9ucyA6IFRIRU9SWQpCRUdJTgogIERlbGF5IDogVFlQRSA9ICBuYXQKRU5E
  IFR5cGVzRGVmaW5pdGlvbnMKCgpDYWNoZUludGVyZmFjZVtTZWxmIDogVFlQRSAsIENvcmUgOiBU
  WVBFXSA6IFRIRU9SWQpCRUdJTgogIElNUE9SVElORyBUeXBlc0RlZmluaXRpb25zCiAgCiAgQ2Fj
  aGVTaWduYXR1cmUgOiBUWVBFID0gCiAgICBbIwogICAgICB3cml0ZSA6IFtbU2VsZiAsIENvcmVd
  IC0+IFtTZWxmICwgRGVsYXldXSAsIAogICAgICBleGNoYW5nZSA6IFtbU2VsZiAsIENvcmVdIC0+
  IFtTZWxmICwgRGVsYXldXSAsIAogICAgICByZXBsYWNlIDogW1tTZWxmICwgQ29yZV0gLT4gW1Nl
  bGYgLCBEZWxheV1dCiAgICAjXQogIApFTkQgQ2FjaGVJbnRlcmZhY2UKCgpDYWNoZUJpc2ltaWxh
  cml0eVtTZWxmMSA6IFRZUEUgLCBTZWxmMiA6IFRZUEUgLCBDb3JlIDogVFlQRV0gOiBUSEVPUlkK
  QkVHSU4KICBJTVBPUlRJTkcgQ2FjaGVJbnRlcmZhY2VbU2VsZjEgLCBDb3JlXSAsIENhY2hlSW50
  ZXJmYWNlW1NlbGYyICwgQ29yZV0KICAKICBjMSA6IFZBUiBDYWNoZVNpZ25hdHVyZVtTZWxmMSAs
  IENvcmVdCiAgCiAgYzIgOiBWQVIgQ2FjaGVTaWduYXR1cmVbU2VsZjIgLCBDb3JlXQogIAogIENh
  Y2hlX1JlbChjMSAsIGMyKSA6CiAgICBbW1tTZWxmMSAsIFNlbGYyXSAtPiBib29sXSAtPiBbW1Nl
  bGYxICwgU2VsZjJdIC0+IGJvb2xdXSA9CiAgICAoTEFNQkRBIChSOiBbW1NlbGYxICwgU2VsZjJd
  IC0+IGJvb2xdKSA6CiAgICAgIChMQU1CREEgKHgxOiBTZWxmMSAsIHgyOiBTZWxmMikgOgogICAg
  ICAgICgoRk9SQUxMIChjMzogQ29yZSkgOgogICAgICAgICAgICAoKFIoUFJPSl8xKHdyaXRlKGMx
  KSh4MSAsIGMzKSkgLCBQUk9KXzEod3JpdGUoYzIpKHgyICwgYzMpKSkpIEFORAogICAgICAgICAg
  ICAgKFBST0pfMih3cml0ZShjMSkoeDEgLCBjMykpID0gUFJPSl8yKHdyaXRlKGMyKSh4MiAsIGMz
  KSkpCiAgICAgICAgICAgICkpCiAgICAgICAgIEFORAogICAgICAgICAoRk9SQUxMIChjMzogQ29y
  ZSkgOgogICAgICAgICAgICAoKFIKICAgICAgICAgICAgICAgIChQUk9KXzEoZXhjaGFuZ2UoYzEp
  KHgxICwgYzMpKSAsIFBST0pfMShleGNoYW5nZShjMikoeDIgLCBjMykpKSkKICAgICAgICAgICAg
  IEFORAogICAgICAgICAgICAgKFBST0pfMihleGNoYW5nZShjMSkoeDEgLCBjMykpID0gUFJPSl8y
  KGV4Y2hhbmdlKGMyKSh4MiAsIGMzKSkpCiAgICAgICAgICAgICkpCiAgICAgICAgIEFORAogICAg
  ICAgICAoRk9SQUxMIChjMzogQ29yZSkgOgogICAgICAgICAgICAoKFIoUFJPSl8xKHJlcGxhY2Uo
  YzEpKHgxICwgYzMpKSAsIFBST0pfMShyZXBsYWNlKGMyKSh4MiAsIGMzKSkpKQogICAgICAgICAg
  ICAgQU5ECiAgICAgICAgICAgICAoUFJPSl8yKHJlcGxhY2UoYzEpKHgxICwgYzMpKSA9IFBST0pf
  MihyZXBsYWNlKGMyKSh4MiAsIGMzKSkpCiAgICAgICAgICAgICkpCiAgICAgICAgKSkpCiAgICA7
  CiAgCiAgYmlzaW11bGF0aW9uPyhjMSAsIGMyKSA6IFtbW1NlbGYxICwgU2VsZjJdIC0+IGJvb2xd
  IC0+IGJvb2xdID0KICAgIChMQU1CREEgKFI6IFtbU2VsZjEgLCBTZWxmMl0gLT4gYm9vbF0pIDoK
  ICAgICAgRk9SQUxMICh4MTogU2VsZjEgLCB4MjogU2VsZjIpIDoKICAgICAgICAoUih4MSAsIHgy
  KSkgSU1QTElFUyAoQ2FjaGVfUmVsKGMxICwgYzIpKFIpKHgxICwgeDIpKSkKICAgIDsKICAKRU5E
  IENhY2hlQmlzaW1pbGFyaXR5CgoKClRocmVlU3RhdGVbY29yZXMgOiBuYXRdIDogRGF0YXR5cGUK
  QmVnaW4KICBjYWNoZShjb3JlIDogYmVsb3coY29yZXMpKSA6IGNhY2hlPwogIG1lbW9yeSA6IG1l
  bW9yeT8KRW5kIFRocmVlU3RhdGUKCgpOMV9TdGF0ZU1vZGVsW251bWJlcl9vZl9jb3JlcyA6IG5h
  dF0gOiBUaGVvcnkKQmVnaW4KCiAgQ29yZSA6IFR5cGUgPSBiZWxvdyhudW1iZXJfb2ZfY29yZXMp
  CgogIEltcG9ydGluZyBDYWNoZUJpc2ltaWxhcml0eSwgVGhyZWVTdGF0ZQoKICBTZWxmIDogVHlw
  ZSA9IFRocmVlU3RhdGVbbnVtYmVyX29mX2NvcmVzXQoKICB3cml0ZShkX2MsIGRfbSwgZF9jdCwg
  ZF93YiA6IERlbGF5KSA6IFtTZWxmLCBDb3JlIC0+IFtTZWxmLCBEZWxheV1dID0gCiAgICBMYW1i
  ZGEocyA6IFNlbGYsIGNvcmUgOiBDb3JlKSA6IAogICAgICBDYXNlcyBzIE9GCiAgICAgICAgbWVt
  b3J5ICAgOiAoY2FjaGUoY29yZSksIGRfbSksCgljYWNoZShpKSA6IAoJICBJRiBpID0gY29yZSAK
  CSAgVGhlbiAocywgZF9jKQoJICBFbHNlIChjYWNoZShjb3JlKSwgZF9jdCkKCSAgRW5kSUYKICAg
  ICAgRW5kQ2FzZXMKCiAgZXhjaGFuZ2UoZF9jLCBkX20sIGRfY3QsIGRfd2IgOiBEZWxheSkgOiBb
  U2VsZiwgQ29yZSAtPiBbU2VsZiwgRGVsYXldXSA9IAogICAgTGFtYmRhKHMgOiBTZWxmLCBjb3Jl
  IDogQ29yZSkgOiAKICAgICAgQ2FzZXMgcyBPRgogICAgICAgIG1lbW9yeSAgIDogKGNhY2hlKGNv
  cmUpLCBkX20gKyBkX2MpLAoJY2FjaGUoaSkgOiAKCSAgSUYgaSA9IGNvcmUKCSAgVGhlbiAocywg
  ZF9jICsgZF9jKQoJICBFbHNlIChjYWNoZShjb3JlKSwgZF9jdCArIGRfYykKCSAgRW5kSUYKICAg
  ICAgRW5kQ2FzZXMKCiAgcmVwbGFjZShkX2MsIGRfbSwgZF9jdCwgZF93YiA6IERlbGF5KSA6IFtT
  ZWxmLCBDb3JlIC0+IFtTZWxmLCBEZWxheV1dID0gCiAgICBMYW1iZGEocyA6IFNlbGYsIGNvcmUg
  OiBDb3JlKSA6IAogICAgICBDYXNlcyBzIE9GCiAgICAgICAgbWVtb3J5ICAgOiAobWVtb3J5LCAw
  KSwKCWNhY2hlKGkpIDogCgkgIElGIGkgPSBjb3JlCgkgIFRoZW4gKG1lbW9yeSwgZF93YikKCSAg
  RWxzZSAocywgMCkKCSAgRW5kSUYKICAgICAgRW5kQ2FzZXMKCiAgbjFfc3RhdGVzKGRfYywgZF9t
  LCBkX2N0LCBkX3diIDogRGVsYXkpIDogQ2FjaGVTaWduYXR1cmVbU2VsZiwgQ29yZV0gPSAoIwog
  ICAgJXJlYWQgOj0gcmVhZChkX2MsIGRfbSwgZF9jdCwgZF93YiksCiAgICB3cml0ZSA6PSB3cml0
  ZShkX2MsIGRfbSwgZF9jdCwgZF93YiksCiAgICBleGNoYW5nZSA6PSBleGNoYW5nZShkX2MsIGRf
  bSwgZF9jdCwgZF93YiksCiAgICByZXBsYWNlIDo9IHJlcGxhY2UoZF9jLCBkX20sIGRfY3QsIGRf
  d2IpCiAgIykKCgpFbmQgTjFfU3RhdGVNb2RlbAoKCk1FU0lTdGF0ZVtjb3JlcyA6IG5hdF0gOiBE
  YXRhdHlwZQpCZWdpbgogIG1lbW9yeSA6IG1lbW9yeT8gJSA9IGludmFsaWQgaW4gYWxsIGNhY2hl
  cwogIG1vZGlmaWVkKGNvcmUgOiBiZWxvdyhjb3JlcykpIDogbW9kaWZpZWQ/CiAgZXhjbHVzaXZl
  KGNvcmUgOiBiZWxvdyhjb3JlcykpIDogZXhjbHVzaXZlPwogIHNoYXJlZChjb3JlX3NldCA6IG5v
  bmVtcHR5X3NldFtiZWxvdyhjb3JlcyldKSA6IHNoYXJlZD8KRW5kIE1FU0lTdGF0ZQoKCgpNRVNJ
  U3RhdGVNb2RlbF9OW251bWJlcl9vZl9jb3JlcyA6IG5hdF0gOiBUaGVvcnkKQmVnaW4KCiAgQ29y
  ZSA6IFR5cGUgPSBiZWxvdyhudW1iZXJfb2ZfY29yZXMpCgogIEltcG9ydGluZyBDYWNoZUJpc2lt
  aWxhcml0eSwgTUVTSVN0YXRlCgogIFNlbGYgOiBUeXBlID0gTUVTSVN0YXRlW251bWJlcl9vZl9j
  b3Jlc10KCiAgd3JpdGUoZF9jLCBkX20sIGRfY3QsIGRfd2IgOiBEZWxheSkgOiBbU2VsZiwgQ29y
  ZSAtPiBbU2VsZiwgRGVsYXldXSA9IAogICAgTGFtYmRhKHMgOiBTZWxmLCBjb3JlIDogQ29yZSkg
  OiAKICAgICAgQ2FzZXMgcyBPRgogICAgICAgIG1lbW9yeSAgICAgIDogKG1vZGlmaWVkKGNvcmUp
  LCBkX20pLAoJbW9kaWZpZWQoaSkgOiAKCSAgSUYgaSA9IGNvcmUKCSAgVGhlbiAocywgZF9jKQoJ
  ICBFbHNlIChtb2RpZmllZChjb3JlKSwgZF9jdCkKCSAgRW5kSUYsCglleGNsdXNpdmUoaSkgOgoJ
  ICBJRiBpID0gY29yZQoJICBUaGVuIChtb2RpZmllZChjb3JlKSwgZF9jKQoJICBFbHNlIChtb2Rp
  ZmllZChjb3JlKSwgZF9tKQoJICBFbmRJRiwKCXNoYXJlZChpcykgOgoJICBJRiBtZW1iZXIoY29y
  ZSwgaXMpCgkgIFRoZW4gKG1vZGlmaWVkKGNvcmUpLCBkX2MpCgkgIEVsc2UgKG1vZGlmaWVkKGNv
  cmUpLCBkX20pCgkgIEVuZElGCiAgICAgIEVuZENhc2VzCgoKICBleGNoYW5nZShkX2MsIGRfbSwg
  ZF9jdCwgZF93YiA6IERlbGF5KSA6IFtTZWxmLCBDb3JlIC0+IFtTZWxmLCBEZWxheV1dID0gCiAg
  ICBMYW1iZGEocyA6IFNlbGYsIGNvcmUgOiBDb3JlKSA6IAogICAgICBDYXNlcyBzIE9GCiAgICAg
  ICAgbWVtb3J5ICAgICAgOiAobW9kaWZpZWQoY29yZSksIGRfbSArIGRfYyksCgltb2RpZmllZChp
  KSA6IAoJICBJRiBpID0gY29yZQoJICBUaGVuIChzLCBkX2MgKyBkX2MpCgkgIEVsc2UgKG1vZGlm
  aWVkKGNvcmUpLCBkX2N0ICsgZF9jKQoJICBFbmRJRiwKCWV4Y2x1c2l2ZShpKSA6CgkgIElGIGkg
  PSBjb3JlCgkgIFRoZW4gKG1vZGlmaWVkKGNvcmUpLCBkX2MgKyBkX2MpCgkgIEVsc2UgKG1vZGlm
  aWVkKGNvcmUpLCBkX20gKyBkX2MpCgkgIEVuZElGLAoJc2hhcmVkKGlzKSA6CgkgIElGIG1lbWJl
  cihjb3JlLCBpcykKCSAgVGhlbiAobW9kaWZpZWQoY29yZSksIGRfYyArIGRfYykKCSAgRWxzZSAo
  bW9kaWZpZWQoY29yZSksIGRfbSArIGRfYykKCSAgRW5kSUYKICAgICAgRW5kQ2FzZXMKCgogIHJl
  cGxhY2UoZF9jLCBkX20sIGRfY3QsIGRfd2IgOiBEZWxheSkgOiBbU2VsZiwgQ29yZSAtPiBbU2Vs
  ZiwgRGVsYXldXSA9IAogICAgTGFtYmRhKHMgOiBTZWxmLCBjb3JlIDogQ29yZSkgOiAKICAgICAg
  Q2FzZXMgcyBPRgogICAgICAgIG1lbW9yeSAgICAgIDogKG1lbW9yeSwgMCksCgltb2RpZmllZChp
  KSA6IAoJICBJRiBpID0gY29yZQoJICBUaGVuIChtZW1vcnksIGRfd2IpCgkgIEVsc2UgKHMsIDAp
  CgkgIEVuZElGLAoJZXhjbHVzaXZlKGkpIDoKCSAgSUYgaSA9IGNvcmUgIAoJICAlIGRpc3Rpbmd1
  aXNoIGNhc2VzIGhlcmUgYmVjYXVzZSB0aGUgZWxzZSB2YXJpYW50IGlzIGltcG9zc2libGUKCSAg
  VGhlbiAobWVtb3J5LCAwKQoJICBFbHNlIChtZW1vcnksIDApIAoJICBFbmRJRiwKCXNoYXJlZChp
  cykgOgoJICBJRiBpcyA9IHNpbmdsZXRvbihjb3JlKQoJICBUaGVuIChtZW1vcnksIDApCgkgIEVs
  c0lGIG1lbWJlcihjb3JlLCBpcykKCSAgVGhlbiAoc2hhcmVkKHJlbW92ZShjb3JlLCBpcykpLCAw
  KQoJICBFbHNlIChzLCAwKQoJICBFbmRJRgogICAgICBFbmRDYXNlcwoKICBtZXNpX25fc3RhdGVz
  KGRfYywgZF9tLCBkX2N0LCBkX3diIDogRGVsYXkpIDogQ2FjaGVTaWduYXR1cmVbU2VsZiwgQ29y
  ZV0gPSAoIwogICAgJXJlYWQgOj0gcmVhZChkX2MsIGRfbSwgZF9jdCwgZF93YiksCiAgICB3cml0
  ZSA6PSB3cml0ZShkX2MsIGRfbSwgZF9jdCwgZF93YiksCiAgICBleGNoYW5nZSA6PSBleGNoYW5n
  ZShkX2MsIGRfbSwgZF9jdCwgZF93YiksCiAgICByZXBsYWNlIDo9IHJlcGxhY2UoZF9jLCBkX20s
  IGRfY3QsIGRfd2IpCiAgIykKCgpFbmQgTUVTSVN0YXRlTW9kZWxfTgogICAgICAKCgoKUmVmaW5l
  X04xX3RvX21lc2kgOiBUaGVvcnkKQmVnaW4KICBJbXBvcnRpbmcgTjFfU3RhdGVNb2RlbCwgTUVT
  SVN0YXRlTW9kZWxfTgoKICBudW1iZXJfb2ZfY29yZXMgOiBWYXIgbmF0CgogIFIobnVtYmVyX29m
  X2NvcmVzKSh0IDogTjFfU3RhdGVNb2RlbFtudW1iZXJfb2ZfY29yZXNdLlNlbGYsIAogICAgICAg
  ICAgICAgICAgICAgICBtIDogTUVTSVN0YXRlTW9kZWxfTltudW1iZXJfb2ZfY29yZXNdLlNlbGYp
  IDogYm9vbCA9CiAgICBtZW1vcnk/KHQpIEFuZCBtZW1vcnk/KG0pICBPUgogICAgY2FjaGU/KHQp
  IEFuZCBtb2RpZmllZD8obSkgQW5kIGNvcmUodCkgPSBjb3JlKG0pCgoKICBiaXNpbXVsYXRpb24g
  OiBMZW1tYSAKICAgIEZvcmFsbChudW1iZXJfb2ZfY29yZXMgOiBuYXQsIGRfYywgZF9tLCBkX2N0
  LCBkX3diIDogRGVsYXkpIDogCiAgICAgIGJpc2ltdWxhdGlvbj8objFfc3RhdGVzKGRfYywgZF9t
  LCBkX2N0LCBkX3diKSwgCiAgICAgIAkJICAgIG1lc2lfbl9zdGF0ZXMoZF9jLCBkX20sIGRfY3Qs
  IGRfd2IpKShSKG51bWJlcl9vZl9jb3JlcykpCgoKRW5kIFJlZmluZV9OMV90b19tZXNpCgoK
  --oUNAYqICBS--

How-To-Repeat: 

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