german_undip.cub

type state = Invalid | Shared | Exclusive
type msg = Empty | Reqs | Reqe | Inv | Invack | Gnts | Gnte

var Exgntd : bool
var Curcmd : msg

array Chan1[proc] : msg
array Chan2[proc] : msg
array Chan3[proc] : msg
array PC[proc] : state
array Invset[proc] : bool
array Shrset[proc] : bool
array Curclient[proc] : bool

init (z) { 		   
     Chan1[z] = Empty &&
     Chan2[z] = Empty &&
     Chan3[z] = Empty &&
     PC[z] = Invalid &&
     Invset[z] = False &&
     Shrset[z] = False &&
     Curcmd = Empty &&
     Exgntd = False &&
     Curclient[z] = False
}


unsafe (z1 z2) { PC[z1] = Exclusive && PC[z2] = Exclusive }

(* #home0
   #r1
LC	currentcommand=requestshared & exclusivegranted=false
      & channeltwo=empty & currentclient=true
      & currentcommand'=empty & sharedlist'=true 
      & channeltwo'=grantshared
*)

transition home0(n)
requires { Curcmd = Reqs && Exgntd = False && Chan2[n] = Empty &&
    Curclient[n] = True }
{ Curcmd := Empty;
Shrset[j] := case | j = n : True | _ : Shrset[j] ;
Chan2[j] := case | j = n : Gnts | _ : Chan2[j] ;
}

(*
#home1
#r2
BDP    currentcommand=requestexclusive & channeltwo=empty
#       & sharedlist=false 
       & currentclient=true
       & currentcommand'=empty & sharedlist'=true
       & exclusivegranted'=true & channeltwo'=grantexclusive
       & [LR: p.sharedlist=false]
*)

transition home1(n)
requires { Curcmd = Reqe && Chan2[n] = Empty &&
    Curclient[n] = True && Shrset[n] = False &&
    forall_other i. Shrset[i] = False }
{
Curcmd := Empty; Exgntd := True;
Shrset[j] := case | j = n : True | _ : Shrset[j] ;
Chan2[j] := case | j = n : Gnte | _ : Chan2[j] ;
}


