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

PVS Bug 670


Synopsis:        Problem with (ABSTRACT)
Severity:        serious
Priority:        medium
Responsible:     shankar
State:           open
Class:           sw-bug
Arrival-Date:    Tue May 21 21:05:01 2002
Originator:      Ralph D. Jeffords
Organization:    itd.nrl.navy.mil
Release:         PVS 2.4
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: 1
  
  Problem is explained in the attached PVS dump:
  ----------
  X-Sun-Data-Type: default
  X-Sun-Data-Description: default
  X-Sun-Data-Name: abstract_bug2.dmp
  X-Sun-Charset: us-ascii
  X-Sun-Content-Lines: 522
  
  
  $$$abstract_bug2.pvs
  %================================================================
  % Problems with (ABSTRACT)
  %
  % Problems are explained in text below
  % 
  % Ralph D. Jeffords
  % Naval Research Lab.
  %
  % PVS version 4.2 patchlevel 1 on SUN
  %
  % 21 may 2002
  %================================================================
  abstract_bug2: THEORY
  BEGIN
  
  	IMPORTING abstract_bug
  
  
  	s,s_: VAR state
  	P,P_: VAR PressureType
  	W,W_: VAR WaterPresType
  
  %-------------------------------------------------------------------
  % Same as Pressure only P_ = P rewritten in terms of atomic formulae
  % in P and P_
  %-------------------------------------------------------------------
  
  Pressure2(W,P,W_,P_):boolean =
  
  	P = TooLow 
  	    & not(W >= 900)    & (W_ >= 900)  & P_=Permitted
  			OR
  	P = Permitted 
  	    & not(W >= 1000)  & (W_ >=  1000) & P_= High
  			OR
  	(P /= TooLow 
  	    or (W >= 900)    or not(W_ >= 900)) &
  	(P /= Permitted 
  	    or (W >= 1000)  or not(W_ >=  1000)) &
  
  	(P_=TooLow & P=TooLow
  		or
  	P_=Permitted & P=Permitted
  		or
  	P_=High & P=High)
  
  rho2(s,s_):bool =
  
    Pressure2(WaterPres(s),Pressure(s),WaterPres(s_),Pressure(s_))
  
  
  %=========================================
  % Definitions related to the abstraction
  %=========================================
  
  
  	as,as_,x1,v: VAR AState
  	R,R_: VAR [AState,AState -> boolean]
  
  
  %---------------------
  % Abstraction mapping
  %---------------------
  
  alpha(s):AState = (# Pressure := s`Pressure,
  		     L := s`WaterPres >= 900,
  		     P := s`WaterPres >= 1000 #)
  
  
  %--------------------------------------------------------
  % P(as) & ~L(as) MUST be disallowed as it corresponds to
  % WaterPres>=1000 & WaterPres<900
  %--------------------------------------------------------
  
  Encoding_axioms(as,as_):boolean = ( P(as) => L(as)) & ( P(as_) => L(as_) )
  
  
  %----------------------------------------------------------------------
  % Definitions of "Sound Abstraction" and "Strongest Sound Abstraction"
  %----------------------------------------------------------------------
  
  Sound_Abstraction?(R):boolean =
  
  	FORALL s,s_: rho(s,s_) => R(alpha(s),alpha(s_))
  
  Strongest_Sound_Abstraction?(R):boolean =
  
  	Sound_Abstraction?(R) &
  
  	(FORALL R_: Sound_Abstraction?(R_) => 
  
  		FORALL as,as_:R(as,as_) =>  R_(as,as_) )
  
  
  %-----------------------------------------------------------------
  % Hand-generated strongest sound abstraction with respect to alpha
  %-----------------------------------------------------------------
  
  abs_rho(as,as_):boolean =
  
  	Encoding_axioms(as,as_) &
  
  	(Pressure(as) = TooLow 
  	    & not L(as)       & L(as_)
              & Pressure(as_)=Permitted
  			OR
  	Pressure(as) = Permitted
  	    & not P(as)           &  P(as_) 
  	    & Pressure(as_)= High
  			OR
  	%----default no-change
  
  	not(Pressure(as) = TooLow 
  	    & not L(as)       & L(as_))
  			AND
  	not(Pressure(as) = Permitted
  	    & not P(as)       & P(as_))
  			AND
  
  	    Pressure(as_)=Pressure(as))
  
  
  %--------------------------------------------------------------------
  % After doing the (ABSTRACT) step of RPropertyMI2 we cut out the
  % transition relation and paste it here as gened_abs_rho2
  %--------------------------------------------------------------------
  
  gened_abs_rho2(x1,v):boolean =
  
    			Q(v) AND TooLow?(x1`Pressure) AND NOT x1`L
                             AND NOT x1`P AND v`L AND Permitted?(v`Pressure)
                             OR
                                  Q(v) AND Permitted?(x1`Pressure)
                              AND NOT x1`P AND v`L AND v`P
                              AND High?(v`Pressure)
                              OR
                              (Q(v) AND NOT TooLow?(x1`Pressure) OR
                                Q(v) AND x1`L OR
                                 Q(v) AND NOT v`L AND NOT v`P)
                               AND
                               (Q(v) AND NOT Permitted?(x1`Pressure) OR
                                 Q(v) AND x1`L AND x1`P OR Q(v) AND NOT v`P)
                                AND
                                (Q(v) AND
                                  TooLow?(v`Pressure) AND
                                   TooLow?(x1`Pressure)
                                  OR
                                  Q(v) AND
                                   Permitted?(v`Pressure) AND
                                    Permitted?(x1`Pressure)
                                   OR
                                   Q(v) AND
                                    High?(v`Pressure) AND
                                     High?(x1`Pressure))
  
  
  
  
  %------------------------------------------
  % Add the encoding axioms to gened_abs_rho2
  %------------------------------------------
  
  gened_abs_rho2_ax(x1,v):boolean = 
  
  		Encoding_axioms(x1,v) & gened_abs_rho2(x1,v)
  
  
  %==============================================================
  % T  H  E  O  R  E  M  S      A  N  D      L  E  M  M  A  T  A
  %==============================================================
  
  %----------------------------------------
  % Verify that rho and rho2 are equivalent
  %----------------------------------------
  
  equiv_rhos: LEMMA
  
  	rho = rho2
  
  %-------------------------------------------------------
  % Hand-generated abstraction is indeed the strongest one
  %-------------------------------------------------------
  
  hand_gened_strongest: THEOREM
  
  	Strongest_Sound_Abstraction?(abs_rho)
  
  %----------------------------------------------------
  % Same as before: just for generating gened_abs_rho2
  %----------------------------------------------------
  
  RPropertyMI2: LEMMA   THETA <=
  
  	AG[state](rho2, LAMBDA s: Pressure(s) = TooLow => WaterPres(s) < 900)
  
  
  %-------------------------------------------------------------
  % The abstraction gened_abs_rho is UNSOUND
  %
  % It appears that the abstraction process does not handle P_ = P
  % expression properly
  %-------------------------------------------------------------
  
  gen1_unsound: LEMMA % (GRIND) fails
  
  	Sound_Abstraction?(gened_abs_rho)
  
  %-----------------------------------------------------------
  % We have   abs_rho < gened_abs_rho2  so it is trivial that
  % gened_abs_rho2 is at least a Sound Abstraction
  %-----------------------------------------------------------
  
  hand_le_gen2: LEMMA
  
  	abs_rho <= gened_abs_rho2
  
  gen2_gt_hand: LEMMA  % GRIND fails
  
  	gened_abs_rho2 <= abs_rho
  
  
  %------------------------------------------------------------------
  % What is missing is the encoding axioms. Adding those axioms to
  % give gened_abs_rho_ax does the job.
  %
  % Thus gened_abs_rho_ is essentially okay, but to be the Strongest
  % Sound abstraction you must add the encoding axioms.
  %------------------------------------------------------------------
  
  equiv: LEMMA
  
  	abs_rho = gened_abs_rho2_ax
  
  END abstract_bug2
  
  $$$abstract_bug2.prf
  (|abstract_bug2|
   (|equiv_rhos| "" (APPLY-EXTENSIONALITY :HIDE? T)
    (("" (GRIND) NIL NIL)) NIL)
   (|hand_gened_strongest| "" (EXPAND "Strongest_Sound_Abstraction?")
    (("" (SPLIT)
      (("1" (GRIND) NIL NIL)
       ("2" (SKOSIMP)
        (("2" (EXPAND "Sound_Abstraction?")
          (("2" (SKOSIMP)
            (("2"
              (INST - "epsilon(LAMBDA s: alpha(s) = as!1)"
               "epsilon(LAMBDA s: alpha(s) = as!2)")
              (("1" (USE "epsilon_ax[state]")
                (("1" (SPLIT)
                  (("1" (REPLACE -1)
                    (("1" (LEMMA "epsilon_ax[state]")
                      (("1" (INST - "LAMBDA s: alpha(s) = as!2")
                        (("1" (SPLIT)
                          (("1" (REPLACE -1)
                            (("1" (ASSERT)
                              (("1" (HIDE 2)
                                (("1"
                                  (REPLACE -1 -3 RL)
                                  (("1"
                                    (REPLACE -2 -3 RL)
                                    (("1"
                                      (HIDE -1 -2)
                                      (("1"
                                        (NAME
                                         "e1"
                                         "epsilon(LAMBDA s: alpha(s) = as!1)")
                                        (("1"
                                          (NAME
                                           "e2"
                                           "epsilon(LAMBDA s: alpha(s) = as!2)"
 )
                                          (("1"
                                            (REPLACE -1)
                                            (("1"
                                              (REPLACE -2)
                                              (("1"
                                                (HIDE -1 -2)
                                                (("1" (GRIND) NIL NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (HIDE-ALL-BUT (-3 1))
                            (("2"
                              (INST +
                               "(# Pressure := as!2`Pressure, WaterPres :=
                                             IF not as!2`L & not as!2`P THEN 0 
 ELSIF as!2`L & not as!2`P THEN 950 ELSE 1050 ENDIF #)")
                              (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                                (("1" (GRIND) NIL NIL)
                                 ("2" (GRIND) NIL NIL)
                                 ("3" (GRIND) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2"
                        (INST +
                         "(# Pressure := TooLow, WaterPres := 0 #)")
                        NIL NIL))
                      NIL))
                    NIL)
                   ("2" (HIDE-ALL-BUT (-2 1))
                    (("2"
                      (INST + "(# Pressure := as!1`Pressure, WaterPres :=
                                      IF not as!1`L & not as!1`P THEN 0 ELSIF a
 s!1`L & not as!1`P THEN 950 ELSE 1050 ENDIF #)")
                      (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                        (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)
                         ("3" (GRIND) NIL NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL)
                 ("2" (INST + "(# Pressure := TooLow, WaterPres := 0 #)")
                  NIL NIL))
                NIL)
               ("2" (INST + "(# Pressure := TooLow, WaterPres := 0 #)")
                NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|RPropertyMI2| ""
    (ABSTRACT "state" "AState"
     (("L" "LAMBDA s: WaterPres(s) >= 900")
      ("P" "LAMBDA s: WaterPres(s) >= 1000")
      ("Pressure" "LAMBDA s: Pressure(s)"))
     :STRATEGY '(GRIND))
    (("" (POSTPONE) NIL NIL)) NIL)
   (|gen1_unsound| "" (EXPAND "Sound_Abstraction?")
    (("" (GRIND)
      (("1" (POSTPONE) NIL NIL) ("2" (POSTPONE) NIL NIL)
       ("3" (POSTPONE) NIL NIL) ("4" (POSTPONE) NIL NIL))
      NIL))
    NIL)
   (|hand_le_gen2| "" (GRIND) NIL NIL)
   (|gen2_gt_hand| "" (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)
   (|equiv| "" (APPLY-EXTENSIONALITY :HIDE? T)
    (("" (IFF)
      (("" (SPLIT) (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL))
      NIL))
    NIL))
  
  
  $$$abstract_bug.pvs
  %================================================================
  % Problems with (ABSTRACT)
  % 
  % Ralph D. Jeffords
  % Naval Research Lab.
  %
  % PVS version 4.2 patchlevel 1 on SUN
  %
  % 21 may 2002
  %================================================================
  abstract_bug: THEORY
  BEGIN
  
  
  WaterPresType: TYPE =   subrange[0,2000]
  
  PressureType: TYPE = { TooLow, Permitted, High }
  
  
  
  state: TYPE = [#	WaterPres: WaterPresType,
  			Pressure:  PressureType
  	      #]
  
  	s,s_: VAR state
  	P,P_: VAR PressureType
  	W,W_: VAR WaterPresType
  
  %-----------------------------------------------------------
  % Pressure Definition
  %
  % Corresponds to a part of the Pressure Mode Class table
  % of Safety Injection using NRL's SCR model:
  %
  %	Old Pressure	Event			New Pressure
  %	---------------------------------------------------
  %	TooLow		@T(Waterpres >= 900)	Permitted
  %	Permitted	@T(WaterPres >= 1000)	High
  %-----------------------------------------------------------
  
  Pressure(W,P,W_,P_):boolean =
  
  	P = TooLow 
  	    & NOT(W >= 900)    & W_ >= 900  & P_=Permitted
  			OR
  	P = Permitted 
  	    & NOT(W >= 1000)  & W_ >=  1000 & P_= High
  			OR
  	%------- otherwise no change -------------
  	(P /= TooLow 
  	    or (W >= 900)    or not(W_ >= 900)) &
  	(P /= Permitted 
  	    or (W >= 1000)  or not(W_ >=  1000)) &
  
  	P_ = P
  
  
  %-------------------------------------------
  % rho is the next state relation 
  %-------------------------------------------
  
  rho(s,s_):boolean =
  
    Pressure(WaterPres(s),Pressure(s),WaterPres(s_),Pressure(s_))
  
  %----------------
  % Initial state
  %----------------
  	
  THETA(s):boolean = WaterPres(s) = 14 & Pressure(s) = TooLow
  
  
  
  %--------------------
  % The abstract state
  %--------------------
  
  AState: TYPE =  [#	L:		boolean,
  			P:		boolean,
  			Pressure: 	PressureType  
  		#]
  
  	as,as_,x1,v: VAR AState
  	R,R_: VAR [AState,AState -> boolean]
  
  %--------------------------------------------------------------------
  % After doing the (ABSTRACT) step of RPropertyMI we cut out the
  % transition relation and paste it here as gened_abs_rho
  %
  % NOTE: Q == true is included to nullify the effects of Q in
  % gened_abs_rho so that you get the true transition relation
  % without having to edit after cutting and pasting!
  %--------------------------------------------------------------------
  
  
  Q(as):boolean = true
  
  gened_abs_rho(x1,v):boolean =
  
  			 Q(v) AND TooLow?(x1`Pressure) AND NOT x1`L
                             AND NOT x1`P AND v`L AND Permitted?(v`Pressure)
                             OR
                                  Q(v) AND Permitted?(x1`Pressure)
                              AND NOT x1`P AND v`L AND v`P
                              AND High?(v`Pressure)
                              OR
                              (Q(v) AND
                                NOT TooLow?(v`Pressure) AND
                                 NOT TooLow?(x1`Pressure)
                                OR
                                     Q(v) AND x1`L AND TooLow?(x1`Pressure)
                                 AND Permitted?(x1`Pressure)
                                 AND High?(x1`Pressure)
                                 OR
                                      Q(v) AND NOT v`L AND NOT v`P
                                  AND TooLow?(x1`Pressure)
                                  AND Permitted?(x1`Pressure)
                                  AND High?(x1`Pressure))
                               AND
                               (Q(v) AND
                                 NOT Permitted?(v`Pressure) AND
                                  NOT Permitted?(x1`Pressure)
                                 OR
                                      Q(v) AND x1`L AND x1`P
                                  AND TooLow?(x1`Pressure)
                                  AND Permitted?(x1`Pressure)
                                  AND High?(x1`Pressure)
                                  OR
                                       Q(v) AND NOT v`P
                                   AND TooLow?(x1`Pressure)
                                   AND Permitted?(x1`Pressure)
                                   AND High?(x1`Pressure))
  
  
  
  
  
  %==============================================================
  % T  H  E  O  R  E  M  S      A  N  D      L  E  M  M  A  T  A
  %==============================================================
  
  %------------------------------------------------------------------
  % This lemma is just used so we can (ABSTRACT) on rho and copy
  % the generated abstract system to gened_abs_rho appearing above.
  %------------------------------------------------------------------
  
  RPropertyMI: LEMMA   THETA <=
  
  	AG[state](rho, LAMBDA s: Pressure(s) = TooLow => WaterPres(s) < 900)
  
  END abstract_bug
  
  $$$abstract_bug.prf
  (|abstract_bug|
   (|RPropertyMI| ""
    (ABSTRACT "state" "AState"
     (("L" "LAMBDA s: WaterPres(s) >= 900")
      ("P" "LAMBDA s: WaterPres(s) >= 1000")
      ("Pressure" "LAMBDA s: Pressure(s)"))
     :STRATEGY '(GRIND))
    (("" (POSTPONE) NIL NIL)) NIL))
  

How-To-Repeat: 

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