From 58f3623ee9ea2efd93acc626601dbdd5cb96d3ad Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 5 Apr 2023 09:35:36 -0700 Subject: [PATCH 1/4] ogma-language-cocospec: Add unary operators ZtoPre, YtoPre. Refs #86. Ogma cannot handle CoCoSpec boolean specifications containing the unary operators ZtoPre or YtoPre. This makes some of the specifications produced by FRET not parseable. This commit modifies the CoCoSpec grammar to include two new unary operators: ZtoPre and YtoPre. --- ogma-language-cocospec/grammar/CoCoSpec.cf | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) 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 ::= "&" ; From fadad15667c00e037092de8d86258eb251bf0c5c Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 5 Apr 2023 09:36:28 -0700 Subject: [PATCH 2/4] ogma-core: Translate ZtoPre and YtoPre to Copilot. Refs #86. Ogma cannot handle CoCoSpec boolean specifications containing the unary operators ZtoPre or YtoPre. This makes some of the specifications produced by FRET not parseable. The CoCoSpec grammar has been extended with two new unary operators ZtoPre and YtoPre. This commit updates the translator from CoCoSpec to Copilot so that it assigns a Copilot construct to those new unary operators. The component spec and requirements db translators are updated to include the necessary Copilot definitions so that the code produced compiles without errors. --- ogma-core/src/Language/Trans/CoCoSpec2Copilot.hs | 2 ++ .../src/Language/Trans/FRETComponentSpec2Copilot.hs | 7 +++++++ ogma-core/src/Language/Trans/FRETReqsDB2Copilot.hs | 11 +++++++++-- 3 files changed, 18 insertions(+), 2 deletions(-) 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." From fced5afadecd959a16f4ec32d74e4b8b871e16fb Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 21 May 2023 05:21:49 -0700 Subject: [PATCH 3/4] ogma-language-cocospec: Document changes in CHANGELOG. Refs #86. --- ogma-language-cocospec/CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) 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). From 6a1054f489edf4373831f8997c06d118db375d35 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 21 May 2023 05:22:25 -0700 Subject: [PATCH 4/4] ogma-core: Document changes in CHANGELOG. Refs #86. --- ogma-core/CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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