diff --git a/ogma-core/CHANGELOG.md b/ogma-core/CHANGELOG.md index 2f2f161..c2bafd4 100644 --- a/ogma-core/CHANGELOG.md +++ b/ogma-core/CHANGELOG.md @@ -1,8 +1,9 @@ # Revision history for ogma-core -## [1.X.Y] - 2023-05-20 +## [1.X.Y] - 2023-05-21 * Allow customizing the names of the C files generated by Copilot (#80). +* Translate ZtoPre and YtoPre to Copilot (#86). ## [1.0.8] - 2023-03-21 diff --git a/ogma-core/src/Language/Trans/CoCoSpec2Copilot.hs b/ogma-core/src/Language/Trans/CoCoSpec2Copilot.hs index f0894b9..6a73cfa 100644 --- a/ogma-core/src/Language/Trans/CoCoSpec2Copilot.hs +++ b/ogma-core/src/Language/Trans/CoCoSpec2Copilot.hs @@ -130,6 +130,8 @@ const2Copilot BoolConstFTP = "ftp" -- operator. opOnePre2Copilot :: Op1Pre -> String opOnePre2Copilot Op1Pre = "pre" +opOnePre2Copilot Op1YtoPre = "pre" +opOnePre2Copilot Op1ZtoPre = "tpre" opOnePre2Copilot Op1Once = "PTLTL.eventuallyPrev" opOnePre2Copilot Op1Hist = "PTLTL.alwaysBeen" opOnePre2Copilot Op1Y = "PTLTL.previous" diff --git a/ogma-core/src/Language/Trans/FRETComponentSpec2Copilot.hs b/ogma-core/src/Language/Trans/FRETComponentSpec2Copilot.hs index 51ae667..d262997 100644 --- a/ogma-core/src/Language/Trans/FRETComponentSpec2Copilot.hs +++ b/ogma-core/src/Language/Trans/FRETComponentSpec2Copilot.hs @@ -87,6 +87,7 @@ fretComponentSpec2Copilot' prefs fretComponentSpec = , pure clock , pure ftp , pure pre + , pure tpre , pure spec , pure main' ] @@ -223,6 +224,12 @@ fretComponentSpec2Copilot' prefs fretComponentSpec = , "pre = ([False] ++)" ] + -- Auxiliary streams: tpre + tpre = [ "" + , "tpre :: Stream Bool -> Stream Bool" + , "tpre = ([True] ++)" + ] + -- Main specification spec :: [String] spec = [ "" diff --git a/ogma-core/src/Language/Trans/FRETReqsDB2Copilot.hs b/ogma-core/src/Language/Trans/FRETReqsDB2Copilot.hs index ef8a61e..72e447c 100644 --- a/ogma-core/src/Language/Trans/FRETReqsDB2Copilot.hs +++ b/ogma-core/src/Language/Trans/FRETReqsDB2Copilot.hs @@ -94,10 +94,12 @@ fret2CopilotModule' prefs smvSpec cocoSpec = unlines $ concat sections else SMV.boolSpecNames smvSpec sections | fretReqsDB2CopilotUseCoCoSpec prefs - = [ imports, propDef, externs, clock, ftp, undef, spec, main' ] + = [ imports, propDef, externs, clock, ftp, undef, tpre, spec + , main' + ] | otherwise - = [ imports, propDef, externs, clock, ftp, spec, main' ] + = [ imports, propDef, externs, clock, ftp, tpre, spec, main' ] imports :: [String] imports = @@ -145,6 +147,11 @@ fret2CopilotModule' prefs smvSpec cocoSpec = unlines $ concat sections , "pre = undefined" ] + tpre = [ "" + , "tpre :: Stream Bool -> Stream Bool" + , "tpre = ([True] ++)" + ] + spec = [ "" , "-- | Complete specification. Calls the C function void handler(); when" , "-- the property is violated." diff --git a/ogma-language-cocospec/CHANGELOG.md b/ogma-language-cocospec/CHANGELOG.md index 07db695..8e67239 100644 --- a/ogma-language-cocospec/CHANGELOG.md +++ b/ogma-language-cocospec/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-language-cocospec +## [1.X.Y] - 2023-05-21 + +* Add unary operators ZtoPre, YtoPre (#86). + ## [1.0.8] - 2023-03-21 * Version bump 1.0.8 (#81). diff --git a/ogma-language-cocospec/grammar/CoCoSpec.cf b/ogma-language-cocospec/grammar/CoCoSpec.cf index be38390..944ce52 100644 --- a/ogma-language-cocospec/grammar/CoCoSpec.cf +++ b/ogma-language-cocospec/grammar/CoCoSpec.cf @@ -49,12 +49,14 @@ BoolSpecOp2ST. BoolSpec ::= "ST" "(" NumExpr "," NumExpr "," BoolSpec "," BoolS -- Boolean Operators -Op1Once. Op1Pre ::= "O" ; -Op1Pre. Op1Pre ::= "pre" ; -Op1Hist. Op1Pre ::= "H" ; -Op1Y. Op1Pre ::= "Y" ; -Op1Not. Op1Pre ::= "not" ; -Op1Bang. Op1Pre ::= "!" ; +Op1Once. Op1Pre ::= "O" ; +Op1Pre. Op1Pre ::= "pre" ; +Op1YtoPre. Op1Pre ::= "YtoPre" ; +Op1ZtoPre. Op1Pre ::= "ZtoPre" ; +Op1Hist. Op1Pre ::= "H" ; +Op1Y. Op1Pre ::= "Y" ; +Op1Not. Op1Pre ::= "not" ; +Op1Bang. Op1Pre ::= "!" ; Op2And. Op2In ::= "and" ; Op2Amp. Op2In ::= "&" ;