module LAI11 where 

import List
import Char
import LAI9
import LAI10
type State = Integer

sameVal :: (Eq a,Eq b) => [(a,b)] -> a -> a -> Bool
sameVal val w1 w2 = apply val w1 == apply val w2

rel2part :: (Eq a) => 
             [a] -> (a -> a -> Bool) -> [[a]]
rel2part [] r = []
rel2part (x:xs) r = xblock : rel2part rest r
  where 
  (xblock,rest) = (x:filter (r x) xs, 
                   filter (not . (r x)) xs)

initPartition :: Eq a => EpistM a -> [[a]]
initPartition (Mo states agents val rel actual) = 
  rel2part states (\ x y -> sameVal val x y) 

bl :: Eq a => [[a]] -> a -> [a]
bl part x = head (filter (elem x) part)

accBlocks :: Eq a => 
           EpistM a -> [[a]] -> a -> Agent -> [[a]]
accBlocks m@(Mo _ _ _ rel _) part s ag = 
    nub [ bl part y | (ag',x,y) <- rel, 
                       ag' == ag, x == s ]

sameAB :: Eq a => 
          EpistM a -> [[a]] -> a -> a -> Bool
sameAB m@(Mo states ags val rel actual) part s t = 
    and [ accBlocks m part s ag 
          == accBlocks m part t  ag | ag <- ags ]

refineStep :: Eq a => EpistM a -> [[a]] -> [[a]]
refineStep m p = refineP m p p 
  where 
  refineP :: Eq a => 
             EpistM a -> [[a]] -> [[a]] -> [[a]]
  refineP m part [] = []
  refineP m part (bl:blocks) = 
     newblocks ++ (refineP m part blocks) 
       where 
         newblocks = 
          rel2part bl (\ x y -> sameAB m part x y) 

refine :: Eq a => EpistM a -> [[a]] -> [[a]]
refine m = lfp (refineStep m)

minimalModel :: (Eq a, Ord a) => 
                 EpistM a -> EpistM [a] 
minimalModel m@(Mo states agents val rel actual) = 
  (Mo states' agents val' rel' actual') 
     where
     states'   = refine m (initPartition m)
     f         = bl states'
     val'      = (nub . sort)
        (map (\ (x,y)   -> (f x, y))      val)
     rel'      = (nub . sort)
        (map (\ (x,y,z) -> (x, f y, f z)) rel)
     actual'   = map f actual

bisim ::  (Eq a, Ord a) => 
           EpistM a -> EpistM State
bisim = convert . minimalModel

lai0 :: EpistM State
lai0 = Mo
        [0..7]
        [a,b,c]
        (zip [0..] 
         ((powerList [P 1, P 2]) 
           ++ (powerList [P 1, P 2])))
        [(ag,x,x) | ag <- [a,b,c], x <- [0..7] ]
        [2]

lai1 :: EpistM State
lai1 = let worlds = [0..10] in 
       Mo
        worlds 
        [a,b,c]
        (zip worlds (repeat [P 0]))
        [(ag,x,y) | ag <- [a,b,c], 
                    x  <- worlds, y <- worlds ]
        [10]

lai2 :: EpistM State
lai2 = let worlds = [0..10] in 
       Mo
        worlds 
        [a,b,c]
        ((0,[Q 0]): (zip [1..10] (repeat [P 0])))
        [(ag,x,y) | ag <- [a,b,c], 
                    x  <- worlds, y <- worlds ]
        [10]