module LabExerc3 where

import List
import LAI9
import LAI10
import LAI11

myModel1 :: EpistM State
myModel1 = Mo [0..6]
              [a,b]
              [(0,[]),(1,[]),(2,[]),(3,[P 0]),
               (4,[P 0]),(5,[]),(6,[P 0])]
              [(a,0,1),(a,1,1),(a,0,2),(a,2,5),(a,5,5),
               (b,1,3),(b,2,4),(b,5,6)]
              [0]

myModel2 :: EpistM State
myModel2 = Mo [0..7]
              [a,b]
              [(0,[]),(1,[]),(2,[]),(3,[]),
               (4,[]),(5,[]),(6,[]),(7,[])]
              [(a,0,1),(a,1,1),(a,0,2),(a,2,5),(a,5,5),
               (b,1,3),(b,2,4),(b,5,6),(b,0,7)]
              [0]

reachable :: Ord state => EpistM state -> [state]
reachable (Mo states agents val rel actual) = 
  (sort.nub) 
    (concat [ commonAlts rel agents states w | w <- actual ])

gsm :: Ord state => EpistM state -> EpistM state
gsm m@(Mo states agents val rel actual) = 
     Mo states' agents val' rel' actual
      where 
        states' = reachable m 
        val'    = [(x,y) | (x,y) <- val, elem x states' ]
        rel'    = [(a,x,y) | (a,x,y) <- rel, 
                              elem x states', elem y states']

gsm_example = 
 Mo [0..3]
    [a..c]
    [(0,[]),(1,[P 0]),(2,[Q 0]),(3,[P 0, Q 0])]
    ([ (a,x,x) | x <- [0..3] ] ++
     [ (b,x,x) | x <- [0..3] ] ++
     [ (c,x,x) | x <- [0..3] ])
    [1]

part2pairs :: [[a]] -> [(a,a)]
part2pairs blocks = [(x,y)| bl <- blocks, x <- bl, y <- bl ]

maxBisim :: Ord state => EpistM state -> Rel state
maxBisim m = part2pairs partition 
  where (Mo partition _ _ _ _) = minimalModel m