Simple Model

of a Flood Control System

Definitions

Port variables

val c_def = |- c = 0 : Thm.thm
val r_def = |- r = 1 : Thm.thm

Local variables of CC (writable only by CC)

val pcC_def = |- pcC = 10 : Thm.thm
val cgh_def = |- cgh = 11 : Thm.thm
val d_def = |- d = 12 : Thm.thm

Local variables of RTU (writable of by RTU)

val pcR_def = |- pcR = 20 : Thm.thm
val g_def = |- g = 22 : Thm.thm
val h_def = |- h = 23 : Thm.thm
val gh_def = |- gh = 24 : Thm.thm
val rd_def = |- rd = 21 : Thm.thm

Variable Sets

val comV_def = |- !v. comV v = (v = c) \/ (v = r) : Thm.thm
val locCC_def = |- !v. locCC v = (v = pcC) \/ (v = cgh) \/ (v = d) : Thm.thm

Program locations of CC

val c0_def = |- c0 = 0 : Thm.thm
val c1_def = |- c1 = 1 : Thm.thm
val c2_def = |- c2 = 2 : Thm.thm 
val c3_def = |- c3 = 3 : Thm.thm
val c4_def = |- c4 = 4 : Thm.thm

Program locations of RTU

val r0_def = |- r0 = 0 : Thm.thm
val r1_def = |- r1 = 1 : Thm.thm
val r2_def = |- r2 = 2 : Thm.thm
val r3_def = |- r3 = 3 : Thm.thm
val r4_def = |- r4 = 4 : Thm.thm
val r5_def = |- r5 = 5 : Thm.thm

Actions of CC

val ac0_def =
|- !Inquiry.
ac0 Inquiry =
(\s. s pcC = c0) Then (c,pcC) ::= (Const Inquiry,Const c1)
: Thm.thm

val ac1_def =
|- ac1 = (\s. (s pcC = c1) /\ ~(s r = 0)) Then pcC := Const c2
: Thm.thm

val ac2_def =
|- ac2 =
(\s. s pcC = c2) Then (cgh,r,pcC) :::= ((\s. s r),Const 0,Const c3)
: Thm.thm

val ac3_def =
|- !Decide.
ac3 Decide =
(\s. s pcC = c3) Then (d,pcC) ::= ((\s. Decide (s cgh)),Const c4)
: Thm.thm

val ac4_def =
|- ac4 = (\s. s pcC = c4) Then (c,pcC) ::= ((\s. s d),Const c1)
: Thm.thm

Actions of RTU

val ar0_def =
|- ar0 = (\s. (s pcR = r0) /\ ~(s c = 0)) Then pcR := Const r1
: Thm.thm

val ar1_def =
|- ar1 = (\s. s pcR = r1) Then (rd,c,pcR) :::= ((\s. s c),Const 0,Const r2)
: Thm.thm 

val ar2_def =
|- !Execute.
ar2 Execute =
(\s. s pcR = r2) Then
(\s t.
Execute (s g,s rd) (t g) /\
(t pcR = r3) /\
(!v. ~(v = g) /\ ~(v = pcR) ==> (t v = s v)))
: Thm.thm

val ar3_def =
|- ar3 =
(\s. s pcR = r3) Then
(\s t. (t pcR = r4) /\ (!v. ~(v = h) /\ ~(v = pcR) ==> (t v = s v)))
: Thm.thm

val ar4_def =
|- !Pack.
ar4 Pack =
(\s. s pcR = r4) Then (gh,pcR) ::= ((\s. Pack (s g,s h)),Const r5)
: Thm.thm

val ar5_def =
|- ar5 = (\s. s pcR = r5) Then (r,pcR) ::= ((\s. s gh),Const r0)
: Thm.thm

The definition of CC

val CC_def =
|- !Inquiry Decide a.
CC Inquiry Decide a =
(a = ac0 Inquiry) \/
(a = ac1) \/
(a = ac2) \/
(a = ac3 Decide) \/
(a = ac4)
: Thm.thm

The definition of RTU

val RTU_def =
|- !Execute Pack a.
RTU Execute Pack a =
(a = ar0) \/
(a = ar1) \/
(a = ar2 Execute) \/
(a = ar3) \/
(a = ar4 Pack) \/
(a = ar5)
: Thm.thm

Invariants of CC

val I_CC1_def =
|- !Pack.
I_CC1 Pack =
(\s. ~(s r = 0)) IMP
(\s. s r = Pack (s g,s h)) AND (\s. s c = 0) AND (\s. s pcR = r0)
: Thm.thm

val I_CC2_def =
|- I_CC2 =
(\s. s c = 0) AND (\s. s r = 0) IMP
((\s. s pcC = c1) EQUAL (\s. ~(s pcR = r0)))
: Thm.thm

val I_CC3_def =
|- !Inquiry Pack Decide.
I_CC3 Inquiry Pack Decide =
((\s. s pcC = c0) IMP
(\s. s d = Inquiry) AND
(\s. s d = (Decide o Pack) (s g,s h)) AND
(\s. s r = 0) AND
(\s. s c = 0) AND
(\s. s pcR = r0)) AND
((\s. s pcC = c2) IMP
(\s. s r = Pack (s g,s h)) AND
(\s. ~(s r = 0)) AND
(\s. s c = 0) AND
(\s. s pcR = r0)) AND
((\s. s pcC = c3) IMP
(\s. s cgh = Pack (s g,s h)) AND
(\s. s r = 0) AND
(\s. s c = 0) AND
(\s. s pcR = r0)) AND
((\s. s pcC = c4) IMP
(\s. s d = (Decide o Pack) (s g,s h)) AND
(\s. s r = 0) AND
(\s. s c = 0) AND
(\s. s pcR = r0))
: Thm.thm

