Some operators in the Bags module return an error when evaluated on any

arguments

This fix treats Bags.tla as the single source of truth.

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

[Bug][TLC]

tlatools/src/tlc2/module/Bags.java

@@ -86,12 +86,11 @@ public class Bags implements ValueConstants
         return IntValue.gen(num);
     }
 
-    public static BoolValue BagIn(Value e, Value b)
+    public static BoolValue BagIn(final Value e, final Value b)
     {
-        FcnRcdValue fcn = FcnRcdValue.convert(b);
-        Value[] domain = fcn.domain;
-        Value[] values = fcn.values;
-        // Value val; // SZ: variable never read locally
+        final FcnRcdValue fcn = FcnRcdValue.convert(b);
+        final Value[] values = fcn.values;
+        final Value[] domain = fcn.getDomainAsValues();
         for (int i = 0; i < domain.length; i++)
         {
             if (e.equals(domain[i]))
@@ -107,12 +106,11 @@ public class Bags implements ValueConstants
         return ValFalse;
     }
 
-    public static IntValue CopiesIn(Value e, Value b)
+    public static IntValue CopiesIn(final Value e, final Value b)
     {
-        FcnRcdValue fcn = FcnRcdValue.convert(b);
-        Value[] domain = fcn.domain;
-        Value[] values = fcn.values;
-        // Value val; // SZ: variable never read locally
+        final FcnRcdValue fcn = FcnRcdValue.convert(b);
+        final Value[] values = fcn.values;
+        final Value[] domain = fcn.getDomainAsValues();
         for (int i = 0; i < domain.length; i++)
         {
             if (e.equals(domain[i]))
@@ -142,9 +140,9 @@ public class Bags implements ValueConstants
             throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "second", "(+)", "bag",
                     Value.ppr(b2.toString()) });
         }
-        Value[] domain1 = fcn1.domain;
+        Value[] domain1 = fcn1.getDomainAsValues();
         Value[] values1 = fcn1.values;
-        Value[] domain2 = fcn2.domain;
+        Value[] domain2 = fcn2.getDomainAsValues();
         Value[] values2 = fcn2.values;
         Vect dVec = new Vect(domain1.length);
         Vect vVec = new Vect(domain1.length);
@@ -197,9 +195,9 @@ public class Bags implements ValueConstants
             throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "second", "(-)", "bag",
                     Value.ppr(b2.toString()) });
         }
-        Value[] domain1 = fcn1.domain;
+        Value[] domain1 = fcn1.getDomainAsValues();
         Value[] values1 = fcn1.values;
-        Value[] domain2 = fcn2.domain;
+        Value[] domain2 = fcn2.getDomainAsValues();
         Value[] values2 = fcn2.values;
         Vect dVec = new Vect(domain1.length);
         Vect vVec = new Vect(domain1.length);
@@ -231,9 +229,9 @@ public class Bags implements ValueConstants
         return new FcnRcdValue(domain, values, fcn1.isNormalized());
     }
 
