Improve error reporting when configuration file illegally substitutes a

non-constant such as a variable for a constant.

Correctly handle in Toolbox.
    
[Bug][TLC]

org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCModelLaunchDataProvider.java

@@ -52,6 +52,7 @@ import org.eclipse.ui.editors.text.FileDocumentProvider;
 import org.eclipse.ui.part.FileEditorInput;
 import org.lamport.tla.toolbox.Activator;
 import org.lamport.tla.toolbox.tool.tlc.launch.IModelConfigurationConstants;
+import org.lamport.tla.toolbox.tool.tlc.model.Assignment;
 import org.lamport.tla.toolbox.tool.tlc.model.Formula;
 import org.lamport.tla.toolbox.tool.tlc.model.Model;
 import org.lamport.tla.toolbox.tool.tlc.model.ModelWriter;
@@ -701,12 +702,16 @@ public class TLCModelLaunchDataProvider implements ITLCOutputListener
 											.getAttribute(attributeName, new ArrayList<String>(0));
                                     int attributeNumber = (attributeIndex != null) ? attributeIndex.intValue() : 0;
 
-                                    if (IModelConfigurationConstants.MODEL_PARAMETER_CONSTANTS.equals(attributeName)
-                                            || IModelConfigurationConstants.MODEL_PARAMETER_CONSTANTS
-                                                    .equals(attributeName))
+                                    if (IModelConfigurationConstants.MODEL_PARAMETER_CONSTANTS.equals(attributeName))
                                     {
-                                        // List valueList = ModelHelper.deserializeAssignmentList(attributeValue);
+                                    	// MK 07/25/2017: Correctly show error when constant is assigned a non-constant.
+                                        final List<Assignment> valueList = ModelHelper.deserializeAssignmentList(attributeValue);
+                                        if (valueList.size() >= (attributeNumber + 1)) {
+	                                        final Assignment assignment = valueList.get(attributeNumber);
+	                                        idReplacement = assignment.getRight();
+                                        } else {
                                         	idReplacement = "'LL claims this should not happen. See Bug in TLCModelLaunchDataProvider.'";
+                                        }
                                     } else
                                     {
                                         // invariants and properties

tlatools/src/tlc2/output/EC.java

@@ -233,8 +233,8 @@ public interface EC
     public static final int TLC_CONFIG_RHS_ID_APPEARED_AFTER_LHS_ID = 2223;
     public static final int TLC_CONFIG_WRONG_SUBSTITUTION = 2224;
     public static final int TLC_CONFIG_WRONG_SUBSTITUTION_NUMBER_OF_ARGS = 2225;
-    public static final int TLC_CONFIG_UNDEFINED_OR_NO_OPERATOR = 22251;
-    public static final int TLC_CONFIG_SUBSTITUTION_NON_CONSTANT = 22252;
+    public static final int TLC_CONFIG_UNDEFINED_OR_NO_OPERATOR = 2280;
+    public static final int TLC_CONFIG_SUBSTITUTION_NON_CONSTANT = 2281;
     public static final int TLC_CONFIG_ID_DOES_NOT_APPEAR_IN_SPEC = 2226;
     public static final int TLC_CONFIG_NOT_BOTH_SPEC_AND_INIT = 2227;
     public static final int TLC_CONFIG_ID_REQUIRES_NO_ARG = 2228;