CTL.hs

module Main where

import Data.List

data CTL a = AG (CTL a) | AF (CTL a) | EG (CTL a) | EF (CTL a) | EU (CTL a) (CTL a) | AU (CTL a) (CTL a) | EX (CTL a) | AX (CTL a) | And (CTL a) (CTL a) | Or (CTL a) (CTL a) | Not (CTL a) | Atom a

data Kripke a = Kripke { t :: (Int -> [Int]), l :: (Int -> [a]) }

paths :: Kripke a -> Int -> [[Int]]
paths m s = paths' [] m s

paths' :: [Int] -> Kripke a -> Int -> [[Int]]
paths' seen m s | s `elem` seen = [[]]
                | otherwise     = let ps = intercalate [] $ map (paths' (s : seen) m) (t m s) in nub $ map (s : ) ps

until :: (Eq a) => Kripke a -> [Int] -> CTL a -> CTL a -> Bool
until _ [] _ _ = False
until m (p:ps) φ ψ = (check m p ψ) || ((check m p φ) && Main.until m ps φ ψ)

check :: (Eq a) => Kripke a -> Int -> CTL a -> Bool
check m s (Atom a) = a `elem` l m s
check m s (Not φ) = not $ check m s φ
check m s (And φ ψ) = (check m s φ) && (check m s ψ)
check m s (Or φ ψ) = (check m s φ) || (check m s ψ)
check m s (AX φ) = all (\x -> check m x φ) (t m s)
check m s (EX φ) = any (\x -> check m x φ) (t m s)
check m s (AG φ) = all (all (\x -> check m x φ)) (paths m s)
check m s (AF φ) = all (any (\x -> check m x φ)) (paths m s)
check m s (EG φ) = any (all (\x -> check m x φ)) (paths m s)
check m s (EF φ) = any (any (\x -> check m x φ)) (paths m s)
check m s (AU φ ψ) = all (\p -> Main.until m p φ ψ) (paths m s)
check m s (EU φ ψ) = any (\p -> Main.until m p φ ψ) (paths m s)