merging ...

muenchnerkindl · muenchnerkindl · commit ef25caf1a3b9 · 2022-03-06T18:24:35.000+01:00
diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
@@ -8,15 +8,5 @@
       "vscjava.vscode-java-pack"
     ],
   
-    // - Do not automatically update extensions (E.g. better-code ext is patched for TLA+)
-    // - Use Java GC that works best with TLC.
-    // - https://github.com/alygin/vscode-tlaplus/wiki/Automatic-Module-Parsing
-    "settings": {
-      "tlaplus.tlc.statisticsSharing": "share",
-      "tlaplus.java.options": "-XX:+UseParallelGC",
-      "tlaplus.java.home": "/home/codespace/.java/current/",
-      "[tlaplus]": {"editor.codeActionsOnSave": {"source": true} }
-      },
-  
     "postCreateCommand": "bash -i .devcontainer/install.sh",
   }
diff --git a/.devcontainer/install.sh b/.devcontainer/install.sh
@@ -12,6 +12,12 @@ wget -qN https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.j
 echo "alias tlcrepl='java -cp /workspace/ewd998/tools/tla2tools.jar:/workspaces/ewd998/tools/tla2tools.jar tlc2.REPL'" >> $HOME/.bashrc
 echo "alias tlc='java -cp /workspace/ewd998/tools/tla2tools.jar:/workspaces/ewd998/tools/tla2tools.jar tlc2.TLC'" >> $HOME/.bashrc
 
+## Install Apache Ant that builds CommunityModules (see build.xml)
+sudo apt-get install -y ant
+
+## Do initial build
+ant -d -f build.xml
+
 ## Install TLAPS (proof system)
 wget -N https://github.com/tlaplus/tlapm/releases/download/v1.4.5/tlaps-1.4.5-x86_64-linux-gnu-inst.bin -P /tmp
 chmod +x /tmp/tlaps-1.4.5-x86_64-linux-gnu-inst.bin
@@ -24,9 +30,3 @@ mkdir -p tools/apalache
 tar xvfz /tmp/apalache.tgz --directory tools/apalache/
 echo 'export PATH=$PATH:/workspace/ewd998/tools/apalache/bin:/workspaces/ewd998/tools/apalache/bin' >> $HOME/.bashrc
 tools/apalache/bin/apalache-mc config --enable-stats=true
-
-## Install Apache Ant that builds CommunityModules (see build.xml)
-sudo apt-get install -y ant
-
-## Do initial build
-ant -f build.xml
diff --git a/.gitignore b/.gitignore
@@ -1,6 +1,9 @@
 tlc/
 dist/
 build/
