[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