f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich{- |

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian MaederModule : $Header$

c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederCopyright : (c) Klaus Hartke, Uni Bremen 2008

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder

75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiMaintainer : Christian.Maeder@dfki.de

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : experimental

75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiPortability : portable

75a6279dbae159d018ef812185416cf6df386c10Till Mossakowski

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder-}

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maedermodule NuSmv (basicExpr, program) where

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederimport Control.Monad (liftM, liftM2)

980c2505814d75dc689de1412f4de30b4d96314fRazvan Pascanuimport Data.Char (toLower)

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maederimport Data.List (intersperse)

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maederimport Text.ParserCombinators.Parsec hiding (State, token)

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder(<<) :: (Monad m) => m a -> m b -> m a

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder(<<) a b = do x <- a

43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder b

a1c6679d00e15a949730ab640159e0adc5b0e3e7Christian Maeder return x

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski

fa388aea9cef5f9734fec346159899a74432ce26Christian Maeder

eb9a06d3b5c6354c0573f0cb93d5a5d558f51136Heng Jiang{------------------------------------------------------------------------------}

fa388aea9cef5f9734fec346159899a74432ce26Christian Maeder

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder

59fddbdd745a05adeaf655b617ab8da947903832Christian MaedercheckWith :: (Show a) => GenParser tok st a -> (a -> Bool) -> GenParser tok st a

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskicheckWith p f = do x <- p

cfaa17b0d2ed0a663f0a4f18b23f98ab876c2f40Christian Maeder if f x then return x

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder else unexpected (show x)

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederreserved :: [String] -> CharParser st String -> CharParser st String

c0c2380bced8159ff0297ece14eba948bd236471Christian Maederreserved l p = try $ checkWith p (`notElem` l)

da333ffa6336cf59a4071fcddad358c5eafd3e61Sonja Gröning

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder

5b50a0fb9834540caf04471389df975fbd356ca3Razvan Pascanu{------------------------------------------------------------------------------}

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu

16281c97e3e04f9f88c806d7da79feb106dbee2aTill Mossakowski

980c2505814d75dc689de1412f4de30b4d96314fRazvan Pascanuws :: Parser ()

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederws = many (oneOf " \t\r\n") >> return ()

74885352ea11b26253d453af28dc904dadc4d530Christian Maeder

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanutoken :: String -> Parser ()

8955ea64c61a6e8b96b7696021863afd1a75f6daRazvan Pascanutoken x = string x >> ws

16281c97e3e04f9f88c806d7da79feb106dbee2aTill Mossakowski

8955ea64c61a6e8b96b7696021863afd1a75f6daRazvan Pascanu

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanukeyword :: String -> Parser ()

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanukeyword x = try (string x >> notFollowedBy alphaNum) >> ws

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu

ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühl

ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühlidentifier :: Parser String

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maederidentifier = liftM2 (:) idFirstChar (many idConsecutiveChar) <?> "identifier"

6e1ecd948a1844206ad678907eb97c7296b805efChristian Maeder where

9726e6290bc036adbad9fa7751fc05c10e79d647Christian Maeder idFirstChar = letter

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu <|> char '_'

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu

08635fe65017b90fe76df12e064d840619f4ec4eChristian Maeder idConsecutiveChar = idFirstChar

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder <|> digit

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu <|> char '$'

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder <|> char '#'

08635fe65017b90fe76df12e064d840619f4ec4eChristian Maeder <|> char '\\'

fa388aea9cef5f9734fec346159899a74432ce26Christian Maeder <|> char '-'

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanuinteger :: Parser Int

fa388aea9cef5f9734fec346159899a74432ce26Christian Maederinteger = liftM read (liftM2 (++) (option "" (string "-")) (many1 digit)) <?> "integer number"

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu{------------------------------------------------------------------------------}

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanukeywords :: [String]

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanukeywords = [ "MODULE", "DEFINE", "CONSTANTS", "VAR", "IVAR", "INIT", "TRANS",

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu "INVAR", "SPEC", "CTLSPEC", "LTLSPEC", "PSLSPEC", "COMPUTE",

48c6e734f777f9fe756f171077560066937a3275Klaus Luettich "INVARSPEC", "FAIRNESS", "JUSTICE", "COMPASSION", "ISA", "ASSIGN",

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu "CONSTRAINT", "SIMPWFF", "CTLWFF", "LTLWFF", "PSLWFF", "COMPWFF",

48c6e734f777f9fe756f171077560066937a3275Klaus Luettich "IN", "MIN", "MAX", "process", "array", "of", "boolean",

16281c97e3e04f9f88c806d7da79feb106dbee2aTill Mossakowski "integer", "real", "word", "word1", "bool", "EX", "AX", "EF",

fe5d536284c81622d823a99a92db6e94fa8583d2Razvan Pascanu "AF", "EG", "AG", "E", "F", "O", "G", "H", "X", "Y", "Z", "A",

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu "U", "S", "V", "T", "BU", "EBF", "ABF", "EBG", "ABG", "case",

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu "esac", "mod", "next", "init", "union", "in", "xor", "xnor",

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu "self", "TRUE", "FALSE" ]

5b50a0fb9834540caf04471389df975fbd356ca3Razvan Pascanu

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu{------------------------------------------------------------------------------}

5b50a0fb9834540caf04471389df975fbd356ca3Razvan Pascanu{- -}

f1dec6898638ba1131a9fadbc4d1544c93dfabb0Klaus Luettich{- Basic Expressions of NuSMV -}

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu{- -}

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu{------------------------------------------------------------------------------}

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder

data Expr = Bool Bool -- Boolean Constant

| Int Int -- Integer Constant

| Var [String] -- Symbol Constant,

-- Variable Identifier,

-- or Define Identifier

| Word Int Int -- Word Constant

| Range Int Int -- Range Constant

| Not Expr -- Logical/Bitwise NOT

| And Expr Expr -- Logical/Bitwise AND

| Or Expr Expr -- Logical/Bitwise OR

| Xor Expr Expr -- Logical/Bitwise XOR

| Xnor Expr Expr -- Logical/Bitwise NOT XOR

| Impl Expr Expr -- Logical/Bitwise Implication

| Equiv Expr Expr -- Logical/Bitwise Equivalence

| Eq Expr Expr -- Equality

| Neq Expr Expr -- Inequality

| Lt Expr Expr -- Less Than

| Gt Expr Expr -- Greater Than

| Leq Expr Expr -- Less Than Or Equal

| Geq Expr Expr -- Greater Than Or Equal

| Neg Expr -- Integer Unary Minus

| Add Expr Expr -- Integer Addition

| Sub Expr Expr -- Integer Subtraction

| Mult Expr Expr -- Integer Multiplication

| Div Expr Expr -- Integer Division

| Mod Expr Expr -- Integer Remainder

| Bsr Expr Expr -- Bit Shift Right

| Bsl Expr Expr -- Bit Shift Left

| Concat Expr Expr -- Word Concatenation

| Select Expr (Int, Int) -- Word Bits Selection

| ToWord Expr -- Boolean to Word[1] convertion

| ToBool Expr -- Word[1] to Boolean convertion

| Union Expr Expr -- Union of Set Expressions

| Set [Expr] -- Set Expression

| In Expr Expr -- Inclusion Expression

| Case [(Expr, Expr)] -- Case Expression

| Next Expr -- Next Expression

instance Show Expr where

show expr = showBasicExpr expr True

showBasicExpr (Bool True) outer = "TRUE"

showBasicExpr (Bool False) outer = "FALSE"

showBasicExpr (Int value) outer = show value

showBasicExpr (Var ids) outer = concat (intersperse "." ids)

showBasicExpr (Word width value) outer = concat [ "0d", show width, "_", show value ]

showBasicExpr (Range from to) outer = concat [ show from, "..", show to ]

showBasicExpr (Not expr) outer = concat [ "!", showBasicExpr expr False ]