+tests/*.out
 *.toolbox/
 *.tlaps/
 states/
+tools/
+_apalache-out/
diff --git a/.gitpod.yml b/.gitpod.yml
@@ -0,0 +1,7 @@
+tasks:
+  - init: sudo ln -s /workspace /workspaces && sdk install ant && bash -i .devcontainer/install.sh
+
+vscode:
+  extensions:
+    - alygin.vscode-tlaplus-nightly
+    - vscjava.vscode-java-pack
diff --git a/.project b/.project
@@ -14,4 +14,15 @@
 	<natures>
 		<nature>org.eclipse.jdt.core.javanature</nature>
 	</natures>
+	<filteredResources>
+		<filter>
+			<id>1644339741492</id>
+			<name></name>
+			<type>30</type>
+			<matcher>
+				<id>org.eclipse.core.resources.regexFilterMatcher</id>
+				<arguments>node_modules|.git|__CREATED_BY_JAVA_LANGUAGE_SERVER__</arguments>
+			</matcher>
+		</filter>
+	</filteredResources>
 </projectDescription>
diff --git a/.smoke/SmokeBagsExt.cfg b/.smoke/SmokeBagsExt.cfg
@@ -0,0 +1 @@
+
diff --git a/.smoke/SmokeBagsExt.tla b/.smoke/SmokeBagsExt.tla
@@ -0,0 +1,4 @@
+------------------------- MODULE SmokeBagsExt -------------------------
+EXTENDS BagsExtTests
+
+=============================================================================
diff --git a/.smoke/SmokeBagsExtTests.cfg b/.smoke/SmokeBagsExtTests.cfg
@@ -0,0 +1 @@
+
diff --git a/.smoke/SmokeBagsExtTests.tla b/.smoke/SmokeBagsExtTests.tla
@@ -0,0 +1,4 @@
+------------------------- MODULE SmokeBagsExtTests -------------------------
+EXTENDS BagsExtTests
+
+=============================================================================
diff --git a/.smoke/SmokeBitwise.cfg b/.smoke/SmokeBitwise.cfg
@@ -0,0 +1 @@
+
diff --git a/.smoke/SmokeBitwise.tla b/.smoke/SmokeBitwise.tla
@@ -0,0 +1,4 @@
+---------------------------- MODULE SmokeBitwise ----------------------------
+EXTENDS BitwiseTests
+
+=============================================================================
diff --git a/.smoke/SmokeBitwiseTests.cfg b/.smoke/SmokeBitwiseTests.cfg
@@ -0,0 +1 @@
+
diff --git a/.smoke/SmokeBitwiseTests.tla b/.smoke/SmokeBitwiseTests.tla
@@ -0,0 +1,4 @@
+---------------------------- MODULE SmokeBitwiseTests ----------------------------
+EXTENDS BitwiseTests
+
+=============================================================================
diff --git a/.smoke/SmokeCSV.cfg b/.smoke/SmokeCSV.cfg
@@ -0,0 +1 @@
+
diff --git a/.smoke/SmokeCSV.tla b/.smoke/SmokeCSV.tla
@@ -0,0 +1,5 @@
+---------------------------- MODULE SmokeCSV ----------------------------
+EXTENDS CSVTests
+  
+=============================================================================
+                                                                    
diff --git a/.smoke/SmokeCSVTests.cfg b/.smoke/SmokeCSVTests.cfg
@@ -0,0 +1 @@
+
diff --git a/.smoke/SmokeCSVTests.tla b/.smoke/SmokeCSVTests.tla
@@ -0,0 +1,5 @@
+---------------------------- MODULE SmokeCSVTests ----------------------------
+EXTENDS CSVTests
+  
+=============================================================================
+                                                                    
diff --git a/.smoke/SmokeCombinatorics.cfg b/.smoke/SmokeCombinatorics.cfg
@@ -0,0 +1 @@
+
diff --git a/.smoke/SmokeCombinatorics.tla b/.smoke/SmokeCombinatorics.tla
@@ -0,0 +1,4 @@
+------------------------- MODULE SmokeCombinatorics -------------------------
+EXTENDS CombinatoricsTests
+
+=============================================================================
diff --git a/.smoke/SmokeCombinatoricsTests.cfg b/.smoke/SmokeCombinatoricsTests.cfg
@@ -0,0 +1 @@
+
diff --git a/.smoke/SmokeCombinatoricsTests.tla b/.smoke/SmokeCombinatoricsTests.tla
@@ -0,0 +1,4 @@
+------------------------- MODULE SmokeCombinatoricsTests -------------------------
+EXTENDS CombinatoricsTests
+
+=============================================================================
diff --git a/.smoke/SmokeFiniteSetsExt.cfg b/.smoke/SmokeFiniteSetsExt.cfg
@@ -0,0 +1 @@
+
diff --git a/.smoke/SmokeFiniteSetsExt.tla b/.smoke/SmokeFiniteSetsExt.tla
@@ -0,0 +1,4 @@
+------------------------- MODULE SmokeFiniteSetsExt -------------------------
+EXTENDS FiniteSetsExtTests
+
+=============================================================================
diff --git a/.smoke/SmokeFiniteSetsExtTests.cfg b/.smoke/SmokeFiniteSetsExtTests.cfg
@@ -0,0 +1 @@
+
diff --git a/.smoke/SmokeFiniteSetsExtTests.tla b/.smoke/SmokeFiniteSetsExtTests.tla
@@ -0,0 +1,4 @@
+------------------------- MODULE SmokeFiniteSetsExtTests -------------------------
+EXTENDS FiniteSetsExtTests
+
+=============================================================================
diff --git a/.smoke/SmokeFolds.cfg b/.smoke/SmokeFolds.cfg
@@ -0,0 +1 @@
+
diff --git a/.smoke/SmokeFolds.tla b/.smoke/SmokeFolds.tla
@@ -0,0 +1,4 @@
+----------------------------- MODULE SmokeFolds ----------------------------
+EXTENDS FoldsTests
+
+=============================================================================
diff --git a/.smoke/SmokeFoldsTests.cfg b/.smoke/SmokeFoldsTests.cfg
@@ -0,0 +1 @@
+
diff --git a/.smoke/SmokeFoldsTests.tla b/.smoke/SmokeFoldsTests.tla
@@ -0,0 +1,4 @@
+----------------------------- MODULE SmokeFoldsTests ----------------------------
+EXTENDS FoldsTests
+
+=============================================================================
diff --git a/.smoke/SmokeFunctions.cfg b/.smoke/SmokeFunctions.cfg
@@ -0,0 +1 @@
+
diff --git a/.smoke/SmokeFunctions.tla b/.smoke/SmokeFunctions.tla
@@ -0,0 +1,4 @@
+------------------------- MODULE SmokeFunctions -------------------------
+EXTENDS FunctionsTests
+
+=============================================================================
diff --git a/.smoke/SmokeFunctionsTests.cfg b/.smoke/SmokeFunctionsTests.cfg
@@ -0,0 +1 @@
+
diff --git a/.smoke/SmokeFunctionsTests.tla b/.smoke/SmokeFunctionsTests.tla
@@ -0,0 +1,4 @@
+------------------------- MODULE SmokeFunctionsTests -------------------------
+EXTENDS FunctionsTests
+
+=============================================================================
diff --git a/.smoke/SmokeGraphs.cfg b/.smoke/SmokeGraphs.cfg
@@ -0,0 +1 @@
+
diff --git a/.smoke/SmokeGraphs.tla b/.smoke/SmokeGraphs.tla
@@ -0,0 +1,7 @@
+------------------------- MODULE SmokeGraphs -------------------------
+EXTENDS GraphsTests
+
+=====================================================================
+\* Modification History
+\* Last modified Tue Dec 21 15:55:45 PST 2021 by Markus Kuppe
+\* Created Mon Dec 20 20:55:45 PST 2021 by Markus Kuppe
diff --git a/.smoke/SmokeGraphsTests.cfg b/.smoke/SmokeGraphsTests.cfg
@@ -0,0 +1 @@
+
diff --git a/.smoke/SmokeGraphsTests.tla b/.smoke/SmokeGraphsTests.tla
@@ -0,0 +1,7 @@
+------------------------- MODULE SmokeGraphsTests -------------------------
+EXTENDS GraphsTests
+
+=====================================================================
+\* Modification History
+\* Last modified Tue Dec 21 15:55:45 PST 2021 by Markus Kuppe
+\* Created Mon Dec 20 20:55:45 PST 2021 by Markus Kuppe
diff --git a/.smoke/SmokeSequencesExt.cfg b/.smoke/SmokeSequencesExt.cfg
@@ -0,0 +1 @@
+
diff --git a/.smoke/SmokeSequencesExt.tla b/.smoke/SmokeSequencesExt.tla
@@ -0,0 +1,4 @@
+------------------------- MODULE SmokeSequencesExt -------------------------
+EXTENDS SequencesExtTests
+
+=============================================================================
diff --git a/.smoke/SmokeSequencesExtTests.cfg b/.smoke/SmokeSequencesExtTests.cfg
@@ -0,0 +1 @@
+
diff --git a/.smoke/SmokeSequencesExtTests.tla b/.smoke/SmokeSequencesExtTests.tla
@@ -0,0 +1,4 @@
+------------------------- MODULE SmokeSequencesExtTests -------------------------
+EXTENDS SequencesExtTests
+
+=============================================================================
diff --git a/.vscode/launch.json b/.vscode/launch.json
@@ -0,0 +1,23 @@
+{
+    // Run TLC's Java VM with -Xdebug -Xrunjdwp:transport=dt_socket,server=y,suspend=n,address=8000
+    "version": "0.2.0",
+    "configurations": [
+        {
+            "type": "java",
+            "name": "Debug Java Module Override",
+            "request": "attach",
+            "hostName": "localhost",
+            "port": "${input:portPrompt}"
+            // vscode-java's process picker broken https://github.com/microsoft/vscode-java-debug/issues/1121
+            // "processId": "${command:PickJavaProcess}"
+        }
+    ],
+    "inputs": [
+        {
+            "id": "portPrompt",
+            "description": "Please enter the port of TLC's Java VM",
+            "default": "8080",
+            "type": "promptString"
+        }
+    ]
+}
diff --git a/.vscode/settings.json b/.vscode/settings.json
@@ -0,0 +1,15 @@
+{
+    "tlaplus.smoke.prefix.path": "../.smoke/",
+    "tlaplus.smoke.prefix.name": "Smoke",
+    "tlaplus.tlc.modelChecker.options": "-deadlock -noTE",
+    "tlaplus.java.options": "-XX:+UseParallelGC -agentlib:jdwp=transport=dt_socket,server=y,suspend=n,address=0 -DTLA-Library=/workspaces/CommunityModules/.smoke/:/workspaces/CommunityModules/modules/:/workspaces/CommunityModules/tests -Dtlc2.overrides.TLCOverrides=tlc2.overrides.TLCOverrides -cp /workspaces/CommunityModules/tlc/tla2tools.jar:/workspaces/CommunityModules/build/modules:/workspaces/CommunityModules/build/deps",
+    "[tlaplus]": {"editor.codeActionsOnSave": {"source": true} },
+    "breadcrumbs.enabled": false,
+    "editor.minimap.enabled": false,
+    "editor.useTabStops": false,
+    "files.exclude": {
+        "tools": true,
+        "*/states/": true,
+        "_apalache-out/": true
+    }
+}
diff --git a/build.xml b/build.xml
@@ -54,6 +54,8 @@
 		</unzip>
 		<unzip src="lib/jgrapht-core-1.5.1.jar" dest="${build}/deps">
 			<patternset>
