{-# OPTIONS -fglasgow-exts #-}

module NuSmv (basicExpr, program) where

import Control.Monad (liftM, liftM2)

import Data.Char (toLower)

import Data.List (intersperse)

import Text.ParserCombinators.Parsec hiding (State, token)

(<<) :: (Monad m) => m a -> m b -> m a

(<<) a b = do x <- a

b

return x

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

checkWith :: (Show a) => GenParser tok st a -> (a -> Bool) -> GenParser tok st a

checkWith p f = do x <- p

if f x then return x

else unexpected (show x)

reserved :: [String] -> CharParser st String -> CharParser st String

reserved l p = try $ checkWith p (`notElem` l)

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

ws :: Parser ()

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

token :: String -> Parser ()

token x = string x >> ws

keyword :: String -> Parser ()

keyword x = try (string x >> notFollowedBy alphaNum) >> ws

identifier :: Parser String

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

where

idFirstChar = letter

<|> char '_'

idConsecutiveChar = idFirstChar

<|> digit

<|> char '$'

<|> char '#'

<|> char '\\'

<|> char '-'

integer :: Parser Int

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

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

keywords :: [String]

keywords = [ "MODULE", "DEFINE", "CONSTANTS", "VAR", "IVAR", "INIT", "TRANS",

"INVAR", "SPEC", "CTLSPEC", "LTLSPEC", "PSLSPEC", "COMPUTE",

"INVARSPEC", "FAIRNESS", "JUSTICE", "COMPASSION", "ISA", "ASSIGN",

"CONSTRAINT", "SIMPWFF", "CTLWFF", "LTLWFF", "PSLWFF", "COMPWFF",

"IN", "MIN", "MAX", "process", "array", "of", "boolean",

"integer", "real", "word", "word1", "bool", "EX", "AX", "EF",

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

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

"esac", "mod", "next", "init", "union", "in", "xor", "xnor",

"self", "TRUE", "FALSE" ]

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

{- -}

{- Basic Expressions of NuSMV -}

{- -}

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

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)

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