module TNP
where 
import DEMO
--Uses DEMO, Dynamic Epistemic MOdelling Tools, developed by Jan van Eijck
--This program implements the three-number-problem in DEMO
--There are three agents (A, B and C) who are assigned three numbers (x, y and z)
--Written by Chris Janssen, Maarten van Grootel, Selwin van Dijk


--Each pair in the set consists of three number between 0 and 10, one of which is the sum of the other two
pairs :: [(Int,Int,Int)]
pairs  = [(x,y,z)|  x<-[0..10], y<-[0..10], z<-[0..10], 
			 (x+y==z || x+z==y || y+z==x)]

--The number of the possible worlds (i.e. pairs)
numpairs =llength(pairs)

--returns the number of elements in the list
llength [] =0
llength (x:xs) = 1+ llength xs

--gives an index to the worlds.
ipairs = zip [0..numpairs-1] pairs

--The model
tnpm :: EpistM
tnpm = (Pmod [0..numpairs-1] val acc [0..numpairs-1])
  where
	val  = [(w,[P x, Q y, R z]) | (w,(x,y,z)) <- ipairs]
  	acc  = [(a,w,v)| (w,(x1,y1,z1)) <- ipairs,(v,(x2,y2,z2)) <- ipairs, y1==y2, z1==z2]++
		 [(b,w,v)| (w,(x1,y1,z1)) <- ipairs,(v,(x2,y2,z2)) <- ipairs, x1==x2, z1==z2]++
	 	 [(c,w,v)| (w,(x1,y1,z1)) <- ipairs,(v,(x2,y2,z2)) <- ipairs, x1==x2, y1==y2]

--Agent A says he does not know his number
aA = Conj [(Disj[Neg (Prop (P x)), Neg (K A ( Prop (P x))) ] )|x <- [0..10]]
annA = public (aA)
--Agent B says he does not know his number either
aB = Conj [(Disj[Neg (Prop (Q y)), Neg (K B ( Prop (Q y))) ] )|y <- [0..10]] 
annB = public (aB)

--Agent C says he does not know his number either
aC = Conj [(Disj[Neg (Prop (R z)), Neg (K C ( Prop (R z) )) ] )|z <- [0..10]] 
annC = public (aC)


--Show the possible solutions after all agents have made their announcements
solution = showM (upds tnpm [annA, annB, annC])

--Agent A says he now knows his number. 
--This announcement does not change any of the agents' knowledge
aA2 = Conj [(Disj[Neg (Prop (P x)), K a (Prop (P x)) ] )|x<-[0..10]] 
annA2 = public (aA2)
--gives same solution as first solution
solution2 = showM (upds tnpm [annA, annB, annC, annA2])