# PVS Bug 623

Synopsis: ground flawed
Severity: serious
Priority: medium
Responsible: dave_sc (Dave Stringer-Calvert)
State: analyzed
Class: sw-bug
Arrival-Date: Wed Nov 28 14:41:32 2001
Originator: John Rushby
Organization: csl.sri.com
Release: PVS 2.4
Environment:
System:
Architecture:
Description:
The proof of before3 used in PVS 2.3 was
(SKOSIMP) (EXPAND "before") (INST - 0) (GROUND)
This no longer works in 2.4. What does work is replacing the
(GROUND) by (ASSERT). But I thought (GROUND) subsumed (ASSERT).
Furthermore, doing (ASSERT) after the (GROUND) doesn't work, so
something fishy is going on.
This is extracted from Holger Pfeifer's ttp proof. There are several
proofs in that (massive) verification that no longer work in 2.4 but
this is the simplest.
John
bug [n:upfrom(3)] : THEORY
BEGIN
% Following should point to the dorectory containing the NASA mod library
mod : LIBRARY = "./NASA-mod/"
IMPORTING mod@mod
time : TYPE+ = nat
postime : TYPE+ = posnat
proc : TYPE+ = below(n) % -- processors numbered 0 .. n-1
memvec : TYPE+ = [proc -> bool] % -- membership vector
p,q,r,a,b,
x,y,z,xs : VAR proc
S : VAR set[proc]
j : VAR postime
i,s,t : VAR time
v,w : VAR memvec
broadcaster(t) : proc = mod(t,n) % -- broadcaster at time t
% -- x will broadcast before y, at time t or later
before(t,x,y) : bool =
FORALL i:
y = broadcaster(t+i) => EXISTS s: s<i AND x=broadcaster(t+s)
before3 : LEMMA
before(t,x,y) => y /= broadcaster(t)
END bug
How-To-Repeat:
Fix: