Revert "The MC.tla no longer extends TLC.tla to prevent name clashes with user"

This reverts commit 640df815.

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:

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);

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}

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);
-	}
 }