val I_CC4_def =
|- I_CC4 =
(\s. s pcC = c0) OR
(\s. s pcC = c1) OR
(\s. s pcC = c2) OR
(\s. s pcC = c3) OR
(\s. s pcC = c4)
: Thm.thm

val I_CC_def =
|- !Inquiry Pack Decide.
I_CC Inquiry Pack Decide =
I_CC1 Pack AND I_CC2 AND I_CC3 Inquiry Pack Decide AND I_CC4
: Thm.thm

Invariants of RTU

val I_RTU1_def =
|- !Decide Pack.
I_RTU1 Decide Pack =
(\s. ~(s c = 0)) IMP
(\s. s c = (Decide o Pack) (s g,s h)) AND
(\s. s r = 0) AND
(\s. s pcC = c1)
: Thm.thm

val I_RTU2_def =
|- I_RTU2 =
(\s. s c = 0) AND (\s. s r = 0) IMP
((\s. s pcC = c1) EQUAL (\s. ~(s pcR = r0)))
: Thm.thm

val I_RTU3_def =
|- !Decide Pack.
I_RTU3 Decide Pack =
((\s. s pcR = r1) IMP
(\s. s c = (Decide o Pack) (s g,s h)) AND
(\s. ~(s c = 0)) AND
(\s. s r = 0) AND
(\s. s pcC = c1)) AND
((\s. s pcR = r2) IMP
(\s. s rd = (Decide o Pack) (s g,s h)) AND
(\s. s c = 0) AND
(\s. s r = 0) AND
(\s. s pcC = c1)) AND
((\s. s pcR = r3) IMP
(\s. s c = 0) AND (\s. s r = 0) AND (\s. s pcC = c1)) AND
((\s. s pcR = r4) IMP
(\s. s c = 0) AND (\s. s r = 0) AND (\s. s pcC = c1)) AND
((\s. s pcR = r5) IMP
(\s. s gh = Pack (s g,s h)) AND
(\s. s c = 0) AND
(\s. s r = 0) AND
(\s. s pcC = c1))
: Thm.thm

val I_RTU4_def =
|- I_RTU4 =
(\s. s pcR = r0) OR
(\s. s pcR = r1) OR
(\s. s pcR = r2) OR
(\s. s pcR = r3) OR
(\s. s pcR = r4) OR
(\s. s pcR = r5)
: Thm.thm

val I_RTU_def =
|- !Decide Pack.
I_RTU Decide Pack =
I_RTU1 Decide Pack AND I_RTU2 AND I_RTU3 Decide Pack AND I_RTU4
: Thm.thm

Theorems

I_CC is an invariant of CC

val I_CC_LOCAL_STAB =
|- ~(Inquiry = 0) /\ (!x. ~(Decide x = 0)) /\ (!x y. ~(Pack (x,y) = 0)) ==>
STABLE (CC Inquiry Decide) (I_CC Inquiry Pack Decide)
: Thm.thm

I_RTU is invariant in RTU

val I_RTU_LOCAL_STAB =
|- ~(Inquiry = 0) /\ (!x. ~(Decide x = 0)) /\ (!x y. ~(Pack (x,y) = 0)) ==>
STABLE (RTU Execute Pack) (I_RTU Decide Pack)
: Thm.thm

I_CC and I_RTU hold in CC [] RTU

val I_COOP_STAB =
|- ~(Inquiry = 0) /\ (!x. ~(Decide x = 0)) /\ (!x y. ~(Pack (x,y) = 0)) ==>
STABLE (CC Inquiry Decide OR RTU Execute Pack)
(I_CC Inquiry Pack Decide AND I_RTU Decide Pack)
: Thm.thm

The P0 Theorem

val CC_CommitReq_SPECP0 =
|- (~(Inquiry = 0) /\
(!x. ~(Decide x = 0)) /\
(!x y. ~(Pack (x,y) = 0))) /\
(locR pcR /\ locR g /\ locR h) /\
|== (NOT (locR IMP locCC OR comV)) /\
IGNORE R I_R locCC /\
STABLE R I_R /\
STABLE (CC Inquiry Decide) (I_CC Inquiry Pack Decide AND I_R) /\
STABLE R (I_CC Inquiry Pack Decide AND I_R) /\
LEADSTO R locR I_R ((\s. s pcR = r4) AND (\s. (s g = X) /\ (s h = Y)))
((\s. s pcR = r0) AND (\s. (s g = X) /\ (s h = Y))) /\
LEADSTO R locR I_R ((\s. s pcR = r1) AND (\s. (s g = X) /\ (s h = Y)))
(\s. Execute (X,(Decide o Pack) (X,Y)) (s g)) /\
UNTIL R (locR OR (\v. v = c)) I_R
((\s. s pcR = r0) AND
(\s. (s g = X) /\ (s h = Y)) AND
NOT (\s. s c = 0))
((\s. s pcR = r1) AND (\s. (s g = X) /\ (s h = Y))) /\
UNLESS R (locR OR (\v. v = c)) I_R
((\s. s pcR = r0) AND (\s. (s g = X) /\ (s h = Y)) AND (\s. s c = 0))
FF /\
CONDWRITE R I_R (\v. v = r) (NOT (\s. s r = 0)) FF /\
STABLE R (\s. s c = 0) /\
LEADSTO R locR I_R TT (\s. s pcR = r0) ==>
LEADSTO (CC Inquiry Decide OR R) (locCC OR comV OR locR)
(I_CC Inquiry Pack Decide AND I_R)
((\s. s pcR = r4) AND (\s. (s g = X) /\ (s h = Y)))
(\s. Execute (X,(Decide o Pack) (X,Y)) (s g))
: Thm.thm