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

PVS Bug 458


Synopsis:        Bug in (ABSTRACT)
Severity:        serious
Priority:        medium
Responsible:     shankar
State:           open
Class:           sw-bug
Arrival-Date:    Fri Apr 21 12:00:00 2000
Originator:      "Ralph D. Jeffords"
Organization:    itd.nrl.navy.mil
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  ----------
  X-Sun-Data-Type: text
  X-Sun-Data-Description: text
  X-Sun-Data-Name: text
  X-Sun-Charset: us-ascii
  X-Sun-Content-Lines: 2
  
  The attached notes and pvs dump outline some problems I encountered upon
  trying to use the (ABSTRACT) and (ABSTRACT-AND-MC) commands in PVS.
  ----------
  X-Sun-Data-Type: default
  X-Sun-Data-Description: default
  X-Sun-Data-Name: abstract_bug.notes
  X-Sun-Charset: us-ascii
  X-Sun-Content-Lines: 143
  
  Bug in PVS (ABSTRACT) Command
  
  In analyzing the simple example that Rushby used in "Integrated Formal
  Verification:...", 5/6 SPIN Int'l Workshops, I found three major problems
  (II. is NOT a bug per se, but part of my analysis that lead to showing
  that (ABSTRACT) gives an incorrect translation in another situation):
  
  I. Incorrect Translation in PVS (ABSTRACT) Command
  ---------------------------------------------------
  
  I consider the non-boolean abstraction (equivalent to the one Rushby used
  with B_1 <--> x >= 2, B_2 <--> x >= 1):
  
  	alpha(s) = (  |-> (s), abstr_x |-> / a   if x(s) <= 0  )
  					  <  b   if x(s) = 1
  					   \ c   if x(s) >= 2
  
  
  abstract THETA:  ---c-->(A)		 
  			 
  abstract rho:    (A,B)---  aa' + ab' + bc' + cc' --->(B)
  
  		  (B) ----- c -----> (A)
  
  We may then boolean-encode this to get a hand created abstract
  transition relation rho1:
  
  	a <=> ~B_2
  	b <=> ~B_1 & B_2
  	c <=> B_1
  
  
  It is easy via (GRIND) to prove that
   
  rho1_ok: THEOREM	rho(s,s_) => rho1(alpha1(s),alpha1(s_))
  
  However, the generated system (without boolean encoding) is
  
  generated
  abstract THETA:  ---c-->(A)		 
  
  generated			 
  abstract rho:    (A,B)---  aa'  + cc' --->(B)
  
  		  (B) ----- c -----> (A)
  
  
  where the transitions under aa' + cc' are TOO STRONG. We easily verify
  this since 
  
  rho1_gen_NOT_ok: LEMMA 
  
  	rho(s,s_) => rho1_gen(alpha1(s),alpha1(s_))
  
  fails to prove via (GRIND). I note that others have found problems with
  the abstract command: error reports 357, and 446.
  
  
  
  
  II. Rushby's abstraction (p. 8) is TOO WEAK
  -------------------------------------------
  
  It is easy to see by hand model-checking that Rushby's abstraction (the
  correct one, not the one generated by (ABSTRACT)) on
  B_1 == x >= 2 and B_2 == x >= 1 is too weak. Intuitively this is because
  the guard "x >= 3" is not captured precisely so that we know that x >=1
  when PC is A. We again use the equivalent non-boolean form where the
  property is translated as
  
  		PC = B => abstr_x=c
  
  	  c		     c,ok
  --- c--->(A)------ cc' ---->(B)------c----->(A)
  
  but this next transition allows any value for abstr_x in state A. Say we take
  the case abstr_x = a then we have
  
  	 a
  	(A)----- aa' + ab' --->(B)
  
  which gives us either  a  or  b in state B, which in either case is
  a contradiction to the property.
  
  A non-boolean abstraction which DOES allow us to successfully prove the
  property via model-checking is the following. Note that this abstraction
  does model the guard "x >= 3" precisely:
  
  	alpha2(s) = (  |-> (s), abstr_x |-> / a	  if x(s) <= 0  )
  					   /  b   if x(s) =  1
  					   \  c   if x(s) =  2
  					    \ d   if x(s) >= 3
  
  where the property is
  
  	PC = B => abstr_x in {c,d}
  
  Applying this abstraction we obtain
  
  abstract THETA:  ---c-->(A)		 
  			 
  abstract rho:    (A,B)---  aa' + ab' + bc' + cd' + dd' --->(B)
  
  		  (B) ----- dd' + dc' + db' -----> (A)
  
  We may easily model-check this (either by hand or using PVS)
  to show that the invariant is true, and thus the invariant
  must be true in the original concrete system.
  
  However, the (ABSTRACT) command gives an incorrect abstraction in this
  situation, too, since the following is unprovable:
  
  rho3_gen_NOT_ok: LEMMA
  
  	rho(s,s_) => rho3_gen(alpha3(s),alpha3(s_))
  
  
  
  
  III. Model-check still fails on subranges of nat
  -------------------------------------------------
  
  Replacing PC_type definition with
  
  	PC_type: TYPE = upto[1]
  
  and defining the constants
  
  	A:PC_type = 0
  	B:PC_type = 1
  
  foils the model-checker. It returns the error message
  
  Failed to Model check:
     could not decode binary encodings of scalar
  
  According to examples in one of the early papers on PVS model-checking
  such subranges should work. I think I reported this problem some time ago,
  but never got a satisfactory answer. This problem seems to be related to
  error reports 271, 369, 370, and 394.
  
  
  
  ----------
  X-Sun-Data-Type: default
  X-Sun-Data-Description: default
  X-Sun-Data-Name: abstract_bug.dmp
  X-Sun-Charset: us-ascii
  X-Sun-Content-Lines: 347
  
  %Patch files loaded: patch2 version 1.2.2.36
  
  $$$abstract_bug.pvs
  %===========================================================
  % Simple example of an infinite state transition system
  % and some invariants (from Rushby, "Integrated Formal
  % Verification" 5th/6th SPIN Workshops.)
  %
  % (ABSTRACT) command is producing incorrect results
  % (see rho1_gen and rho3_gen).
  %===========================================================
  abstract_bug: THEORY
  BEGIN
  
  %--------------------------------------------------------
  % (MODELCHECK) won't work with the alternate upto[1] type
  %--------------------------------------------------------
  
  PC_type: TYPE =  { A, B }	% upto[1]
  
  				% A:PC_type = 0
  				% B:PC_type = 1
  
  State: TYPE = [#	PC: PC_type,
  			x: int		#]
  
  	s,s_: VAR State
  
  
  THETA(s):boolean = x(s) = 2 & PC(s) = A
  
  rho(s,s_):boolean = 
  
  		PC(s) = A & x(s_) = x(s) + 1 & PC(s_) = B
  
  				or
  
  		PC(s) = B & x(s_) = x(s) + 1 & PC(s_) = B
  
  				or
  
  		PC(s) = B & x(s) >= 3 & x(s_) = x(s) - 2 & PC(s_) = A
  
  Ainv(s):boolean = PC(s) = A => x(s) >= 1
  
  Binv(s):boolean =  PC(s) = B => x(s) >= 2
  
  
  %---------------------------------------------------------------------------
  % Boolean abstraction using 
  %
  %	alpha1(s) = ( PC |-> PC(s), B_1 |-> x(s) >= 2, B_2 |-> x(s) >= 1 )
  %
  % NOTE: we may consider the equivalent nonboolean abstraction
  %
  %					  / a	if x(s) <= 0
  %	alpha(s) = ( PC |-> PC(s), x |-> <  b	if x(s) = 1    )
  %					  \ c   if x(s) >= 2
  %
  % For comparison the definition of rho1 is marked with these equivalent
  % values.
  %---------------------------------------------------------------------------
  
  
  State1: TYPE = [#	PC: PC_type,
  			B_1: boolean,   % x >= 2
  			B_2: boolean #] % x >= 1
  
  	s1,s1_: VAR State1
  
  alpha1(s):State1 = (# PC := PC(s), B_1 := x(s) >= 2, B_2 := x(s) >= 1 #)
  
  
  THETA1(s1):boolean = B_1(s1) & B_2(s1) & PC(s1) = A
  
  rho1(s1,s1_):boolean = not ( B_1(s1) & not B_2(s1)) 
  
  			& not ( B_1(s1_) & not B_2(s1_))
  
  			and
  %				    a		a'
   ( (PC(s1) = A or PC(s1) = B) & ( not B_2(s1) & not B_2(s1_) or
  %				    a           b'
  				 not B_2(s1) & not B_1(s1_) & B_2(s1_) or
  %				    b		c'
  				 not B_1(s1) & B_2(s1) & B_1(s1_) or
  %				    c		c'
  				 B_1(s1) &     B_1(s1_) ) & PC(s1_) = B
  			or
  %				    c
  		   PC(s1) = B & ( B_1(s1) ) & PC(s1_) = A )
  
  %----------------------------------------------------------
  % The following is the transition system generated by
  % (ABSTRACT ( "LAMBDA s: x(s) >= 2" "LAMBDA s: x(s) >=1"))
  % for THETA(s) => AG[State](rho,Bprop)(s)
  %
  % NOTE: the respective generated names abs_x1 and abs_v have
  % been replaced by s1 and s1_
  %----------------------------------------------------------
  
  rho1_gen(s1,s1_):boolean =
  
   			 (PC(s1) = A AND
                              ((B_2(s1_)) AND
                                (B_1(s1_)) AND (B_1(s1))
                                OR
                                NOT (B_2(s1_)) AND
                                 NOT (B_2(s1)) AND NOT (B_1(s1)))
                               AND PC(s1_) = B
                              OR
                              PC(s1) = B AND
                               ((B_2(s1_)) AND
                                 (B_1(s1_)) AND (B_1(s1))
                                 OR
                                 NOT (B_2(s1_)) AND
                                  NOT (B_2(s1)) AND NOT (B_1(s1)))
                                AND PC(s1_) = B
                               OR
                               PC(s1) = B AND
                                ((B_2(s1)) AND (B_1(s1))) AND
                                 ((B_2(s1)) AND (B_1(s1))) AND
                                  PC(s1_) = A)
  
  Binv1(s1):boolean = PC(s1) = B => B_1(s1)
  
  
  %------------------------------------------------------------
  % A non-boolean abstraction using
  %
  %				      / a  if x(s) <= 0
  % alpha2(s) = ( PC |-> PC(s), x2 |-> /  b  if x(s) = 1      )
  %				     \  c  if x(s) = 2
  %				      \ d  if x(s) >= 3
  %------------------------------------------------------------
  
  
  int2: TYPE = { a,b,c,d }
  
  
  State2: TYPE = [#	PC: PC_type,
  			x2: int2	#]
  
  	s2,s2_: VAR State2
  
  
  alpha2(s):State2 = (# PC := PC(s), x2 := IF x(s) <= 0 THEN
  						a
  					   ELSIF x(s) = 1 THEN
  						b
  					   ELSIF x(s) = 2 THEN
  						c
  					   ELSE
  						d
  					   ENDIF #)
  
  THETA2(s2):boolean = PC(s2) = A & x2(s2) = c
  
  rho2(s2,s2_):boolean =
  
  	(PC(s2) = A or PC(s2) = B) &
  
  		( x2(s2) = a & x2(s2_) = a
  				or
  		  x2(s2) = a & x2(s2_) = b
  				or
  		  x2(s2) = b & x2(s2_) = c
  				or
  		  x2(s2) = c & x2(s2_) = d
  				or
  		  x2(s2) = d & x2(s2_) = d ) & PC(s2_) = B
  
  				OR
  
  	PC(s2) = B & x2(s2) = d & x2(s2_) /= a  & PC(s2_) = A
  
  Binv2(s2):boolean = PC(s2) = B => x2(s2) = c or x2(s2) = d
  
  %======================================================================
  % Boolean-encoded version of alpha2 abstraction:
  %
  % alpha3(s) = ( PC |-> PC(s), B_1|-> x(s) >= 2, B_2 |-> x(s) in {1,2} )
  %=======================================================================
  
  State3: TYPE = [#	PC: PC_type,
  			B_1: boolean,
  			B_2: boolean	#]
  
  	s3,s3_: VAR State3
  
  alpha3(s):State3 =
  
  	(# PC := PC(s), B_1 := x(s) >= 2, B_2 := x(s) = 1 or x(s) = 2 #)
  
  
  %-------------------------------------------------------------------------
  % The following was the transition relation generated from 
  % (ABSTRACT-AND-MC ("lambda s: x(s) >= 2" "lambda s: x(s) = 1 or x(s) = 2")
  % for THETA(s) => AG[State](rho,Binv)(s)
  %
  % NOTE: the respective generated names abs_x1 and abs_v have
  % been replaced by s3 and s3_
  %-------------------------------------------------------------------------
  
  
  rho3_gen(s3,s3_):boolean =
  
   			(PC(s3) = A AND
                              ((B_2(s3_)) AND NOT (B_2(s3)) OR
                                (B_2(s3_)) AND NOT (B_1(s3_)) OR
                                 NOT (B_2(s3)) AND NOT (B_1(s3)))
                               AND PC(s3_) = B
                              OR
                              PC(s3) = B AND
                               ((B_2(s3_)) AND NOT (B_2(s3)) OR
                                 (B_2(s3_)) AND NOT (B_1(s3_)) OR
                                  NOT (B_2(s3)) AND NOT (B_1(s3)))
                                AND PC(s3_) = B
                               OR
                               PC(s3) = B AND
                                ((B_2(s3)) AND NOT (B_1(s3))) AND
                                 ((B_2(s3)) AND NOT (B_1(s3))) AND
                                  PC(s3_) = A)
  
  Binv3(s3):boolean = PC(s3) = B => B_1(s3)
  
  
  
  %========================
  % T  H  E  O  R  E  M  S
  %========================	
  
  
  %----------------------------------------------------------------
  % (ABSTRACT-AND-MC ( "LAMBDA s: x(s) >= 2" "LAMBDA s: x(s) >=1"))
  % is NOT strong enough to prove Binv. . .
  %----------------------------------------------------------------
  
  abstract_and_mc_fails: THEOREM
  
  	THETA(s) => AG[State](rho,Binv)(s)
  
  %-------------------------------------------------------------------
  % . . . more importantly, the abstraction is incorrect--(GRIND) fails
  %-------------------------------------------------------------------
  
  rho1_gen_NOT_ok: LEMMA
  
  		rho(s,s_) => rho1_gen(alpha1(s),alpha1(s_))
  
  
  
  %=================================================
  % The boolean abstraction alpha1 (hand-generated)
  %=================================================
  
  %---------------------------------------------------------------
  % The abstraction alpha1 satisfies the standard three properties
  %---------------------------------------------------------------
  
  THETA1_ok: LEMMA
  
  	THETA(s) => THETA1(alpha1(s))
  
  rho1_ok: LEMMA
  
  	rho(s,s_) => rho1(alpha1(s),alpha1(s_))
  
  Binv1_ok: LEMMA
  
  	Binv1(alpha1(s)) => Binv(s)
  
  %---------------------------------------------------
  % The hand-coded correct abstraction
  % is NOT strong enough when we (MODEL-CHECK)
  %---------------------------------------------------
  
  hand_abstract1_still_too_weak: THEOREM
  
  	THETA1(s1) => AG[State1](rho1,Binv1)(s1)
  
  
  
  
  %===============================================
  % We next try the nonboolean abstraction alpha2
  %===============================================
  
  %---------------------------------------------------------------
  % The abstraction alpha2 satisfies the standard three properties
  %---------------------------------------------------------------
  
  THETA2_ok: LEMMA
  
  	THETA(s) => THETA2(alpha2(s))
  
  rho2_ok: LEMMA
  
  	rho(s,s_) => rho2(alpha2(s),alpha2(s_))
  
  Binv2_ok: LEMMA
  
  	Binv2(alpha2(s)) => Binv(s)
  
  %------------------------------------------------
  % (MODEL-CHECK) succeeds for abstraction alpha2
  %-----------------------------------------------
  
  hand_abstract2: THEOREM
  
  	THETA2(s2) => AG[State2](rho2,Binv2)(s2)
  
  
  %===========================================================
  % The boolean abstraction alpha3 (boolean version of alpha2)
  %===========================================================
  
  %-------------------------------------
  % rho3_gen is incorrect, (GRIND) fails
  %-------------------------------------
  
  rho3_gen_NOT_ok: LEMMA
  
  	rho(s,s_) => rho3_gen(alpha3(s),alpha3(s_))
  
  END abstract_bug
  
  $$$abstract_bug.prf
  (|abstract_bug|
   (|abstract_and_mc_fails| ""
    (ABSTRACT-AND-MC ("LAMBDA s: x(s) >= 2" "LAMBDA s: x(s) >= 1"))
    (("" (POSTPONE) NIL NIL)) NIL)
   (|rho1_gen_NOT_ok| "" (GRIND)
    (("1" (POSTPONE) NIL NIL) ("2" (POSTPONE) NIL NIL)) NIL)
   (|THETA1_ok| "" (GRIND) NIL NIL) (|rho1_ok| "" (GRIND) NIL NIL)
   (|Binv1_ok| "" (GRIND) NIL NIL)
   (|hand_abstract1_still_too_weak| "" (MODEL-CHECK)
    (("" (POSTPONE) NIL NIL)) NIL)
   (|THETA2_ok| "" (GRIND) NIL NIL) (|rho2_ok| "" (GRIND) NIL NIL)
   (|Binv2_ok| "" (GRIND) NIL NIL)
   (|hand_abstract2| "" (MODEL-CHECK) NIL NIL)
   (|rho3_gen_NOT_ok| "" (GRIND)
    (("1" (POSTPONE) NIL NIL) ("2" (POSTPONE) NIL NIL)
     ("3" (POSTPONE) NIL NIL) ("4" (POSTPONE) NIL NIL)
     ("5" (POSTPONE) NIL NIL) ("6" (POSTPONE) NIL NIL))
    NIL))

How-To-Repeat: 

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