diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 9c4a8c839f9344adb7eeacc058022a749a27f55c..96ff23d0a487b4007fc07cd533f094556dbf4169 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -4,7 +4,7 @@ on:
push:
# Sequence of patterns matched against refs/heads
branches:
- - v1.7.1 # Push events on master branch
+ - v1.7.2 # Push events on master branch
jobs:
@@ -12,18 +12,12 @@ jobs:
runs-on: ${{ matrix.operating-system }}
strategy:
matrix:
- operating-system: [ubuntu-latest, macos-latest]
+ operating-system: [ubuntu-latest]
include:
- - operating-system: macos-latest
- MVN_COMMAND: mvn -Dmaven.test.skip=true
- GITHUB_RELEASE_NAME: The Brontinus release
- TOOLBOX_PRODUCT_ZIP: TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip
-
- operating-system: ubuntu-latest
MVN_COMMAND: xvfb-run mvn -Dtest.skip=true -Dmaven.test.failure.ignore=true
- GITHUB_RELEASE_NAME: The Brontinus release
- TOOLBOX_PRODUCT_ZIP: TLAToolbox-1.7.1-linux.gtk.x86_64.zip
- TOOLBOX_PRODUCT_ZIP_WIN: TLAToolbox-1.7.1-win32.win32.x86_64.zip
+ GITHUB_RELEASE_NAME: The Theano release
+ TOOLBOX_PRODUCT_ZIP: TLAToolbox-1.7.2-linux.gtk.x86_64.zip
steps:
@@ -58,64 +52,11 @@ jobs:
env:
GPG_PRIVATE_KEY: ${{ secrets.GPG_PRIVATE_KEY }}
- ##
- ## Configure SSH privkey (INRIA upload below)
- ##
- - name: Set up SSH private key
- run: 'mkdir -p ~/.ssh && echo "$INRIA_SSH_PRIVKEY" > ~/.ssh/id_rsa && chmod 600 ~/.ssh/id_rsa'
- shell: bash
- env:
- INRIA_SSH_PRIVKEY: ${{ secrets.INRIA_SSH_PRIVKEY }}
-
- ##
- ## Set up Comodo code signing cert/key and configure maven (settings.xml) to
- ## have CODESIGN_KEYSTOREPASS_KEY, path to ComodoCertificate.p12, and the alias
- ## of the cert/key in ComodoCertificate.p12.
- ##
- - name: Set up maven credentials
- run: 'echo "$MVN_SETTINGS_XML" > ~/.m2/settings.xml'
- shell: bash
- env:
- MVN_SETTINGS_XML: ${{ secrets.MVN_SETTINGS_XML }}
- - name: Set up Comodo Codesign keystore part I
- run: 'echo "$COMODO_CODESIGN_COMBINED_PEM" > ComodoCertificate.pem'
- shell: bash
- env:
- COMODO_CODESIGN_COMBINED_PEM: ${{ secrets.COMODO_CODESIGN_COMBINED_PEM }}
- - name: Set up Comodo Codesign keystore part II
- run: |
- openssl pkcs12 -export -name ComodoCertificate -out ComodoCertificate.p12 -passout pass:${{ secrets.CODESIGN_KEYSTOREPASS_KEY }} -in ComodoCertificate.pem
- rm ComodoCertificate.pem
- keytool -importkeystore -srckeystore ComodoCertificate.p12 -srcstoretype pkcs12 -srcstorepass ${{ secrets.CODESIGN_KEYSTOREPASS_KEY }} -deststoretype pkcs12 -destkeystore ~/.m2/ComodoCertificate.jks -destkeypass ${{ secrets.CODESIGN_KEYSTOREPASS_KEY }} -deststorepass ${{ secrets.CODESIGN_KEYSTOREPASS_KEY }}
- rm ComodoCertificate.p12
-
##
## Build TLC and Toolbox (logger reduces verbosity).
##
- - name: Build with Maven (Linux)
- run: ${{ matrix.MVN_COMMAND }} -Pcodesigning -Dorg.slf4j.simpleLogger.log.org.apache.maven.cli.transfer.Slf4jMavenTransferListener=warn -fae -B verify --file pom.xml
-
- ##
- ## Create signed apt repository out of Linux Toolbox zip.
- ##
- - name: Create apt repository
- if: matrix.operating-system == 'ubuntu-latest'
- run: |
- chmod -x toolbox/org.lamport.tla.toolbox.product.product/createAptRepo.sh
- cp toolbox/org.lamport.tla.toolbox.product.product/target/*.deb toolbox/org.lamport.tla.toolbox.product.product/target/repository/
- cd toolbox/org.lamport.tla.toolbox.product.product/target/repository/
- bash -x ../../createAptRepo.sh .
-
- ##
- ## Create RPM out of Linux Toolbox zip.
- ##
-# - name: Create RPM (RedHat/CentOS package)
-# if: matrix.operating-system == 'ubuntu-latest'
-# run: |
-# sudo apt-get install alien --no-install-recommends -y
-# cd toolbox/org.lamport.tla.toolbox.product.product/target/
-# fakeroot alien --to-rpm --scripts TLAToolbox-?.?.?-linux.gtk.amd64.deb
-# cp TLA*.rpm products/
+ - name: Build with Ant (Linux)
+ run: ant -f tlatools/org.lamport.tlatools/customBuild.xml
##
## Upload Linux and Windows Toolbox zip and tla2tools.jar to Github release.
@@ -131,45 +72,15 @@ jobs:
curl -sS -X DELETE -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/assets/$ID
curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://uploads.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets?name=tla2tools.jar --upload-file tlatools/org.lamport.tlatools/dist/tla2tools.jar
- ID=$(curl -sS -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets --header "Content-Type: application/json" | jq '.[]| select(.name == "${{matrix.TOOLBOX_PRODUCT_ZIP_WIN}}") | .id')
- curl -sS -X DELETE -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/assets/$ID
- curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://uploads.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets?name=${{matrix.TOOLBOX_PRODUCT_ZIP_WIN}} --upload-file toolbox/org.lamport.tla.toolbox.product.product/target/products/${{matrix.TOOLBOX_PRODUCT_ZIP_WIN}}
-
- ID=$(curl -sS -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets --header "Content-Type: application/json" | jq '.[]| select(.name == "${{matrix.TOOLBOX_PRODUCT_ZIP}}") | .id')
- curl -sS -X DELETE -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/assets/$ID
- curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://uploads.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets?name=${{matrix.TOOLBOX_PRODUCT_ZIP}} --upload-file toolbox/org.lamport.tla.toolbox.product.product/target/products/${{matrix.TOOLBOX_PRODUCT_ZIP}}
-
- ID=$(curl -sS -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets --header "Content-Type: application/json" | jq '.[]| select(.name == "TLAToolbox-1.7.1.deb") | .id')
- curl -sS -X DELETE -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/assets/$ID
- curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://uploads.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.1.deb --upload-file toolbox/org.lamport.tla.toolbox.product.product/target/TLAToolbox-1.7.1-linux.gtk.amd64.deb
-
- ID=$(curl -sS -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets --header "Content-Type: application/json" | jq '.[]| select(.name == "p2repository.zip") | .id')
- curl -sS -X DELETE -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/assets/$ID
- curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://uploads.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets?name=p2repository.zip --upload-file toolbox/org.lamport.tla.toolbox.product.product/target/org.lamport.tla.toolbox.product.product-1.4.0-SNAPSHOT.zip
-
## Generate changelog
cd general/docs/changelogs
## Append sha1 sum to changelog (last line of changelog has the table header).
- echo "$(sha1sum ../../../tlatools/org.lamport.tlatools/dist/tla2tools.jar | cut -f 1 -d " ")|tla2tools.jar" >> ch1_7_1.md
- echo "$(sha1sum ../../../toolbox/org.lamport.tla.toolbox.product.product/target/products/${{matrix.TOOLBOX_PRODUCT_ZIP_WIN}} | cut -f 1 -d " ")|${{matrix.TOOLBOX_PRODUCT_ZIP_WIN}}" >> ch1_7_1.md
- echo "$(sha1sum ../../../toolbox/org.lamport.tla.toolbox.product.product/target/products/${{matrix.TOOLBOX_PRODUCT_ZIP}} | cut -f 1 -d " ")|${{matrix.TOOLBOX_PRODUCT_ZIP}}" >> ch1_7_1.md
- echo "TBD|macOS" >> ch1_7_1.md
+ echo "$(sha1sum ../../../tlatools/org.lamport.tlatools/dist/tla2tools.jar | cut -f 1 -d " ")|tla2tools.jar" >> ch1_7_2.md
## Two above as one-liner without intermediate file.
- $(jq -n --argjson changelog "$(cat ch1_7_1.md | jq --raw-input --slurp .)" -f gh-1_7_1.jq > gh-1_7_1.json)
+ $(jq -n --argjson changelog "$(cat ch1_7_2.md | jq --raw-input --slurp .)" -f gh-1_7_2.jq > gh-1_7_2.json)
## Update draft release with latest changelog in case it changed.
## https://developer.github.com/v3/repos/releases/#edit-a-release
- curl -sS -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE -d @gh-1_7_1.json -X PATCH --header "Content-Type: application/json"
-
- - name: Upload assets to INRIA
- if: matrix.operating-system == 'ubuntu-latest'
- run: |
- ## Thanks Apple for your walled garden! Delete the *unsigned* Toolbox maxOS zip created by the Linux/ubuntu job. The macOS job below creates and rsyncs a *signed* zip file.
- rm toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip
- ## Upload p2 and apt repository to INRIA machine.
- rsync -e "ssh -o StrictHostKeyChecking=no -i ~/.ssh/id_rsa" --delete -av tlatools/org.lamport.tlatools/dist/tla2tools.jar github@upload.tlapl.us:dist/
- rsync -e "ssh -o StrictHostKeyChecking=no -i ~/.ssh/id_rsa" --delete -av toolbox/org.lamport.tla.toolbox.product.product/target/products/*.zip github@upload.tlapl.us:products/
- rsync -e "ssh -o StrictHostKeyChecking=no -i ~/.ssh/id_rsa" --delete -av toolbox/org.lamport.tla.toolbox.product.product/target/repository/ github@upload.tlapl.us:repository/
- rsync -e "ssh -o StrictHostKeyChecking=no -i ~/.ssh/id_rsa" --delete -av toolbox/org.lamport.tla.toolbox.doc/html/ github@upload.tlapl.us:doc/
+ curl -sS -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE -d @gh-1_7_2.json -X PATCH --header "Content-Type: application/json"
##
## Update all git tags to make the download urls work, i.e.
@@ -183,66 +94,3 @@ jobs:
git config --local user.email "tlaplus-action@github.com"
git config --local user.name "TLA+ GitHub Action"
git push https://${{ github.actor }}:${{ secrets.GITHUB_TOKEN }}@github.com/${{ github.repository }}.git --follow-tags --tags --force
-
- ##
- ## Upload tla2tools.jar to Github maven packages.
- ##
- - name: Upload to Github maven packages
- if: matrix.operating-system == 'ubuntu-latest'
- run: |
- cd tlatools/org.lamport.tlatools/
- ## Strip packages from the tla2tools.jar fatjar that are declared dependencies of the maven package (see github.xml).
- zip -d dist/tla2tools.jar javax/\* com/\* META-INF/mailcap META-INF/javamail*
- ## github.xml replaces the Tycho pom.xml with a specific one to publish tla2tools.jar.
- mvn deploy:deploy-file -Dgithub.packages.username=${{ github.actor }} -Dgithub.packages.password=${{ secrets.GITHUB_TOKEN }} -Dfile=dist/tla2tools.jar -Durl=https://maven.pkg.github.com/${{ github.repository }} -DpomFile=github.xml -DrepositoryId=github -f github.xml
-
- ################################# macOS #################################
-
- ##
- ## Sign Toolbox macOS zip file.
- ##
- - name: Set up Apple Certs
- if: matrix.operating-system == 'macos-latest'
- run: 'echo "$APPLE_CODESIGN_CERTS" > certs.pem'
- shell: bash
- env:
- APPLE_CODESIGN_CERTS: ${{ secrets.APPLE_CODESIGN_CERTS }}
- - name: Set up Apple Key (submission)
- if: matrix.operating-system == 'macos-latest'
- run: 'echo "$APPLE_CODESIGN_SUBMISSION_PRIVKEY" > submission.pem'
- shell: bash
- env:
- APPLE_CODESIGN_SUBMISSION_PRIVKEY: ${{ secrets.APPLE_CODESIGN_SUBMISSION_PRIVKEY }}
- - name: Set up Apple Key (dev)
- if: matrix.operating-system == 'macos-latest'
- run: 'echo "$APPLE_CODESIGN_DEVELOPER_PRIVKEY" > dev.pem'
- shell: bash
- env:
- APPLE_CODESIGN_DEVELOPER_PRIVKEY: ${{ secrets.APPLE_CODESIGN_DEVELOPER_PRIVKEY }}
- - name: Create macOS keychain, unzip, sign, and zip up TLA+ Toolbox for macOS
- if: matrix.operating-system == 'macos-latest'
- run: |
- ## Convert pems stored as Github secrets to .p12 files that 'security import' accepts.
- openssl pkcs12 -export -inkey submission.pem -in certs.pem -out submission.p12 -passin pass:${{ secrets.APPLE_CERT_PASSWORD }} -passout pass:${{ secrets.APPLE_CERT_PASSWORD }}
- openssl pkcs12 -export -inkey dev.pem -in certs.pem -out dev.p12 -passin pass:${{ secrets.APPLE_CERT_PASSWORD }} -passout pass:${{ secrets.APPLE_CERT_PASSWORD }}
- ## Create a fresh keychain "tla" and import certs and keys into it.
- security create-keychain -p ${{ secrets.APPLE_CERT_PASSWORD }} tla
- security import certs.pem -k tla -P ${{ secrets.APPLE_CERT_PASSWORD }} -T /usr/bin/codesign
- security import submission.p12 -k tla -P ${{ secrets.APPLE_CERT_PASSWORD }} -T /usr/bin/codesign
- security import dev.p12 -k tla -P ${{ secrets.APPLE_CERT_PASSWORD }} -T /usr/bin/codesign
- ## Listing the keychain once is apparently required for codesign to work.
- security list-keychains -s tla
- ## Not sure what this is for, but hey: https://stackoverflow.com/a/40039594
- security set-key-partition-list -S apple-tool:,apple: -s -k ${{ secrets.APPLE_CERT_PASSWORD }} tla
- ## Unzip, sign, and zip up the TLA Toolbox.
- unzip toolbox/org.lamport.tla.toolbox.product.product/target/products/${{ matrix.TOOLBOX_PRODUCT_ZIP }}
- codesign --keychain tla --deep --display --entitlements toolbox/org.lamport.tla.toolbox.product.product/entitlements.plist --options runtime --verbose=4 -h -f -s "Developer ID Application: M K (3PCM4M3RWK)" "TLA+ Toolbox.app"
- ditto -ck --sequesterRsrc --keepParent "TLA+ Toolbox.app" ${{ matrix.TOOLBOX_PRODUCT_ZIP }}
- xcrun altool --notarize-app --primary-bundle-id "org.lamport.tla.toolbox.product.product" --username "${{secrets.APPLE_CODESIGN_DEVELOPER_ID}}" --password "${{secrets.APPLE_CODESIGN_DEVELOPER_PASSWORD}}" --file "${{ matrix.TOOLBOX_PRODUCT_ZIP }}"
- ## Upload signed TLAToolbox zip to Github release.
- DRAFT_RELEASE=$(curl -sS -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases --header "Content-Type: application/json" | jq '.[]| select(.name=="${{ matrix.GITHUB_RELEASE_NAME }}") | .id')
- ID=$(curl -sS -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets --header "Content-Type: application/json" | jq '.[]| select(.name == "${{ matrix.TOOLBOX_PRODUCT_ZIP }}") | .id')
- curl -sS -X DELETE -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/assets/$ID
- curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://uploads.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets?name=${{ matrix.TOOLBOX_PRODUCT_ZIP }} --upload-file ${{ matrix.TOOLBOX_PRODUCT_ZIP }}
- ## Upload p2 and apt repository to INRIA machine.
- rsync -e "ssh -o StrictHostKeyChecking=no -i ~/.ssh/id_rsa" --delete -av ${{ matrix.TOOLBOX_PRODUCT_ZIP }} github@upload.tlapl.us:products/
diff --git a/general/docs/changelogs/ch1_7_2.md b/general/docs/changelogs/ch1_7_2.md
new file mode 100644
index 0000000000000000000000000000000000000000..8dfd77e2bc3e642e21c6a724afee9bd55ad655b4
--- /dev/null
+++ b/general/docs/changelogs/ch1_7_2.md
@@ -0,0 +1,13 @@
+The [Theano](https://en.wikipedia.org/wiki/Theano_(philosopher)) release is based on the [1.7.1 branch](https://github.com/tlaplus/tlaplus/releases/tag/v1.7.1) and fixes the two issues below.
+
+### Changelog
+* [Name clash between variable in refined spec and operator in instantiated spec](https://github.com/tlaplus/tlaplus/issues/362)
+* [Thread safety concerns due to "memory barrier" pattern in value classes](https://github.com/tlaplus/tlaplus/issues/439)
+
+### Contributors
+
+We are grateful for contributions from [Calvin Loncaric](https://github.com/Calvin-L) and [Dmitry Kulagin](https://github.com/craft095).
+
+### Checksums
+sha1sum|file
+------------ | -------------
diff --git a/general/docs/changelogs/gh-1_7_2.jq b/general/docs/changelogs/gh-1_7_2.jq
new file mode 100644
index 0000000000000000000000000000000000000000..81420d465a9ff90d73097631173cb799dbf4bc71
--- /dev/null
+++ b/general/docs/changelogs/gh-1_7_2.jq
@@ -0,0 +1,7 @@
+{
+ "tag_name": "v1.7.2",
+ "name": "The Theano release",
+ "draft": true,
+ "prerelease": false,
+ "body": $changelog
+}
\ No newline at end of file
diff --git a/tlatools/org.lamport.tlatools/github.xml b/tlatools/org.lamport.tlatools/github.xml
index 2ac40936ea97723f97222628edd636c3f057131e..098473a97da955fa58de84c7b7193a6fe4237c8a 100644
--- a/tlatools/org.lamport.tlatools/github.xml
+++ b/tlatools/org.lamport.tlatools/github.xml
@@ -10,7 +10,7 @@
<groupId>org.lamport</groupId>
<artifactId>tla2tools</artifactId>
<name>TLA+ Tools</name>
- <version>1.7.0-SNAPSHOT</version>
+ <version>1.7.2-SNAPSHOT</version>
<description>The TLC model checker, the syntax and semantic checker SANY, the PlusCal translator, and the LaTeX pretty printer.</description>
<packaging>jar</packaging>
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/TLCGlobals.java b/tlatools/org.lamport.tlatools/src/tlc2/TLCGlobals.java
index d68116ed66325a1ca4b4f3f87dd6fd430cc0af2e..d821d03a0ef3a2a050867b6d3a0a6bf134785357 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/TLCGlobals.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/TLCGlobals.java
@@ -23,7 +23,7 @@ public class TLCGlobals
public static final int DEFAULT_CHECKPOINT_DURATION = (30 * 60 * 1000) + 42;
// The current version of TLC
- public static String versionOfTLC = "Version 2.16 of 31 December 2020";
+ public static String versionOfTLC = "Version 2.17 of 02 February 2022";
// The bound for set enumeration, used for pretty printing
public static int enumBound = 2000;
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Spec.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Spec.java
index e3b13d034e80db1a62850354ab7cb97ad8007218..5ba1c7f41833c89a2831d3921620e1b55562e595 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Spec.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Spec.java
@@ -349,19 +349,27 @@ abstract class Spec
*/
public final Object lookup(SymbolNode opNode, Context c, TLCState s, boolean cutoff)
{
- Object result = lookup(opNode, c, cutoff, toolId);
- if (result != opNode) {
- return result;
- }
- result = s.lookup(opNode.getName());
- if (result != null) {
- return result;
+ Object result = lookup(opNode, c, cutoff, toolId);
+ 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) {
- return lookup(opNode, Context.Empty, false, toolId);
+ public final Object lookup(final SymbolNode opNode)
+ {
+ return lookup(opNode, Context.Empty, false, toolId);
}
/**
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/value/impl/FcnRcdValue.java b/tlatools/org.lamport.tlatools/src/tlc2/value/impl/FcnRcdValue.java
index b8c18ab21d7f6fa86631c40377f931931fb13e61..95e8619d9018f70ada980df15339c30ddfe1fe54 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/value/impl/FcnRcdValue.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/value/impl/FcnRcdValue.java
@@ -7,7 +7,6 @@
package tlc2.value.impl;
import java.io.IOException;
-import java.util.Arrays;
import java.util.Map;
import tlc2.tool.EvalControl;
@@ -30,7 +29,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue {
public final IntervalValue intv;
public final Value[] values;
private boolean isNorm;
- private int[] indexTbl; // speed up function application
public static final Value EmptyFcn = new FcnRcdValue(new Value[0], new Value[0], true);
/* Constructor */
@@ -39,7 +37,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue {
this.values = values;
this.intv = null;
this.isNorm = isNorm;
- this.indexTbl = null;
}
public FcnRcdValue(IntervalValue intv, Value[] values) {
@@ -47,7 +44,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue {
this.values = values;
this.domain = null;
this.isNorm = true;
- this.indexTbl = null;
}
public FcnRcdValue(IntervalValue intv, Value[] values, CostModel cm) {
@@ -60,7 +56,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue {
this.intv = fcn.intv;
this.values = values;
this.isNorm = fcn.isNorm;
- this.indexTbl = fcn.indexTbl;
}
public FcnRcdValue(ValueVec elems, Value[] values, boolean isNorm) {
@@ -80,45 +75,6 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue {
@Override
public final byte getKind() { return FCNRCDVALUE; }
- /* We create an index only when the domain is not very small. */
- private final void createIndex() {
- if (this.domain != null && this.domain.length > 10) {
- int len = this.domain.length * 2 + 1;
-
- int[] tbl = new int[len];
- Arrays.fill(tbl, -1);
-
- synchronized(this) {
- for (int i = 0; i < this.domain.length; i++) {
- int loc = (this.domain[i].hashCode() & 0x7FFFFFFF) % len;
- while (tbl[loc] != -1) {
- loc = (loc + 1) % len;
- }
- tbl[loc] = i;
- }
- }
-
- synchronized(this) { this.indexTbl = tbl; }
- }
- }
-
- private final int lookupIndex(Value arg) {
- int len = this.indexTbl.length;
- int loc = (arg.hashCode() & 0x7FFFFFFF) % len;
- while (true) {
- int idx = this.indexTbl[loc];
- if (idx == -1) {
- Assert.fail("Attempted to apply function:\n" + Values.ppr(this.toString()) +
- "\nto argument " + Values.ppr(arg.toString()) +
- ", which is not in the domain of the function.");
- }
- if (this.domain[idx].equals(arg)) {
- return idx;
- }
- loc = (loc + 1) % len;
- }
- }
-
@Override
public final int compareTo(Object obj) {
try {
@@ -348,22 +304,12 @@ public class FcnRcdValue extends Value implements Applicable, IFcnRcdValue {
}
else {
// domain is represented as an array of values:
- if (this.indexTbl != null) {
- return this.values[this.lookupIndex(arg)];
- }
- if (this.isNorm) this.createIndex();
-
- if (this.indexTbl != null) {
- return this.values[this.lookupIndex(arg)];
- }
- else {
int len = this.domain.length;
for (int i = 0; i < len; i++) {
if (this.domain[i].equals(arg)) {
return this.values[i];
}
}
- }
}
return null;
diff --git a/tlatools/org.lamport.tlatools/test-model/Github362.cfg b/tlatools/org.lamport.tlatools/test-model/Github362.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..dbbd7f2a293042e29cff5cca9741e11fa1cbe4f3
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/test-model/Github362.cfg
@@ -0,0 +1,4 @@
+INIT Init
+NEXT Next
+PROPERTY Correct
+CONSTANT overloadedConst = 4711
diff --git a/tlatools/org.lamport.tlatools/test-model/Github362.tla b/tlatools/org.lamport.tlatools/test-model/Github362.tla
new file mode 100644
index 0000000000000000000000000000000000000000..058242a52c374c77939eb7488c25482bde189be3
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/test-model/Github362.tla
@@ -0,0 +1,34 @@
+---- 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
+
+==================
diff --git a/tlatools/org.lamport.tlatools/test-model/Github362B.tla b/tlatools/org.lamport.tlatools/test-model/Github362B.tla
new file mode 100644
index 0000000000000000000000000000000000000000..9a5e0e20870709f16145a4ce9a2bd4f6a8a83748
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/test-model/Github362B.tla
@@ -0,0 +1,29 @@
+---- 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
+
+==================
diff --git a/tlatools/org.lamport.tlatools/test/tlc2/tool/Github362Test.java b/tlatools/org.lamport.tlatools/test/tlc2/tool/Github362Test.java
new file mode 100644
index 0000000000000000000000000000000000000000..2e9d564ff70c41c98ee531f86305e8c8986d5c16
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/test/tlc2/tool/Github362Test.java
@@ -0,0 +1,66 @@
+/*******************************************************************************
+ * 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));
+ }
+
+}
diff --git a/toolbox/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product b/toolbox/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product
index e79ef3fa9372269920d06b4d75113bffcb817287..2de5c6477f1556e023fdc4b61630d50b8fe020a5 100644
--- a/toolbox/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product
+++ b/toolbox/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product
@@ -1,16 +1,16 @@
<?xml version="1.0" encoding="UTF-8"?>
<?pde version="3.5"?>
-<product name="TLA+ Toolbox" uid="org.lamport.tla.toolbox.product.product" id="org.lamport.tla.toolbox.product.standalone.product" application="org.lamport.tla.toolbox.application" version="1.7.1.qualifier" useFeatures="true" includeLaunchers="true">
+<product name="TLA+ Toolbox" uid="org.lamport.tla.toolbox.product.product" id="org.lamport.tla.toolbox.product.standalone.product" application="org.lamport.tla.toolbox.application" version="1.7.2.qualifier" useFeatures="true" includeLaunchers="true">
<aboutInfo>
<image path="/org.lamport.tla.toolbox.product.standalone/images/splash_small.png"/>
<text>
TLA+ Toolbox provides a user interface for TLA+ Tools.
-This is Version 1.7.1 of 31 December 2020 and includes:
+This is Version 1.7.2 of 02 February 2022 and includes:
- SANY Version 2.2 of 20 April 2020
- - TLC Version 2.16 of 31 December 2020
+ - TLC Version 2.17 of 02 Febraury 2022
- PlusCal Version 1.11 of 31 December 2020
- TLATeX Version 1.0 of 20 September 2017
@@ -95,11 +95,11 @@ openFile
<plugin id="org.lamport.tla.toolbox.jclouds" autoStart="true" startLevel="4" />
<plugin id="packet" autoStart="true" startLevel="4" />
<plugin id="sts" autoStart="true" startLevel="4" />
- <property name="eclipse.buildId" value="1.7.1" />
+ <property name="eclipse.buildId" value="1.7.2" />
</configurations>
<repositories>
- <repository location="http://lamport.org/tlatoolbox/branches/1.7.1/toolboxUpdate/" enabled="true" />
+ <repository location="http://lamport.org/tlatoolbox/branches/1.7.2/toolboxUpdate/" enabled="true" />
<repository location="http://lamport.org/tlatoolbox/ci/toolboxUpdate/" enabled="false" />
</repositories>
diff --git a/toolbox/org.lamport.tla.toolbox.product.standalone/plugin.xml b/toolbox/org.lamport.tla.toolbox.product.standalone/plugin.xml
index 98d54a174ed9411d1a92667eccad0a4f5fac20ed..bd29e511149b9741082d1e20eb63b8d8ed0f79d4 100644
--- a/toolbox/org.lamport.tla.toolbox.product.standalone/plugin.xml
+++ b/toolbox/org.lamport.tla.toolbox.product.standalone/plugin.xml
@@ -30,7 +30,7 @@
</property>
<property
name="aboutText"
- value="TLA+ Toolbox provides a user interface for TLA+ Tools. 

This is Version 1.7.1 of 31 December 2020 and includes:
 - SANY Version 2.2 of 20 April 2020
 - TLC Version 2.16 of 31 December 2020
 - PlusCal Version 1.11 of 31 December 2020
 - TLATeX Version 1.0 of 20 September 2017

Don't forget to click on help. You can learn about features that you never knew about or have forgotten.

Please send us reports of problems or suggestions; see https://groups.google.com/d/forum/tlaplus .

Some icons used in the Toolbox were provided by www.flaticon.com">
+ value="TLA+ Toolbox provides a user interface for TLA+ Tools. 

This is Version 1.7.2 of 02 February 2022 and includes:
 - SANY Version 2.2 of 20 April 2020
 - TLC Version 2.17 of 02 February 2022
 - PlusCal Version 1.11 of 31 December 2020
 - TLATeX Version 1.0 of 20 September 2017

Don't forget to click on help. You can learn about features that you never knew about or have forgotten.

Please send us reports of problems or suggestions; see https://groups.google.com/d/forum/tlaplus .

Some icons used in the Toolbox were provided by www.flaticon.com">
</property>
<property
name="aboutImage"
diff --git a/toolbox/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java b/toolbox/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java
index 8a8e21c454c87eed26cb8338f85c680c91538165..d8c0d4ef620c2c070cfa440e6240e54b10a3e769 100644
--- a/toolbox/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java
+++ b/toolbox/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java
@@ -431,7 +431,7 @@ public class ToolboxIntroPart extends IntroPart implements IIntroPart {
final Label lblVersion = new Label(outerContainer, SWT.WRAP);
lblVersion.setLayoutData(new GridData(SWT.FILL, SWT.CENTER, false, false, 2, 1));
- lblVersion.setText("Version 1.7.1 of 31 December 2020");
+ lblVersion.setText("Version 1.7.2 of 02 February 2022");
lblVersion.setBackground(backgroundColor);
}