+				<!-- https://github.com/jgrapht/jgrapht/issues/1112 -->
+		        <exclude name="**/*rensenIndexLinkPrediction.class"/>
 		        <include name="**/*.class"/>
 			</patternset>
 		</unzip>
diff --git a/modules/tlc2/overrides/BagsExt.java b/modules/tlc2/overrides/BagsExt.java
@@ -25,60 +25,49 @@
  ******************************************************************************/
 package tlc2.overrides;
 
-import java.util.Arrays;
-
-import tlc2.module.Bags;
 import tlc2.output.EC;
 import tlc2.tool.EvalControl;
 import tlc2.tool.EvalException;
 import tlc2.value.Values;
-// import tlc2.value.impl.Applicable;
-// import tlc2.value.impl.BoolValue;
-// import tlc2.value.impl.Enumerable;
 import tlc2.value.impl.FcnRcdValue;
+import tlc2.value.impl.IntValue;
 import tlc2.value.impl.OpValue;
-// import tlc2.value.impl.SetOfRcdsValue;
-// import tlc2.value.impl.TupleValue;
 import tlc2.value.impl.Value;
-import tlc2.value.impl.IntValue;
-// import tlc2.value.impl.ValueEnumeration;
 
 public final class BagsExt {
-	
+
 	private BagsExt() {
 		// no-instantiation!
 	}
-	
+
 	@TLAPlusOperator(identifier = "FoldBag", module = "BagsExt", warn = false)
 	public static Value foldBag(final OpValue op, final Value base, final Value bag) {
 		// Can assume type of OpValue because tla2sany.semantic.Generator.java will
 		// make sure that the first parameter is a binary operator.
 
-            FcnRcdValue bfcn = (FcnRcdValue) bag.toFcnRcd();
-            if (bfcn == null) {
-                throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
-                                        new String[] { "third", "FoldBag", "bag",
-                                                       Values.ppr(bag.toString()) });
-            }
+		FcnRcdValue bfcn = (FcnRcdValue) bag.toFcnRcd();
+		if (bfcn == null) {
+			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
+					new String[] { "third", "FoldBag", "bag", Values.ppr(bag.toString()) });
+		}
 
