IsABag inconsistent with Bags.tla when parameter is not a bag.

[Bug][TLC][Changelog]

tlatools/src/tlc2/module/Bags.java

@@ -35,18 +35,20 @@ public class Bags implements ValueConstants
         return EmptyFcn;
     }
 
-    public static BoolValue IsABag(Value b)
+    public static BoolValue IsABag(final Value b)
     {
-        FcnRcdValue fcn = FcnRcdValue.convert(b);
+        final FcnRcdValue fcn = FcnRcdValue.convert(b);
         if (fcn == null)
         {
-            throw new EvalException(EC.TLC_MODULE_APPLYING_TO_WRONG_VALUE, new String[] { "IsBag",
-                    "a function with a finite domain", Value.ppr(b.toString()) });
+        	// MAK 02/23/2018 Changed to return ValFalse instead of exception when Value is not a bag.
+            //throw new EvalException(EC.TLC_MODULE_APPLYING_TO_WRONG_VALUE, new String[] { "IsBag",
+            //        "a function with a finite domain", Value.ppr(b.toString()) });
+        	return ValFalse;
         }
-        Value[] vals = fcn.values;
+        final Value[] vals = fcn.values;
         for (int i = 0; i < vals.length; i++)
         {
-            if (!(vals[i] instanceof IntValue) || ((IntValue) vals[i]).val < 0)
+            if (!(vals[i] instanceof IntValue) || ((IntValue) vals[i]).val <= 0)
             {
                 return ValFalse;
             }

tlatools/test-model/BagsTest.cfg

 SPECIFICATION
 Spec
+CONSTANT
+C = C
\ No newline at end of file

tlatools/test-model/BagsTest.tla

 ---------------------------- MODULE BagsTest ----------------------------
 EXTENDS Bags, TLC, Integers
 
+CONSTANT C
+
 strings == {"a","b","c","d","e","f","g","h","i","j","k","l","m","n","o"}
 
 s == {"a","b","c"}
@@ -26,18 +28,26 @@ ASSUME(IsABag(f))
 ASSUME(IsABag(g))
 ASSUME(IsABag(h))
 
+ASSUME(IsABag(SetToBag({})))
+
 t == <<0>>
 u == 2 :> -1
-v == <<0>>
+v == <<1,0>>
 w == <<0,1>>
 x == <<0,0,0>>
 y == <<-1,-2,-3>>
 z == <<"a","b","c">>
 
+ASSUME(~IsABag(t))
 ASSUME(~IsABag(u))
+ASSUME(~IsABag(v))
+ASSUME(~IsABag(w))
+ASSUME(~IsABag(x))
 ASSUME(~IsABag(y))
-\*ASSUME(~IsABag(z)) \* With the standard module TLC fails with "Cannot decide if element "a" is element of Nat"
+ASSUME(~IsABag(z)) \* With the standard module TLC fails with "Cannot decide if element "a" is element of Nat"
 
+ASSUME(\A bool \in BOOLEAN : ~IsABag(bool))
+ASSUME(~IsABag(C))	
 
 \* BagCardinality
 ASSUME(BagCardinality(a) = 0)