ogma-core-1.14.0: Ogma: Helper tool to interoperate between Copilot and other languages.

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.

opOneAlone2Copilot :: Op1Name -> String Source #

Return the Copilot representation of a unary logical non-MTL SMV operator.

opOneMTL2Copilot :: Op1Name -> OrdOp -> Number -> String Source #

Return the Copilot representation of a unary logical MTL SMV operator.

opOneMTLRange2Copilot :: Op1Name -> Number -> Number -> String Source #

Return the Copilot representation of a unary logical MTL SMV operator that uses an explicit range.

opOneMTL2Copilot' :: Op1Name -> String Source #

Return the Copilot representation of a unary logical possibly MTL SMV operator.

number2Copilot :: Number -> String Source #

Return the Copilot representation of an SMV number.

opTwo2Copilot :: OpTwo -> String Source #

Return the Copilot representation of a binary logical non-MTL SMV operator.

ident2Copilot :: Ident -> String Source #

Return the Copilot representation of an SMV identifier.

boolSpecNames :: BoolSpec -> [String] Source #

Return all identifiers used in a BoolSpec that are not reserved keywords.

numExprNames :: NumExpr -> [String] Source #

Return all identifiers used in a numeric expression.