MC.hs

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 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

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^-1(S,R) in the slides.)

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 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

MC.hs

CTL model checking, keeping it as simple as possible