From b9af101906a7628e05bf39ada3d3bdaec56360e4 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Sat, 23 Nov 2024 09:13:49 +0100
Subject: [PATCH] add comments for removed debugPrints
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
.../src/de/prob/eventb/translator/ContextTranslator.java | 4 +++-
.../de/prob/eventb/translator/internal/ModelTranslator.java | 6 +++++-
2 files changed, 8 insertions(+), 2 deletions(-)
diff --git a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
index b8ac510f..e0c56078 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
@@ -321,6 +321,7 @@ public final class ContextTranslator extends AbstractComponentTranslator {
final ICarrierSet ucs = (ICarrierSet) carrierSet.getSource(); // comments only attached in unchecked source
if (ucs.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) {
+ // The carrier set has a comment attached to it, we convert it to a description pragma:
final String commentString = ucs.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE);
final TPragmaFreeText desc = new TPragmaFreeText(commentString);
ADescriptionPragma descPragma = new ADescriptionPragma(Collections.singletonList(desc));
@@ -354,13 +355,13 @@ public final class ContextTranslator extends AbstractComponentTranslator {
} catch (IllegalArgumentException E) {
// the attribute did not exist
}
- // TODO: check unchecked constant and see if we have a comment and generate ADescriptionExpression
final AIdentifierExpression cstid = new AIdentifierExpression(Arrays
.asList(new TIdentifierLiteral[] { new TIdentifierLiteral(constant.getIdentifierString()) }));
final IConstant ucc = (IConstant) constant.getSource(); // comments only attached in unchecked source
if (ucc.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) {
+ // The constant has a comment attached to it, we convert it to a description pragma:
final String commentString = ucc.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE);
final TPragmaFreeText desc = new TPragmaFreeText(commentString);
ADescriptionPragma descPragma = new ADescriptionPragma(Collections.singletonList(desc));
@@ -410,6 +411,7 @@ public final class ContextTranslator extends AbstractComponentTranslator {
final PPredicate predicate = translatePredicate(ff, te, element);
final IAxiom uca = (IAxiom) element.getSource(); // comments only attached in unchecked source
if (uca.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) {
+ // The axiom has a comment attached to it, we convert it to a description pragma:
final String commentString = uca.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE);
final TPragmaFreeText desc = new TPragmaFreeText(commentString);
ADescriptionPragma descPragma = new ADescriptionPragma(Collections.singletonList(desc));
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
index aa980fd2..a04c51e0 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
@@ -366,8 +366,11 @@ public class ModelTranslator extends AbstractComponentTranslator {
// System.out.println("Description 1 of " + revent.getLabel() + ": " + ((ICommentedElement) ucevent).getComment());
//}
if (ucevent.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) {
+ // The event has a comment attached to it, we convert it to a description pragma
+ // these descriptions are treated like template strings (containing ${Expr}) by ProB
+ // to generate descriptions for transitions
final String commentString = ucevent.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE);
- System.out.println("Event " + revent.getLabel() + " has description " + commentString);
+ // System.out.println("Event " + revent.getLabel() + " has description " + commentString);
final TPragmaFreeText desc = new TPragmaFreeText(commentString);
ADescriptionPragma descPragma = new ADescriptionPragma(Collections.singletonList(desc));
eventsList.add(new ADescriptionEvent(descPragma, event));
@@ -457,6 +460,7 @@ public class ModelTranslator extends AbstractComponentTranslator {
final IVariable ucv = (IVariable) variable.getSource(); // comments only attached in unchecked source
if (ucv.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) {
+ // The variable has a comment attached to it, we convert it to a description pragma:
final String commentString = ucv.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE);
final TPragmaFreeText desc = new TPragmaFreeText(commentString);
ADescriptionPragma descPragma = new ADescriptionPragma(Collections.singletonList(desc));
--
GitLab