Safe Haskell	None
Language	Haskell2010

Language.Trans.SMV2Copilot

Description

Transform an SMV TL specification into a Copilot specification.

Normally, this module would be implemented as a conversion between ASTs, but we want to add comments to the generated code, which are not representable in the abstract syntax tree.

Synopsis

boolSpec2Copilot :: BoolSpec -> String
const2Copilot :: BoolConst -> String
numExpr2Copilot :: NumExpr -> String
additiveOp2Copilot :: AdditiveOp -> String
multOp2Copilot :: MultOp -> String
ordOp2Copilot :: OrdOp -> String
opOne2Copilot :: OpOne -> String
opOneAlone2Copilot :: Op1Name -> String
opOneMTL2Copilot :: Op1Name -> OrdOp -> Number -> String
opOneMTLRange2Copilot :: Op1Name -> Number -> Number -> String
opOneMTL2Copilot' :: Op1Name -> String
number2Copilot :: Number -> String
opTwo2Copilot :: OpTwo -> String
ident2Copilot :: Ident -> String
boolSpecNames :: BoolSpec -> [String]
numExprNames :: NumExpr -> [String]

Documentation

boolSpec2Copilot :: BoolSpec -> String Source #

Return the Copilot representation of an SMV BoolSpec.

This function returns the temporal property only. The string does not contain any top-level names, any imports, or auxiliary definitions that may be required.

const2Copilot :: BoolConst -> String Source #

Return the Copilot representation of an SMV boolean constant.

numExpr2Copilot :: NumExpr -> String Source #

Return the Copilot representation of a numeric expression.

additiveOp2Copilot :: AdditiveOp -> String Source #

Return the Copilot representation of an SMV additive operator.

multOp2Copilot :: MultOp -> String Source #

Return the Copilot representation of an SMV multiplicative operator.

ordOp2Copilot :: OrdOp -> String Source #

Return the Copilot representation of an SMV comparison operator.

opOne2Copilot :: OpOne -> String Source #

Return the Copilot representation of a unary logical SMV operator.