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

PVS Bug 652


Synopsis:        MODEL-CHECK soundness bug with multiple subrange( , ) fields
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Wed Jan 23 12:30:00 2002
Originator:      Mark Lawford
Organization:    mcmaster.ca
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  
  Hello PVS Developers.
  
  The (model-check) command seems to have a problem when the state record
  type includes more than one field of type subrange( , ).  The dump file
  below contains some simplified definitions from a file for modeling Timed
  Transition Models in PVS that I was working on with my graduate student
  Hong Zhang when I discovered the bug. 
  
  Please let me know if you receive this bug report since we have been 
  having problems with our mailer.  Thanks for your help.
  
  Regards,
  Mark
  
  Mark Lawford
  McMaster University
  
  $$$unsound.pvs
  unsound : THEORY
  
    BEGIN
    
    sub_int:TYPE = subrange[0,10]
  
    state_t:TYPE = [# u, v:sub_int #]
  
    state:VAR state_t
  
  % declare initial state for system
    init(state: state_t):bool = state`u=0 and state`v=1 
  
  s: VAR state_t
  
  % Something that should never be true of a state
  lessthan0(s: state_t):bool = u(s)<0
  
  % Following proves with model-check in PVS 2.4p1 although it should not
  ucheck_funny: THEOREM
  init(s) => lessthan0(s)
  not_ucheck_funny: THEOREM
  (init(s) => NOT lessthan0(s))
  
  init_check: THEOREM
  exists s: init(s)
  
  inconsistent:THEOREM FALSE
  
    END unsound
  
  $$$unsound.prf
  (|unsound| (|ucheck_funny| "" (MODEL-CHECK) NIL NIL)
   (|not_ucheck_funny| "" (MODEL-CHECK) NIL NIL)
   (|init_check| "" (INST 1 "(#u:=0,v:=1#)")
    (("" (EXPAND "init") (("" (PROPAX) NIL NIL)) NIL)) NIL)
   (|inconsistent| "" (LEMMA "not_ucheck_funny")
    (("" (LEMMA "ucheck_funny")
      (("" (LEMMA "init_check")
        (("" (SKOLEM!)
          (("" (INST?) (("" (INST?) (("" (BDDSIMP) NIL NIL)) NIL)) NIL))
  NIL))
        NIL))
      NIL))
    NIL))
  
  
  

How-To-Repeat: 

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