Name clash between variable in refined spec and operator in instantiated

spec

Fixes Github issue #362
https://github.com/tlaplus/tlaplus/issues/362



Co-authored-by: Markus Alexander Kuppe <tlaplus.net@lemmster.de>

[Bug][TLC]

tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Spec.java

@@ -352,14 +352,22 @@ abstract class Spec
         if (result != opNode) {
             return result;
         }
+
+		// CalvinL/LL/MAK 02/2021: Added conditional as part of Github issue #362 Name
+		// clash between variable in refined spec and operator in instantiated spec. See
+		// releated test in Github362.java.
+        if (opNode.getKind() != UserDefinedOpKind) {
 			result = s.lookup(opNode.getName());
 			if (result != null) {
 				return result;
 			}
+		}
+
         return opNode;
     }
 
-    public final Object lookup(final SymbolNode opNode) {
+    public final Object lookup(final SymbolNode opNode)
+    {
         return lookup(opNode, Context.Empty, false, toolId);
     }
 

tlatools/org.lamport.tlatools/test-model/Github362.cfg

+INIT Init
+NEXT Next
+PROPERTY Correct
+CONSTANT overloadedConst = 4711

tlatools/org.lamport.tlatools/test-model/Github362.tla

+---- CONFIG Github362 ----
+INIT Init
+NEXT Next
+PROPERTY Correct
+CONSTANT overloadedConst = 4711
+====
+
+---- MODULE Github362 ----
+
+EXTENDS TLC
+
+CONSTANT overloadedConst
+
+VARIABLES overloadedName
+
+\* Github362B.tla contains the definition "overloadedName == x".  It is
+\* unrelated to the variable "overloadedName" defined above.
+Abstract == INSTANCE Github362B WITH
+    x <- "x",
+    C <- 42
+
+Init ==
+    /\ overloadedName = "fizzbuzz"
+    /\ overloadedConst = 4711
+    /\ Print(<<"Evaluated initial state in A; overloadedName is: ", overloadedName>>, TRUE)        \* fizzbuzz
+    /\ Print(<<"From A's perspective, B's overloadedName is: ", Abstract!overloadedName>>, TRUE)   \* x
+    /\ Print(<<"Evaluated initial state in A; overloadedConst is: ", overloadedConst>>, TRUE)      \* 4711
+    /\ Print(<<"From A's perspective, B's overloadedConst is: ", Abstract!overloadedConst>>, TRUE) \* 42
+
+Next == UNCHANGED overloadedName
+
+Correct == Abstract!Spec
+
+==================

tlatools/org.lamport.tlatools/test-model/Github362B.tla

+---- MODULE Github362B ----
+
+\* Auxiliary spec instantiated by Github362.tla.
+
+EXTENDS TLC
+
+CONSTANT C
+
+VARIABLES x
+
+\* This name also exists in Github362.tla with a different definition (it is a
+\* variable rather than a user-defined operator).  The definition in Github362
+\* should not conflict with this one.
+overloadedName == x
+
+overloadedConst == C
+
+Init ==
+    /\ Print(<<"Evaluating initial state in B; overloadedName is ", overloadedName>>, TRUE) \* x
+    /\ overloadedName = "x" \* overloadedName -> variable x -> value "x"
+    /\ x = "x"
+    /\ Print(<<"Evaluating initial state in B; overloadedConst is ", overloadedConst>>, TRUE) \* 42
+    /\ overloadedConst = 42 \* overloadedConst -> const C -> 42
+    /\ C = 42
+
+Next == UNCHANGED x
+Spec == Init /\ [][Next]_x
+
+==================

tlatools/org.lamport.tlatools/test/tlc2/tool/Github362Test.java

+/*******************************************************************************
+ * Copyright (c) 2019 Microsoft Research. All rights reserved.
+ *
+ * The MIT License (MIT)
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+ * of the Software, and to permit persons to whom the Software is furnished to do
+ * so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * Contributors:
+ *   Markus Alexander Kuppe - initial API and implementation
+ ******************************************************************************/
+package tlc2.tool;
+
+import static org.junit.Assert.assertTrue;
+
+import org.junit.Test;
+
+import tlc2.output.EC;
+import tlc2.output.EC.ExitStatus;
+import tlc2.tool.liveness.ModelCheckerTestCase;
+import util.TestPrintStream;
+import util.ToolIO;
+
+public class Github362Test extends ModelCheckerTestCase {
+
+  private TestPrintStream testPrintStream;
+
+  public Github362Test() {
+    super("Github362", ExitStatus.SUCCESS);
+  }
+
+  @Override
+  public void beforeSetUp() {
+    testPrintStream = new TestPrintStream();
+    ToolIO.out = testPrintStream;
+  }
+
+  @Test
+  public void testSpec() {
+    testPrintStream.assertSubstring("<<\"Evaluated initial state in A; overloadedName is: \", \"fizzbuzz\">>");
+    testPrintStream.assertSubstring("<<\"From A's perspective, B's overloadedName is: \", \"x\">>");
+    testPrintStream.assertSubstring("<<\"Evaluating initial state in B; overloadedName is \", \"x\">>");
+
+    testPrintStream.assertSubstring("<<\"Evaluated initial state in A; overloadedConst is: \", 4711>>");
+    testPrintStream.assertSubstring("<<\"From A's perspective, B's overloadedConst is: \", 42>>");
+    testPrintStream.assertSubstring("<<\"Evaluating initial state in B; overloadedConst is \", 42>>");
+    
+    assertTrue(recorder.recorded(EC.TLC_FINISHED));
+    assertTrue(recorder.recorded(EC.TLC_SUCCESS));
+  }
+
+}