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)

(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-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