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

PVS Bug 369


Synopsis:        model-check
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Thu Oct 28 11:00:02 1999
Originator:      mokkedem
Organization:    segsrv.hlo.dec.com
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  
  Hi,
  
  the following theory is not modelcheckable, even though the state is finite.
  
  Quite interesting, when you replace length with 2 in  seq: [below[length] -> 
 bool]
  it becomes modelcheckable.
  
  Thanks for your help.
  
  abdel
  
  % ------------- not modelcheckable ----------------------
  
  mctest : THEORY
  
  BEGIN
  
  myfinseq2: TYPE = [# length: below[2], seq: [below[length] -> bool] #]
  
  State : TYPE = [# x : {n : nat | n <= 2}, y : myfinseq2 #]
  
  trans(s,s_n : State) : bool = x(s_n) = IF x(s) = 2 THEN 0 ELSE x(s) + 1 ENDIF
  
  inv(s:State) : bool = x(s) <= 2
  
  IMPORTING ctlops[State]
  
  thm : THEOREM FORALL (s:State) : AG(trans,inv)(s)
  
  END mctest
  
  % ------------- modelcheckable ----------------------
  
  mctest : THEORY
  
  BEGIN
  
  myfinseq2: TYPE = [# length: below[2], seq: [below[2] -> bool] #]
  
  State : TYPE = [# x : {n : nat | n <= 2}, y : myfinseq2 #]
  
  trans(s,s_n : State) : bool = x(s_n) = IF x(s) = 2 THEN 0 ELSE x(s) + 1 ENDIF
  
  inv(s:State) : bool = x(s) <= 2
  
  IMPORTING ctlops[State]
  
  thm : THEOREM FORALL (s:State) : AG(trans,inv)(s)
  
  END mctest

How-To-Repeat: 

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