-    public static Value BagUnion(Value s)
+    public static Value BagUnion(final Value s)
     {
-        SetEnumValue s1 = SetEnumValue.convert(s);
+        final SetEnumValue s1 = SetEnumValue.convert(s);
         if (s1 == null)
         {
             throw new EvalException(EC.TLC_MODULE_APPLYING_TO_WRONG_VALUE, new String[] { "BagUnion",
@@ -241,10 +239,12 @@ public class Bags implements ValueConstants
         }
         ValueVec elems = s1.elems;
         int sz = elems.size();
-        if (sz == 0)
+        if (sz == 0) {
         	return EmptyFcn;
-        if (sz == 1)
+        }
+        if (sz == 1) {
         	return elems.elementAt(0);
+        }
         ValueVec dVec = new ValueVec();
         ValueVec vVec = new ValueVec();
         FcnRcdValue fcn = FcnRcdValue.convert(elems.elementAt(0));
@@ -252,7 +252,7 @@ public class Bags implements ValueConstants
         {
             throw new EvalException(EC.TLC_MODULE_BAG_UNION1, Value.ppr(s.toString()));
         }
-        Value[] domain = fcn.domain;
+        Value[] domain = fcn.getDomainAsValues();
         Value[] values = fcn.values;
         for (int i = 0; i < domain.length; i++)
         {
@@ -267,7 +267,7 @@ public class Bags implements ValueConstants
 
                 throw new EvalException(EC.TLC_MODULE_BAG_UNION1, Value.ppr(s.toString()));
             }
-            domain = fcn.domain;
+            domain = fcn.getDomainAsValues();
             values = fcn.values;
             for (int j = 0; j < domain.length; j++)
             {
@@ -315,9 +315,9 @@ public class Bags implements ValueConstants
             throw new EvalException(EC.TLC_MODULE_APPLYING_TO_WRONG_VALUE, new String[] { "\\sqsubseteq",
                     "a function with a finite domain", Value.ppr(b2.toString()) });
         }
-        Value[] domain1 = fcn1.domain;
+        Value[] domain1 = fcn1.getDomainAsValues();
         Value[] values1 = fcn1.values;
-        Value[] domain2 = fcn2.domain;
+        Value[] domain2 = fcn2.getDomainAsValues();
         Value[] values2 = fcn2.values;
         for (int i = 0; i < domain1.length; i++)
         {
@@ -353,7 +353,7 @@ public class Bags implements ValueConstants
         Applicable ff = (Applicable) f;
         ValueVec dVec = new ValueVec();
         ValueVec vVec = new ValueVec();
-        Value[] domain = fcn.domain;
+        Value[] domain = fcn.getDomainAsValues();
         Value[] values = fcn.values;
         Value[] args = new Value[1];
         for (int i = 0; i < domain.length; i++)

tlatools/src/tlc2/value/FcnRcdValue.java

@@ -8,16 +8,15 @@ package tlc2.value;
 
 import java.util.Arrays;
 
-import tlc2.tool.ModelChecker;
-import tlc2.tool.FingerprintException;
 import tlc2.tool.EvalControl;
+import tlc2.tool.FingerprintException;
 import tlc2.util.FP64;
 import util.Assert;
 
 public class FcnRcdValue extends Value implements Applicable {
-  public Value[] domain;
-  public IntervalValue intv;
-  public Value[] values;
+  public final Value[] domain;
+  public final IntervalValue intv;
+  public final Value[] values;
   private boolean isNorm;
   private int[] indexTbl;  // speed up function application
 
@@ -433,6 +432,18 @@ public class FcnRcdValue extends Value implements Applicable {
     }
   }
 
+  /**
+   * Returns the domain of this FunctionRecordValue regardless of its internal
+   * representation as either Value[] or IntervalValue as Value[].
+   */
+  public Value[] getDomainAsValues() {
+	  if (this.intv != null) {
+		  return this.intv.asValues();
+	  } else {
+          return this.domain;		  
+	  }
+  }
+  
   public final int size() {
     try {
       this.normalize();

tlatools/src/tlc2/value/IntervalValue.java

@@ -6,7 +6,6 @@
 
 package tlc2.value;
 
-import tlc2.tool.ModelChecker;
 import tlc2.tool.FingerprintException;
 import tlc2.util.FP64;
 import util.Assert;
@@ -106,6 +105,19 @@ implements Enumerable, Reducible {
     }
   }
 
+	/**
+	 * @return Converts this IntervalValue instance into a Value[]. This can be seen
+	 *         as the inverse to the performance optimization that the IntervalValue
+	 *         actually is.
+	 */
+	final Value[] asValues() {
+		final Value[] values = new Value[size()];
+		for (int i = 0; i < size(); i++) {
+			values[i] = IntValue.gen(this.low + i);
+		}
+		return values;
+	}
+  
   /* Return this - val.  */
   public final Value diff(Value val) {
     try {

tlatools/src/tlc2/value/SetEnumValue.java

@@ -429,6 +429,13 @@ implements Enumerable, Reducible {
       // used only for printing the value, it seems that correcting this should
       // not do any harm.  Therefore, LL added the following if statement
       // on 5 Mar 2012.
+      // Beware:
+      // normalize() mutates a SetEnumValue's state. Thus calling toString() 
+      // on a SetEnumValue mutates its state. By convention, toString methods
+      // generally do not mutate an instance's state (side-effect free) and
+      // and are thus safe to be called. Failing to adhere to this convention
+      // can lead to subtle bugs. E.g. think of a programmer who inspects an
+      // instance with a debugger unconsciously mutating the instance's state.
       if (!this.isNormalized()) {
           this.normalize();
       }

tlatools/src/tlc2/value/TupleValue.java

@@ -7,7 +7,6 @@
 package tlc2.value;
 
 import tla2sany.semantic.SymbolNode;
-import tlc2.tool.ModelChecker;
 import tlc2.tool.FingerprintException;
 import tlc2.output.EC;
 import tlc2.output.MP;

tlatools/test-model/BagsTest.cfg

+SPECIFICATION
+Spec

tlatools/test-model/BagsTest.tla

+---------------------------- MODULE BagsTest ----------------------------
+EXTENDS Bags, TLC, Integers
+
+strings == {"a","b","c","d","e","f","g","h","i","j","k","l","m","n","o"}
+
+s == {"a","b","c"}
+
+a == <<>>
+b == <<1,2,3>>
+c == <<2,3,4>>
+d == <<1,1,1>>
+e == 1 :> 1
+f == 2 :> 1
+g == [x \in {1,2,3} |-> x * x]
+h == [a |-> 3, b |-> 2, c |-> 1]
+
+ASSUME(EmptyBag = <<>>)
+
+\* IsABag
+ASSUME(IsABag(a))
+ASSUME(IsABag(b))
+ASSUME(IsABag(c))
+ASSUME(IsABag(d))
+ASSUME(IsABag(e))
+ASSUME(IsABag(f))
+ASSUME(IsABag(g))
+ASSUME(IsABag(h))
+
+t == <<0>>
+u == 2 :> -1
+v == <<0>>
+w == <<0,1>>
+x == <<0,0,0>>
+y == <<-1,-2,-3>>
+z == <<"a","b","c">>
+
+ASSUME(~IsABag(u))
+ASSUME(~IsABag(y))
+\*ASSUME(~IsABag(z)) \* With the standard module TLC fails with "Cannot decide if element "a" is element of Nat"
+
+
+\* BagCardinality
+ASSUME(BagCardinality(a) = 0)
+ASSUME(BagCardinality(b) = 6)
+ASSUME(BagCardinality(c) = 9)
+ASSUME(BagCardinality(d) = 3)
+ASSUME(BagCardinality(e) = 1)
+ASSUME(BagCardinality(f) = 1)
+ASSUME(BagCardinality(g) = (1*1+2*2+3*3))
+ASSUME(BagCardinality(h) = 6)
+
+ASSUME(BagCardinality(<<1>>) = 1)
+ASSUME(BagCardinality(<<1,3>>) = 4)
+
+\* BagIn
+ASSUME(\A elem \in 1..10: ~BagIn(elem, a))
+ASSUME(\A elem \in 1..3: BagIn(elem, b))
+ASSUME(\A elem \in 4..10: ~BagIn(elem, b))
+ASSUME(\A dom \in DOMAIN c: BagIn(dom, c))
+ASSUME(\A dom \in DOMAIN d: BagIn(dom, d))
+ASSUME(\A dom \in DOMAIN e: BagIn(dom, e))
+ASSUME(\A dom \in DOMAIN f: BagIn(dom, f))
+ASSUME(\A dom \in DOMAIN f: BagIn(dom, f))
+ASSUME(\A dom \in DOMAIN g: BagIn(dom, g))
+ASSUME(\A dom \in DOMAIN h: BagIn(dom, h))
+ASSUME(\A str \in (strings \ DOMAIN h): ~BagIn(str, h))
+ASSUME(\A elem \in s : BagIn(elem, SetToBag(s)))
+
+
+\* SetToBag and BagToSet
+Codomain(fun) == {fun[i] : i \in DOMAIN fun}  
+ASSUME(SetToBag(s) = [elem \in s |-> 1])
+ASSUME(DOMAIN SetToBag(s) = s)
+ASSUME(Codomain(SetToBag(s)) = {1})
+ASSUME(BagToSet(SetToBag(s)) = s)
+
+ASSUME(BagToSet(a) = {})
+ASSUME(BagToSet(b) = DOMAIN b)
+ASSUME(BagToSet(c) = DOMAIN c)
+ASSUME(BagToSet(d) = DOMAIN d)
+ASSUME(BagToSet(e) = {1})
+ASSUME(BagToSet(f) = {2})
+ASSUME(BagToSet(g) = DOMAIN g)
+ASSUME(BagToSet(h) = s)
+
+
+\* CopiesIn
+ASSUME(\A str \in strings: CopiesIn(str, a) = 0)
+
+ASSUME(\A dom \in DOMAIN b: CopiesIn(dom, b) = b[dom])
+ASSUME(\A elem \in 5..10: CopiesIn(elem, b) = 0)
+ASSUME(\A dom \in DOMAIN c: CopiesIn(dom, c) = c[dom])
+ASSUME(\A elem \in 5..10: CopiesIn(elem, c) = 0)
+ASSUME(\A dom \in DOMAIN d: CopiesIn(dom, d) = d[dom])
+ASSUME(\A elem \in 5..10: CopiesIn(elem, d) = 0)
+
+ASSUME(CopiesIn(1, e) = 1)
+ASSUME(CopiesIn(2, f) = 1)
+ASSUME(CopiesIn(1, f) = 0)
+ASSUME(CopiesIn(1, 1 :> 0) = 0)
+ASSUME(CopiesIn(2, 2 :> -1) = -1)
+
+ASSUME(\A dom \in DOMAIN g: CopiesIn(dom, g) = dom * dom)
+
+ASSUME(CopiesIn("a", h) = 3)
+ASSUME(CopiesIn("b", h) = 2)
+ASSUME(CopiesIn("c", h) = 1)
+ASSUME(\A str \in (strings \ DOMAIN h): CopiesIn(str, h) = 0)
+
+ASSUME(\A aelem \in s: CopiesIn(aelem, [elem \in s |-> 42]) = 42)
+ASSUME(\A aelem \in s: CopiesIn(aelem, [elem \in s |-> 0]) = 0)
+
+
+\* (+)
+ASSUME(EmptyBag (+) EmptyBag = EmptyBag)
+ASSUME(a (+) a = a)
+ASSUME(b (+) b = <<2,4,6>>)
+ASSUME(b (+) EmptyBag = b)
+ASSUME(c (+) c = <<4,6,8>>)
+ASSUME(d (+) d = <<2,2,2>>)
+ASSUME(e (+) e = <<2>>)
+ASSUME(b (+) c = c (+) b)
+ASSUME(b (+) c = <<3,5,7>>)
+ASSUME(h (+) h = [a |-> 6, b |-> 4, c |-> 2])
+ASSUME([c |-> 3, d |-> 2, e |-> 1] (+) h = [a |-> 3, b |-> 2, c |-> 4, d |-> 2, e |-> 1])
+
+
+\* (-)
+ASSUME(a (-) a = a)
+ASSUME(b (-) b = EmptyBag)
+ASSUME(b (-) EmptyBag = b)
+ASSUME(c (-) c = EmptyBag)
+ASSUME(d (-) d = EmptyBag)
+ASSUME(e (-) e = EmptyBag)
+ASSUME(b (-) c = b (-) c)
+ASSUME(b (-) c = EmptyBag)
+ASSUME(c (-) b = <<1,1,1>>)
+ASSUME([c |-> 3, d |-> 2, e |-> 1] (-) h = [c |-> 2, d |-> 2, e |-> 1])
+ASSUME((1:>1) (-) EmptyBag = <<1>>)
+
+
+\* BagUnion
+ASSUME(BagUnion({a,a}) = a)
+ASSUME(BagUnion({a,b,c,d}) = <<4,6,8>>)
+ASSUME(BagUnion({EmptyBag, EmptyBag}) = <<>>)
+ASSUME(BagUnion({[a |-> 3, b |-> 2, c |-> 1],[c |-> 3, d |-> 2, e |-> 1]}) = [a |-> 3, b |-> 2, c |-> 4, d |-> 2, e |-> 1])
+ASSUME(BagUnion({1 :> 2, 2 :> 2, 3 :> 3}) = (1 :> 2) (+) (2 :> 2) (+) (3 :> 3))
+ASSUME(BagUnion({<<>>, <<1,1,1>>, <<1,2,3,4>>}) = (1:>2 @@ 2:>3 @@ 3:>4 @@ 4:>4))
+
+
+\* \sqsubseteq
+ASSUME((a \sqsubseteq a) = TRUE)
+ASSUME((a \sqsubseteq b) = TRUE)
+ASSUME((a \sqsubseteq c) = TRUE)
+ASSUME((a \sqsubseteq d) = TRUE)
+ASSUME((b \sqsubseteq b) = TRUE)
+ASSUME((c \sqsubseteq c) = TRUE)
+ASSUME((h \sqsubseteq [a |-> 3]) = FALSE)
+ASSUME((h \sqsubseteq [a |-> 3, b |-> 2]) = FALSE)
+ASSUME(([a |-> 3] \sqsubseteq h) = TRUE)
+ASSUME(([a |-> 3, b |-> 2] \sqsubseteq h) = TRUE)
+ASSUME(([a |-> 3, c |-> 1] \sqsubseteq h) = TRUE)
+ASSUME(([b |-> 2, c |-> 1] \sqsubseteq h) = TRUE)
+ASSUME((h \sqsubseteq h) = TRUE)
+
+
+\* BagOfAll
+ASSUME(BagOfAll(LAMBDA elem : elem, a) = a)
+ASSUME(BagOfAll(LAMBDA elem : TRUE, a) = a)
+ASSUME(BagOfAll(LAMBDA elem : elem, h) = h)
+ASSUME(BagOfAll(LAMBDA elem : TRUE, h) = TRUE :> 6)
+ASSUME(BagOfAll(LAMBDA elem : IF elem = "a" THEN "b" ELSE elem, [a |-> 3, b |-> 2, c |-> 1]) = [b |-> 5, c |-> 1])
+
+
+\* SubBag
+\* Module overwrite does not overwrite SubBag
+
+\* A dummy spec to make TLC run model checking as required by BagsTest.java.
+Spec == [][TRUE]_<<>>
+
+=============================================================================

tlatools/test/tlc2/tool/BagsTest.java

+/*******************************************************************************
+ * Copyright (c) 2018 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.assertFalse;
+import static org.junit.Assert.assertTrue;
+
+import org.junit.Test;
+
+import tlc2.output.EC;
+import tlc2.tool.liveness.ModelCheckerTestCase;
+
+public class BagsTest extends ModelCheckerTestCase {
+
+	public BagsTest() {
+		super("BagsTest");
+	}
+
+	@Test
+	public void testSpec() {
+		// ModelChecker has finished and generated the expected amount of states
+		assertTrue(recorder.recorded(EC.TLC_FINISHED));
+		assertFalse(recorder.recorded(EC.GENERAL));
+		assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, "0", "0", "0"));
+	}
+}