module LAI14 where 

import List
import Char
import LAI9
import LAI10
import LAI11
import LAI12
import LAI13

upd ::  (Eq state, Ord state) => 
       EpistM state -> FAM state 
                    -> EpistM State 
upd m a = bisim (up m a)

public :: Form -> FAM State
public form ags = 
 Am [0] ags [(0,form)] [(a,0,0)| a <- ags ] [0]

m0 = up s5example (public p)
m1 = upd s5example (public p)

groupM :: [Agent] -> Form -> FAM State
groupM gr form agents = 
  if sort gr == sort agents
    then public form agents
    else 
      (Am
       [0,1] 
        agents
       [(0,form),(1,Top)]
        ([ (a,0,0) | a <- agents ] 
         ++ [ (a,0,1) | a <- agents \\ gr ] 
         ++ [ (a,1,0) | a <- agents \\ gr ] 
         ++ [ (a,1,1) | a <- agents          ])
       [0])

e0 = initM [a,b,c] [P 0,Q 0]
m2 = up e0 (groupM [a,b] (Neg p))
m3 = upd e0 (groupM [a,b] (Neg p))

message :: Agent -> Form -> FAM State
message agent = groupM [agent] 

m4 = up e0 (message c (Disj [p,q]))
m5 = upd e0 (message c (Disj [p,q]))

test :: Form -> FAM State
test = groupM [] 

m6 = up e0 (test (Neg p))
m7 = upd e0 (test (Neg p))

negation :: Form -> Form
negation (Neg form) = form
negation form       = (Neg form)

info :: [Agent] -> Form -> FAM State
info ags form agents = 
   Am 
   [0,1]
   agents 
   [(0,form),(1,negation form)]
   ([ (a,0,0) | a <- agents ] 
     ++ [ (a,1,1) | a <- agents ] 
     ++ [ (a,0,1) | a <- others ] 
     ++ [ (a,1,0) | a <- others ])
   [0,1]
     where others = agents \\ ags 

m8 = up e0 (info [a,b] p)
m9 = upd e0 (info [a,b] p)

mo0 = initM [a,b,c,d] [P 1, P 2, P 3, P 4]

p1,p2,p3,p4 :: Form
p1 = Prop (P 1); p2 = Prop (P 2)
p3 = Prop (P 3); p4 = Prop (P 4)

capsInfo :: Form
capsInfo = 
  Disj [Conj [f, g, Neg h, Neg j] | 
              f <- [p1, p2, p3, p4], 
              g <- [p1, p2, p3, p4] \\ [f],
              h <- [p1, p2, p3, p4] \\ [f,g],
              j <- [p1, p2, p3, p4] \\ [f,g,h], 
              f < g, h < j                     ]

mo1 = upd mo0 (public capsInfo)

awarenessFirstCap  = info [b,c] p1
awarenessSecondCap = info [c]   p2

mo2  = upd (upd mo1 awarenessFirstCap)
                    awarenessSecondCap 

bK =  Disj [K b p2, K b (Neg p2)]
cK =  Disj [K c p3, K c (Neg p3)]

mo3a = upd  mo2 (public cK) 
mo3b = upd  mo2 (public (Neg cK))

impl :: Form -> Form -> Form 
impl form1 form2 = Disj [Neg form1, form2]

equiv :: Form -> Form -> Form 
equiv form1 form2 = 
  Conj [form1 `impl` form2, form2 `impl` form1]

test1 = isTrue mo3a bK
test2 = isTrue mo3b bK
test3 = isTrue mo3a (K a (equiv p1 p2))
test4 = isTrue mo3b (K a (equiv p1 p2))

mo4a = upd mo3a (public bK)
mo4b = upd mo3b (public bK)