Merge pull request #1 from tlaplus/master

Merge changes from upstream

.classpath

@@ -1,11 +1,15 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <classpath>
 	<classpathentry kind="src" path="modules"/>
+	<classpathentry combineaccessrules="false" kind="src" path="/tlatools"/>
 	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER">
 		<attributes>
 			<attribute name="module" value="true"/>
 		</attributes>
 	</classpathentry>
-	<classpathentry combineaccessrules="false" kind="src" path="/tlatools"/>
+	<classpathentry kind="lib" path="tlc/tla2tools.jar"/>
+	<classpathentry kind="lib" path="lib/jackson-annotations-2.10.2.jar"/>
+	<classpathentry kind="lib" path="lib/jackson-core-2.10.2.jar"/>
+	<classpathentry kind="lib" path="lib/jackson-databind-2.10.2.jar"/>
 	<classpathentry kind="output" path="build"/>
 </classpath>

.github/workflows/main.yml

@@ -0,0 +1,56 @@
+name: CI
+
+on: [push]
+
+jobs:
+  build:
+
+    runs-on: ubuntu-latest
+
+    steps:
+    - uses: actions/checkout@v2
+    - name: Set up JDK 1.9
+      uses: actions/setup-java@v1
+      with:
+        java-version: 9.0.x
+    - name: Get current date
+      id: date
+      run: echo "::set-output name=date::$(date +'%Y%m%d%H%M')"
+    # Do not download and install TLAPS over and over again.
+    - uses: actions/cache@v1
+      id: cache
+      with:
+        path: tlaps/
+        key: tlaps1.4.5
+    - name: Get TLAPS
+      if: steps.cache.outputs.cache-hit != 'true' # see actions/cache above
+      run: wget https://tla.msr-inria.inria.fr/tlaps/dist/current/tlaps-1.4.5-x86_64-linux-gnu-inst.bin
+    - name: Install TLAPS
+      if: steps.cache.outputs.cache-hit != 'true' # see actions/cache above
+      run: |
+        chmod +x tlaps-1.4.5-x86_64-linux-gnu-inst.bin
+        ./tlaps-1.4.5-x86_64-linux-gnu-inst.bin -d tlaps
+    - name: Run TLAPS
+      run: tlaps/bin/tlapm --cleanfp -I tlaps/ -I modules/ modules/SequencesExtTheorems_proofs.tla
+    - name: Build with Ant
+      run: ant -noinput -buildfile build.xml -Dtimestamp=${{steps.date.outputs.date}}
+    - name: Create Release
+      id: create_release
+      uses: actions/create-release@v1
+      env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+      with:
+        tag_name: ${{steps.date.outputs.date}}
+        release_name: ${{steps.date.outputs.date}}
+        draft: false
+        prerelease: false
+    - name: Upload Release Asset
+      id: upload-release-asset 
+      uses: actions/[email protected]
+      env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+      with:
+        upload_url: ${{ steps.create_release.outputs.upload_url }}
+        asset_path: dist/CommunityModules-${{steps.date.outputs.date}}.jar
+        asset_name: CommunityModules-${{steps.date.outputs.date}}.jar
+        asset_content_type: application/zip

.gitignore

@@ -1,4 +1,4 @@
-lib/
+tlc/
 dist/
 build/
 *.toolbox/

CNAME

@@ -0,0 +1 @@
+modules.tlapl.us

README.md

@@ -10,11 +10,10 @@ How to use it
 
 Just copy & paste the snippet, the operators or the set of modules you are interested in.
 
