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

PVS Bug 877


Synopsis:        trivial consequence of trichotomy crashes PVS3.2 with Stack overflow
Severity:        serious
Priority:        medium
Responsible:     shankar
State:           open
Class:           sw-bug
Arrival-Date:    Wed Dec  1 11:50:00 2004
Originator:      "Ricky W. Butler"
Organization:    larc.nasa.gov
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
  
  --=-moyeb9zn5UFHnFCYmB+h
  Content-Type: text/plain
  Content-Transfer-Encoding: 7bit
  
  
  
  Run the proof "signs_ve_z" in theory "bug1"
  and you will reach:
  
    signs_ve_z.1.1 :  
  
    {-1}  ve!1`z * CC!1 > 0
    [-2]  s!1`z >= H
    [-3]  ve!1`z * CC!1 = (H - s!1`z)
      |-------
    {1}   (ve!1`z * CC!1 = 0)
  
    Rule? 
  
  Hit this sequent with (ASSERT) and the prover goes into
  an infinite loop, even though this sequent is a trivial
  consequence of trichotomy.  It eventually crashes with
  
      Error: Stack overflow (signal 1000)
      [condition type: synchronous-operating-system-signal]
  
  
  Interestingly, the equivalent sequent in lemma "b1" does
  not suffer from this:
  
    b1 :  
  
      |-------
    {1}   FORALL (CC: posreal, s, ve: Vect3):
            ve`z * CC > 0 AND s`z >= H AND ve`z * CC = (H - s`z) IMPLIES
             ve`z * CC = 0
  
    Rerunning step: (skosimp*)
    Repeatedly Skolemizing and flattening,
    this simplifies to: 
    b1 :  
  
    {-1}  ve!1`z * CC!1 > 0
    {-2}  s!1`z >= H
    {-3}  ve!1`z * CC!1 = (H - s!1`z)
      |-------
    {1}   ve!1`z * CC!1 = 0
  
    Rerunning step: (assert)
    Simplifying, rewriting, and recording with decision procedures,
    Q.E.D.
  
  
  Rick Butler
  
  
  --=-moyeb9zn5UFHnFCYmB+h
  Content-Disposition: attachment; filename=bug1.dmp
  Content-Type: text/plain; name=bug1.dmp; charset=UTF-8
  Content-Transfer-Encoding: 7bit
  
  
  %% PVS Version 3.2
  %% 6.2 [Linux (x86)] (Nov 3, 2004 23:30)
  (load-prelude-library "Field/")
  (load-prelude-library "Manip/")
  
  (defmethod copy-untyped* ((ex fieldappl))
    (with-slots (id actuals argument) ex
      (copy ex
        'id id
        'type nil
        'actuals (copy-untyped* actuals)
        'argument (copy-untyped* argument))))
  
  
  
  (defmethod copy-untyped* ((ex fieldappl))
    (with-slots (id actuals argument) ex
      (copy ex
        'id id
        'type nil
        'actuals (copy-untyped* actuals)
        'argument (copy-untyped* argument))))
  
  
  $$$sign.pvs
  sign : THEORY
  BEGIN
  
    Sign : TYPE = {i:int|i=1 OR i=-1}
  
    x, y: VAR real
  
    sign(x): Sign = IF x > 0 THEN 1 ELSE -1 ENDIF
  
    abs_plus: LEMMA
      x*y >= 0 IMPLIES abs(x+y) = abs(x) + abs(y)
  
    sign_times: LEMMA
      x*y /= 0 IMPLIES sign(x*y) = sign(x)*sign(y)
  
  END sign
  
  $$$sign.prf
  (sign (abs_plus 0
         (abs_plus-1 nil 3287930046 nil
          ("" (skosimp*)
           (("" (expand "abs")
             (("" (rewrite "pos_times_ge" -1)
               (("" (prop)
                 (("1" (assert)
                   (("1" (case "x!1 = 0 OR y!1 = 0")
                     (("1" (split -)
                       (("1" (replace*) (("1" (assert) nil nil)) nil)
                        ("2" (replace*) (("2" (assert) nil nil)) nil))
                       nil)
                      ("2" (flatten) (("2" (assert) nil nil)) nil))
                     nil))
                   nil)
                  ("2" (assert) nil nil))
                 nil))
               nil))
             nil))
           nil)
          unchecked
          ((abs const-decl "{n: nonneg_real | n >= m}" real_defs nil)
           (= const-decl "[T, T -> boolean]" equalities nil)
           (OR const-decl "[bool, bool -> bool]" booleans nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (real nonempty-type-from-decl nil reals nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (boolean nonempty-type-decl nil booleans nil)
           (number nonempty-type-decl nil numbers nil)
           (pos_times_ge formula-decl nil real_props nil))
          nil nil nil nil))
        (sign_times 0
         (sign_times-1 nil 3287930046 nil
          ("" (skosimp*)
           (("" (expand "sign")
             (("" (case "x!1 * y!1 > 0")
               (("1" (assert)
                 (("1" (rewrite "pos_times_gt" -1)
                   (("1" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil))
                     nil))
                   nil))
                 nil)
                ("2" (assert)
                 (("2" (rewrite "pos_times_gt" 1)
                   (("2" (prop)
                     (("1" (assert) nil nil) ("2" (assert) nil nil)
                      ("3" (assert) nil nil) ("4" (assert) nil nil))
                     nil))
                   nil))
                 nil))
               nil))
             nil))
           nil)
          unchecked
          ((sign const-decl "Sign" sign nil)
           (pos_times_gt formula-decl nil real_props nil)
           (number nonempty-type-decl nil numbers nil)
           (boolean nonempty-type-decl nil booleans nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (real nonempty-type-from-decl nil reals nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (> const-decl "bool" reals nil)
           (numfield nonempty-type-eq-decl nil number_fields nil)
           (* const-decl "[numfield, numfield -> numfield]" number_fields nil))
          nil nil nil nil)))
  
  
  $$$Vectors.pvs
  Vectors : THEORY
  BEGIN
    x,y,z : VAR real
  
    Vect3 : TYPE = [#
      x,y,z:real
    #]
  
    vect3 : VAR Vect3
  
    v,w : VAR Vect3
    a,b   : VAR real
  
    -(v): Vect3=(# x := -v`x, y := -v`y, z := -v`z #) ;
  
    +(v,w):Vect3=(#
      x:= v`x + w`x,
      y:= v`y + w`y,
      z:= v`z + w`z
    #);
  
  
    -(v,w):Vect3=(#
      x:= v`x - w`x,
      y:= v`y - w`y,
      z:= v`z - w`z
    #);
  
    *(v,w):real =  v`x * w`x + v`y * w`y + v`z * w`z;
  
    *(a,w):Vect3=(#
      x:= a * w`x,
      y:= a * w`y,
      z:= a * w`z
    #)
  
    sq_norm(v):real = v*v
    sq_norm2(v):real = v`x*v`x + v`y*v`y
  
    vect_dist    : LEMMA a*(v+w) = a*v + a*w
  
    vect_dist_sub: LEMMA a*(v-w) = a*v - a*w
  
    vect_split_add: LEMMA (a+b)*v = a*v + b*v
  
    vect_split_sub: LEMMA (a-b)*v = a*v - b*v
  
    
  
  END Vectors
  
  $$$Vectors.prf
  (Vectors
   (vect_dist 0
    (vect_dist-1 nil 3287930046 nil ("" (grind) nil nil) unchecked
     ((+ const-decl "Vect3" Vectors nil) (* const-decl "Vect3" Vectors nil)) ni
 l
     nil nil nil))
   (vect_dist_sub 0
    (vect_dist_sub-1 nil 3287930046 nil ("" (grind) nil nil) unchecked
     ((* const-decl "Vect3" Vectors nil)) nil nil nil nil))
   (vect_split_add 0
    (vect_split_add-1 nil 3287930046 nil ("" (grind) nil nil) unchecked
     ((* const-decl "Vect3" Vectors nil) (+ const-decl "Vect3" Vectors nil)) ni
 l
     nil nil nil))
   (vect_split_sub 0
    (vect_split_sub-1 nil 3287930046 nil ("" (grind) nil nil) unchecked
     ((* const-decl "Vect3" Vectors nil)) nil nil nil nil)))
  
  
  $$$bug1.pvs
  bug1: THEORY
  BEGIN
     
  
    IMPORTING Vectors, sign, reals@sqrt
              % criteria, 
              % common_defs
  
  
    l,r,b,c : VAR real
    a   : VAR nonzero_real
    st  : VAR Vect3 % Target position
    si  : VAR Vect3 % Intruder position
    vi  : VAR Vect3 % Intruder velocity
    te  : VAR real  % Escape time
    voe : VAR Vect3 % Escape velocity
    tr  : VAR real  % Recovery time
    vor : VAR Vect3 % Recovery velocity
    s   : VAR Vect3 % Relative ownship position
    v   : VAR Vect3 % Relative ownship velocity
    ve  : VAR Vect3 % Relative escape velocity
    vr  : VAR Vect3 % Relative recovery velocity
  
    sr  : VAR Vect3 % Relative final position
  
  
    eps, epsp : VAR Sign
    p, vop : VAR Vect3
    t, t1, t2, t3 : VAR real
    v1, v2 : VAR Vect3
    CC: VAR posreal
  
    D  : posreal %% Half the diameter
    H  : posreal %% Half the height
  
    hor_sep?(s) : bool = sq(s`x) + sq(s`y) >= sq(D)   % horizontal separation
  
    vert_sep?(s) : bool = abs(s`z) >= H    % vertical separation
  
    pred_sep?(s,v,t2) : bool =          % predicted separation until time t2
      FORALL t: 0 <= t AND t <= t2 => hor_sep?(s+t*v) OR vert_sep?(s+t*v)
  
  
    signs_are_opposite: LEMMA
        NOT pred_sep?(s,v,tr) AND
        abs(s`z) >= H
      IMPLIES
        sign(s`z) = -sign(v`z)
  
  
    b1: LEMMA ve`z * CC > 0  AND
              s`z >= H AND
              ve`z * CC = (H - s`z) 
          IMPLIES
              ve`z * CC = 0 
  
    signs_ve_z: LEMMA  %% NEW %%
        NOT pred_sep?(s,v,tr) AND
        abs(s`z) >= H AND
        ve`z = (-sign(v`z)*H - s`z)/CC AND
        ve`z /= 0 
      IMPLIES
          sign(ve`z) = sign(v`z)
  
  
  
   
  END bug1
  
  
  $$$bug1.prf
  (bug1
   (signs_are_opposite 0
    (signs_are_opposite-1 nil 3287832817 3310903922
     ("" (skosimp*)
      (("" (expand "pred_sep?")
        (("" (skosimp*)
          (("" (hide 1)
            (("" (expand "vert_sep?")
              (("" (expand "+ ")
                (("" (expand "*")
                  (("" (case "v!1`z > 0")
                    (("1" (mult-ineq -1 -2) (("1" (grind) nil nil)) nil)
                     ("2" (case-replace "v!1`z = 0")
                      (("1" (assert) nil nil)
                       ("2" (flip-ineq 2)
                        (("2" (mult-ineq -1 -2 (- +))
                          (("2" (grind) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unfinished
     ((pred_sep? const-decl "bool" common_defs nil)
      (+ const-decl "Vect3" Vectors nil)
      (Vect3 type-eq-decl nil Vectors nil)
      (sign const-decl "Sign" sign nil)
      (* const-decl "Vect3" Vectors nil)
      (vert_sep? const-decl "bool" criteria nil))
     1613 920 nil nil))
   (b1 0
    (b1-1 nil 3310916343 3310916345
     ("" (skosimp*) (("" (assert) nil nil)) nil) unchecked nil 2025 450 t
     shostak))
   (signs_ve_z 0
    (signs_ve_z-1 nil 3287832817 3310916646
     ("" (skosimp*)
      (("" (lemma "signs_are_opposite")
        (("" (inst?)
          (("" (assert)
            (("" (replace -1 * rl)
              (("" (mult-by -3 "CC!1")
                (("" (mult-by 2 "CC!1")
                  (("" (assert)
                    (("" (case "ve!1`z > 0")
                      (("1" (expand "abs")
                        (("1" (expand "sign")
                          (("1" (lift-if)
                            (("1" (lift-if)
                              (("1" (ground)
                                (("1"
                                  (mult-by -1 "CC!1")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (case-replace
                                       "(H - s!1`z) / CC!1 * CC!1 = (H - s!1`z)
  ")
                                      (("1"
                                        (hide-all-but (-2 -3 -7 6))
                                        (("1"
                                          (rewrite "zero_times1")
                                          (("1" (postpone) nil nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (hide-all-but 1)
                                        (("2" (real-props) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (expand "sign")
                        (("2" (expand "abs")
                          (("2" (lift-if)
                            (("2" (lift-if)
                              (("2" (assert)
                                (("2"
                                  (ground)
                                  (("2"
                                    (mult-by 3 "CC!1")
                                    (("2"
                                      (rewrite "div_cancel2")
                                      (("2"
                                        (move-terms -3 r 1)
                                        (("2"
                                          (hide-all-but (-3 -5 1 5))
                                          (("2"
                                            (name-replace
                                             "veCC"
                                             "ve!1`z * CC!1")
                                            (("2"
                                              (rewrite "zero_times1")
                                              (("2"
                                                (rewrite "neg_mult")
                                                (("2"
                                                  (name-replace
                                                   "SS"
                                                   "1 * s!1`z")
                                                  (("2"
                                                    (postpone)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unfinished
     ((H const-decl "posreal" criteria nil)
      (sign const-decl "Sign" sign nil) (Sign type-eq-decl nil sign nil)
      (Vect3 type-eq-decl nil Vectors nil))
     47819 2160 t nil)))
  
  
  --=-moyeb9zn5UFHnFCYmB+h--

How-To-Repeat: 

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