From c068c7cfe242f193072bab0af12fae76d08a4f55 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 22 Nov 2024 21:23:09 +0000 Subject: [PATCH 1/2] ogma-core: Correct name in documentation. Refs #176. The documentation of ogma-core/src/Language/Trans/SMV2Copilot.hs does not refer to the boolean expressions as those in the SMV language, but incorrectly refers to them as FRET expressions, which was old documentation left over after renaming the module. This commit renames all occurrences to SMV in the module documentation. --- ogma-core/src/Language/Trans/SMV2Copilot.hs | 28 ++++++++++----------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/ogma-core/src/Language/Trans/SMV2Copilot.hs b/ogma-core/src/Language/Trans/SMV2Copilot.hs index bdb0c6d7..7e48842c 100644 --- a/ogma-core/src/Language/Trans/SMV2Copilot.hs +++ b/ogma-core/src/Language/Trans/SMV2Copilot.hs @@ -29,7 +29,7 @@ -- AGREEMENT. -- --- | Transform a FRET TL specification into a Copilot specification. +-- | 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 @@ -40,7 +40,7 @@ import Language.SMV.AbsSMV (AdditiveOp (..), BoolConst (..), BoolSpec (..), Ident (..), MultOp (..), NumExpr (..), Number (..), Op1Name (..), OpOne (..), OpTwo (..), OrdOp (..)) --- | Return the Copilot representation of a FRET BoolSpec. +-- | 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 @@ -96,7 +96,7 @@ boolSpec2Copilot b = case b of ++ " " ++ boolSpec2Copilot spec2 ++ ")" --- | Return the Copilot representation of a FRET boolean constant. +-- | Return the Copilot representation of an SMV boolean constant. const2Copilot :: BoolConst -> String const2Copilot BoolConstTrue = "true" const2Copilot BoolConstFalse = "false" @@ -119,17 +119,17 @@ numExpr2Copilot (NumMult x op y) = "(" ++ numExpr2Copilot y ++ ")" --- | Return the Copilot representation of a FRET additive operator. +-- | Return the Copilot representation of an SMV additive operator. additiveOp2Copilot :: AdditiveOp -> String additiveOp2Copilot OpPlus = "+" additiveOp2Copilot OpMinus = "-" --- | Return the Copilot representation of a FRET multiplicative operator. +-- | Return the Copilot representation of an SMV multiplicative operator. multOp2Copilot :: MultOp -> String multOp2Copilot OpTimes = "*" multOp2Copilot OpDiv = "/" --- | Return the Copilot representation of a FRET comparison operator. +-- | Return the Copilot representation of an SMV comparison operator. ordOp2Copilot :: OrdOp -> String ordOp2Copilot OrdOpLT = "<" ordOp2Copilot OrdOpLE = "<=" @@ -138,13 +138,13 @@ ordOp2Copilot OrdOpNE = "/=" ordOp2Copilot OrdOpGT = ">" ordOp2Copilot OrdOpGE = ">=" --- | Return the Copilot representation of a unary logical FRET operator. +-- | Return the Copilot representation of a unary logical SMV operator. 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 +-- | Return the Copilot representation of a unary logical non-MTL SMV -- operator. opOneAlone2Copilot :: Op1Name -> String opOneAlone2Copilot Op1Pre = "pre" @@ -156,7 +156,7 @@ opOneAlone2Copilot Op1Z = "notPreviousNot" opOneAlone2Copilot Op1Hist = "PTLTL.alwaysBeen" opOneAlone2Copilot Op1O = "PTLTL.eventuallyPrev" --- | Return the Copilot representation of a unary logical MTL FRET operator. +-- | Return the Copilot representation of a unary logical MTL SMV operator. opOneMTL2Copilot :: Op1Name -> OrdOp -> Number -> String opOneMTL2Copilot operator _comparison number = opOneMTL2Copilot' operator ++ " " ++ show (0 :: Int) @@ -164,7 +164,7 @@ opOneMTL2Copilot operator _comparison number = ++ " " ++ "clock" ++ " " ++ show (1 :: Int) --- | Return the Copilot representation of a unary logical MTL FRET operator +-- | Return the Copilot representation of a unary logical MTL SMV operator -- that uses an explicit range. opOneMTLRange2Copilot :: Op1Name -> Number -> Number -> String opOneMTLRange2Copilot operator mn mx = @@ -173,7 +173,7 @@ opOneMTLRange2Copilot operator mn mx = ++ " " ++ "clock" ++ " " ++ show (1 :: Int) --- | Return the Copilot representation of a unary logical possibly MTL FRET +-- | Return the Copilot representation of a unary logical possibly MTL SMV -- operator. opOneMTL2Copilot' :: Op1Name -> String opOneMTL2Copilot' Op1Pre = "pre" @@ -185,11 +185,11 @@ opOneMTL2Copilot' Op1Z = "notPreviousNot" opOneMTL2Copilot' Op1Hist = "MTL.alwaysBeen" opOneMTL2Copilot' Op1O = "MTL.eventuallyPrev" --- | Return the Copilot representation of a FRET number. +-- | Return the Copilot representation of an SMV number. number2Copilot :: Number -> String number2Copilot (NumberInt n) = show n --- | Return the Copilot representation of a binary logical non-MTL FRET +-- | Return the Copilot representation of a binary logical non-MTL SMV -- operator. opTwo2Copilot :: OpTwo -> String opTwo2Copilot Op2S = "`since`" @@ -197,7 +197,7 @@ opTwo2Copilot Op2T = "`triggers`" opTwo2Copilot Op2V = "`releases`" opTwo2Copilot Op2U = "`until`" --- | Return the Copilot representation of a FRET identifier. +-- | Return the Copilot representation of an SMV identifier. ident2Copilot :: Ident -> String ident2Copilot (Ident i) = i From 5092faf6fbf346b9d5ad59aa0c9c7553f76c1410 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 22 Nov 2024 21:24:39 +0000 Subject: [PATCH 2/2] ogma-core: Document changes in CHANGELOG. Refs #176. --- ogma-core/CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/ogma-core/CHANGELOG.md b/ogma-core/CHANGELOG.md index 86183901..e398703b 100644 --- a/ogma-core/CHANGELOG.md +++ b/ogma-core/CHANGELOG.md @@ -8,6 +8,7 @@ * Fix comment in generated Copilot spec (#164). * Add missing notPreviousNot to generated spec (#168). * Introduce new standalone command (#170). +* Correct name in documentation (#176). ## [1.4.1] - 2024-09-21