CTL.hs

Plain text version of CTL.hs

CTL formulas

module CTL where

infixr 3 &
infixr 2 `Or`
infixr 1 ==>

A type for formulas in Computation Tree Logic 

data CTL a
    = Atom a
    | Not (CTL a)
    | Or (CTL a) (CTL a)
    | EX (CTL a)
    | EF (CTL a)
    | EG (CTL a)
    | EU (CTL a) (CTL a)
    deriving (Eq,Ord,Show)

Some derived operators 

p & q = Not (Not p `Or` Not q)
p ==> q = Not p `Or` q

ag = Not . EF . Not 
af = Not . EG . Not
ax = Not . EX . Not
-- could add more ...