-- Example from 
-- Common Knowledge and Update in Finite Environments, R. van der Meyden, TARK 94/I&C 98
-- Alice sends a message to Bob, 
-- the channel delays the message at most one tick of the clock 
-- (corrected version 24/8/06) 


sent : Bool
delayed : Bool
received : Bool 

init_cond = neg (sent \/ delayed \/ received)

agent Alice "sender" (sent)
agent Bob  "receiver" (received)

-- this environment description assumes a single send occurs 
transitions 
begin 
if 
 Alice.Send -> begin sent := True; delayed := True end 
[] 
 Alice.Send  -> begin sent := True; received := True end 
[] 
 delayed -> begin received := True; delayed := False end 
fi 
end 







-- the message is eventually sent 
fairness = sent 



-- sanity check on delivery 
spec_obs_ctl = AF sent 
spec_obs_ctl = AF received  

spec_obs_ctl = Alice.x => EX received 
spec_obs_ctl = (neg Alice.x) => EX EX received 


-- observational knowledge is insufficient for Alice to ever learn that the
-- message has been received 
spec_obs_ctl = neg EF Knows Alice received 


-- received is local to Bob, so even under observational knowledge we have  
spec_obs_ctl = AG (received => Knows Bob received) 


-- with respect to perfect recall, 
-- if the message is sent and immediately received, the amount of mutual knowledge increases
-- with the amount time they wait afterwards 

-- after one step

spec_spr_ltl_nested = X ( received => Knows Bob received )

spec_spr_ltl_nested = X ( received => neg Knows Alice received )

-- after two steps 
 
spec_spr_ltl_nested = X ( received => X Knows Alice received )

spec_spr_ltl_nested = X ( received => X Knows Bob (Knows Alice received ))

spec_spr_ltl_nested = X ( received => X Knows Alice (Knows Bob received ))

spec_spr_ltl_nested = X ( received => X Knows Bob (Knows Alice (Knows Bob received )))

spec_spr_ltl_nested = X ( received => X neg Knows Alice (Knows Bob (Knows Alice received )))


-- after 3 steps 

spec_spr_ltl_nested = X ( received => X 2 Knows Alice (Knows Bob (Knows Alice received )))

spec_spr_ltl_nested = X ( received => X 2 Knows Bob (Knows Alice (Knows Bob (Knows Alice received ))))

spec_spr_ltl_nested = X ( received => X 2 neg Knows Alice (Knows Bob (Knows Alice (Knows Bob (Knows Alice received )))))


-- after 4 steps 

spec_spr_ltl_nested = X ( received => X 3 Knows Alice (Knows Bob (Knows Alice (Knows Bob (Knows Alice received )))))


spec_spr_ltl_nested = X ( received => X  3 Knows Bob (Knows Alice (Knows Bob (Knows Alice (Knows Bob (Knows Alice received ))))))


spec_spr_ltl_nested = X ( received => X  3 neg Knows Alice (Knows Bob (Knows Alice (Knows Bob (Knows Alice (Knows Bob (Knows Alice received )))))))


-- after 5 steps 

spec_spr_ltl_nested = X ( received => X  4 Knows Alice (Knows Bob (Knows Alice (Knows Bob (Knows Alice (Knows Bob (Knows Alice received )))))))

spec_spr_ltl_nested = X ( received => X  4 Knows Bob (Knows Alice (Knows Bob (Knows Alice (Knows Bob (Knows Alice (Knows Bob (Knows Alice received ))))))))

spec_spr_ltl_nested = X ( received => X  4 neg Knows Alice (Knows Bob (Knows Alice (Knows Bob (Knows Alice (Knows Bob (Knows Alice (Knows Bob (Knows Alice received )))))))))

-- etc ...


-- Alice's protocol.
protocol "sender" (sent: observable Bool)

x: Bool 
-- x represents whether the send happens in the next step 

begin
do 
 neg x -> skip
 []  neg x -> x:= True 
 [] break -> << Send >>
od; 
do 
  True -> skip
od 
end



-- Bob's protocol.
protocol "receiver" (received: observable Bool)

begin
do 
  True -> skip
od 
end