-            final Value[] domain = bfcn.getDomainAsValues();
-            final Value[] values = bfcn.values;
-            final Value acc[] = new Value[2];
-            acc[0] = base;
+		final Value[] domain = bfcn.getDomainAsValues();
+		final Value[] values = bfcn.values;
+		final Value acc[] = new Value[2];
+		acc[0] = base;
 
-            for (int i=0; i < domain.length; i++) {
-                acc[1] = domain[i];
-                if (!(values[i] instanceof IntValue) || (((IntValue)values[i]).val <= 0)) {
-                    throw new EvalException(EC.TLC_MODULE_APPLYING_TO_WRONG_VALUE,
-                                            new String[] { "third", "FoldBag", "bag",
-                                                           Values.ppr(bag.toString()) });
-                }
-                for (int j=0; j < ((IntValue)values[i]).val; j++) {
-                    acc[0] = op.apply(acc, EvalControl.Clear);
-                }
-            }
+		for (int i = 0; i < domain.length; i++) {
+			acc[1] = domain[i];
+			if (!(values[i] instanceof IntValue) || (((IntValue) values[i]).val <= 0)) {
+					throw new EvalException(EC.TLC_MODULE_APPLYING_TO_WRONG_VALUE,
+							new String[] { "FoldBag", "an element of Nat", Values.ppr(values[i].toString()) + " (in: "
+									+ Values.ppr(domain[i].toString()) + ":>" + Values.ppr(values[i].toString()) + ")" });
+			}
+			for (int j = 0; j < ((IntValue) values[i]).val; j++) {
+				acc[0] = op.apply(acc, EvalControl.Clear);
+			}
+		}
 
