ogma-core: Translate MTL operators with number ranges. Refs nasa#101.

The current translation module for SMV into Copilot does not support MTL
operators with number ranges, only those with comparison operators and a
numeric limit.

A prior commit has extended the grammar to support MTL operators with number
ranges. This commit extends the translation module from SMV to Copilot.

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