2162N/A{- |

2362N/AModule : $EmptyHeader$

2162N/ADescription : <optional short description entry>

2162N/ACopyright : (c) <Authors or Affiliations>

2162N/ALicense : GPLv2 or higher

2162N/A

2162N/AMaintainer : <email>

2162N/AStability : unstable | experimental | provisional | stable | frozen

2162N/APortability : portable | non-portable (<reason>)

2162N/A

2162N/A<optional description>

2162N/A-}

2162N/A{-# OPTIONS -fglasgow-exts #-}

2162N/A

2162N/Amodule ModalCasl where

2162N/A

2162N/Aimport Control.Monad (liftM, liftM2)

2162N/Aimport Text.ParserCombinators.Parsec hiding (State)

2362N/A

2362N/A

2362N/A{------------------------------------------------------------------------------}

2162N/A{- -}

2162N/A{- Formulas of Modal CASL -}

2162N/A{- -}

2162N/A{------------------------------------------------------------------------------}

2162N/A

2162N/A

2162N/Adata StateFormula a = Var a

2162N/A -- Boolean Operators

2162N/A | Snot (StateFormula a)

2162N/A | Sand (StateFormula a) (StateFormula a)

2162N/A | Sor (StateFormula a) (StateFormula a)

2162N/A -- Path Quantifiers

2162N/A | E (PathFormula a)

2162N/A | A (PathFormula a)

2162N/A -- Future Modalities

2162N/A | Diamond (StateFormula a)

2162N/A | Box (StateFormula a)

2162N/A -- Past Modalities

2162N/A | DiamondPast (StateFormula a)

2162N/A | BoxPast (StateFormula a)

2162N/A -- Fixpoint Opertors

2162N/A | Mu a (StateFormula a)

2162N/A | Nu a (StateFormula a)

2162N/A

2162N/A

2162N/Adata PathFormula a = State (StateFormula a)

2162N/A -- Boolean Operators

2162N/A | Pnot (PathFormula a)

2162N/A | Pand (PathFormula a) (PathFormula a)

2162N/A | Por (PathFormula a) (PathFormula a)

2162N/A -- Future Temporal Operators

2162N/A | X (PathFormula a)

2162N/A | G (PathFormula a)

2162N/A | F (PathFormula a)

2162N/A | W (PathFormula a) (PathFormula a)

2162N/A | U (PathFormula a) (PathFormula a)

2162N/A | B (PathFormula a) (PathFormula a)

2162N/A | W' (PathFormula a) (PathFormula a)

2162N/A | U' (PathFormula a) (PathFormula a)

2162N/A | B' (PathFormula a) (PathFormula a)

-- Past Temporal Operators

| XPast (PathFormula a)

| GPast (PathFormula a)

| FPast (PathFormula a)

| WPast (PathFormula a) (PathFormula a)

| UPast (PathFormula a) (PathFormula a)

| BPast (PathFormula a) (PathFormula a)

| XPast' (PathFormula a)

| WPast' (PathFormula a) (PathFormula a)

| UPast' (PathFormula a) (PathFormula a)

| BPast' (PathFormula a) (PathFormula a)

instance (Show a) => Show (StateFormula a) where

show phi = showStateFormula phi True

instance (Show a) => Show (PathFormula a) where

show phi = showPathFormula phi True

showStateFormula (Var x) outer = show x

showStateFormula (Snot phi) outer = "not " ++ showStateFormula phi False

showStateFormula (Sand phi psi) True = showStateFormula phi False ++ " /\\ " ++ showStateFormula psi False

showStateFormula (Sor phi psi) True = showStateFormula phi False ++ " \\/ " ++ showStateFormula psi False

showStateFormula (E phi) outer = "E " ++ showPathFormula phi False

showStateFormula (A phi) outer = "A " ++ showPathFormula phi False

showStateFormula (Diamond phi) True = "<> " ++ showStateFormula phi False

showStateFormula (Box phi) True = "[] " ++ showStateFormula phi False

showStateFormula (DiamondPast phi) True = "<~> " ++ showStateFormula phi False

showStateFormula (BoxPast phi) True = "[~] " ++ showStateFormula phi False

showStateFormula (Mu x phi) True = "mu " ++ show x ++ " . " ++ showStateFormula phi False

showStateFormula (Nu x phi) True = "nu " ++ show x ++ " . " ++ showStateFormula phi False

showStateFormula phi False = "(" ++ showStateFormula phi True ++ ")"

showPathFormula (State phi) outer = showStateFormula phi outer

showPathFormula (Pnot phi) outer = "not " ++ showPathFormula phi False

showPathFormula (Pand phi psi) True = showPathFormula phi False ++ " /\\ " ++ showPathFormula psi False

showPathFormula (Por phi psi) True = showPathFormula phi False ++ " \\/ " ++ showPathFormula psi False

showPathFormula (X phi) outer = "X " ++ showPathFormula phi False

showPathFormula (G phi) outer = "G " ++ showPathFormula phi False

showPathFormula (F phi) outer = "F " ++ showPathFormula phi False

showPathFormula (W phi psi) True = showPathFormula phi False ++ " W " ++ showPathFormula psi False

showPathFormula (U phi psi) True = showPathFormula phi False ++ " U " ++ showPathFormula psi False

showPathFormula (B phi psi) True = showPathFormula phi False ++ " B " ++ showPathFormula psi False

showPathFormula (W' phi psi) True = showPathFormula phi False ++ " W! " ++ showPathFormula psi False

showPathFormula (U' phi psi) True = showPathFormula phi False ++ " U! " ++ showPathFormula psi False

showPathFormula (B' phi psi) True = showPathFormula phi False ++ " B! " ++ showPathFormula psi False

showPathFormula (XPast phi) outer = "~X " ++ showPathFormula phi False

showPathFormula (GPast phi) outer = "~G " ++ showPathFormula phi False

showPathFormula (FPast phi) outer = "~F " ++ showPathFormula phi False

showPathFormula (WPast phi psi) True = showPathFormula phi False ++ " ~W " ++ showPathFormula psi False

showPathFormula (UPast phi psi) True = showPathFormula phi False ++ " ~U " ++ showPathFormula psi False

showPathFormula (BPast phi psi) True = showPathFormula phi False ++ " ~B " ++ showPathFormula psi False

showPathFormula (XPast' phi) outer = "~X! " ++ showPathFormula phi False

showPathFormula (WPast' phi psi) True = showPathFormula phi False ++ " ~W! " ++ showPathFormula psi False

showPathFormula (UPast' phi psi) True = showPathFormula phi False ++ " ~U! " ++ showPathFormula psi False

showPathFormula (BPast' phi psi) True = showPathFormula phi False ++ " ~B! " ++ showPathFormula psi False

showPathFormula phi False = "(" ++ showPathFormula phi True ++ ")"

{------------------------------------------------------------------------------}

parser :: Parser a -> Parser (StateFormula a)

parser var = between spaces eof stateImpl where

stateImpl = chainl1 stateOr (do string "->"

spaces

return (Sor . Snot))

stateOr = chainl1 stateAnd (do string "\\/"

spaces

return Sor)

stateAnd = chainl1 state (do string "/\\"

spaces

return Sand)

state = (do char '('

spaces

x <- stateImpl

char ')'

spaces

return x)

<|> (do string "not"

spaces

liftM Snot state)

<|> (do string "E"

spaces

liftM E pathImpl)

<|> (do string "A"

spaces

liftM A pathImpl)

<|> (do x <- string "<"

y <- option "" (string "~")

z <- string ">"

spaces

case concat [x, y, z] of

"<>" -> liftM Diamond state

"<~>" -> liftM DiamondPast state)

<|> (do x <- string "["

y <- option "" (string "~")

z <- string "]"

spaces

case concat [x, y, z] of

"[]" -> liftM Box state

"[~]" -> liftM BoxPast state)

<|> (do string "mu"

space

spaces

x <- var

spaces

char '.'

spaces

liftM (Mu x) stateImpl)

<|> (do string "nu"

space

spaces

x <- var

spaces

char '.'

spaces

liftM (Nu x) stateImpl)

<|> (do x <- var

spaces

return (Var x))

pathImpl = chainl1 pathOr (do string "->"

spaces

return (Por . Pnot))

pathOr = chainl1 pathAnd (do string "\\/"

spaces

return Por)

pathAnd = chainl1 pathBinary (do string "/\\"

spaces

return Pand)

pathBinary = chainl1 pathUnary $ (do x <- option "" (string "~")

y <- (string "W" <|> string "U" <|> string "B")

z <- option "" (string "!")

spaces

case concat [x, y, z] of

"W" -> return W

"U" -> return U

"B" -> return B

"W!" -> return W'

"U!" -> return U'

"B!" -> return B'

"~W" -> return WPast

"~U" -> return UPast

"~B" -> return BPast

"~W!" -> return WPast'

"~U!" -> return UPast'

"~B!" -> return BPast')

pathUnary = (do char '('

spaces

x <- pathImpl

char ')'

spaces

return x)

<|> (do string "not"

spaces

liftM Pnot pathUnary)

<|> (do x <- option "" (string "~")

y <- (string "X" <|> string "G" <|> string "F")

z <- if concat [x, y] == "~X" then option "" (string "!")

else return ""

spaces

case concat [x, y, z] of

"X" -> liftM X pathUnary

"G" -> liftM G pathUnary

"F" -> liftM F pathUnary

"~X" -> liftM XPast pathUnary

"~G" -> liftM GPast pathUnary

"~F" -> liftM FPast pathUnary

"~X!" -> liftM XPast' pathUnary)

<|> liftM State state

{------------------------------------------------------------------------------}