(* Improved four-buffer protocol based on MSMIE *)
(* The following constraints on memory states are used
to reduce the size of the generated agent. It is
easy to prove the constraints by showing they hold
initially and are invariant over the transitions.
1. (rm = emptyset and #masters = 0) or
(not rm = emptyset and #masters = 1)
2. Likewise but for old masters.
*)
const I = "i"
const S = "s"
const N = "n"
const M = "m"
const O = "old"
const Status = {I,S,N,M,O}
const MI = {1,2}
const BI = {1,2,3,4}
const readers = pow(MI)
const rpair = {p|union(diff(MI,p#1),diff(MI,p#2)) = MI
where p:prod(readers,readers)}
const b1 = {{<>,<>,<>,<>}|
a:prod(Status,Status,Status,Status)}
const b2 = {b:b1|size({c:b|c#1 = S}) = 1}
const b3 = {b:b2|size({c:b|c#1 = N}) < 2}
const b4 = {b:b3|size({c:b|c#1 = M}) < 2}
const Bufs = {b:b4|size({c:b|c#1 = O}) < 2}
label slave
label ma_MI, ma'_MI, mr_MI
label ma1,ma2,ma1',ma2',mr1,mr2
agent Buffers(B:Bufs,r:rpair) =
(* 1,2 *)
sum(b1:B, sum(b2:diff(B,{b1}), sum(b3:diff(B,{b1,b2}),
((if b1#1 = S and b2#1 = N and b3#1 = I then
slave.(Buffers(union({<>,<>,<>},
diff(B,{b1,b2,b3})),r)
+ Buffers(union({<>,<>,<>},
diff(B,{b1,b2,b3})),r)))))))
(* 3 *)
+ sum(b1:B, sum(b2:diff(B,{b1}),
(if b1#1 = S and b2#1 = I and not member(N,{b#1|b:diff(B,{b1,b2})}) then
slave.Buffers(union({<>,<>},diff(B,{b1,b2})),r))))
(* 4 *)
+ sum(b1:B, sum(b2:diff(B,{b1}),
(if b1#1 = S and b2#1 = N and not member(I,{b#1|b:diff(B,{b1,b2})}) then
slave.Buffers(union({<>,<>},diff(B,{b1,b2})),r))))
(* 5 *)
+ sum(b1:B, sum(b2:diff(B,{b1}),
(if b1#1 = M and b2#1 = O then
sum(k:diff(MI,union(r#1,r#2)),
ma_k.Buffers(union({<>,<>},
diff(B,{b1,b2})),<>)))))
(* 6 *)
+ sum(b1:B,
(if b1#1 = M and not member(N,{b#1|b:diff(B,{b1})}) then
sum(k:diff(MI,union(r#1,r#2)),
ma_k.Buffers(union({<>},diff(B,{b1})),
<>))))
(* 7 *)
+ sum(b1:B, sum(b2:diff(B,{b1}),
(if b1#1 = M and b2#1 = N and r#1 = {} then
sum(k:diff(MI,r#2),
ma'_k.Buffers(union({<>,<>},
diff(B,{b1,b2})),<>)))))
(* 8 *)
+ sum(b1:B,
(if b1#1 = N and r#2 = {} then
sum(k:diff(MI,r#1),
ma'_k.Buffers(union({<>},
diff(B,{b1})),<>))))
(* 9 *)
+ (if size(r#1) > 1 then
sum(k:r#1, mr_k.Buffers(B,<>)))
(* 10 *)
+ sum(b1:B,
(if b1#1 = O and size(r#1) = 1 then
sum(k:r#1, mr_k.Buffers(union({<>},
diff(B,{b1})),<<{},r#2>>))))
(* 11 *)
+ (if size(r#2) > 1 then
sum(k:r#2, mr_k.Buffers(B,<>)))
(* 12 *)
+ sum(b1:B, sum(b2:diff(B,{b1}),
(if b1#1 = M and b2#1 = N and size(r#2) = 1 then
sum(k:r#2, ma_k.Buffers(union({<>,<>},
diff(B,{b1,b2})),<>)))))
(* 13 *)
+ sum(b1:B,
(if b1#1 = M and size(r#2) = 1 and not member(N,{b#1|b:diff(B,{b1})})
then sum(k:r#2,
ma_k.Buffers(union({<>},diff(B,{b1})),<>))))
agent NewMsmie = Buffers({<>,<>,<>,<>},<<{},{}>>)
[ma1/ma_1,ma1'/ma'_1,ma2/ma_2,ma2'/ma'_2,mr1/mr_1,mr2/mr_2]