-            return acc[0];
-        }
+		return acc[0];
+	}
 }
-
diff --git a/modules/tlc2/overrides/CommunityModules.java b/modules/tlc2/overrides/CommunityModules.java
@@ -28,6 +28,6 @@
 public abstract class CommunityModules {
 
 	public static final String popularModules() {
-		return String.join(",", "FiniteSetsExt", "Functions", "SequencesExt", "Folds", "IOUtils");
+		return String.join(",", "FiniteSetsExt", "Functions", "SequencesExt", "Folds", "BagsExt", "IOUtils");
 	}
 }
diff --git a/tests/BagsExtTests.tla b/tests/BagsExtTests.tla
@@ -4,7 +4,7 @@ NEXT Next
 =====
 
 ---------------------------- MODULE BagsExtTests ----------------------------
-EXTENDS Integers, TLC, Bags, BagsExt
+EXTENDS Integers, TLC, Bags, BagsExt, Sequences, TLCExt
 
 ASSUME LET T == INSTANCE TLC IN T!PrintT("BagsExtTests")
 
@@ -60,6 +60,16 @@ ASSUME SumBag((1:>2) @@ (-2:>1)) = 0
 
 ASSUME ProductBag((1:>2) @@ (-2:>1)) = -2
 
+ASSUME FoldBag(LAMBDA x,y : Append(x, y), <<>>, SetToBag({"a", "b"}) (+) SetToBag({"a"})) = <<"a", "a", "b">>
+
+ASSUME AssertError(
+           "Applying FoldBag to the following value,\nwhich is not an element of Nat:\n-1 (in: \"b\":>-1)", 
+           ProductBag(("b":>-1)) = 42)
+
+ASSUME AssertError(
+           "The third argument of FoldBag should be a bag, but instead it is:\n42", 
+           ProductBag(42) = 42)
+
 (***************************************************************************)
 (* The two following tests fail without the Java override for FoldBag.     *)
 (***************************************************************************)
