ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu{-# OPTIONS -fglasgow-exts #-}

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiumodule ModalCasl where

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiuimport Control.Monad (liftM, liftM2)

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiuimport Text.ParserCombinators.Parsec hiding (State)

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu{------------------------------------------------------------------------------}

c038fcf2030a6cfac7a261dee48a9eb29edb78eaFelix Gabriel Mance{- -}

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu{- Formulas of Modal CASL -}

15d62726781e67fe6458fbcf0a8c46832a7bb8daFelix Gabriel Mance{- -}

c038fcf2030a6cfac7a261dee48a9eb29edb78eaFelix Gabriel Mance{------------------------------------------------------------------------------}

c038fcf2030a6cfac7a261dee48a9eb29edb78eaFelix Gabriel Mance

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiudata StateFormula a = Var a

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu -- Boolean Operators

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu | Snot (StateFormula a)

ed1b8e97e72b2e3e92edaf2eb22a4b5373d705f1Felix Gabriel Mance | Sand (StateFormula a) (StateFormula a)

5180a08007989fd364622fc9bc01f82141643f7bFelix Gabriel Mance | Sor (StateFormula a) (StateFormula a)

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu -- Path Quantifiers

c038fcf2030a6cfac7a261dee48a9eb29edb78eaFelix Gabriel Mance | E (PathFormula a)

c038fcf2030a6cfac7a261dee48a9eb29edb78eaFelix Gabriel Mance | A (PathFormula a)

8d246de26958f1e8c35714b260b9d85c933c060aFrancisc Nicolae Bungiu -- Future Modalities

8d246de26958f1e8c35714b260b9d85c933c060aFrancisc Nicolae Bungiu | Diamond (StateFormula a)

6995877e4e201fcf8bb936066da2d259aed7c008Felix Gabriel Mance | Box (StateFormula a)

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu -- Past Modalities

19e01e1a7e319063434bd86c8ecbc5f241ef9993Felix Gabriel Mance | DiamondPast (StateFormula a)

19e01e1a7e319063434bd86c8ecbc5f241ef9993Felix Gabriel Mance | BoxPast (StateFormula a)

19e01e1a7e319063434bd86c8ecbc5f241ef9993Felix Gabriel Mance -- Fixpoint Opertors

19e01e1a7e319063434bd86c8ecbc5f241ef9993Felix Gabriel Mance | Mu a (StateFormula a)

19e01e1a7e319063434bd86c8ecbc5f241ef9993Felix Gabriel Mance | Nu a (StateFormula a)

c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance

c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiudata PathFormula a = State (StateFormula a)

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu -- Boolean Operators

c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance | Pnot (PathFormula a)

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu | Pand (PathFormula a) (PathFormula a)

dda7065c0c0f383558d7d4e8072969c8c41a8ed7Francisc Nicolae Bungiu | Por (PathFormula a) (PathFormula a)

8e1b180fc839e96d7a4f1f63dfc563c75139c683Francisc Nicolae Bungiu -- Future Temporal Operators

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance | X (PathFormula a)

15d62726781e67fe6458fbcf0a8c46832a7bb8daFelix Gabriel Mance | G (PathFormula a)

15d62726781e67fe6458fbcf0a8c46832a7bb8daFelix Gabriel Mance | F (PathFormula a)

c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance | W (PathFormula a) (PathFormula a)

dda7065c0c0f383558d7d4e8072969c8c41a8ed7Francisc Nicolae Bungiu | U (PathFormula a) (PathFormula a)

15d62726781e67fe6458fbcf0a8c46832a7bb8daFelix Gabriel Mance | B (PathFormula a) (PathFormula a)

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance | W' (PathFormula a) (PathFormula a)

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance | U' (PathFormula a) (PathFormula a)

dda7065c0c0f383558d7d4e8072969c8c41a8ed7Francisc Nicolae Bungiu | B' (PathFormula a) (PathFormula a)

ed1b8e97e72b2e3e92edaf2eb22a4b5373d705f1Felix Gabriel Mance -- Past Temporal Operators

c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance | XPast (PathFormula a)

c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance | 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

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