From 928b42f0986a80f9d5108defcac2677f4a62815c Mon Sep 17 00:00:00 2001
From: Ivan Perez <ivan.perezdominguez@nasa.gov>
Date: Wed, 5 Apr 2023 10:15:43 -0700
Subject: [PATCH] ogma-core: Translate MTL operators with number ranges. Refs
 #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 | 10 ++++++++++
 1 file changed, 10 insertions(+)

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