{-+
CTL model checking, keeping it as simple as possible
----------------------------------------------------
-}
module MC where
import Ix
import Data.Set -- a library data type for sets
import CTL
import Model
{-+
The model checking function #mc# takes a model and a CTL formula and returns
the set of states in which the formula is true.
-}
--mc :: ... => Model a s -> CTL a -> Set s
mc m p =
  case p of
    Atom a -> fromList [s|s<-enumAll, atom m a s]
    Not p -> complement (mc m p)
    Or p q -> mc m p `union` mc m q
    EX p -> img_prev m $ mc m p
    EF p -> lfp (\ s -> s0 `union` img_prev m s)
         where s0 = mc m p
    EG p -> gfp (\ s -> s0 `intersection` img_prev m s)
         where s0 = mc m p
    EU p q -> lfp (\ s -> qs `union` (ps `intersection` img_prev m s))
         where
           ps = mc m p
           qs = mc m q

{-+ Set complement -}
--complement :: ... => Set s -> Set s -> Set s
complement s = difference universe s

universe :: (Bounded s,Ix s) => Set s
universe = fromList enumAll

{-+
Compute the backward image of a set of states, e.g. the preceeding states
according to the state transition relation.
(This function is called Image<sup>-1</sup>(S,R) in the slides.)
-}
-- img_prev :: ... => Model a s -> Set s -> Set s
img_prev m = fromList . concatMap (prev m) . toList

{-+
Fixed point iteration: #lfp# (least fixed point) starts from the empty set.
 #gfp# (greatest fixed point) starts from the universe. The function #f# should
be monotonic.
-}
-- lfp, gfl :: (Set s->Set s)->Set s
lfp f = fix f empty
gfp f = fix f universe

fix :: (Eq x) => (x -> x) -> x -> x
fix f x = if x'==x then x else fix f x'
  where x' = f x