showBasicExpr (And exprA exprB) True = concat [ showBasicExpr exprA False, " & ", showBasicExpr exprB False ]

showBasicExpr (Or exprA exprB) True = concat [ showBasicExpr exprA False, " | ", showBasicExpr exprB False ]

showBasicExpr (Xor exprA exprB) True = concat [ showBasicExpr exprA False, " xor ", showBasicExpr exprB False ]

showBasicExpr (Xnor exprA exprB) True = concat [ showBasicExpr exprA False, " xnor ", showBasicExpr exprB False ]

showBasicExpr (Impl exprA exprB) True = concat [ showBasicExpr exprA False, " -> ", showBasicExpr exprB False ]

showBasicExpr (Equiv exprA exprB) True = concat [ showBasicExpr exprA False, " <-> ", showBasicExpr exprB False ]

showBasicExpr (Eq exprA exprB) True = concat [ showBasicExpr exprA False, " = ", showBasicExpr exprB False ]

showBasicExpr (Neq exprA exprB) True = concat [ showBasicExpr exprA False, " != ", showBasicExpr exprB False ]

showBasicExpr (Lt exprA exprB) True = concat [ showBasicExpr exprA False, " < ", showBasicExpr exprB False ]

showBasicExpr (Gt exprA exprB) True = concat [ showBasicExpr exprA False, " > ", showBasicExpr exprB False ]

showBasicExpr (Leq exprA exprB) True = concat [ showBasicExpr exprA False, " <= ", showBasicExpr exprB False ]

showBasicExpr (Geq exprA exprB) True = concat [ showBasicExpr exprA False, " >= ", showBasicExpr exprB False ]

showBasicExpr (Neg expr) outer = concat [ "-", showBasicExpr expr False ]

showBasicExpr (Add exprA exprB) True = concat [ showBasicExpr exprA False, " + ", showBasicExpr exprB False ]

showBasicExpr (Sub exprA exprB) True = concat [ showBasicExpr exprA False, " - ", showBasicExpr exprB False ]

showBasicExpr (Mult exprA exprB) True = concat [ showBasicExpr exprA False, " * ", showBasicExpr exprB False ]

showBasicExpr (Div exprA exprB) True = concat [ showBasicExpr exprA False, " / ", showBasicExpr exprB False ]

showBasicExpr (Mod exprA exprB) True = concat [ showBasicExpr exprA False, " mod ", showBasicExpr exprB False ]

showBasicExpr (Bsr exprA exprB) True = concat [ showBasicExpr exprA False, " >> ", showBasicExpr exprB False ]

showBasicExpr (Bsl exprA exprB) True = concat [ showBasicExpr exprA False, " << ", showBasicExpr exprB False ]

showBasicExpr (Concat exprA exprB) True = concat [ showBasicExpr exprA False, " :: ", showBasicExpr exprB False ]

showBasicExpr (Select expr (from, to)) outer = concat [ showBasicExpr expr False, "[", show from, ", ", show to, "]" ]

showBasicExpr (ToWord expr) outer = concat [ "word1(", showBasicExpr expr True, ")" ]

showBasicExpr (ToBool expr) outer = concat [ "bool(", showBasicExpr expr True, ")" ]

showBasicExpr (Union exprA exprB) True = concat [ showBasicExpr exprA False, " union ", showBasicExpr exprB False ]

showBasicExpr (Set exprs) outer = concat [ "{", concat (intersperse ", " (map (\expr-> showBasicExpr expr False) exprs)), "}" ]

showBasicExpr (In exprA exprB) True = concat [ showBasicExpr exprA False, " in ", showBasicExpr exprB False ]

showBasicExpr (Case cases) outer = concat [ "case ", concat (intersperse "\n" (map (\(exprA, exprB)-> concat [showBasicExpr exprA False, " : ", showBasicExpr exprB False, ";"]) cases)), " esac" ]

showBasicExpr (Next expr) outer = concat [ "next(", showBasicExpr expr True, ")" ]

