-- This MCK program solves the Russian Cards Problem
-- Given actual deal 012.345.6,
-- Anne says: "My hand is one of 012, 034, 056, 135, and 246", 
-- and then Bill says: "Cath holds card 6"

-- numbers of card per player
type Counter = {0..3}
na : Counter
nb : Counter
nc : Counter

-- stage of the transitions
-- initial stage: 0; the cards are dealt: stage 0 -> 1; 
-- Anne announces: stage 1 -> 2; Bill announces: stage 2 -> 3
-- final stage: 3
stage : Counter 

-- hand of cards per player, which is list of seven booleans
a_hand : Bool[7]
b_hand : Bool[7]
c_hand : Bool[7]

-- true after Anne's announcement
a_announce : Bool

-- true after Bill's announcement
b_announce : Bool

-- Initially all counters are set to 0 and 
-- all booleans are set to false
init_cond = 
  (  na == 0 /\ nb == 0 /\ nc == 0 /\ stage == 0 /\ neg (
     a_announce  \/ b_announce  \/
     a_hand[0] \/ a_hand[1] \/ a_hand[2] \/ 
     a_hand[3] \/ a_hand[4] \/ a_hand[5] \/ a_hand[6] \/
     b_hand[0] \/ b_hand[1] \/ b_hand[2] \/ 
     b_hand[3] \/ b_hand[4] \/ b_hand[5] \/ b_hand[6] \/
     c_hand[0] \/ c_hand[1] \/ c_hand[2] \/ c_hand[3] \/ 
     c_hand[4] \/ c_hand[5] \/ c_hand[6]    ) 
  )

-- Agents Anne, Bill, and Cath are created.
-- They use protocols "anne", "bill", and "cath", defined below.
-- Their four arguments list locally observable variable (instances).
agent A "anne" (a_hand, a_announce, b_announce, stage)
agent B "bill" (b_hand, a_announce, b_announce, stage)
agent C "cath" (c_hand, a_announce, b_announce, stage)

-- begin of transitions (these specify the results of actions)

transitions
begin
if 
-- In stage 0 cards 0, 1, ..., 6 are dealt in that order.
-- Anne and Bill each receive three cards, Cath receives one.
 stage == 0  -> 
   begin
     if 
      na < 3  -> begin a_hand[0]:=True; na:= na+1 end [] 
      nb < 3  -> begin b_hand[0]:=True; nb:= nb+1 end [] 
      nc == 0 -> begin c_hand[0]:=True; nc:= 1 end
     fi;
     if 
      na < 3  -> begin a_hand[1]:=True; na:= na+1 end [] 
      nb < 3  -> begin b_hand[1]:=True; nb:= nb+1 end [] 
      nc == 0 -> begin c_hand[1]:=True; nc:= 1 end
     fi;
     if 
      na < 3  -> begin a_hand[2]:=True; na:= na+1 end [] 
      nb < 3  -> begin b_hand[2]:=True; nb:= nb+1 end [] 
      nc == 0 -> begin c_hand[2]:=True; nc:= 1 end
     fi;
     if 
      na < 3  -> begin a_hand[3]:=True; na:= na+1 end [] 
      nb < 3  -> begin b_hand[3]:=True; nb:= nb+1 end [] 
      nc == 0 -> begin c_hand[3]:=True; nc:= 1 end
     fi;
     if 
      na < 3  -> begin a_hand[4]:=True; na:= na+1 end [] 
      nb < 3  -> begin b_hand[4]:=True; nb:= nb+1 end [] 
      nc == 0 -> begin c_hand[4]:=True; nc:= 1 end
     fi;
     if 
      na < 3  -> begin a_hand[5]:=True; na:= na+1 end [] 
      nb < 3  -> begin b_hand[5]:=True; nb:= nb+1 end [] 
      nc == 0 -> begin c_hand[5]:=True; nc:= 1 end
     fi;
     if 
      na < 3  -> begin a_hand[6]:=True; na:= na+1 end [] 
      nb < 3  -> begin b_hand[6]:=True; nb:= nb+1 end [] 
      nc == 0 -> begin c_hand[6]:=True; nc:= 1 end
     fi
   end 

[] 
-- In stage 1, Anne announces that her hand is one of five hands. 
-- This is determined by the protocol introduced below.
 stage == 1 /\ A.Announce -> a_announce := True 
  
[]
-- In stage 2 Bill announces that Cath holds card 6.
-- (Alternatively, not here, Bill announces 'the card of Cath'.)
 stage == 2 /\ B.Announce /\ c_hand[6] -> b_announce:=True

fi; 

-- Update the stage counter
if 
 stage == 0 -> stage := 1 [] 
 stage == 1 -> stage := 2 []
 stage == 2 -> stage := 3
fi 
end 
-- end of transitions

-- begin of verification of properties