-Being a community-driven repository we, as the TLA+ developers, do not take any
-responsibility for the validity and correctness of the submissions. We will
-try to keep this place in order, but we can't guarantee the quality of the
-modules here available and therefore do not provide any assistance on eventual
-malfunctions.
+Alternatively, you can download a [library archive](https://github.com/tlaplus/CommunityModules/releases) and add it to TLC's or the Toolbox's *TLA+ library path*.  The advantage of the library archive is that TLC will evaluate an operator faster if the operator comes with a (Java) implementation (see e.g. [SequencesExt.Java](https://github.com/tlaplus/CommunityModules/blob/master/modules/SequencesExt.java)).  Run TLC with ```-DTLA-Library=/path/to/lib/archive``` or add the library archive to the Toolbox (```File > Preferences > TLA+ Preferences > TLA+ library path locations```).
+
+Being a community-driven repository puts the community in charge to check the validity and correctness of submissions. The maintainers of this repository will try to keep this place in order, but we can't guarantee the quality of the
+modules and therefore cannot provide any assistance on eventual malfunctions.
 
 Contributing
 ------------
@@ -32,4 +31,4 @@ We take the discretion to approve or reject submissions at our will.
 Download
 --------
 
-[![Build Status](https://dev.azure.com/tlaplus/tlaplus/_apis/build/status/tlaplus.CommunityModules?branchName=master)](https://dev.azure.com/tlaplus/tlaplus/_build/latest?definitionId=4&branchName=master)
+![CI](https://github.com/tlaplus/CommunityModules/workflows/CI/badge.svg)

build.xml

@@ -1,39 +1,99 @@
-<project name="CommunityModules" default="dist" basedir=".">
-
-  <property name="src" location="modules/"/>
-  <property name="build" location="build"/>
-  <property name="dist" location="dist"/>
-  <property name="lib" location="lib"/>
-
-  <target name="init" description="Create the build and dist directory structure">
-    <mkdir dir="${build}"/>
-    <mkdir dir="${dist}"/>
-    <mkdir dir="${lib}"/>
-  </target>
-
-  <target name="compile" depends="init" description="compile the java module overwrites">
-    <get src="https://nightly.tlapl.us/dist/tla2tools.jar" dest="${lib}"/>
-    <javac srcdir="${src}" destdir="${build}" classpath="${lib}/tla2tools.jar"
+<project name="CommunityModules" default="test" basedir=".">
+
+	<property name="src" location="modules/"/>
+	<property name="build" location="build"/>
+	<property name="dist" location="dist"/>
+	<property name="lib" location="lib"/>
+	<property name="tests" location="tests"/>
+	<property name="tlc" location="tlc"/>
+
+	<tstamp>
+		<format property="timestamp"
+          pattern="yyyyMMdHHmm"
+          locale="en,UK"/>
+	</tstamp>
+
+	<target name="init" description="Create the build and dist directory structure">
+		<mkdir dir="${build}"/>
+		<mkdir dir="${dist}"/>
+		<mkdir dir="${tlc}"/>
+	</target>
+
+	<target name="download" depends="init" description="downloads tla2tools.jar" unless="skip.download">
+		<get src="https://github.com/tlaplus/tlaplus/releases/download/v1.6.1/tla2tools.jar" dest="${tlc}"/>
+		<!-- https://nightly.tlapl.us/dist/tla2tools.jar -->
+	</target>
+
+	<target name="compile" depends="download" description="compile the java module overwrites">
+		<javac srcdir="${src}" destdir="${build}" classpath="${tlc}/tla2tools.jar:${lib}/jackson-core-2.10.2.jar:${lib}/jackson-databind-2.10.2.jar:${lib}/jackson-annotations-2.10.2.jar"
            source="1.8"
            target="1.8"
            includeantruntime="false"/>
-  </target>
-
-  <target name="dist" depends="compile" description="Combine the module overwrites and the TLA+ definitions into a distribution">
-    <tstamp/>
-    <jar jarfile="${dist}/CommunityModules-${DSTAMP}${TSTAMP}.jar">
-         <fileset dir="${build}/"
-             includes="*.class"/>
-         <fileset dir="${src}/"
+	</target>
+
+	<target name="dist" depends="compile" description="Combine the module overwrites and the TLA+ definitions into a distribution">
+		<tstamp/>
+		<jar jarfile="${dist}/CommunityModules-${timestamp}.jar">
+			<fileset dir="${build}/"
+             includes="**/*.class"/>
+			<fileset dir="${src}/"
              includes="*.tla,*.java"/>
-         <fileset dir="."
+			<fileset dir="."
              includes="LICENSE,README.md"/>
-    </jar>
-  </target>
-
-  <target name="clean" description="Delete the ${build} and ${dist} directory trees">
-    <delete dir="${build}"/>
-    <delete dir="${dist}"/>
-    <delete dir="${lib}"/>
-  </target>
+		</jar>
+	</target>
+
+	<target name="test" depends="dist" description="Run the modules in tests/ on the TLA+ modules in dist/">
+		<!-- If an assert fails, TLC will return a non-zero exit value which is makes the ant target fail. -->
+		<java classname="tlc2.TLC" fork="true" failonerror="true">
+			<!-- Tell Java to use a garbage collector which makes TLC happy. -->
+			<jvmarg value="-XX:+UseParallelGC"/>
+
+			<!-- Report execution statistics as azure-pipelien -->
+			<sysproperty key="tlc2.TLC.ide" value="azure-pipeline"/>
+			<sysproperty key="util.ExecutionStatisticsCollector.id" value="01ed03e40ba44f278a934849dd2b1038"/>
+
+			<arg value="-metadir"/>
+			<arg value="${basedir}/build/states"/>
+			<arg value="-cleanup"/>
+			<arg value="${basedir}/tests/AllTests"/>
+
+			<classpath>
+				<pathelement location="${tlc}/tla2tools.jar" />
+				<pathelement location="${lib}/jackson-core-2.10.2.jar" />
+				<pathelement location="${lib}/jackson-databind-2.10.2.jar" />
+				<pathelement location="${lib}/jackson-annotations-2.10.2.jar" />
+				<!-- The jar that has just been built by the dist target. -->
+				<pathelement location="${dist}/CommunityModules-${timestamp}.jar" />
+			</classpath>
+		</java>
+
+		<!-- If an assert fails, TLC will return a non-zero exit value which is makes the ant target fail. -->
+		<java classname="tlc2.TLC" fork="true" failonerror="true">
+			<!-- Tell Java to use a garbage collector which makes TLC happy. -->
+			<jvmarg value="-XX:+UseParallelGC"/>
+
+			<!-- Report execution statistics as azure-pipelien -->
+			<sysproperty key="tlc2.TLC.ide" value="azure-pipeline"/>
+			<sysproperty key="util.ExecutionStatisticsCollector.id" value="01ed03e40ba44f278a934849dd2b1038"/>
+
+			<arg value="-metadir"/>
+			<arg value="${basedir}/build/states"/>
+			<arg value="-cleanup"/>
+			<arg value="-deadlock"/>
+			<arg value="${basedir}/tests/GH005/TLCExtTrace"/>
+
+			<classpath>
+				<pathelement location="${tlc}/tla2tools.jar" />
+				<!-- The jar that has just been built by the dist target. -->
+				<pathelement location="${dist}/CommunityModules-${timestamp}.jar" />
+			</classpath>
+		</java>
+	</target>
+
+	<target name="clean" description="Delete the ${build}, ${tlc} and ${dist} directory trees">
+		<delete dir="${build}"/>
+		<delete dir="${dist}"/>
+		<delete dir="${tlc}"/>
+	</target>
 </project>

modules/Bitwise.tla

@@ -0,0 +1,35 @@
+------------------------------- MODULE Bitwise -------------------------------
+LOCAL INSTANCE Integers
+
+\* https://en.wikipedia.org/wiki/Bitwise_operation#Mathematical_equivalents
+RECURSIVE And(_,_,_,_)
+LOCAL And(x,y,n,m) == 
+        LET exp == 2^n
+        IN IF m = 0 
+           THEN 0
+           ELSE exp * ((x \div exp) % 2) * ((y \div exp) % 2) 
+                    + And(x,y,n+1,m \div 2)
+
+x & y == 
+    (***************************************************************************)
+    (* Bitwise AND of (non-negative) x and y (defined for Nat \cup {0}).       *)
+    (***************************************************************************)
+    And(x, y, 0, x) \* Infix variant of And(x,y)
+
+
+RECURSIVE shiftR(_,_)
+shiftR(n,pos) == 
+    (***************************************************************************)
+    (* Logical bit-shifting the (non-negative) n by pos positions to the right *)
+    (* shifting zeros in from the left/MSB (defined for Nat \cup {0}).         *)
+    (***************************************************************************)
+    IF pos = 0 
+    THEN n
+    ELSE LET odd(z) == z % 2 = 1
+             m == IF odd(n) THEN (n-1) \div 2 ELSE n \div 2
+         IN shiftR(m, pos - 1)
+
+=============================================================================
+\* Modification History
+\* Last modified Thu April 25 10:56:12 CEST 2018 by markus
+\* Created Mon May 16 15:09:18 CEST 2016 by markus

modules/DifferentialEquations.tla

@@ -0,0 +1,36 @@
+----------------------- MODULE DifferentialEquations ------------------------
+LOCAL INSTANCE Reals
+LOCAL INSTANCE Sequences
+LOCAL PosReal == {r \in Real : r > 0}
+LOCAL OpenInterval(a, b) == {s \in Real : a < s /\ s < b}
+LOCAL Nbhd(r,e) ==  OpenInterval(r-e, r+e)
+LOCAL IsFirstDeriv(df, f) ==
+        /\ df \in [DOMAIN f -> Real]
+        /\ \A r \in DOMAIN f : 
+              \A e \in PosReal :
+                 \E d \in PosReal : 
+                    \A s \in Nbhd(r,d) \ {r} :
+                        (f[s] - f[r])/(s - r) \in Nbhd(df[r], e)
+
+LOCAL IsDeriv(n, df, f) == 
+  LET IsD[k \in 0..n,  g \in [DOMAIN f -> Real]] ==
+         IF k = 0 
+           THEN g = f
+           ELSE \E gg \in [DOMAIN f -> Real] : /\ IsFirstDeriv(g, gg)
+                                               /\ IsD[k-1, gg]
+  IN  IsD[n, df]
+
+Integrate(D, a, b, InitVals) ==
+  LET n == Len(InitVals)
+      gg == CHOOSE g : 
+              \E e \in PosReal : 
+                 /\ g \in [0..n -> [OpenInterval(a-e, b+e) -> Real]]
+                 /\ \A i \in 1..n : /\ IsDeriv(i, g[i], g[0])
+                                    /\ g[i-1][a] = InitVals[i]
+                 /\ \A r \in OpenInterval(a-e, b+e) :
+                        D[ <<r>> \o [i \in 1..(n+1) |-> g[i-1][r]] ] = 0
+  IN  [i \in 1..n |-> gg[i-1][b]]
+=============================================================================
+
+
+