[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] PVS Help (fwd)
Forgot to cc this mail to the pvs-help. Would appreciate any help in this
regard. Please see enclosed text.
Best,
Purnendu
---------- Forwarded message ----------
Date: Wed, 16 Feb 2005 03:30:33 -0500 (EST)
From: Dr. Purnendu Sinha <sinha@encs.concordia.ca>
To: owre@csl.sri.com
Cc: Neeraj Suri <suri@informatik.tu-darmstadt.de>
Subject: PVS Help
Hello,
I am trying to work with a PVS theory that appeared in the paper "Formally
Verified On-Line Diagnosis" by Walter, Lincoln and Suri. As the PVS source
is not available, I tried to reproduce the code from latex-ified code
which appears in the paper. A pvs file is attached to this mail.
I am running into problems as described below:
1. While doing type-check (M-x tcp), it always gives an error ", expected
here". But I do not see a need for "," in line 102. (part of MEASURE...)
2. Also, if I change MEASURE to something different to get pass that
error, it then complains about the theories that are being imported.
I am using PVS 3.1 running on Solaris. I would appreciate if you could
guide me to resolve this problem.
It would be much appreciated if a complete dump file with a complete proof
could be provided.
Thanks in advance.
Best regards,
Purnendu Sinha
pp [m:posnat,n:posnat,T:TYPE,error:T,BAD:{x:T|not x = error},
GOOD:{x:T|(not x = error) and (not x= BAD)},
Val :[upto[m] -> {x:T |not(x=error or x=BAD or x=GOOD)}]]
: THEORY
BEGIN
rounds: TYPE = upto[m]
t:VAR T
fcu : TYPE = below[n]
fcuset:TYPE =setof[fcu]
fcuvector:TYPE = [fcu -> T]
G,p,q,z : VAR fcu
v,v1,v2 :var fcuvector
caucus : VAR fcuset
r,R,R2: VAR rounds
PSET: TYPE =fcu
pset: VAR setof[PSET]
i,j,k,i2,j2 :VAR PSET
Accuse,OldAccuse : VAR [PSET,PSET -> bool]
AllDeclare:VAR [PSET,PSET -> bool]
Importing card_set[fcu,n,identity[fcu]],
finite_cardinality[fcu,n,identity[fcu]],
filters[fcu],hybridmjrty[T,n,error]
statuses : TYPE = {symmetric,manifest,good}
status :[fcu -> statuses]
g(z) : bool = good?(status(z))
s(z) : bool = symmetric?(status(z))
c(z) : bool = manifest?(status(z))
cs(caucus):fcuset = filter(caucus,c)
ss(caucus):fcuset = filter(caucus,s)
gs(caucus):fcuset = filter(caucus,g)
fincard_all : LEMMA
fincard(caucus)
= fincard(cs(caucus))+ fincard(ss(caucus))+ fincard(gs(caucus))
send : [T,fcu,fcu -> T]
send1: AXIOM g(p) implies send(t,p,q)=t
send2: AXIOM c(p) implies send(t,p,q)= error
send4: AXIOM s(p) implies (t,p,q) = send(t,p,z)
send5: LEMMA send(t,p,q) = send(t,p,z)
HybridMajority(caucus,v):T = PROJ_1(Hybrid_mjrty(caucus,v,n))
HybridMajority1: LEMMA
fincard(gs(caucus)) > fincard(ss(caucus)) and
( forall p : g(p) and member(p,caucus) implies v(p)=t) and
t/= error and (forall p : c(p) and member (p,caucus) implies
v(p)= error) implies Hybridmajority(caucus,v)=t
HybridMajority2: LEMMA
(forall p : member (p, caucus) implies v1(p)= v2(p))
implies HybridMajority(caucus,v1) = HybridMajority(caucus,v2)
HybridMajority3: LEMMA
HybridMajority(caucus,v) = t and (forall p,q : g(p) and g(q) and
member (p,caucus) and member (q,caucus) implies
(v(p) =v(q) and v(p) /= error )) and
fincard (gs(caucus)) > fincard (ss(caucus)) and
( forall p : c(p) and member (p,caucus) implies v(p)=error)
implies (forall p: g(p) and memeber(p,caucus) implies v(p)=t)
Syndrome(R,j,i,OldAccuse): T =
IF OldAccuse(i,j) or (not VAL(R) = send(Val(R),j,i)) THEN BAD
ELSE GOOD
ENDIF
KDeclare(pset,R,OldAccuse,j,k):bool =
HybridMajority(pset, lambda i : send(Syndrome(R,j,i,OldAccuse),i,k))=BAD
PP(pset,R,OldAccuse)(i,j):
RECURSIVE bool = If R=0 Then FALSE
ELSE
KDeclareJ(pset,R,OldAccuse,j,i)
or
PP(pset,R-1,
( lambda i2,k:
OldAccuse(i2,k)
or EXISTS j2: (KDeclareJ(pset,R,OldAccuse,j2,i2) /=
(send(Syndrome(R,j2,k,OldAccuse),k,i2) = BAD))))(i,j)
ENDIF
MEASURE (lambda pset, OldAccuse, implies nat : R)
Correctness_Prop(R):bool=
(Forall i,j, pset, OldAccuse: g(i) AND member(i,pset) AND member(j,pset) AND
fincard(gs(pset)) > fincard(ss(pset))+1 AND PP(pset,R,OldAccuse)(i,j) AND
(forall p,q,k: ((g(p) AND g(q) AND OldAccuse(p,k)) IMPLIES
OldAccuse(q,k) AND (c(k) OR s(k)))) IMPLIES c(j) OR s(j))
Correctness: LEMMA Correctness_Prop(R)
Completeness_Prop(R): bool = (forall i,j, pset, OldAccuse: g(i) AND
member(i,pset) AND member(j,pset) AND (c(j) OR (s(j) AND (forall t,p:
send(t,j,p) /= t))) AND fincard(gs(pset)) > fincard(ss(pset)) +1 IMPLIES
PP(pset,R,OldAccuse)(i,j))
Completeness : LEMMA (forall R: Completeness_Prop(R) OR R =0)
Empty(i,j) : bool = FALSE
Final_Correctness : Theorem
(forall i,j: g(i) AND (c(j) OR (s(j) AND (forall t,p: send(t,j,p) /= t))) AND
fincard(gs(fullset[fcu])) > fincard(ss(fullset[fcu])) + 1 AND R > 0
IMPLIES PP(fullset[fcu], R, Empty)(i,j))
% ASSUMING
% assuming declarations
% ENDASSUMING
END pp