showBasicExpr expr False = concat [ "(", showBasicExpr expr True, ")" ]

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

{- -}

{- Parser for Basic Expressions -}

{- -}

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

basicExpr :: Parser Expr

basicExpr = implExpr

where

implExpr = chainr1 equivExpr (token "->" >> return Impl)

equivExpr = chainl1 orExpr (token "<->" >> return Equiv)

orExpr = chainl1 andExpr ((token "|" >> return Or) <|>

(keyword "xor" >> return Xor) <|>

(keyword "xnor" >> return Xnor))

andExpr = chainl1 eqExpr (token "&" >> return And)

eqExpr = chainl1 inExpr ((token "=" >> return Eq) <|>

(token "!=" >> return Neq) <|>

(try (token "<=" >> return Leq)) <|>

(try (token ">=" >> return Geq)) <|>

(token "<" >> return Lt) <|>

(token ">" >> return Gt))

inExpr = chainl1 unionExpr (keyword "in" >> return In)

unionExpr = chainl1 shiftExpr (keyword "union" >> return Union)

shiftExpr = chainl1 modExpr ((try (token ">>" >> return Bsr)) <|>

(try (token "<<" >> return Bsl)))

modExpr = chainl1 addSubExpr (keyword "mod" >> return Mod)

addSubExpr = chainl1 multDivExpr ((token "+" >> return Add) <|>

(token "-" >> return Sub))

multDivExpr = chainl1 negateExpr ((token "*" >> return Mult) <|>

(token "/" >> return Div))

negateExpr = (token "-" >> (liftM Neg negateExpr)) <|>

concatExpr

concatExpr = chainl1 selectExpr (try (token "::") >> return Concat)

selectExpr = do expr <- notExpr

option expr (do token "[" <?> "selector"

bits <- sepBy1 bit (token "[")

return (foldl Select expr bits))

notExpr = (token "!" >> (liftM Not notExpr)) <|>

primaryExpr

primaryExpr = parenthesizedExpr <|>

(liftM Set (between (token "{") (token "}")

(sepBy1 implExpr (char ',' >> ws)))) <|>

(do expr <- constantExpr << ws

case expr of

Var ["word1"] -> liftM ToWord parenthesizedExpr

Var ["bool"] -> liftM ToBool parenthesizedExpr

Var ["case"] -> caseExpr

Var ["next"] -> liftM Next parenthesizedExpr

_ -> return expr)

parenthesizedExpr = between (token "(") (token ")") implExpr

caseExpr = liftM Case (manyTill (do lhs <- implExpr

token ":"

rhs <- implExpr

token ";"

return (lhs, rhs)) (token "esac"))

bit = do value1 <- integer << ws

token ":"

value2 <- integer << ws

token "]"

return (value1, value2)

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

{- -}

{- Parser for Constant Expressions -}

{- -}

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

constantExpr :: Parser Expr

constantExpr = (constantA <?> "integer constant") <|>

(constantB <?> "boolean constant") <|>

(constantE <?> "symbolic constant") <|>

(constantF <?> "variable identifier") <|>

(constantG <?> "define identifier")

where

constantA = do char '-'

value <- many1 digit

range (negate (read value))

constantB = do char '0'

constantC <|> constantD

constantC = do base <- oneOf "bBoOdDhH"

width <- many digit

char '_'

value <- case toLower base of

'b' -> many1 (oneOf "01_")

'o' -> many1 (octDigit <|> char '_')

'd' -> many1 (digit <|> char '_')

'h' -> many1 (hexDigit <|> char '_')

let width' = case width of

"" -> case toLower base of

'b' -> 1 * length value

'o' -> 3 * length value

'd' -> error "Cannot calculate width of decimal integers"

'h' -> 4 * length value

_ -> read width

let value' = case toLower base of

'b' -> error "Cannot decode binary integer"

'o' -> read ("0o" ++ (filter (/= '_') value))

'd' -> read (filter (/= '_') value)

'h' -> read ("0x" ++ (filter (/= '_') value))

return (Word width' value')