(*
#home2: channelone=requestshared, sharedlist=false
#r3
BDP    currentcommand=empty & channelone=requestshared
       & currentcommand'=requestshared & channelone'=empty
       & invalidatelist'=false & currentclient'=true
       & [LR: p.invalidatelist'=true & p.sharedlist=true
             & p.currentclient'=false]
       & [LR: p.invalidatelist'=false & p.sharedlist=false
             & p.currentclient'=false]
*)

transition home2r3(n)
requires { Curcmd = Empty && Chan1[n] = Reqs (* && Shrset[n] = False *)}
{ 
Curcmd := Reqs;
Chan1[j] := case | j = n : Empty | _ : Chan1[j] ;
Invset[j] := case | j = n : False | _ : Shrset[j] ;
Curclient[j] := case | j = n : True | _ : False 
}

(*
#home2: channelone=requestexclusive, sharedlist=false
#r4
BDP    currentcommand=empty & channelone=requestexclusive
       & currentcommand'=requestexclusive & channelone'=empty
       & invalidatelist'=false & currentclient'=true
       & [LR: p.invalidatelist'=true & p.sharedlist=true
             & p.currentclient'=false]
       & [LR: p.invalidatelist'=false & p.sharedlist=false
             & p.currentclient'=false]
*)

transition home2r4(n)
requires { Curcmd = Empty && Chan1[n] = Reqe (* && Shrset[n] = False *)}
{
Curcmd := Reqe;
Chan1[j] := case | j = n : Empty | _ : Chan1[j] ;
Invset[j] := case | j = n : False | _ : Shrset[j] ;
Curclient[j] := case | j = n : True | _ : False 
}


(*
#home2: channelone=requestshared, sharedlist=true
#r5
BDP    currentcommand=empty & channelone=requestshared
       & currentcommand'=requestshared & channelone'=empty
       & invalidatelist'=true & currentclient'=true
       & [LR: p.invalidatelist'=true & p.sharedlist=true
             & p.currentclient'=false]
       & [LR: p.invalidatelist'=false & p.sharedlist=false
             & p.currentclient'=false]
*)

transition home2r5(n)
requires { Curcmd = Empty && Chan1[n] = Reqs (* && Shrset[n] = True *)}
{ 
Curcmd := Reqs;
Chan1[j] := case | j = n : Empty | _ : Chan1[j] ;
Invset[j] := case | j = n : True | _ : Shrset[j] ;
Curclient[j] := case | j = n : True | _ : False
}

(*
#home2: channelone=requestexclusive, sharedlist=true
#r6
BDP    currentcommand=empty & channelone=requestexclusive
       & currentcommand'=requestexclusive & channelone'=empty
       & invalidatelist'=true & currentclient'=true
       & [LR: p.invalidatelist'=true & p.sharedlist=true
             & p.currentclient'=false]
       & [LR: p.invalidatelist'=false & p.sharedlist=false
             & p.currentclient'=false]
*)

transition home2r6(n)
requires { Curcmd = Empty && Chan1[n] = Reqe (* && Shrset[n] = True *)}
{
Curcmd := Reqe;
Chan1[j] := case | j = n : Empty | _ : Chan1[j] ;
Invset[j] := case | j = n : True | _ : Shrset[j] ;
Curclient[j] := case | j = n : True | _ : False 
}


(*
#home3
#r7
LC     currentcommand=requestshared & exclusivegranted=true
       & invalidatelist=true & channeltwo=empty
       & invalidatelist'=false & channeltwo'=invalidate
*)

transition home3(n)
requires { Curcmd = Reqs && Exgntd = True && Chan2[n] = Empty &&
    Invset[n] = True }
{
Invset[j] := case | j = n : False | _ : Invset[j] ;
Chan2[j] := case | j = n : Inv | _ : Chan2[j] ;
}

(*
#home4
#r8
LC     currentcommand=requestexclusive 
       & invalidatelist=true   & channeltwo=empty
       & invalidatelist'=false & channeltwo'=invalidate
*)

transition home4(n)
requires { Curcmd = Reqe  && Chan2[n] = Empty && Invset[n] = True }
{
Invset[j] := case | j = n : False | _ : Invset[j] ;
Chan2[j] := case | j = n : Inv | _ : Chan2[j] ;
}


(*
#home5 grantshared,grantexclusive, invalidate
#LC     currentcommand not empty & channelthree=invalidatevack
#       & sharedlist'=false & exclusivegranted'=false
#       & channelythree'=empty
*)

(*
transition home5(n)
requires { Curcmd <> Empty && Chan3[n] = Invack }
{
Exgntd := False;
Shrset[j] := case | j = n : False | _ : Shrset[j] ;
Chan3[j] := case | j = n : Empty | _ : Chan3[j] ;
}
*)

(*
#home5 grantshared
#r9
LC     currentcommand=grantshared
       & channelthree=invalidateack
       & sharedlist'=false & exclusivegranted'=false
       & channelthree'=empty
*)

transition home5r9(n)
requires { Curcmd = Gnts && Chan3[n] = Invack }
{
Exgntd := False;
Shrset[j] := case | j = n : False | _ : Shrset[j] ;
Chan3[j] := case | j = n : Empty | _ : Chan3[j] ;
}

(*
#home5 grantexclusive
#r10
LC     currentcommand=grantexclusive
       & channelthree=invalidateack
       & sharedlist'=false & exclusivegranted'=false
       & channelthree'=empty
*)

transition home5r10(n)
requires { Curcmd = Gnte && Chan3[n] = Invack }
{
Exgntd := False;
Shrset[j] := case | j = n : False | _ : Shrset[j] ;
Chan3[j] := case | j = n : Empty | _ : Chan3[j] ;
}


(*
#client1
#r11
LC     pc=invalid 
       & channelone=empty
       & channelone'=requestshared
*)

transition client1(n)
requires { PC[n] = Invalid && Chan1[n] = Empty }
{ 
Chan1[j] := case | j = n : Reqs | _ : Chan1[j] ;
}


(*
#client 2
#r12
LC     pc=invalid 
       & channelone=empty
       & channelone'=requestexclusive
*)

transition client2(n)
requires { PC[n] = Invalid && Chan1[n] = Empty }
{
Chan1[j] := case | j = n : Reqe | _ : Chan1[j] ;
}

(*
#client3
#r13
LC    pc=shared
      & channelone=empty
      & channelone'=requestexclusive
*)

transition client3(n)
requires { PC[n] = Shared && Chan1[n] = Empty }
{
Chan1[j] := case | j = n : Reqe | _ : Chan1[j] ;
}

(*
#client4
#r14
LC    pc'=invalid
      & channeltwo=invalidate & channelthree=empty
      & channeltwo'=empty & channelthree'=invalidateack
*)

transition client4(n)
requires { Chan2[n] = Inv && Chan3[n] = Empty }
{
PC[j] := case | j = n : Invalid | _ : PC[j] ;
Chan2[j] := case | j = n : Empty | _ : Chan2[j] ;
Chan3[j] := case | j = n : Invack | _ : Chan3[j] ;
}

(*
#client5
#r15
LC    pc'=shared 
      & channeltwo=grantshared
      & channeltwo'=empty
*)

transition client5(n)
requires { Chan2[n] = Gnts }
{
PC[j] := case | j = n : Shared | _ : PC[j] ;
Chan2[j] := case | j = n : Empty | _ : Chan2[j] ;
}

(*
#client6
#r16
LC    pc'=exclusive 
      & channeltwo=grantexclusive
      & channeltwo'=empty
*)

transition client6(n)
requires { Chan2[n] = Gnte }
{
PC[j] := case | j = n : Exclusive | _ : PC[j] ;
Chan2[j] := case | j = n : Empty | _ : Chan2[j] ;
}