-- After Anne's announcement, Bill knows Anne's cards, 
-- whenever her announcement could have been made. 
-- (Therefore this is public knowledge.)
spec_spr_xn = X 2 ( 
    a_announce
      => 
   ( ((Knows B a_hand[0]) \/ (Knows B (neg a_hand[0]))) /\ 
     ((Knows B a_hand[1]) \/ (Knows B (neg a_hand[1]))) /\ 
     ((Knows B a_hand[2]) \/ (Knows B (neg a_hand[2]))) /\ 
     ((Knows B a_hand[3]) \/ (Knows B (neg a_hand[3]))) /\ 
     ((Knows B a_hand[4]) \/ (Knows B (neg a_hand[4]))) /\ 
     ((Knows B a_hand[5]) \/ (Knows B (neg a_hand[5]))) /\ 
     ((Knows B a_hand[6]) \/ (Knows B (neg a_hand[6]))) )  
   		  )

-- After Anne's announcement, Anne does not yet know Bill's cards.
-- Therefore the following fails. 
spec_spr_xn = X 2 (
   a_announce
     =>
  (  (((Knows A b_hand[0]) \/ (Knows A neg b_hand[0]))) /\ 
     (((Knows A b_hand[1]) \/ (Knows A neg b_hand[1]))) /\
     (((Knows A b_hand[2]) \/ (Knows A neg b_hand[2]))) /\
     (((Knows A b_hand[3]) \/ (Knows A neg b_hand[3]))) /\
     (((Knows A b_hand[4]) \/ (Knows A neg b_hand[4]))) /\
     (((Knows A b_hand[5]) \/ (Knows A neg b_hand[5]))) /\ 
     (((Knows A b_hand[6]) \/ (Knows A neg b_hand[6]))) ))

-- After Anne's announcement, Cath remains ignorant, whenever 
-- the announcement could be made (therefore this is public knowledge)
spec_spr_xn = X 2 (
    a_announce
      =>
   ( neg ((Knows C a_hand[0]) \/ (Knows C b_hand[0])) /\ 
     neg ((Knows C a_hand[1]) \/ (Knows C b_hand[1])) /\
     neg ((Knows C a_hand[2]) \/ (Knows C b_hand[2])) /\
     neg ((Knows C a_hand[3]) \/ (Knows C b_hand[3])) /\
     neg ((Knows C a_hand[4]) \/ (Knows C b_hand[4])) /\
     neg ((Knows C a_hand[5]) \/ (Knows C b_hand[5])) /\ 
     neg ((Knows C a_hand[6]) \/ (Knows C b_hand[6]))  )  )

-- After Bill's announcement, (it is public that) Anne knows Bill's cards.
spec_spr_xn = X 3 (
   ( a_announce /\ b_announce )
     =>
  (  (((Knows A b_hand[0]) \/ (Knows A neg b_hand[0]))) /\ 
     (((Knows A b_hand[1]) \/ (Knows A neg b_hand[1]))) /\
     (((Knows A b_hand[2]) \/ (Knows A neg b_hand[2]))) /\
     (((Knows A b_hand[3]) \/ (Knows A neg b_hand[3]))) /\
     (((Knows A b_hand[4]) \/ (Knows A neg b_hand[4]))) /\
     (((Knows A b_hand[5]) \/ (Knows A neg b_hand[5]))) /\ 
     (((Knows A b_hand[6]) \/ (Knows A neg b_hand[6]))) ))

-- After Bill's announcement, (it is public that) Cath remains ignorant.
spec_spr_xn = X 3 (
   ( a_announce /\ b_announce )
      =>
   ( neg ((Knows C a_hand[0]) \/ (Knows C b_hand[0])) /\ 
     neg ((Knows C a_hand[1]) \/ (Knows C b_hand[1])) /\
     neg ((Knows C a_hand[2]) \/ (Knows C b_hand[2])) /\
     neg ((Knows C a_hand[3]) \/ (Knows C b_hand[3])) /\
     neg ((Knows C a_hand[4]) \/ (Knows C b_hand[4])) /\
     neg ((Knows C a_hand[5]) \/ (Knows C b_hand[5])) /\ 
     neg ((Knows C a_hand[6]) \/ (Knows C b_hand[6]))  )  )

-- begin of protocols

-- the protocol "anne" for agent A
-- In stage 1 Anne announces "My hand is one of 012, 034, 056, 135, and 246".
-- Action <<Announce>> results in proposition a_announce becoming true.
protocol "anne" (cards: observable Bool[7], 
                 a_announce: observable Bool, 
                 b_announce: observable Bool,
                 stage: observable Counter)
begin
  skip; if  
    ((cards[0] /\ cards[1] /\ cards[2]) \/
     (cards[0] /\ cards[3] /\ cards[4]) \/ 
     (cards[0] /\ cards[5] /\ cards[6]) \/
     (cards[1] /\ cards[3] /\ cards[5]) \/ 
     (cards[2] /\ cards[4] /\ cards[6]) )
   		-> <<Announce>>
  fi
end

-- the protocol "bill" for agent B
-- Bill announces Cath's card in stage 2 (indirectly, in the transitions)
protocol "bill" (cards: observable Bool[7], 
                 a_announce: observable Bool, 
                 b_announce: observable Bool,
                 stage: observable Counter)
begin
 skip; skip; 
 if stage == 2 /\ a_announce -> <<Announce>>
 fi
end 

-- the protocol "cath" for agent C
-- Cath does not act.
protocol "cath" (cards: observable Bool[7], 
                 a_announce: observable Bool, 
                 b_announce: observable Bool,
                 stage: observable Counter)
begin
 skip; skip ; skip 
end 

-- end of protocols