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 b8ac510fab9ea5707f94c97436579ef2cadb45a8..e0c56078501a778c56dc70d82e68f6afbe34cf3e 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 aa980fd2c1032c21573739ebd9a861995f2a7eb4..a04c51e04d7c1b37f8ac13da1ab4e008ee0b6b09 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));