module Language.Trans.SMV2Copilot where
import Language.SMV.AbsSMV (AdditiveOp (..), BoolConst (..), BoolSpec (..),
Ident (..), MultOp (..), NumExpr (..), Number (..),
Op1Name (..), OpOne (..), OpTwo (..), OrdOp (..))
boolSpec2Copilot :: BoolSpec -> String
boolSpec2Copilot :: BoolSpec -> String
boolSpec2Copilot BoolSpec
b = case BoolSpec
b of
BoolSpecConst BoolConst
bc -> BoolConst -> String
const2Copilot BoolConst
bc
BoolSpecNum NumExpr
nc -> NumExpr -> String
numExpr2Copilot NumExpr
nc
BoolSpecSignal Ident
i -> Ident -> String
ident2Copilot Ident
i
BoolSpecCmp BoolSpec
spec1 OrdOp
op2 BoolSpec
spec2 -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec1
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ OrdOp -> String
ordOp2Copilot OrdOp
op2
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec2
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
BoolSpecNeg BoolSpec
spec -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"not"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
BoolSpecAnd BoolSpec
spec1 BoolSpec
spec2 -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec1
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"&&"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec2
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
BoolSpecOr BoolSpec
spec1 BoolSpec
spec2 -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec1
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"||"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec2
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
BoolSpecXor BoolSpec
spec1 BoolSpec
spec2 -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec1
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"`xor`"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec2
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
BoolSpecImplies BoolSpec
spec1 BoolSpec
spec2 -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec1
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"==>"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec2
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
BoolSpecEquivs BoolSpec
spec1 BoolSpec
spec2 -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec1
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"=="
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec2
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
BoolSpecOp1 OpOne
op BoolSpec
spec -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ OpOne -> String
opOne2Copilot OpOne
op
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
BoolSpecOp2 BoolSpec
spec1 OpTwo
op2 BoolSpec
spec2 -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec1
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ OpTwo -> String
opTwo2Copilot OpTwo
op2
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BoolSpec -> String
boolSpec2Copilot BoolSpec
spec2
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
const2Copilot :: BoolConst -> String
const2Copilot :: BoolConst -> String
const2Copilot BoolConst
BoolConstTrue = String
"true"
const2Copilot BoolConst
BoolConstFalse = String
"false"
const2Copilot BoolConst
BoolConstFTP = String
"ftp"
const2Copilot BoolConst
BoolConstLAST = String
"last"
numExpr2Copilot :: NumExpr -> String
numExpr2Copilot :: NumExpr -> String
numExpr2Copilot (NumId Ident
i) = Ident -> String
ident2Copilot Ident
i
numExpr2Copilot (NumConstI Integer
i) = Integer -> String
forall a. Show a => a -> String
show Integer
i
numExpr2Copilot (NumConstD Double
i) = Double -> String
forall a. Show a => a -> String
show Double
i
numExpr2Copilot (NumAdd NumExpr
x AdditiveOp
op NumExpr
y) = String
"("
String -> String -> String
forall a. [a] -> [a] -> [a]
++ NumExpr -> String
numExpr2Copilot NumExpr
x
String -> String -> String
forall a. [a] -> [a] -> [a]
++ AdditiveOp -> String
additiveOp2Copilot AdditiveOp
op
String -> String -> String
forall a. [a] -> [a] -> [a]
++ NumExpr -> String
numExpr2Copilot NumExpr
y
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
numExpr2Copilot (NumMult NumExpr
x MultOp
op NumExpr
y) = String
"("
String -> String -> String
forall a. [a] -> [a] -> [a]
++ NumExpr -> String
numExpr2Copilot NumExpr
x
String -> String -> String
forall a. [a] -> [a] -> [a]
++ MultOp -> String
multOp2Copilot MultOp
op
String -> String -> String
forall a. [a] -> [a] -> [a]
++ NumExpr -> String
numExpr2Copilot NumExpr
y
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
additiveOp2Copilot :: AdditiveOp -> String
additiveOp2Copilot :: AdditiveOp -> String
additiveOp2Copilot AdditiveOp
OpPlus = String
"+"
additiveOp2Copilot AdditiveOp
OpMinus = String
"-"
multOp2Copilot :: MultOp -> String
multOp2Copilot :: MultOp -> String
multOp2Copilot MultOp
OpTimes = String
"*"
multOp2Copilot MultOp
OpDiv = String
"/"
ordOp2Copilot :: OrdOp -> String
ordOp2Copilot :: OrdOp -> String
ordOp2Copilot OrdOp
OrdOpLT = String
"<"
ordOp2Copilot OrdOp
OrdOpLE = String
"<="
ordOp2Copilot OrdOp
OrdOpEQ = String
"=="
ordOp2Copilot OrdOp
OrdOpNE = String
"/="
ordOp2Copilot OrdOp
OrdOpGT = String
">"
ordOp2Copilot OrdOp
OrdOpGE = String
">="
opOne2Copilot :: OpOne -> String
opOne2Copilot :: OpOne -> String
opOne2Copilot (Op1Alone Op1Name
x) = Op1Name -> String
opOneAlone2Copilot Op1Name
x
opOne2Copilot (Op1MTL Op1Name
x OrdOp
op Number
v) = Op1Name -> OrdOp -> Number -> String
opOneMTL2Copilot Op1Name
x OrdOp
op Number
v
opOne2Copilot (Op1MTLRange Op1Name
op Number
mn Number
mx) = Op1Name -> Number -> Number -> String
opOneMTLRange2Copilot Op1Name
op Number
mn Number
mx
opOneAlone2Copilot :: Op1Name -> String
opOneAlone2Copilot :: Op1Name -> String
opOneAlone2Copilot Op1Name
Op1Pre = String
"pre"
opOneAlone2Copilot Op1Name
Op1X = String
"next"
opOneAlone2Copilot Op1Name
Op1G = String
"always"
opOneAlone2Copilot Op1Name
Op1F = String
"eventually"
opOneAlone2Copilot Op1Name
Op1Y = String
"PTLTL.previous"
opOneAlone2Copilot Op1Name
Op1Z = String
"notPreviousNot"
opOneAlone2Copilot Op1Name
Op1Hist = String
"PTLTL.alwaysBeen"
opOneAlone2Copilot Op1Name
Op1O = String
"PTLTL.eventuallyPrev"
opOneMTL2Copilot :: Op1Name -> OrdOp -> Number -> String
opOneMTL2Copilot :: Op1Name -> OrdOp -> Number -> String
opOneMTL2Copilot Op1Name
operator OrdOp
_comparison Number
number =
Op1Name -> String
opOneMTL2Copilot' Op1Name
operator String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
0 :: Int)
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Number -> String
number2Copilot Number
number
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"clock" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
1 :: Int)
opOneMTLRange2Copilot :: Op1Name -> Number -> Number -> String
opOneMTLRange2Copilot :: Op1Name -> Number -> Number -> String
opOneMTLRange2Copilot Op1Name
operator Number
mn Number
mx =
Op1Name -> String
opOneMTL2Copilot' Op1Name
operator String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Number -> String
number2Copilot Number
mn
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Number -> String
number2Copilot Number
mx
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"clock" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
1 :: Int)
opOneMTL2Copilot' :: Op1Name -> String
opOneMTL2Copilot' :: Op1Name -> String
opOneMTL2Copilot' Op1Name
Op1Pre = String
"pre"
opOneMTL2Copilot' Op1Name
Op1X = String
"next"
opOneMTL2Copilot' Op1Name
Op1G = String
"always"
opOneMTL2Copilot' Op1Name
Op1F = String
"eventually"
opOneMTL2Copilot' Op1Name
Op1Y = String
"MTL.previous"
opOneMTL2Copilot' Op1Name
Op1Z = String
"notPreviousNot"
opOneMTL2Copilot' Op1Name
Op1Hist = String
"MTL.alwaysBeen"
opOneMTL2Copilot' Op1Name
Op1O = String
"MTL.eventuallyPrev"
number2Copilot :: Number -> String
number2Copilot :: Number -> String
number2Copilot (NumberInt Integer
n) = Integer -> String
forall a. Show a => a -> String
show Integer
n
opTwo2Copilot :: OpTwo -> String
opTwo2Copilot :: OpTwo -> String
opTwo2Copilot OpTwo
Op2S = String
"`since`"
opTwo2Copilot OpTwo
Op2T = String
"`triggers`"
opTwo2Copilot OpTwo
Op2V = String
"`releases`"
opTwo2Copilot OpTwo
Op2U = String
"`until`"
ident2Copilot :: Ident -> String
ident2Copilot :: Ident -> String
ident2Copilot (Ident String
i) = String
i
boolSpecNames :: BoolSpec -> [String]
boolSpecNames :: BoolSpec -> [String]
boolSpecNames BoolSpec
b = case BoolSpec
b of
BoolSpecConst BoolConst
_bc -> []
BoolSpecSignal (Ident String
i) -> [String
i]
BoolSpecNum NumExpr
e -> NumExpr -> [String]
numExprNames NumExpr
e
BoolSpecCmp BoolSpec
spec1 OrdOp
_op2 BoolSpec
spec2 -> BoolSpec -> [String]
boolSpecNames BoolSpec
spec1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ BoolSpec -> [String]
boolSpecNames BoolSpec
spec2
BoolSpecNeg BoolSpec
spec -> BoolSpec -> [String]
boolSpecNames BoolSpec
spec
BoolSpecAnd BoolSpec
spec1 BoolSpec
spec2 -> BoolSpec -> [String]
boolSpecNames BoolSpec
spec1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ BoolSpec -> [String]
boolSpecNames BoolSpec
spec2
BoolSpecOr BoolSpec
spec1 BoolSpec
spec2 -> BoolSpec -> [String]
boolSpecNames BoolSpec
spec1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ BoolSpec -> [String]
boolSpecNames BoolSpec
spec2
BoolSpecXor BoolSpec
spec1 BoolSpec
spec2 -> BoolSpec -> [String]
boolSpecNames BoolSpec
spec1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ BoolSpec -> [String]
boolSpecNames BoolSpec
spec2
BoolSpecImplies BoolSpec
spec1 BoolSpec
spec2 -> BoolSpec -> [String]
boolSpecNames BoolSpec
spec1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ BoolSpec -> [String]
boolSpecNames BoolSpec
spec2
BoolSpecEquivs BoolSpec
spec1 BoolSpec
spec2 -> BoolSpec -> [String]
boolSpecNames BoolSpec
spec1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ BoolSpec -> [String]
boolSpecNames BoolSpec
spec2
BoolSpecOp1 OpOne
_op BoolSpec
spec -> BoolSpec -> [String]
boolSpecNames BoolSpec
spec
BoolSpecOp2 BoolSpec
spec1 OpTwo
_op2 BoolSpec
spec2 -> BoolSpec -> [String]
boolSpecNames BoolSpec
spec1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ BoolSpec -> [String]
boolSpecNames BoolSpec
spec2
numExprNames :: NumExpr -> [String]
numExprNames :: NumExpr -> [String]
numExprNames NumExpr
numExpr = case NumExpr
numExpr of
NumId (Ident String
i) -> [String
i]
NumConstI Integer
_c -> []
NumConstD Double
_c -> []
NumAdd NumExpr
expr1 AdditiveOp
_op NumExpr
expr2 -> NumExpr -> [String]
numExprNames NumExpr
expr1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ NumExpr -> [String]
numExprNames NumExpr
expr2
NumMult NumExpr
expr1 MultOp
_op NumExpr
expr2 -> NumExpr -> [String]
numExprNames NumExpr
expr1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ NumExpr -> [String]
numExprNames NumExpr
expr2