From 11ab426b566821e018cdfcfa9726037eb6c75e9b Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <tlaplus.net@lemmster.de>
Date: Mon, 8 Jan 2018 08:00:44 +0100
Subject: [PATCH] Revert "The MC.tla no longer extends TLC.tla to prevent name
clashes with user"
This reverts commit 640df815333323bcb6a5be9af009615f16f52ff7.
---
.../tool/tlc/launch/TLCModelLaunchDelegate.java | 4 ++--
.../tla/toolbox/tool/tlc/model/ModelWriter.java | 15 +++------------
.../tla/toolbox/tool/tlc/util/ModelHelper.java | 4 ----
tlatools/src/tlc2/module/MC.java | 17 +++++------------
4 files changed, 10 insertions(+), 30 deletions(-)
diff --git a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TLCModelLaunchDelegate.java b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TLCModelLaunchDelegate.java
index 00eea8133..d2dcdf104 100644
--- a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TLCModelLaunchDelegate.java
+++ b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TLCModelLaunchDelegate.java
@@ -412,8 +412,8 @@ public class TLCModelLaunchDelegate extends LaunchConfigurationDelegate implemen
}
// calculator expression
- writer.addConstantExpressionEvaluation(model.getEvalExpression(), Model.MODEL_EXPRESSION_EVAL,
- !ModelHelper.hasOpDefNode("PrintT"), !ModelHelper.hasOpDefNode("Print"));
+
+ writer.addConstantExpressionEvaluation(model.getEvalExpression(), Model.MODEL_EXPRESSION_EVAL);
switch (specType) {
case MODEL_BEHAVIOR_TYPE_NO_SPEC:
diff --git a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/ModelWriter.java b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/ModelWriter.java
index 659392272..07a6b3db6 100644
--- a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/ModelWriter.java
+++ b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/ModelWriter.java
@@ -1085,21 +1085,10 @@ public class ModelWriter
* @param expression
* @param attributeName
*/
- public void addConstantExpressionEvaluation(String expression, String attributeName, final boolean definePrintT, final boolean definePrint)
+ public void addConstantExpressionEvaluation(String expression, String attributeName)
{
if (!((expression.trim().length()) == 0))
{
- // @see tlc2.module.MC
- if (definePrintT || definePrint) {
- tlaBuffer.append(COMMENT).append("Constant expression helper definition of PrintT and Print.").append(CR);
- if (definePrintT) {
- tlaBuffer.append("LOCAL PrintT(out) == TRUE").append(CR);
- }
- if (definePrint) {
- tlaBuffer.append("LOCAL Print(out, val) == val").append(CR);
- }
- tlaBuffer.append(SEP).append(CR).append(CR);
- }
/*
* Identifier definition
* We define an identifier for more sensible error messages
@@ -1126,6 +1115,8 @@ public class ModelWriter
// value of the constant expression in the TLC output
tlaBuffer.append(COMMENT).append("Constant expression ASSUME statement ").append(ATTRIBUTE).append(
attributeName).append(CR);
+ // @see tlc2.module.MC
+ tlaBuffer.append("LOCAL PrintT(out) == TRUE").append(CR);
tlaBuffer.append("ASSUME PrintT(").append(BEGIN_TUPLE).append(CONSTANT_EXPRESSION_EVAL_IDENTIFIER).append(
COMMA).append(id).append(END_TUPLE).append(")").append(CR);
tlaBuffer.append(SEP).append(CR).append(CR);
diff --git a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/util/ModelHelper.java b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/util/ModelHelper.java
index 1f69748b8..fd07160c3 100644
--- a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/util/ModelHelper.java
+++ b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/util/ModelHelper.java
@@ -900,10 +900,6 @@ public class ModelHelper implements IModelConfigurationConstants, IModelConfigur
return null;
}
- public static boolean hasOpDefNode(final String name) {
- return getOpDefNode(name) != null;
- }
-
/**
* Checks, whether a model attribute is a list
* @param attributeName name of the attribute, see {@link IModelConfigurationConstants}
diff --git a/tlatools/src/tlc2/module/MC.java b/tlatools/src/tlc2/module/MC.java
index 6ee5a00da..9ffdb5d07 100644
--- a/tlatools/src/tlc2/module/MC.java
+++ b/tlatools/src/tlc2/module/MC.java
@@ -48,25 +48,18 @@ import tlc2.value.Value;
* but produces no output. This class effectively associates MC.tla's PrintT with
* tlc2.module.TLC#PrintT.
*
+ * The only operator for which this approach obviously does not work is PrintT itself.
+ * If the actual specification declares PrintT, evaluating a constant expression will
+ * fail. However - contrary to Permutations/SortSeq/... - this is handled gracefully
+ * with a proper error message.
+ *
* @see org.lamport.tla.toolbox.tool.tlc.model.ModelWriter.addConstantExpressionEvaluation(String, String)
*/
public class MC {
public static final long serialVersionUID = 20171027L;
- /**
- * @see TLC#PrintT(Value)
- */
public static Value PrintT(Value v1) {
return TLC.PrintT(v1);
}
-
- // For symmetry reasons also support Print (would be confusing if eval
- // expression support PrintT but not Print).
- /**
- * @see TLC#Print(Value, Value)
- */
- public static Value Print(Value v1, Value v2) {
- return TLC.Print(v1, v2);
- }
}
--
GitLab