module RUSnew
where 
import DEMO
-- This is an implementation of Russian Cards problem in DEMO
-- By using this, we can check whether some communications are effective and safe.

-- Three agens Anne/Bill/Cath are represented by a/b/c.
-- Make sure to enable `last_agent = c' in line 29 of DEMO source file.

-- generate all possible deals
deals  = [(d0,d1,d2,d3,d4,d5,d6)|  
				d0<-[0..6], d1<-[d0+1..6],d2<-[d1+1..6],
				d3<-[0..6], d4<-[d3+1..6],d5<-[d4+1..6],d6<-[0..6],
				d0/=d3, d0/=d4,d0/=d5,d0/=d6,
				d1/=d3, d1/=d4,d1/=d5,d1/=d6,
				d2/=d3, d2/=d4,d2/=d5,d2/=d6,
				d3/=d6, d4/=d6,d5/=d6]

--give an index for each deal
ideals = zip [0..139] deals

rus:: EpistM
rus = (Pmod [0..139] val acc [0])
	where
	val=[(w,[P d0, P d1, P d2, Q d3, Q d4, Q d5, R d6])|
			(w, (d0,d1,d2,d3,d4,d5,d6))<-ideals]
	acc=[(a,w,v)|(w,(d0,d1,d2,d3,d4,d5,d6))<-ideals,(v,(d0',d1',d2',d3',d4',d5',d6'))<-ideals,
			 d0==d0',d1==d1',d2==d2']++
	    [(b,w,v)|(w,(d0,d1,d2,d3,d4,d5,d6))<-ideals,(v,(d0',d1',d2',d3',d4',d5',d6'))<-ideals,
			 d3==d3',d4==d4',d5==d5']++
	    [(c,w,v)|(w,(d0,d1,d2,d3,d4,d5,d6))<-ideals,(v,(d0',d1',d2',d3',d4',d5',d6'))<-ideals,
				 d6==d6']

--The action model for: Anne says "My hand is one of 012,034,056,135,246"
a_announce =public( K a (Disj[
			Conj[Prop (P 0), Prop (P 1), Prop (P 2)],
			Conj[Prop (P 0), Prop (P 3), Prop (P 4)],
			Conj[Prop (P 0), Prop (P 5), Prop (P 6)],
			Conj[Prop (P 1), Prop (P 3), Prop (P 5)],
			Conj[Prop (P 2), Prop (P 4), Prop (P 6)]]))
										
--The action model for: Bill says "Cath holds card 6"
b_announce= public (K b (Prop (R 6)))


-- Formulas to present agents' knowledge.
-- Anne knows Bill's cards

a_knows_bs = Conj[Disj[K a (Prop (Q i)), K a (Neg(Prop (Q i)))]| i<-[0..6]]

-- Bill knows Anne's cards
b_knows_as = Conj[Disj[K b (Prop (P i)), K b (Neg(Prop (P i)))]| i<-[0..6]]

-- Cath is ignorant. 
c_ignorant = Conj[Conj[Neg (K c (Prop (P i))), Neg (K c (Prop (Q i)))]| i<-[0..6]]

-- Checking for knowledge during the communication:
--Step 1
-- After Anne announces five hands, Bill knows Anne's card. And this is commonly known by a,b.
check1 = isTrue ( upd rus a_announce ) b_knows_as
check2 = isTrue ( upd rus a_announce ) (CK [a,b] b_knows_as)
-- And Bill knows Cath's card. (This is entailed by the fact that Bill knows Anne's cards.)
check3 = isTrue ( upd rus a_announce ) (K b (Prop (R 6)))
-- Cath remains ignorant of anne's and Bill's cards, and this is common knowledge.
check4 = isTrue ( upd rus a_announce ) (CK [a,b,c] c_ignorant)

--Step 2
-- After Bill announces Cath's card, Anne knows Bill's cards, with Cath remains ignorant.
check5 = isTrue ( upd ( upd rus a_announce ) b_announce) (CK [a,b] a_knows_bs)
check6 = isTrue ( upd ( upd rus a_announce ) b_announce) (CK [a,b] b_knows_as)

check7 = isTrue ( upd ( upd rus a_announce ) b_announce) (CK [a,b,c] c_ignorant)