Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ogma-core: Correct name in documentation. Refs #176. #177

Merged
merged 2 commits into from
Nov 22, 2024
Merged

ogma-core: Correct name in documentation. Refs #176. #177

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c068c7c
ogma-core: Correct name in documentation. Refs #176.
ivanperez-keera Nov 22, 2024
5092faf
ogma-core: Document changes in CHANGELOG. Refs #176.
ivanperez-keera Nov 22, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions ogma-core/CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
28 changes: 14 additions & 14 deletions ogma-core/src/Language/Trans/SMV2Copilot.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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"
Expand All @@ -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 = "<="
Expand All @@ -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"
Expand All @@ -156,15 +156,15 @@ 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)
++ " " ++ number2Copilot 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 =
Expand All @@ -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"
Expand All @@ -185,19 +185,19 @@ 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`"
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

Expand Down