diff --git a/ogma-core/src/Language/Trans/SMV2Copilot.hs b/ogma-core/src/Language/Trans/SMV2Copilot.hs index b39f3d6..1df050a 100644 --- a/ogma-core/src/Language/Trans/SMV2Copilot.hs +++ b/ogma-core/src/Language/Trans/SMV2Copilot.hs @@ -142,6 +142,7 @@ ordOp2Copilot OrdOpGE = ">=" opOne2Copilot :: OpOne -> String opOne2Copilot (Op1Alone x) = opOneAlone2Copilot x opOne2Copilot (Op1MTL x op v) = opOneMTL2Copilot x op v +opOne2Copilot (Op1MTLRange op mn mx) = opOneMTLRange2Copilot op mn mx -- | Return the Copilot representation of a unary logical non-MTL FRET -- operator. @@ -163,6 +164,15 @@ opOneMTL2Copilot operator _comparison number = ++ " " ++ "clock" ++ " " ++ show (1 :: Int) +-- | Return the Copilot representation of a unary logical MTL FRET operator +-- that uses an explicit range. +opOneMTLRange2Copilot :: Op1Name -> Number -> Number -> String +opOneMTLRange2Copilot operator mn mx = + opOneMTL2Copilot' operator ++ " " ++ number2Copilot mn + ++ " " ++ number2Copilot mx + ++ " " ++ "clock" ++ " " + ++ show (1 :: Int) + -- | Return the Copilot representation of a unary logical possibly MTL FRET -- operator. opOneMTL2Copilot' :: Op1Name -> String