constantD = do value <- many digit

case value of

"" -> return (Bool False)

_ -> range (read ('0':value))

constantE = do char '1'

value <- many digit

case value of

"" -> return (Bool True)

_ -> range (read ('1':value))

constantF = do value <- many1 digit

range (read value)

constantG = do value <- sepBy1 identifier (char '.')

case value of

["FALSE"] -> return (Bool False)

["TRUE"] -> return (Bool True)

_ -> return (Var value)

range x = (string ".." >> liftM (Range x) integer)

<|> (return (Int x))

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

{- -}

{- Complex Identifiers -}

{- -}

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

data ComplexId = Id String

| ComplexId ComplexId String

| IndexedId ComplexId Int

| Self

instance Show ComplexId where

show (Id s) = s

show (ComplexId id s) = (show id) ++ "." ++ s

show (IndexedId id i) = (show id) ++ "[" ++ (show i) ++ "]"

show (Self) = "self"

complexId :: Parser ComplexId

complexId = do id <- reserved keywords identifier << ws

return (Id id) --TODO: really complex identifiers

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

{- -}

{- NuSMV Programs -}

{- -}

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

data Program = Program [Module]

data Module = Module String [String] [Element]

data Element = VarDecl [(String, Type)]

| IVarDecl [(String, Type)]

| DefineDecl [(String, Expr)]

| ConstDecl [String]

| Init Expr

| Invar Expr

| Trans Expr

| Assign [(AssignLhs, AssignRhs)]

| Fairness Expr

| Justice Expr

| Compassion Expr Expr

data Type = BoolType

| WordType Int

| EnumType [EnumValue]

| RangeType Int Int

| ArrayType Int Int Type

data EnumValue = Symbol String

| Number Int

data AssignLhs = CurrentValue ComplexId

| InitialValue ComplexId

| NextValue ComplexId

type AssignRhs = Expr

instance Show Program where

show program = showProgram program

showProgram (Program mods) = concatMap showModule mods

instance Show Module where

show mod = showModule mod

showModule (Module name params elements) = concat [ "MODULE ", name, showParams params, "\n", concatMap showElement elements ]

where

showParams [] = ""

showParams params = concat [ "(", concat (intersperse ", " params), ")" ]

instance Show Element where

show element = showElement element

showElement (VarDecl vars) = concat [ "VAR", concatMap showVar vars, "\n" ]

where

showVar (id, ty) = concat [ " ", id, " : ", showType ty, ";" ]

showElement (IVarDecl vars) = concat [ "IVAR", concatMap showVar vars, "\n" ]

where

showVar (id, ty) = concat [ " ", id, " : ", showType ty, ";" ]

showElement (DefineDecl defs) = concat [ "DEFINE", concatMap showDefine defs, "\n" ]

where

showDefine (id, expr) = concat [ " ", id, " := ", showBasicExpr expr True, ";" ]

showElement (ConstDecl consts) = concat [ "CONSTANTS ", concat (intersperse ", " consts), ";\n" ]

showElement (Init expr) = concat [ "INIT ", showBasicExpr expr True, ";\n" ]

showElement (Invar expr) = concat [ "INVAR ", showBasicExpr expr True, ";\n" ]

showElement (Trans expr) = concat [ "TRANS ", showBasicExpr expr True, ";\n" ]

showElement (Assign assigns) = concat [ "ASSIGN", concatMap showAssign assigns, "\n" ]

where

showAssign (lhs, rhs) = concat [ " ", show lhs, " := ", show rhs, ";" ]

showElement (Fairness expr) = concat [ "FAIRNESS ", showBasicExpr expr True, ";\n" ]

showElement (Justice expr) = concat [ "JUSTICE ", showBasicExpr expr True, ";\n" ]

showElement (Compassion exprA exprB) = concat [ "COMPASSION(", showBasicExpr exprA True, ", ", showBasicExpr exprB True, ");\n" ]

instance Show Type where

show ty = showType ty

showType BoolType = "boolean"

showType (WordType width) = concat [ "word[", show width, "]" ]

showType (EnumType values) = concat [ "{", concat (intersperse "," (map showValue values)), " }" ]

where

showValue (Symbol symbol) = concat [ " ", symbol ]

showValue (Number number) = concat [ " ", show number ]

showType (RangeType from to) = concat [ show from, "..", show to ]

showType (ArrayType from to ty) = concat [ "array ", show from, "..", show to, " of ", showType ty ]

instance Show AssignLhs where

show (CurrentValue id) = show id

show (InitialValue id) = "init(" ++ (show id) ++ ")"

show (NextValue id) = "next(" ++ (show id) ++ ")"

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

{- -}

{- Parser for Programs -}

{- -}

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

program :: Parser Program

program = liftM Program (many modul)

modul :: Parser Module

modul = do keyword "MODULE"

name <- reserved keywords identifier << ws

params <- option [] (between (token "(") (token ")") parameters)

elements <- many element

return (Module name params elements)

where

parameters = sepBy1 (reserved keywords identifier << ws) (token ",")

element :: Parser Element

element = varDecl

<|> ivarDecl

<|> constDecl

<|> defineDecl

<|> initConstraint

<|> invarConstraint

<|> transConstraint

<|> assign

<|> fairness

<|> justice

<|> compassion

where

varDecl = do keyword "VAR"

vars <- many1 (do id <- (reserved keywords identifier) << ws

token ":"

ty <- typeSpec

token ";"

return (id, ty))

return (VarDecl vars)

ivarDecl = do keyword "IVAR"

vars <- many1 (do id <- (reserved keywords identifier) << ws

token ":"

ty <- typeSpec

token ";"

return (id, ty))

return (IVarDecl vars)

defineDecl = do keyword "DEFINE"

defs <- many1 (do id <- (reserved keywords identifier) << ws

token ":="

expr <- basicExpr

token ";"

return (id, expr))

return (DefineDecl defs)

constDecl = do keyword "CONSTANTS"

consts <- sepBy1 (reserved keywords identifier << ws) (token ",")

token ";"

return (ConstDecl consts)

initConstraint = do keyword "INIT"

expr <- basicExpr

optional (token ";")

return (Init expr)

invarConstraint = do keyword "INVAR"

expr <- basicExpr

optional (token ";")

return (Invar expr)

transConstraint = do keyword "TRANS"

expr <- basicExpr

optional (token ";")

return (Trans expr)

assign = do keyword "ASSIGN"

assigns <- many1 (do lhs <- assignLhs

token ":="

rhs <- basicExpr

token ";"

return (lhs, rhs))

return (Assign assigns)

where

assignLhs = do keyword "init"

token "("

id <- complexId

token ")"

return (InitialValue id)

<|> do keyword "next"

token "("

id <- complexId

token ")"

return (NextValue id)

<|> do id <- complexId

return (CurrentValue id)

fairness = do keyword "FAIRNESS"

expr <- basicExpr

optional (token ";")

return (Fairness expr)

justice = do keyword "JUSTICE"

expr <- basicExpr

optional (token ";")

return (Justice expr)

compassion = do keyword "COMPASSION"

token "("

exprA <- basicExpr

token ","

exprB <- basicExpr

token ")"

optional (token ";")

return (Compassion exprA exprB)

typeSpec :: Parser Type

typeSpec = boolSpec

<|> wordSpec

<|> enumSpec

<|> rangeSpec

<|> arraySpec

where

boolSpec = do keyword "boolean"

return BoolType

wordSpec = do keyword "word"

token "["

width <- integer

token "]"

return (WordType width)

enumSpec = do token "{"

values <- sepBy1 (liftM Symbol identifier <|> liftM Number integer) (ws >> token ",")

token "}"

return (EnumType values)

rangeSpec = do from <- integer

token ".."

to <- integer

return (RangeType from to)

arraySpec = do keyword "array"

from <- integer

token ".."

to <- integer

keyword "of"

ty <- typeSpec

return (ArrayType from to ty)

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