diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 4aaec0695ebc79962b7115cfbbc7143adc4efae9..9c4a8c839f9344adb7eeacc058022a749a27f55c 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:
- - master # Push events on master branch
+ - v1.7.1 # Push events on master branch
jobs:
@@ -16,14 +16,14 @@ jobs:
include:
- operating-system: macos-latest
MVN_COMMAND: mvn -Dmaven.test.skip=true
- GITHUB_RELEASE_NAME: The Aristotle release
- TOOLBOX_PRODUCT_ZIP: TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip
+ 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 Aristotle release
- TOOLBOX_PRODUCT_ZIP: TLAToolbox-1.7.0-linux.gtk.x86_64.zip
- TOOLBOX_PRODUCT_ZIP_WIN: TLAToolbox-1.7.0-win32.win32.x86_64.zip
+ 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
steps:
@@ -139,9 +139,9 @@ 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=${{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.0.deb") | .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 == "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.0.deb --upload-file toolbox/org.lamport.tla.toolbox.product.product/target/TLAToolbox-1.7.0-linux.gtk.amd64.deb
+ 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
@@ -150,23 +150,26 @@ jobs:
## 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_0.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_0.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_0.md
- echo "TBD|macOS" >> ch1_7_0.md
+ 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
## Two above as one-liner without intermediate file.
- $(jq -n --argjson changelog "$(cat ch1_7_0.md | jq --raw-input --slurp .)" -f gh-1_7_0.jq > gh-1_7_0.json)
+ $(jq -n --argjson changelog "$(cat ch1_7_1.md | jq --raw-input --slurp .)" -f gh-1_7_1.jq > gh-1_7_1.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_0.json -X PATCH --header "Content-Type: application/json"
+ 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" -av tlatools/org.lamport.tlatools/dist/tla2tools.jar github@upload.tlapl.us:dist/
- rsync -e "ssh -o StrictHostKeyChecking=no -i ~/.ssh/id_rsa" -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" -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 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/
##
## Update all git tags to make the download urls work, i.e.
@@ -179,8 +182,6 @@ jobs:
run: |
git config --local user.email "tlaplus-action@github.com"
git config --local user.name "TLA+ GitHub Action"
- git tag -f nightly
- git tag -f v1.7.0
git push https://${{ github.actor }}:${{ secrets.GITHUB_TOKEN }}@github.com/${{ github.repository }}.git --follow-tags --tags --force
##
@@ -237,8 +238,11 @@ jobs:
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/.jenkins.groovy b/.jenkins.groovy
index 77b56fdc4e11a67677951f235e006f33985c369b..5ca9fabaf89a34cfed99379c5e607fda966cd66f 100644
--- a/.jenkins.groovy
+++ b/.jenkins.groovy
@@ -46,7 +46,7 @@ for (x in labels) {
}
// the macosx zip on the master node to have it signed with the Apple certificate on macosx. However, only master
// has the lamport certificate to sign the individual toolbox bundles.
- stash includes: 'toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip', name: 'toolbox'
+ stash includes: 'toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip', name: 'toolbox'
} else {
withMaven(
// Maven installation declared in the Jenkins "Global Tool Configuration"
@@ -153,7 +153,7 @@ node ('master') {
}
stage('RenderChangelog') { // Render the github flavord markdown to html
- sh 'grip --context=tlaplus/tlaplus --export ${WORKSPACE}/general/docs/changelogs/ch1_7_0.md ${WORKSPACE}/general/docs/changelogs/changelog.html'
+ sh 'grip --context=tlaplus/tlaplus --export ${WORKSPACE}/general/docs/changelogs/ch1_7_1.md ${WORKSPACE}/general/docs/changelogs/changelog.html'
}
}
@@ -162,11 +162,11 @@ node ('macos') {
sh 'rm -rf *'
unstash 'toolbox'
sh 'ls -lah'
- sh 'unzip toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip'
+ sh 'unzip toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip'
sh 'codesign -f -s "Developer ID Application: M K (3PCM4M3RWK)" -v "TLA+ Toolbox.app" --deep'
- sh 'ditto -ck --sequesterRsrc --keepParent "TLA+ Toolbox.app" TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip'
- sh 'mv TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip toolbox/org.lamport.tla.toolbox.product.product/target/products/'
- stash includes: 'toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip', name: 'signed'
+ sh 'ditto -ck --sequesterRsrc --keepParent "TLA+ Toolbox.app" TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip'
+ sh 'mv TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip toolbox/org.lamport.tla.toolbox.product.product/target/products/'
+ stash includes: 'toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip', name: 'signed'
}
}
@@ -188,21 +188,21 @@ node ('master') {
cd ${WORKSPACE}/general/docs/changelogs
## Append sha1 sum to changelog (last line of changelog has the table header).
- echo "$(sha1sum ${WORKSPACE}/tlatools/org.lamport.tlatools/dist/tla2tools.jar | cut -f 1 -d " ")|tla2tools.jar" >> ch1_7_0.md
- echo "$(sha1sum ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.0-win32.win32.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.7.0-win32.win32.x86_64.zip" >> ch1_7_0.md
- echo "$(sha1sum ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip" >> ch1_7_0.md
- echo "$(sha1sum ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.0-linux.gtk.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.7.0-linux.gtk.x86_64.zip" >> ch1_7_0.md
+ echo "$(sha1sum ${WORKSPACE}/tlatools/org.lamport.tlatools/dist/tla2tools.jar | cut -f 1 -d " ")|tla2tools.jar" >> ch1_7_1.md
+ echo "$(sha1sum ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-win32.win32.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.7.1-win32.win32.x86_64.zip" >> ch1_7_1.md
+ echo "$(sha1sum ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip" >> ch1_7_1.md
+ echo "$(sha1sum ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-linux.gtk.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.7.1-linux.gtk.x86_64.zip" >> ch1_7_1.md
## Two above as one-liner without intermediate file.
- $(jq -n --argjson changelog "$(cat ch1_7_0.md | jq --raw-input --slurp .)" -f gh-1_7_0.jq > gh-1_7_0.json)
+ $(jq -n --argjson changelog "$(cat ch1_7_1.md | jq --raw-input --slurp .)" -f gh-1_7_1.jq > gh-1_7_1.json)
## Get id of existing draft release with given name.
- DRAFT_RELEASE=$(curl -sS -H "Authorization: token ${GITHUB_TOKEN}" https://api.github.com/repos/tlaplus/tlaplus/releases --header "Content-Type: application/json" | jq '.[]| select(.draft==true and .name=="The Aristotle release") | .id')
+ DRAFT_RELEASE=$(curl -sS -H "Authorization: token ${GITHUB_TOKEN}" https://api.github.com/repos/tlaplus/tlaplus/releases --header "Content-Type: application/json" | jq '.[]| select(.draft==true and .name=="The Brontinus release") | .id')
echo $DRAFT_RELEASE
## 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 ${GITHUB_TOKEN}" https://api.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE -d @gh-1_7_0.json -X PATCH --header "Content-Type: application/json"
+ curl -sS -H "Authorization: token ${GITHUB_TOKEN}" https://api.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE -d @gh-1_7_1.json -X PATCH --header "Content-Type: application/json"
## Remove old assets otherwise upload below will error.
ASSETS=$(curl -sS -H "Authorization: token ${GITHUB_TOKEN}" https://api.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets --header "Content-Type: application/json" | jq '.[]| .id')
@@ -216,15 +216,15 @@ node ('master') {
## tla2tools.jar
curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=tla2tools.jar --upload-file ${WORKSPACE}/tlatools/org.lamport.tlatools/dist/tla2tools.jar
## macOS
- curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.0-macosx.cocoa.x86_64.zip
+ curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip
## win32
- curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.0-win32.win32.x86_64.zip --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.0-win32.win32.x86_64.zip
+ curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.1-win32.win32.x86_64.zip --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-win32.win32.x86_64.zip
## Linux
- curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.0-linux.gtk.x86_64.zip --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.0-linux.gtk.x86_64.zip
+ curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.1-linux.gtk.x86_64.zip --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-linux.gtk.x86_64.zip
## deb
- #curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.0-linux.gtk.amd64.deb --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/repository/TLAToolbox-1.7.0-linux.gtk.amd64.deb
+ #curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.1-linux.gtk.amd64.deb --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/repository/TLAToolbox-1.7.1-linux.gtk.amd64.deb
## RPM
- #curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.0-linux.gtk.amd64.rpm --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLA\\+Toolbox-1.7.0~*.x86_64.rpm
+ #curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.1-linux.gtk.amd64.rpm --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLA\\+Toolbox-1.7.1~*.x86_64.rpm
'''
}
}
diff --git a/general/docs/changelogs/ch1_7_1.md b/general/docs/changelogs/ch1_7_1.md
new file mode 100644
index 0000000000000000000000000000000000000000..464ce96a44bbbf8ba03085aecaa3cd7757882336
--- /dev/null
+++ b/general/docs/changelogs/ch1_7_1.md
@@ -0,0 +1,19 @@
+### Changelog
+The high level changelog is available at http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html#release. The [1.7.1 milestone](https://github.com/tlaplus/tlaplus/issues?q=is%3Aissue+milestone%3A1.7.1+is%3Aclosed) lists all completed issues:
+
+* Re-worked PlusCal/TLA+ divergence warning ([please manually remove 1.7.0 markers](https://github.com/tlaplus/tlaplus/issues/558), i.e. everything on the line following `\* BEGIN TRANSLATION`). https://github.com/tlaplus/tlaplus/issues/558
+* TLC shows no error *trace* for violations of `TLC!Assert`, ... https://github.com/tlaplus/tlaplus/issues/461
+* NoClassDefError when running TLC on Java 1.8. https://github.com/tlaplus/tlaplus/issues/462
+* Dot visualization (graphviz) fails due to invalid character ! when spec uses instantiation https://github.com/tlaplus/tlaplus/issues/452
+* Simulation mode ignores ASSUMPTIONS. https://github.com/tlaplus/tlaplus/issues/496
+* Back to state missing for lasso error trace found by simulation https://github.com/tlaplus/tlaplus/issues/497
+* AtNode does not show up in (dot) graph output of semantic explorer 52f3b01
+* Replace custom implementation of (heap) sort in TeX with java.utils.Arrays#sort https://github.com/tlaplus/tlaplus/issues/539
+* End support for liveness checking and multiple workers in DFID mode because both features are unreliable https://github.com/tlaplus/tlaplus/issues/548 https://github.com/tlaplus/tlaplus/issues/544
+* Multiline trace expressions fail to parse in Toolbox. defe0c74915b1c27c6af2fb55c8163f3574c8918
+* Upgrade Eclipse foundation to its 2020-06 release for better HiDPI support. https://github.com/tlaplus/tlaplus/issues/472
+* Toolbox intermittently shows no error trace on an invariant violation https://github.com/tlaplus/tlaplus/issues/538
+
+### Checksums
+sha1sum|file
+------------ | -------------
diff --git a/general/docs/changelogs/gh-1_7_1.jq b/general/docs/changelogs/gh-1_7_1.jq
new file mode 100644
index 0000000000000000000000000000000000000000..42663e4a31d94853123d1fdd6fabaa653178fb9c
--- /dev/null
+++ b/general/docs/changelogs/gh-1_7_1.jq
@@ -0,0 +1,7 @@
+{
+ "tag_name": "v1.7.1",
+ "name": "The Brontinus release",
+ "draft": true,
+ "prerelease": false,
+ "body": $changelog
+}
\ No newline at end of file
diff --git a/general/ide/TLA.setup b/general/ide/TLA.setup
index ab94371f5e86ded713abafa362c359114632652a..e1f8b085a3dfb0138fc9953d745a9dae334b9148 100644
--- a/general/ide/TLA.setup
+++ b/general/ide/TLA.setup
@@ -86,7 +86,7 @@
<repository
url="http://download.eclipse.org/e4/snapshots/org.eclipse.e4.tools/latest/"/>
<repository
- url="jar:https://dl.bintray.com/abstratt-oss/abstratt-oss/com/abstratt/eclipsegraphviz/com.abstratt.eclipsegraphviz.repository/2.5.201812/com.abstratt.eclipsegraphviz.repository-2.5.201812.zip!/"/>
+ url="jar:https://raw.githubusercontent.com/tlaplus/tlaplus/master/toolbox/org.lamport.tla.toolbox.product.product/cachedTargetPlatform/com.abstratt.eclipsegraphviz.repository-2.5.201812.zip!/"/>
<repository
url="https://download.eclipse.org/rcptt/release/2.4.3/repository/"/>
<repository
diff --git a/pom.xml b/pom.xml
index 30f092d39260c9ddb0034d1d8999ab11d9ef4678..801dfde2289aef3fd078e8d5e707c13d800dfbfe 100644
--- a/pom.xml
+++ b/pom.xml
@@ -78,7 +78,7 @@
<module>toolbox/org.lamport.tla.toolbox.product.product</module>
<!-- Finally run UI tests on fully built product (AUT) -->
- <module>toolbox/org.lamport.tla.toolbox.product.uitest</module>
+<!-- <module>toolbox/org.lamport.tla.toolbox.product.uitest</module>-->
</modules>
<!-- tycho requires maven >= 3.0 -->
@@ -123,7 +123,7 @@
<!-- Align toolbox.version with the version in
org.lamport.tla.toolbox.product.product.product
product.version. -->
- <toolbox.version>1.7.0</toolbox.version>
+ <toolbox.version>1.7.1</toolbox.version>
<!-- This is used in org.lamport.tla.toolbox.product.uitest but
has been placed at the top level should it need be referenced
diff --git a/tlatools/org.lamport.tlatools/ossrh.xml b/tlatools/org.lamport.tlatools/ossrh.xml
index 1b495f1fb9f0afe1e76fa90716b58dc1c0f97263..f6f7a40e38d059bc777c43a5f0ff1beddb4fc3c4 100644
--- a/tlatools/org.lamport.tlatools/ossrh.xml
+++ b/tlatools/org.lamport.tlatools/ossrh.xml
@@ -17,7 +17,7 @@
<groupId>org.lamport</groupId>
<artifactId>tla2tools</artifactId>
<name>TLA+ Tools</name>
- <version>1.7.0-SNAPSHOT</version>
+ <version>1.7.1-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/pcal/PcalParams.java b/tlatools/org.lamport.tlatools/src/pcal/PcalParams.java
index b83937d9a73257838721061f012af9d527efbfb4..51be055c814bf01e5d2a60033e494c3e902295e3 100644
--- a/tlatools/org.lamport.tlatools/src/pcal/PcalParams.java
+++ b/tlatools/org.lamport.tlatools/src/pcal/PcalParams.java
@@ -18,8 +18,13 @@ public final class PcalParams
/**
* Parameters to be updated on each new release.
*/
- public static final String modDate = "10 July 2019";
- public static final String version = "1.9";
+ public static final String modDate = "31 December 2020";
+ // Can't increment 1.9 to 1.10 because VersionToNumber(str) calculates a lower
+ // numerical value for 1.10 than it does for 1.9. This breaks the FairSeq?Test
+ // tests. Until we switch from 1.xx to 2.0, increment versionWeight along with
+ // version.
+ public static final int versionWeight = 1902;
+ public static final String version = "1.11";
/**
* SZ Mar 9, 2009:
* Added re-initialization method. Since PcalParams class
@@ -50,7 +55,7 @@ public final class PcalParams
NoDoneDisjunct = false;
optionsInFile = false;
versionOption = null;
- inputVersionNumber = VersionToNumber(PcalParams.version);
+ inputVersionNumber = PcalParams.versionWeight;
PcalTLAGen.wrapColumn = 78;
PcalTLAGen.ssWrapColumn = 45;
tlaPcalMapping = null ;
@@ -191,17 +196,10 @@ public final class PcalParams
***********************************************************************/
public static final String BeginXlation1 = "BEGIN" ;
public static final String BeginXlation2 = "TRANSLATION" ;
- public static final String BeginXlation3 = "- the hash of the PCal code:" ;
public static final String EndXlation1 = "END" ;
public static final String EndXlation2 = "TRANSLATION" ;
- public static final String EndXlation3 = "- the hash of the generated TLA code (remove "
- + "to silence divergence warnings):" ;
- // Checksum marker keywords - introduced as part of https://github.com/tlaplus/tlaplus/issues/296
- public static final String PCAL_CHECKSUM_KEYWORD = "PCal-";
- public static final String TRANSLATED_PCAL_CHECKSUM_KEYWORD = "TLA-";
-
/*************************************************************************
* The string identifying the end of the automatically generated part of *
* the .cfg file and the beginning of the user-added part. *
@@ -254,7 +252,7 @@ public final class PcalParams
// way because of the way the code evolved, and no intelligent
// design has stepped in to fix it.
public static String versionOption = null;
- public static int inputVersionNumber = VersionToNumber(PcalParams.version);
+ public static int inputVersionNumber = PcalParams.versionWeight;
// The input file's version number * 1000
// public static boolean readOnly = false;
// True iff this is a .pcal input file and the .tla file should
@@ -317,7 +315,7 @@ public final class PcalParams
PcalDebug.reportError("Illegal version " + ver + " specified.");
return false;
}
- if (vnum > VersionToNumber(PcalParams.version)) {
+ if (vnum > PcalParams.versionWeight) {
PcalDebug.reportError("Specified version " + ver +
" later than current version " + PcalParams.version);
return false;
diff --git a/tlatools/org.lamport.tlatools/src/pcal/Translator.java b/tlatools/org.lamport.tlatools/src/pcal/Translator.java
index ade7335dd052d84c2e0fbaa306203dd795aa1082..b9a880530b8e338c588c4a907e31a4a090bc9102 100644
--- a/tlatools/org.lamport.tlatools/src/pcal/Translator.java
+++ b/tlatools/org.lamport.tlatools/src/pcal/Translator.java
@@ -62,14 +62,14 @@ public class Translator
* @param args
* @return
*/
- public boolean translate() {
+ public boolean translate(final ValidationCallBack cb) {
// The input .tla file might have unix or windows line ending. If we fail to
// properly split the input (a line per array cell), the pcal translator will
// silently fail as well.
final String[] lines = input.split("\\r?\\n");
final List<String> in = Arrays.asList(lines);
- final List<String> out = trans.performTranslation(in);
+ final List<String> out = trans.performTranslation(in, cb);
if (out != null) {
final StringBuilder buf = new StringBuilder();
final String lineSeparator = System.getProperty("line.separator");
diff --git a/tlatools/org.lamport.tlatools/src/pcal/ValidationCallBack.java b/tlatools/org.lamport.tlatools/src/pcal/ValidationCallBack.java
new file mode 100644
index 0000000000000000000000000000000000000000..91c8558039998c133aa0a367d0179c3926c997e1
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/src/pcal/ValidationCallBack.java
@@ -0,0 +1,49 @@
+/*******************************************************************************
+ * Copyright (c) 2020 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 pcal;
+
+public interface ValidationCallBack {
+
+ public enum Generate {
+ NOT_NOW, IGNORE, DO_IT;
+ }
+
+ public class Noop implements ValidationCallBack {
+ @Override
+ public boolean shouldCancel() {
+ return false;
+ }
+
+ @Override
+ public Generate shouldGenerate() {
+ return Generate.NOT_NOW;
+ }
+ }
+
+ boolean shouldCancel();
+
+ Generate shouldGenerate();
+}
diff --git a/tlatools/org.lamport.tlatools/src/pcal/Validator.java b/tlatools/org.lamport.tlatools/src/pcal/Validator.java
index b42f0d0b9f0337521f53203dadf4ff9e824181c2..2c3660e8c2c3b9d51a510891393fd702b17f0549 100644
--- a/tlatools/org.lamport.tlatools/src/pcal/Validator.java
+++ b/tlatools/org.lamport.tlatools/src/pcal/Validator.java
@@ -1,19 +1,24 @@
package pcal;
import java.io.BufferedInputStream;
-import java.io.ByteArrayOutputStream;
+import java.io.BufferedReader;
import java.io.IOException;
import java.io.InputStream;
-import java.nio.charset.StandardCharsets;
-import java.security.MessageDigest;
-import java.security.NoSuchAlgorithmException;
+import java.io.InputStreamReader;
+import java.util.ArrayList;
import java.util.Arrays;
+import java.util.HashSet;
import java.util.List;
+import java.util.Set;
import java.util.Vector;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
+import java.util.zip.CRC32;
import pcal.exception.ParseAlgorithmException;
+import pcal.exception.RemoveNameConflictsException;
+import tla2sany.modanalyzer.ParseUnit;
+import tla2sany.st.Location;
import util.TLAConstants;
/**
@@ -21,6 +26,7 @@ import util.TLAConstants;
* blocks.
*/
public class Validator {
+
public enum ValidationResult {
/** No PlusCal algorithm exists in the specification */
NO_PLUSCAL_EXISTS,
@@ -28,11 +34,11 @@ public class Validator {
/** No translation exists - BUT THERE IS PLUSCAL IN THE SPECIFICATION! */
NO_TRANSLATION_EXISTS,
- /** PlusCal and a translation block exist, but there are no checksums calculated. */
- NO_CHECKSUMS_EXIST,
+ NO_TLA_CHECKSUMS_EXIST,
+ NO_PCAL_CHECKSUMS_EXIST,
- /** One or both Checksum in the spec do not match the checksums calculated for what was found in the spec. */
- DIVERGENCE_EXISTS,
+ TLA_DIVERGENCE_EXISTS,
+ PCAL_DIVERGENCE_EXISTS,
/** A Java error was encountered while attempting to validate. */
ERROR_ENCOUNTERED,
@@ -41,72 +47,69 @@ public class Validator {
NO_DIVERGENCE;
}
+ static final String PCAL_CHECKSUM = "pcalchecksum";
+ static final String TLA_CHECKSUM = "tlachecksum";
- static protected boolean PRE_TRIM_VALIDATION_CONTENT = true;
+ static final String CHECKSUM_TEMPLATE_IGNORE = "(chksum(pcal) \\in STRING /\\ chksum(tla) \\in STRING)";
+ static final String CHECKSUM_TEMPLATE = "(chksum(pcal) = \"%s\" /\\ chksum(tla) = \"%s\")";
- static final Pattern PCAL_CHECKSUM_PATTERN = Pattern.compile(PcalParams.PCAL_CHECKSUM_KEYWORD + "[0-9a-f]+$");
- static final Pattern TRANSLATED_PCAL_CHECKSUM_PATTERN
- = Pattern.compile(PcalParams.TRANSLATED_PCAL_CHECKSUM_KEYWORD + "[0-9a-f]+$");
+ static final Pattern CHECKSUM_PATTERN = Pattern
+ .compile("\\\\\\* BEGIN TRANSLATION\\s+\\(\\s*((?i)ch(ec)?ksum\\(p(lus)?cal\\)(?-i))\\s*(=\\s*\\\"(?<"
+ + PCAL_CHECKSUM + ">[0-9A-Fa-f]*)\\\"|\\\\in\\s*"
+ + "STRING)\\s*\\/\\\\\\s*((?i)ch(ec)?ksum\\(tla\\+?\\)(?-i))\\s*(=\\s*\\\"(?<" + TLA_CHECKSUM
+ + ">[0-9A-Fa-f]*)\\\"|\\\\in\\s*STRING)\\s*\\)");
- private static final Pattern MODULE_PREFIX_PATTERN = Pattern.compile(TLAConstants.MODULE_OPENING_PREFIX_REGEX);
private static final Pattern MODULE_CLOSING_PATTERN = Pattern.compile(TLAConstants.MODULE_CLOSING_REGEX);
-
- /*
- * This regex is appropriate for only pre-MODULE-lines; the PlusCal specification states that the options line
- * may exist before the module, after the module, or within the module in a comment line or block. For our
- * purposes, we only care if it exists before the module and therefore the following regex.
- */
- private static final Pattern PLUSCAL_OPTIONS = Pattern.compile("^[\\s]*PlusCal[\\s]+options",
- Pattern.CASE_INSENSITIVE);
- /**
- * This method is a convenience wrapped around {@link #validate(List)}.
- *
- * @param inputStream an stream to the entire specification to be validated; this stream is not closed.
- * @return the result of the validation, as enumerated by the inner enum of this class.
- */
- public static ValidationResult validate(final InputStream inputStream)
+ public static Set<ValidationResult> validate(ParseUnit parseUnit, InputStream inputStream)
throws IOException {
- final String specContents;
- final ByteArrayOutputStream baos = new ByteArrayOutputStream();
- final byte[] buffer = new byte[4096];
- final BufferedInputStream bis = (inputStream instanceof BufferedInputStream)
- ? (BufferedInputStream)inputStream
- : new BufferedInputStream(inputStream);
-
- int bytesRead;
- while ((bytesRead = bis.read(buffer)) != -1) {
- baos.write(buffer, 0, bytesRead);
- }
-
- specContents = new String(baos.toByteArray(), "UTF-8");
-
- final String[] lines = specContents.split("\\r?\\n");
- int startLine = -1;
- if (PRE_TRIM_VALIDATION_CONTENT) {
- for (int i = 0; i < lines.length; i++) {
- final Matcher m = MODULE_PREFIX_PATTERN.matcher(lines[i]);
- if (m.find()) {
- startLine = i;
- break;
- } else {
- final Matcher m2 = PLUSCAL_OPTIONS.matcher(lines[i]);
- if (m2.find()) {
- startLine = i;
- break;
- }
+ final BufferedReader reader = new BufferedReader(
+ new InputStreamReader((inputStream instanceof BufferedInputStream) ? (BufferedInputStream) inputStream
+ : new BufferedInputStream(inputStream)));
+ return validate(parseUnit, reader);
+ }
+
+ public static Set<ValidationResult> validate(final ParseUnit parseUnit, final BufferedReader reader) throws IOException {
+ // Instead of matching the module start and end markers, whe while loop use SANY's
+ // parse tree that has the location of the start and end markers.
+ final Location loc = parseUnit.getParseTree().getLocation();
+
+ // Pre-allocate the number of lines we will read below.
+ final List<String> lines = new ArrayList<>(loc.endLine() - loc.beginLine());
+
+ // TODO It would be faster to let SANY look for a PlusCal algorithm when it
+ // parses the TLA+ spec (although SANY probably doesn't parse comments, it
+ // could look for the "--algorithm" or "--fair algorithm" tokens).
+ boolean seenAlgo = false;
+ int cnt = 1; // Location is 1-indexed.
+ String line;
+ while ((line = reader.readLine()) != null) {
+ // Skip lines that are not within the range given by location.
+ // This implies that this loop will miss "pluscal options" before
+ // or after the module's start and end markers. While it is legal to
+ // put options there, I've decided we don't want to pay the price
+ // of parsing the lines preceding or after a module. Users can
+ // put the options into a comment inside the module, which I
+ // believe to be the choice for most users anyway.
+ if (loc.beginLine() <= cnt && cnt <= loc.endLine()) {
+ if (line.indexOf(PcalParams.BeginAlg.substring(2)) > 0) {
+ seenAlgo = true;
}
+ lines.add(line);
+ } else if (cnt >= loc.endLine()) {
+ break;
}
+ cnt++;
}
- if (startLine < 1) {
- return validate(Arrays.asList(lines));
- } else {
- final int reducedLength = lines.length - startLine;
- final String[] reducedLines = new String[reducedLength];
-
- System.arraycopy(lines, startLine, reducedLines, 0, reducedLength);
- return validate(Arrays.asList(reducedLines));
+
+ if (!seenAlgo) {
+ // No "algorithm" string in the input => No PlusCal algorithm.
+ // The appearance of "algorithm", however, might be a false
+ // positive of which validate will take care of (I don't have
+ // time to move the logic up here).
+ return setOf(ValidationResult.NO_PLUSCAL_EXISTS);
}
+ return validate(lines);
}
/**
@@ -116,7 +119,7 @@ public class Validator {
* @param specificationText the entire specification, line by line - for historical reasons.
* @return the result of the validation, as enumerated by the inner enum of this class.
*/
- private static ValidationResult validate(final List<String> specificationText) {
+ private static Set<ValidationResult> validate(final List<String> specificationText) {
final Vector<String> deTabbedSpecification = trans.removeTabs(specificationText);
final IntPair searchLoc = new IntPair(0, 0);
@@ -187,104 +190,108 @@ public class Validator {
}
}
}
- if (!foundBegin) {
- return ValidationResult.NO_PLUSCAL_EXISTS;
- }
+
+ final Set<ValidationResult> res = new HashSet<>();
+
+ // TLA+ translation
final int translationLine = trans.findTokenPair(deTabbedSpecification, 0,
PcalParams.BeginXlation1, PcalParams.BeginXlation2);
- final String pcalMD5;
- final String translatedMD5;
if (translationLine == -1) {
- return ValidationResult.NO_TRANSLATION_EXISTS;
- } else {
- final int endTranslationLine = trans.findTokenPair(deTabbedSpecification, translationLine + 1,
- PcalParams.EndXlation1, PcalParams.EndXlation2);
- if (endTranslationLine == -1) {
- return ValidationResult.NO_TRANSLATION_EXISTS;
- }
+ res.add(ValidationResult.NO_TRANSLATION_EXISTS);
+ }
+
+ final int endTranslationLine = trans.findTokenPair(deTabbedSpecification, translationLine + 1,
+ PcalParams.EndXlation1, PcalParams.EndXlation2);
+ if (endTranslationLine == -1) {
+ res.add(ValidationResult.NO_TRANSLATION_EXISTS);
+ }
+ if (translationLine == -1 && endTranslationLine == -1) {
+ return res;
+ }
- final String beginLine = deTabbedSpecification.get(translationLine);
- Matcher m = Validator.PCAL_CHECKSUM_PATTERN.matcher(beginLine);
- if (m.find()) {
- pcalMD5 = beginLine.substring(m.start() + PcalParams.PCAL_CHECKSUM_KEYWORD.length());
- } else {
- return ValidationResult.NO_CHECKSUMS_EXIST;
- }
- final String endLine = deTabbedSpecification.get(endTranslationLine);
- m = Validator.TRANSLATED_PCAL_CHECKSUM_PATTERN.matcher(endLine);
- if (m.find()) {
- translatedMD5 = endLine.substring(m.start() + PcalParams.TRANSLATED_PCAL_CHECKSUM_KEYWORD.length());
+ // PlusCal algorithm
+ if (!foundBegin) {
+ res.add(ValidationResult.NO_PLUSCAL_EXISTS);
+ } else {
- final Vector<String> translation = new Vector<>(specificationText.subList((translationLine + 1),
- endTranslationLine));
- final String calculatedMD5 = calculateMD5(translation);
- if (!translatedMD5.equals(calculatedMD5)) {
- return ValidationResult.DIVERGENCE_EXISTS;
- }
- } else {
- translatedMD5 = null;
- }
- }
-
- try {
- ParseAlgorithm.uncomment(deTabbedSpecification, algLine, algCol);
- } catch (ParseAlgorithmException e) {
- PcalDebug.reportError(e);
- return ValidationResult.ERROR_ENCOUNTERED;
- }
+ // Get the PlusCal AST by parsing it.
+ try {
+ ParseAlgorithm.uncomment(deTabbedSpecification, algLine, algCol);
+ } catch (ParseAlgorithmException e) {
+ PcalDebug.reportError(e);
+ return setOf(ValidationResult.ERROR_ENCOUNTERED);
+ }
+
+ final TLAtoPCalMapping mapping = new TLAtoPCalMapping() ;
+ mapping.algColumn = algCol;
+ mapping.algLine = algLine;
+ PcalParams.tlaPcalMapping = mapping;
+
+ AST ast = new AST();
+ try {
+ final PcalCharReader reader = new PcalCharReader(deTabbedSpecification, algLine, algCol,
+ specificationText.size(), 0);
+ ast = ParseAlgorithm.getAlgorithm(reader, foundFairBegin);
+
+ // The call translate mutates the ast in pcal.PcalTranslate.Explode(AST, PcalSymTab).
+ // I'm ignoring the PcalParams.tlcTranslation() alternative in trans.java
+ // because I doubt the "-spec" feature is used widely (if at all).
+ final PCalTLAGenerator pcalTLAGenerator = new PCalTLAGenerator(ast);
+ pcalTLAGenerator.removeNameConflicts();
+ pcalTLAGenerator.translate();
+ } catch (ParseAlgorithmException | RemoveNameConflictsException e) {
+ PcalDebug.reportError(e);
+ // The PlusCal algorithm doesn't parse because of a syntax error. This indicates
+ // that the algorithm has been modified since it wouldn't have been possible to
+ // calculate a checksum earlier. ast will be empty string and, thus, not match below.
+ }
+
+ // Calculate the checksum value for the PlusCal's AST and compare unless no
+ // checksum to compare it with is given (or it has been disabled).
+ final Matcher m = Validator.CHECKSUM_PATTERN.matcher(deTabbedSpecification.get(translationLine));
+ if (m.find()) {
+ if (m.group(Validator.PCAL_CHECKSUM) != null) {
- // This seems like crazy poor design - we're already passing around algLine and algCol, but if we don't make
- // this arbitrary object, throw it into a global public static setting, and also assign values to it there,
- // then the ParseAlgorithm won't pick up the values..
- final TLAtoPCalMapping mapping = new TLAtoPCalMapping() ;
- mapping.algColumn = algCol;
- mapping.algLine = algLine;
- PcalParams.tlaPcalMapping = mapping;
-
- final PcalCharReader reader = new PcalCharReader(deTabbedSpecification, algLine, algCol,
- specificationText.size(), 0);
- final AST ast;
- try {
- ast = ParseAlgorithm.getAlgorithm(reader, foundFairBegin);
- } catch (ParseAlgorithmException e) {
- PcalDebug.reportError(e);
- return ValidationResult.ERROR_ENCOUNTERED;
+ final String chksumPCalAST = Validator.checksum(ast.toString());
+ if (!m.group(Validator.PCAL_CHECKSUM).equals(chksumPCalAST)) {
+ // Mismatch between the PlusCal algorithm and its checksum.
+ res.add(ValidationResult.PCAL_DIVERGENCE_EXISTS);
+ }
+ }
+ if (m.group(Validator.TLA_CHECKSUM) != null) {
+ final Vector<String> translation = new Vector<>(
+ specificationText.subList((translationLine + 1), endTranslationLine));
+ final String chksumTLATranslation = Validator.checksum(translation);
+
+ if (!m.group(Validator.TLA_CHECKSUM).equals(chksumTLATranslation)) {
+ // Mismatch between the TLA+ translation and its checksum.
+ res.add(ValidationResult.TLA_DIVERGENCE_EXISTS);
+ }
+ }
+ } else {
+ res.add(ValidationResult.NO_PCAL_CHECKSUMS_EXIST);
+ }
}
-
- final String calculatedMD5 = Validator.calculateMD5(ast.toString());
- if (!pcalMD5.equals(calculatedMD5)) {
- return ValidationResult.DIVERGENCE_EXISTS;
- }
-
- return ValidationResult.NO_DIVERGENCE;
+ return res.isEmpty() ? setOf(ValidationResult.NO_DIVERGENCE) : res;
}
- static String calculateMD5(final Vector<String> lines) {
+ public static String checksum(final Vector<String> lines) {
final StringBuilder sb = new StringBuilder();
for (final String str : lines) {
sb.append(str);
}
- return calculateMD5(sb.toString());
+ return checksum(sb.toString());
}
- static String calculateMD5(final String string) {
- try {
- final MessageDigest digest = MessageDigest.getInstance("MD5");
- final byte[] hash = digest.digest(string.getBytes(StandardCharsets.UTF_8));
- final StringBuffer hexString = new StringBuffer();
- for (int i = 0; i < hash.length; i++) {
- final String hex = Integer.toHexString(0xff & hash[i]);
- if (hex.length() == 1) {
- hexString.append('0');
- }
- hexString.append(hex);
- }
- return hexString.toString();
- } catch (final NoSuchAlgorithmException e) {
- PcalDebug.reportError("Unable to calculate MD5: " + e.getMessage());
- return null;
- }
+ static String checksum(final String string) {
+ final CRC32 crc32 = new CRC32();
+ crc32.update(string.getBytes());
+ return Long.toHexString(crc32.getValue());
+ }
+
+ private static Set<ValidationResult> setOf(ValidationResult... res) {
+ return new HashSet<>(Arrays.asList(res));
}
}
diff --git a/tlatools/org.lamport.tlatools/src/pcal/trans.java b/tlatools/org.lamport.tlatools/src/pcal/trans.java
index 57fe07a9ce91a59c4606deb5d9ffe1899f6b17fe..428dbcda55863f27945be154b49e9ac8b6d99dad 100644
--- a/tlatools/org.lamport.tlatools/src/pcal/trans.java
+++ b/tlatools/org.lamport.tlatools/src/pcal/trans.java
@@ -13,6 +13,7 @@ import java.util.List;
import java.util.Vector;
import java.util.regex.Matcher;
+import pcal.ValidationCallBack.Generate;
import pcal.exception.FileToStringVectorException;
import pcal.exception.ParseAlgorithmException;
import pcal.exception.PcalResourceFileReaderException;
@@ -290,9 +291,9 @@ class trans {
static final int STATUS_EXIT_WITH_ERRORS = -1;
private static final String PCAL_TRANSLATION_COMMENT_LINE_PREFIX
- = "\\* " + PcalParams.BeginXlation1 + " " + PcalParams.BeginXlation2 + " " + PcalParams.BeginXlation3;
+ = "\\* " + PcalParams.BeginXlation1 + " " + PcalParams.BeginXlation2;
private static final String TLA_TRANSLATION_COMMENT_LINE_PREFIX
- = "\\* " + PcalParams.EndXlation1 + " " + PcalParams.EndXlation2 + " " + PcalParams.EndXlation3;
+ = "\\* " + PcalParams.EndXlation1 + " " + PcalParams.EndXlation2;
/**
@@ -570,6 +571,10 @@ class trans {
// For some reason this method used to both mutate the argument, and then also returns that argument... ?
// Now we copy the argument, mutate the copy, and return that.
public static List<String> performTranslation(final List<String> specificationText) {
+ return performTranslation(specificationText, new ValidationCallBack.Noop());
+ }
+
+ public static List<String> performTranslation(final List<String> specificationText, ValidationCallBack cb) {
/**
* Create the new TLAtoPCalMapping object, call it mapping
* here and set PcalParams.tlaPcalMapping to point to it.
@@ -679,9 +684,10 @@ class trans {
final ArrayList<String> output = new ArrayList<>(specificationText);
translationLine = findTokenPair(untabInputVec, 0, PcalParams.BeginXlation1, PcalParams.BeginXlation2);
+ int endTranslationLine = -1;
if (translationLine != -1)
{
- int endTranslationLine = findTokenPair(untabInputVec, translationLine + 1,
+ endTranslationLine = findTokenPair(untabInputVec, translationLine + 1,
PcalParams.EndXlation1, PcalParams.EndXlation2);
if (endTranslationLine == -1)
{
@@ -689,12 +695,13 @@ class trans {
return null;
}
- endTranslationLine--;
- while (translationLine < endTranslationLine)
+
+ int etl = endTranslationLine - 1;
+ while (translationLine < etl)
{
- output.remove(endTranslationLine);
- untabInputVec.remove(endTranslationLine);
- endTranslationLine--;
+ output.remove(etl);
+ untabInputVec.remove(etl);
+ etl--;
}
}
@@ -744,7 +751,7 @@ class trans {
*/
mapping.algColumn = algCol;
mapping.algLine = algLine;
-
+
if (translationLine == -1)
{
/****************************************************************
@@ -836,7 +843,8 @@ class trans {
return null ;
} ;
- output.add((ecLine + 1), (PCAL_TRANSLATION_COMMENT_LINE_PREFIX + " "));
+ output.add((ecLine + 1), (PCAL_TRANSLATION_COMMENT_LINE_PREFIX + " "
+ + String.format(Validator.CHECKSUM_TEMPLATE, "ffffffff", "ffffffff")));
untabInputVec.insertElementAt(PCAL_TRANSLATION_COMMENT_LINE_PREFIX, (ecLine + 1));
output.add((ecLine + 2), (TLA_TRANSLATION_COMMENT_LINE_PREFIX + " "));
untabInputVec.insertElementAt(TLA_TRANSLATION_COMMENT_LINE_PREFIX, (ecLine + 2));
@@ -845,26 +853,18 @@ class trans {
//System.out.println(ecLine + ", " + ecCol);
//Debug.printVector(inputVec, "foo");
}
- else {
- // if it has an existing checksum suffix then get rid of it
- final String originalBeginLine = output.remove(translationLine);
- Matcher m = Validator.PCAL_CHECKSUM_PATTERN.matcher(originalBeginLine);
- String outputLine;
- if (m.find()) {
- outputLine = PCAL_TRANSLATION_COMMENT_LINE_PREFIX + " ";
- } else {
- outputLine = originalBeginLine + " ";
- }
- output.add(translationLine, outputLine);
-
- final String originalEndLine = output.remove(translationLine + 1);
- m = Validator.TRANSLATED_PCAL_CHECKSUM_PATTERN.matcher(originalEndLine);
- if (m.find()) {
- outputLine = TLA_TRANSLATION_COMMENT_LINE_PREFIX + " ";
- } else {
- outputLine = originalEndLine + " ";
- }
- output.add((translationLine + 1), outputLine);
+ else {
+ // Check if the existing TLA+ translation has been modified by the user and
+ // raise a warning (via cb) if translation should be cancelled to not
+ // lose/overwrite the user changes.
+ final Matcher m = Validator.CHECKSUM_PATTERN.matcher(output.get(translationLine));
+ if (m.find() && m.group(Validator.TLA_CHECKSUM) != null) {
+ final String checksumTLATranslation = Validator
+ .checksum(new Vector<>(specificationText.subList((translationLine + 1), endTranslationLine)));
+ if (!m.group(Validator.TLA_CHECKSUM).equals(checksumTLATranslation) && cb.shouldCancel()) {
+ return null;
+ }
+ }
}
/*
@@ -922,7 +922,6 @@ class trans {
}
PcalDebug.reportInfo("Parsing completed.");
- final String pcalMD5 = Validator.calculateMD5(ast.toString());
// tla-pcal debugging
//System.out.println("Translation Output:");
//System.out.println(ast.toString());
@@ -995,13 +994,34 @@ class trans {
return null ; // added for testing
}
}
-
- final String beginLine = output.remove(mapping.tlaStartLine - 1);
- output.add((mapping.tlaStartLine - 1), (beginLine + PcalParams.PCAL_CHECKSUM_KEYWORD + pcalMD5));
-
- final String translationMD5 = Validator.calculateMD5(translation);
- final String endLine = output.remove(mapping.tlaStartLine);
- output.add(mapping.tlaStartLine, (endLine + PcalParams.TRANSLATED_PCAL_CHECKSUM_KEYWORD + translationMD5));
+
+ final Matcher m = Validator.CHECKSUM_PATTERN.matcher(output.get(mapping.tlaStartLine - 1));
+ ValidationCallBack.Generate g = null;
+ if (m.find()) {
+ // Do TLA_CHECKSUM first because doing PCAL_CHECKSUM (at the front of the
+ // string) invalidates start end enf of the TLA_CHECKSUM match.
+ if (m.group(Validator.TLA_CHECKSUM) != null) {
+ output.set(mapping.tlaStartLine - 1,
+ new StringBuilder(output.get(mapping.tlaStartLine - 1)).replace(m.start(Validator.TLA_CHECKSUM),
+ m.end(Validator.TLA_CHECKSUM), Validator.checksum(translation)).toString());
+ }
+ if (m.group(Validator.PCAL_CHECKSUM) != null) {
+ output.set(mapping.tlaStartLine - 1,
+ new StringBuilder(output.get(mapping.tlaStartLine - 1))
+ .replace(m.start(Validator.PCAL_CHECKSUM), m.end(Validator.PCAL_CHECKSUM),
+ Validator.checksum(ast.toString()))
+ .toString());
+ }
+ } else if ((g = cb.shouldGenerate()) != Generate.NOT_NOW) {
+ if (g == Generate.DO_IT) {
+ output.set(mapping.tlaStartLine - 1,
+ output.get(mapping.tlaStartLine - 1) + " " + String.format(Validator.CHECKSUM_TEMPLATE,
+ Validator.checksum(ast.toString()), Validator.checksum(translation)));
+ } else {
+ output.set(mapping.tlaStartLine - 1,
+ output.get(mapping.tlaStartLine - 1) + " " + Validator.CHECKSUM_TEMPLATE_IGNORE);
+ }
+ }
/*********************************************************************
* Add the translation to outputVec. *
@@ -1924,6 +1944,14 @@ class trans {
}
next = next + 1;
}
+ // The following line is a hack to eliminate a rare bug that caused
+ // the translation to loop forever if a line ended with a symbol
+ // that is the prefix of a legal BUILT_IN token and that is not
+ // a legal token but has a prefix that is a legal token--for
+ // example "(+" and "::" (since ::= is a legal operator).
+ // It was added by LL on 13 May 2020
+ newLine = newLine + " ";
+
newVec.add(newLine);
}
diff --git a/tlatools/org.lamport.tlatools/src/tla2sany/drivers/SANY.java b/tlatools/org.lamport.tlatools/src/tla2sany/drivers/SANY.java
index ac724a869dacc2b4d97fc2093bc32ba83ef7a7b9..2ae22d90d45f955d61217e07cf3752cc9cfe06fc 100644
--- a/tlatools/org.lamport.tlatools/src/tla2sany/drivers/SANY.java
+++ b/tlatools/org.lamport.tlatools/src/tla2sany/drivers/SANY.java
@@ -197,6 +197,10 @@ public class SANY {
// Parse all of the files referred to by the top-level file in specification
public static void frontEndParse(SpecObj spec, PrintStream syserr)
+ throws ParseException {
+ frontEndParse(spec, syserr, true);
+ }
+ public static void frontEndParse(SpecObj spec, PrintStream syserr, boolean validatePCalTranslation)
throws ParseException {
/***********************************************************************
* Modified on 12 May 2008 by LL to remove "throws AbortException", *
@@ -206,7 +210,7 @@ public class SANY {
try
{
// Actual parsing method called from inside loadSpec()
- if (!spec.loadSpec(spec.getFileName(), spec.parseErrors, true))
+ if (!spec.loadSpec(spec.getFileName(), spec.parseErrors, validatePCalTranslation))
{
// dead code SZ 02. Aug 2009
/*
diff --git a/tlatools/org.lamport.tlatools/src/tla2sany/modanalyzer/SpecObj.java b/tlatools/org.lamport.tlatools/src/tla2sany/modanalyzer/SpecObj.java
index 544993ce298daeaf2e1cdb0c1b15818feb07532a..307699145876438d0d922b141336d115b3f7208a 100644
--- a/tlatools/org.lamport.tlatools/src/tla2sany/modanalyzer/SpecObj.java
+++ b/tlatools/org.lamport.tlatools/src/tla2sany/modanalyzer/SpecObj.java
@@ -11,6 +11,7 @@ import java.util.Hashtable;
import java.util.Set;
import pcal.Validator;
+import pcal.Validator.ValidationResult;
import tla2sany.semantic.AbortException;
import tla2sany.semantic.Errors;
import tla2sany.semantic.ExternalModuleTable;
@@ -1006,30 +1007,44 @@ public class SpecObj
final File f = parseUnit.getNis().sourceFile();
try (final FileInputStream fis = new FileInputStream(f)) {
- final Validator.ValidationResult result = Validator.validate(fis);
+ final Set<ValidationResult> results = Validator.validate(parseUnit, fis);
- switch (result) {
- case NO_PLUSCAL_EXISTS:
- case NO_DIVERGENCE:
- case NO_CHECKSUMS_EXIST:
- break;
- case ERROR_ENCOUNTERED:
- ToolIO.err.println("A Java problem was encountered attempting to validate the specification for "
- + parseUnit.getName());
-
- break;
- case NO_TRANSLATION_EXISTS:
- ToolIO.out.println("PlusCal was found in the specification for " + parseUnit.getName()
- + " but no TLA+ translation block for it could be found.");
-
- break;
- case DIVERGENCE_EXISTS:
- ToolIO.out.println("!! WARNING: Either the PlusCal or its TLA+ translation has changed in the "
- + "specification for " + parseUnit.getName()
- + " since the last time translation was performed.");
-
- break;
- }
+ if (results.contains(ValidationResult.TLA_DIVERGENCE_EXISTS) && results.contains(ValidationResult.PCAL_DIVERGENCE_EXISTS)) {
+ /* Both hashes are invalid.
+ This is probably a sequel to Case 3, in which the user has decided either
+ (1) she has fixed the bug or (2) wants to change the spec and will later
+ modify the translation.
+ TLC called: By default, a warning should be raised. It should be considered
+ the same as Case 2. */
+ ToolIO.out.println(String.format(
+ "!! WARNING: The PlusCal algorithm and its TLA+ translation in "
+ + "module %s filename since the last translation.",
+ parseUnit.getName()));
+ } else if (results.contains(ValidationResult.TLA_DIVERGENCE_EXISTS)) {
+ /* The algorithm hash is valid and the translation hash is invalid.
+ There are two reasons: (1) The user is debugging the spec, or
+ (2) She needed to modify the translation because she wants a spec that can't
+ be produced by PlusCal.
+ TLC called: In both cases, no warning should be needed. However,
+ in (1), she might have finished debugging and forgotten to run the
+ translator. To handle case (1), I suggest the default should be to run
+ TLC but raise a transient window with a warning that is easily ignored.
+ For case (2), it should be possible to put something in a translation
+ comment to disable the warning. */
+ ToolIO.out.println(String.format("!! WARNING: The TLA+ translation in "
+ + "module %s has changed since its last translation.", parseUnit.getName()));
+ } else if (results.contains(ValidationResult.PCAL_DIVERGENCE_EXISTS)) {
+ /* The algorithm hash is invalid and the translation hash is valid.
+ TLC called: By default, a warning should be generated. I see little reason
+ for not generating the warning. So, it doesn't matter if its inconvenient
+ to turn off the warning, but turning it off should affect only the current
+ spec; and it should be easy to turn back on. */
+ ToolIO.out.println(String.format("!! WARNING: The PlusCal algorithm in "
+ + "module %s has changed since its last translation.", parseUnit.getName()));
+ } else if (results.contains(ValidationResult.ERROR_ENCOUNTERED)) {
+ ToolIO.err.println("A unexpected problem was encountered attempting to validate the specification for "
+ + parseUnit.getName());
+ }
} catch (final IOException e) {
ToolIO.err.println("Encountered an exception while attempt to validate " + f.getAbsolutePath() + " - "
+ e.getMessage());
@@ -1053,4 +1068,8 @@ public class SpecObj
this.globalContextErrors = globalContextErrors;
}
+ public ParseUnit getRootParseUnit() {
+ return this.parseUnitContext.get(this.getName());
+ }
+
}
\ No newline at end of file
diff --git a/tlatools/org.lamport.tlatools/src/tla2sany/semantic/AtNode.java b/tlatools/org.lamport.tlatools/src/tla2sany/semantic/AtNode.java
index 2a673d779722fed014cb8314f131435962e58774..1d7f522ee9954272d71e926b0e7fa85b58efbc14 100644
--- a/tlatools/org.lamport.tlatools/src/tla2sany/semantic/AtNode.java
+++ b/tlatools/org.lamport.tlatools/src/tla2sany/semantic/AtNode.java
@@ -153,8 +153,10 @@ public class AtNode extends ExprNode {
*/
@Override
public final void walkGraph(Hashtable<Integer, ExploreNode> h, ExplorerVisitor visitor) {
+ visitor.preVisit(this);
// Empty because there are no nodes reachable through an AtNode that are not
// reachable by other paths through the semantic graph.
+ visitor.postVisit(this);
} // end walkGraph()
diff --git a/tlatools/org.lamport.tlatools/src/tla2tex/LaTeXOutput.java b/tlatools/org.lamport.tlatools/src/tla2tex/LaTeXOutput.java
index 051caaa6f6baebf5b49ca2d98061bc36f74d86dc..001b9aaa128ee9b3741d23611d87cc955d091637 100644
--- a/tlatools/org.lamport.tlatools/src/tla2tex/LaTeXOutput.java
+++ b/tlatools/org.lamport.tlatools/src/tla2tex/LaTeXOutput.java
@@ -41,6 +41,7 @@ import java.io.FileInputStream;
import java.io.FileNotFoundException;
import java.io.IOException;
import java.io.InputStreamReader;
+import java.util.Arrays;
import java.util.Vector;
import util.ToolIO;
@@ -566,7 +567,7 @@ private static void InnerWriteAlignmentFile(Token[][] spec,
line = line + 1;
} ;
- PosAndCol.sort(posCols);
+ Arrays.sort(posCols);
/************************************************************************
* Compute preSpace fields for tokens in the order they appear in the *
diff --git a/tlatools/org.lamport.tlatools/src/tla2tex/PosAndCol.java b/tlatools/org.lamport.tlatools/src/tla2tex/PosAndCol.java
index 828613fb0a932b67875a25e1a9470522c352113a..d33ab345896177cef279f8edbb55c5126b86682e 100644
--- a/tlatools/org.lamport.tlatools/src/tla2tex/PosAndCol.java
+++ b/tlatools/org.lamport.tlatools/src/tla2tex/PosAndCol.java
@@ -13,7 +13,7 @@
package tla2tex;
// import tlatex.Position;
//import java.util.Comparator;
-public class PosAndCol extends Position
+public class PosAndCol extends Position implements Comparable<PosAndCol>
{ public int column ;
public PosAndCol(int l, int i, int c)
@@ -22,72 +22,19 @@ public class PosAndCol extends Position
column = c ;
} ;
- /************************************************************************
- * The following heap-sorting method was obtained by trivially modifying *
- * a method found on the web with the following header: *
- * *
- * HeapSortAlgorithm.java 1.0 95/06/23 Jason Harrison *
- * Copyright (c) 1995 University of British Columbia *
- * *
- * Permission to use, copy, modify, and distribute this software *
- * and its documentation for NON-COMMERCIAL purposes and without *
- * fee is hereby granted provided that this copyright notice *
- * appears in all copies. *
- * *
- * UBC MAKES NO REPRESENTATIONS OR WARRANTIES ABOUT THE SUITABILITY *
- * OF THE SOFTWARE, EITHER EXPRESS OR IMPLIED, INCLUDING BUT NOT *
- * LIMITED TO THE IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS *
- * FOR A PARTICULAR PURPOSE, OR NON-INFRINGEMENT. UBC SHALL NOT BE *
- * LIABLE FOR ANY DAMAGES SUFFERED BY LICENSEE AS A RESULT OF *
- * USING, MODIFYING OR DISTRIBUTING THIS SOFTWARE OR ITS *
- * DERIVATIVES *
- ************************************************************************/
- public static void sort(PosAndCol a[])
- { int N = a.length;
- for (int k = N/2; k > 0; k--)
- { downHeap(a, k, N);
- }
- do { PosAndCol T = a[0];
- a[0] = a[N - 1];
- a[N - 1] = T;
- N = N - 1;
- downHeap(a, 1, N);
- }
- while (N > 1);
- }
- private static void downHeap(PosAndCol a[], int k, int N)
- { PosAndCol T = a[k - 1];
- while (k <= N/2)
- { int j = k + k;
- if ((j < N) && PosAndCol.lessThan(a[j - 1],a[j]))
- { j++; }
- if ( ! PosAndCol.lessThan(T, a[j - 1]) )
- { break; }
- else
- { a[k - 1] = a[j - 1];
- k = j;
- }
- }
- a[k - 1] = T;
- }
-
- private static boolean lessThan(PosAndCol pc1, PosAndCol pc2)
- { if (pc1.column < pc2.column)
- { return true ;}
- else
- { if (pc1.column == pc2.column)
- { return (pc1.line < pc2.line) ;
- }
- else
- { return false ;
- }
- }
- }
public String toString()
{ return "[line |-> " + line + ", item |-> " + item
+ ", col |-> " + column + "]";
}
+
+ @Override
+ public int compareTo(final PosAndCol other) {
+ if (column == other.column) {
+ return Integer.compare(line, other.line);
+ }
+ return Integer.compare(column, other.column);
+ }
}
/* Last modified on Tue 18 Sep 2007 at 6:51:12 PST0by lamport */
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/TLC.java b/tlatools/org.lamport.tlatools/src/tlc2/TLC.java
index 2e3e38adaa51e981410592df69d498b5eae0e59b..2be228550dbfe50d760faf65896e8f05b7d78ebd 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/TLC.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/TLC.java
@@ -26,7 +26,7 @@ import java.util.List;
import java.util.Map;
import java.util.Random;
import java.util.TimeZone;
-import java.util.concurrent.atomic.AtomicBoolean;
+import java.util.concurrent.Phaser;
import model.InJarFilenameToStream;
import model.ModelInJar;
@@ -137,7 +137,7 @@ public class TLC {
private MCParserResults mcParserResults;
private MCOutputPipeConsumer mcOutputConsumer;
private boolean avoidMonolithSpecTECreation;
- private final AtomicBoolean waitingOnGenerationCompletion;
+ private final Phaser waitingOnGenerationCompletion;
/**
* Initialization
@@ -164,7 +164,8 @@ public class TLC {
fpSetConfiguration = new FPSetConfiguration();
avoidMonolithSpecTECreation = false;
- waitingOnGenerationCompletion = new AtomicBoolean(false);
+ waitingOnGenerationCompletion = new Phaser();
+ waitingOnGenerationCompletion.register();
}
/*
@@ -438,7 +439,7 @@ public class TLC {
final Runnable r = () -> {
boolean haveClosedOutputStream = false;
try {
- waitingOnGenerationCompletion.set(true);
+ waitingOnGenerationCompletion.register();
mcOutputConsumer.consumeOutput(false);
bos.flush();
@@ -480,10 +481,7 @@ public class TLC {
monolithCreator.copy();
}
- waitingOnGenerationCompletion.set(false);
- synchronized(this) {
- notifyAll();
- }
+ waitingOnGenerationCompletion.arriveAndDeregister();
} catch (final Exception e) {
MP.printMessage(EC.GENERAL,
"A model checking error occurred while parsing tool output; the execution "
@@ -747,7 +745,7 @@ public class TLC {
{
try
{
- int num = args[index].strip().toLowerCase().equals("auto")
+ int num = args[index].trim().toLowerCase().equals("auto")
? Runtime.getRuntime().availableProcessors()
: Integer.parseInt(args[index]);
if (num < 1)
@@ -1132,13 +1130,7 @@ public class TLC {
TLCGlobals.tool ? Long.toString(runtime) + "ms" : convertRuntimeToHumanReadable(runtime));
MP.flush();
- while (waitingOnGenerationCompletion.get()) {
- synchronized (this) {
- try {
- wait();
- } catch (final InterruptedException ie) { }
- }
- }
+ waitingOnGenerationCompletion.arriveAndAwaitAdvance();
}
}
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/TLCGlobals.java b/tlatools/org.lamport.tlatools/src/tlc2/TLCGlobals.java
index e6aee0b5c60b17f2d671a4038194dada25ccfe68..d68116ed66325a1ca4b4f3f87dd6fd430cc0af2e 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.15 of Day Month 20??";
+ public static String versionOfTLC = "Version 2.16 of 31 December 2020";
// The bound for set enumeration, used for pretty printing
public static int enumBound = 2000;
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/module/TLC.java b/tlatools/org.lamport.tlatools/src/tlc2/module/TLC.java
index 1f87e6cea5471800cf97d19c15381dd40dd4dbd7..b1a5277f1f056ec7be82f9ff2887ce7ddb87e2d2 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/module/TLC.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/module/TLC.java
@@ -252,7 +252,7 @@ public class TLC implements ValueConstants
TLCGlobals.mainChecker.setAllValues(idx, val);
} else
{
- tlc2.TLCGlobals.simulator.setLocalValue(idx, val);
+ tlc2.TLCGlobals.simulator.setAllValues(idx, val);
}
return BoolValue.ValTrue;
}
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/output/SpecTraceExpressionWriter.java b/tlatools/org.lamport.tlatools/src/tlc2/output/SpecTraceExpressionWriter.java
index 0ccd401726e88e50bf6a875a3f9cf4d19e559a90..38d4cc4e6968030a9c7fa253ca8c8f2a2b1c14f9 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/output/SpecTraceExpressionWriter.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/output/SpecTraceExpressionWriter.java
@@ -265,7 +265,7 @@ public class SpecTraceExpressionWriter extends AbstractSpecWriter {
initAndNext.append(TLAConstants.TRACE_NA);
} else {
// add the actual expression if it is not temporal level
- initAndNext.append(expressionInfo.getExpression());
+ initAndNext.append(expressionInfo.getIdentifier());
}
initAndNext.append(TLAConstants.CR).append(TLAConstants.INDENT).append(TLAConstants.INDENT);
@@ -453,7 +453,7 @@ public class SpecTraceExpressionWriter extends AbstractSpecWriter {
subActionsAndConstraint.append(expressionInfo.getVariableName()).append(TLAConstants.PRIME);
subActionsAndConstraint.append(TLAConstants.EQ).append(TLAConstants.L_PAREN).append(TLAConstants.CR);
subActionsAndConstraint.append(TRI_INDENT);
- subActionsAndConstraint.append(expressionInfo.getExpression()).append(TLAConstants.CR);
+ subActionsAndConstraint.append(expressionInfo.getIdentifier()).append(TLAConstants.CR);
subActionsAndConstraint.append(TRI_INDENT).append(TLAConstants.R_PAREN);
if (expressionInfo.getLevel() < 2) {
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/ConcurrentTLCTrace.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/ConcurrentTLCTrace.java
index 5fb94b5761659bc643594fceeeef5728a3e7ce4c..0cf1ce2b3a15d4f16e9ff95eb7b6db2911b2fc6f 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/ConcurrentTLCTrace.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/ConcurrentTLCTrace.java
@@ -25,6 +25,7 @@
******************************************************************************/
package tlc2.tool;
+import java.io.File;
import java.io.IOException;
import tlc2.TLCGlobals;
@@ -157,6 +158,23 @@ public class ConcurrentTLCTrace extends TLCTrace {
for (Worker worker : workers) {
worker.commitChkpt();
}
+ // MAK 06/08/2020:
+ // Touch MC.st.chkpt (in addition to the worker-created MC-${N}.chkpt files)
+ // that (single-worker) TLCTrace creates. The Toolbox checks for the existence
+ // of checkpoints by looking for this file (see
+ // org.lamport.tla.toolbox.tool.tlc.model.Model.getCheckpoints(boolean)). If
+ // the Toolbox check fails, a user cannot resume/restart model-checking from
+ // the checkpoint. Addresses Github issue #469 at
+ // https://github.com/tlaplus/tlaplus/issues/469
+ //
+ // We create an empty file here instead of changing the Toolbox in case 3rd party
+ // integrations and scripts rely on the file's existence. Reading the empty
+ // MC.st.chkpt with an older TLC release will crash and thus make a user aware
+ // that recovery fails.
+ //
+ // createNewFile is safe to call periodically when a checkpoint get taken
+ // because it does *not* throw an exception if the file already exists.
+ new File(filename + ".chkpt").createNewFile();
}
public void recover() throws IOException {
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/DFIDModelChecker.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/DFIDModelChecker.java
index 404fc7b6b66873cd7bc9a3377afb7595a256bff1..c333ed588ace262232bccedf31ab9ff82803cf8b 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/DFIDModelChecker.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/DFIDModelChecker.java
@@ -20,6 +20,7 @@ import tlc2.util.IStateWriter;
import tlc2.util.IdThread;
import tlc2.util.LongVec;
import tlc2.util.SetOfStates;
+import util.Assert;
import util.FileUtil;
import util.UniqueString;
@@ -58,7 +59,14 @@ public class DFIDModelChecker extends AbstractChecker
// call the abstract constructor
super(tool, metadir, stateWriter, deadlock, fromChkpt, startTime);
- this.theInitStates = null;
+ // https://github.com/tlaplus/tlaplus/issues/548
+ Assert.check(TLCGlobals.getNumWorkers() == 1, EC.GENERAL,
+ "Depth-First Iterative Deepening mode does not support multiple workers (https://github.com/tlaplus/tlaplus/issues/548). Please run TLC with a single worker.");
+ // https://github.com/tlaplus/tlaplus/issues/548
+ Assert.check(this.checkLiveness == false, EC.GENERAL,
+ "Depth-First Iterative Deepening mode does not support checking liveness properties (https://github.com/tlaplus/tlaplus/issues/548). Please check liveness properties in Breadth-First-Search mode.");
+
+ this.theInitStates = null;
this.theInitFPs = null;
this.theFPSet = new MemFPIntSet(); // init the state set
this.theFPSet.init(TLCGlobals.getNumWorkers(), this.metadir, this.tool.getRootFile());
@@ -186,7 +194,9 @@ public class DFIDModelChecker extends AbstractChecker
result = this.runTLC(level);
// Recent done flag before after the workers have checked the
// current level in preparation for the next level.
- this.done = false;
+ synchronized (this) {
+ this.done = false;
+ }
if (result != EC.NO_ERROR)
return result;
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/EvalException.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/EvalException.java
index c8bdfe0e3a87beab4126642a486ca1a8299c0aa8..11c64865172b6e245edd54997794f451e91698d5 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/EvalException.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/EvalException.java
@@ -21,28 +21,38 @@ public class EvalException extends RuntimeException
private final int errorCode;
+ private final String[] parameters;
public EvalException(int errorCode, String[] parameters)
{
super(MP.getMessage(errorCode, parameters));
this.errorCode = errorCode;
+ this.parameters = parameters;
}
public EvalException(int errorCode, String parameter)
{
- super(MP.getMessage(errorCode, parameter));
- this.errorCode = errorCode;
+ this(errorCode, new String[] {parameter});
}
public EvalException(int errorCode)
{
super(MP.getMessage(errorCode));
- this.errorCode = errorCode;
+ this.errorCode = errorCode;
+ this.parameters = null;
}
public int getErrorCode() {
return errorCode;
}
+
+ public String[] getParameters() {
+ return parameters;
+ }
+
+ public boolean hasParameters() {
+ return parameters != null;
+ }
// SZ Jul 14, 2009: refactored and deprecated, all usage changed to standard constructor
// public EvalException(int type, String message)
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/ITool.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/ITool.java
index 79b93dcd76af14e745afd58e90414eff74625ea2..4f0924ce78cf166d97b1f984332a16298172e392 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/ITool.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/ITool.java
@@ -162,6 +162,8 @@ public interface ITool extends TraceApp {
boolean[] getAssumptionIsAxiom();
+ int checkAssumptions();
+
String[] getInvNames();
String[] getImpliedActNames();
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/ModelChecker.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/ModelChecker.java
index 22f3c315b00a83c8092bb79d721d01b4cef390f7..44025b2f9e7547438b018af77d31f3c81801fe80 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/ModelChecker.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/ModelChecker.java
@@ -14,7 +14,6 @@ import java.util.concurrent.ExecutionException;
import java.util.concurrent.Future;
import java.util.stream.Collectors;
-import tla2sany.semantic.ExprNode;
import tla2sany.semantic.OpDeclNode;
import tlc2.TLCGlobals;
import tlc2.output.EC;
@@ -283,6 +282,10 @@ public class ModelChecker extends AbstractChecker
} catch (FingerprintException e)
{
result = MP.printError(EC.TLC_FINGERPRINT_EXCEPTION, new String[]{e.getTrace(), e.getRootCause().getMessage()});
+ } catch (EvalException e) {
+ // Do not replace the actual error code, such as assert violation, with TLC_NESTED_EXPRESSION.
+ MP.printError(EC.TLC_NESTED_EXPRESSION, cTool.toString());
+ result = e.getErrorCode();
} catch (Throwable e)
{
// Assert.printStack(e);
@@ -324,27 +327,7 @@ public class ModelChecker extends AbstractChecker
*/
public int checkAssumptions()
{
- ExprNode[] assumps = this.tool.getAssumptions();
- boolean[] isAxiom = this.tool.getAssumptionIsAxiom();
- int assumptionsError = EC.NO_ERROR;
- for (int i = 0; i < assumps.length; i++)
- {
- try
- {
- if ((!isAxiom[i]) && !this.tool.isValid(assumps[i]))
- {
- OutputCollector.addViolatedAssumption(assumps[i]);
- assumptionsError = MP.printError(EC.TLC_ASSUMPTION_FALSE, assumps[i].toString());
- }
- } catch (Exception e)
- {
- // Assert.printStack(e);
- OutputCollector.addViolatedAssumption(assumps[i]);
- assumptionsError = MP.printError(EC.TLC_ASSUMPTION_EVALUATION_ERROR,
- new String[] { assumps[i].toString(), e.getMessage() });
- }
- }
- return assumptionsError;
+ return this.tool.checkAssumptions();
}
/**
@@ -639,6 +622,9 @@ public class ModelChecker extends AbstractChecker
} else if (e instanceof AssertionError)
{
ec = EC.TLC_BUG;
+ } else if (e instanceof EvalException)
+ {
+ ec = ((EvalException) e).getErrorCode();
} else
{
ec = EC.GENERAL;
@@ -648,7 +634,15 @@ public class ModelChecker extends AbstractChecker
{
if (!(ec == EC.GENERAL && e.getMessage() == null))
{
- MP.printError(ec, e);
+ if (e instanceof EvalException && ((EvalException) e).hasParameters()) {
+ // An EvalException pretty-prints itself in its constructor, i.e. converts the
+ // parameters into the human readable string. However, MP.print* will
+ // pretty-print it a second time, which is why we pass the original parameters
+ // instead of the EvalException itself. Exception handling in TLC is a mess!
+ MP.printError(ec, ((EvalException) e).getParameters(), e);
+ } else {
+ MP.printError(ec, e);
+ }
}
this.trace.printTrace(curState, succState);
this.theStateQueue.finishAll();
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/SimulationWorker.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/SimulationWorker.java
index 64a4940fcebd3df054ebb73628cf3758986bb43e..0e40e2890342e1b8dc16e84a740c51133e2e2354 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/SimulationWorker.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/SimulationWorker.java
@@ -68,7 +68,7 @@ public class SimulationWorker extends IdThread {
StateVec stateTrace;
// The set of initial states for the spec.
- private final StateVec initStates;
+ private StateVec initStates;
// The queue that the worker places its results onto.
private final BlockingQueue<SimulationWorkerResult> resultQueue;
@@ -181,7 +181,7 @@ public class SimulationWorker extends IdThread {
}
- public SimulationWorker(int id, ITool tool, StateVec initStates, BlockingQueue<SimulationWorkerResult> resultQueue,
+ public SimulationWorker(int id, ITool tool, BlockingQueue<SimulationWorkerResult> resultQueue,
long seed, long maxTraceDepth, long maxTraceNum, boolean checkDeadlock, String traceFile,
ILiveCheck liveCheck, LongAdder numOfGenStates, LongAdder numOfGenTraces) {
super(id);
@@ -190,7 +190,6 @@ public class SimulationWorker extends IdThread {
this.maxTraceDepth = maxTraceDepth;
this.maxTraceNum = maxTraceNum;
this.resultQueue = resultQueue;
- this.initStates = initStates;
this.checkDeadlock = checkDeadlock;
this.traceFile = traceFile;
this.liveCheck = liveCheck;
@@ -410,4 +409,13 @@ public class SimulationWorker extends IdThread {
// Finished trace generation without any errors.
return Optional.empty();
}
+
+ public final StateVec getTrace() {
+ return stateTrace;
+ }
+
+ public void start(StateVec initStates) {
+ this.initStates = initStates;
+ this.start();
+ }
}
\ No newline at end of file
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/Simulator.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/Simulator.java
index cd1dfa77bb227c374db35849ded75760640fcb49..d972edaea356225a8a8e86dc895c802423e4d393 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/Simulator.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/Simulator.java
@@ -72,8 +72,6 @@ public class Simulator {
this.rng = rng;
this.seed = seed;
this.aril = 0;
- this.numWorkers = numWorkers;
- this.workers = new ArrayList<>(numWorkers);
// Initialization for liveness checking
if (this.checkLiveness) {
if (EXPERIMENTAL_LIVENESS_SIMULATION) {
@@ -86,6 +84,14 @@ public class Simulator {
liveCheck = new NoOpLiveCheck(tool, specDir);
}
+ this.numWorkers = numWorkers;
+ this.workers = new ArrayList<>(numWorkers);
+ for (int i = 0; i < this.numWorkers; i++) {
+ this.workers.add(new SimulationWorker(i, this.tool, this.workerResultQueue, this.rng.nextLong(),
+ this.traceDepth, this.traceNum, this.checkDeadlock, this.traceFile, this.liveCheck,
+ this.numOfGenStates, this.numOfGenTraces));
+ }
+
if (TLCGlobals.isCoverageEnabled()) {
CostModelCreator.create(this.tool);
}
@@ -126,13 +132,6 @@ public class Simulator {
private final RandomGenerator rng;
private final long seed;
private long aril;
- private IValue[] localValues = new IValue[4];
-
- // The set of all initial states for the given spec. This should be only be
- // computed once and re-used whenever a new random trace is generated. This
- // variable should not be written to concurrently, but is allowed to be read
- // concurrently.
- private StateVec initStates = new StateVec(0);
// Each simulation worker pushes their results onto this shared queue.
private BlockingQueue<SimulationWorkerResult> workerResultQueue = new LinkedBlockingQueue<>();
@@ -174,26 +173,32 @@ public class Simulator {
* @return an error code, or <code>EC.NO_ERROR</code> on success
*/
public int simulate() throws Exception {
+ final int res = this.tool.checkAssumptions();
+ if (res != EC.NO_ERROR) {
+ return res;
+ }
+
TLCState curState = null;
+ // The init states are calculated only ever once and never change
+ // in the loops below. Ideally the variable would be final.
+ StateVec initStates = this.tool.getInitStates();
+
//
// Compute the initial states.
//
try {
- // The init states are calculated only ever once and never change
- // in the loops below. Ideally the variable would be final.
- this.initStates = this.tool.getInitStates();
// This counter should always be initialized at zero.
assert (this.numOfGenStates.longValue() == 0);
- this.numOfGenStates.add(this.initStates.size());
+ this.numOfGenStates.add(initStates.size());
MP.printMessage(EC.TLC_COMPUTING_INIT_PROGRESS, this.numOfGenStates.toString());
// Check all initial states for validity.
- for (int i = 0; i < this.initStates.size(); i++) {
- curState = this.initStates.elementAt(i);
+ for (int i = 0; i < initStates.size(); i++) {
+ curState = initStates.elementAt(i);
if (this.tool.isGoodState(curState)) {
for (int j = 0; j < this.invariants.length; j++) {
if (!this.tool.isValid(this.invariants[j], curState)) {
@@ -225,7 +230,7 @@ public class Simulator {
// It appears deepNormalize brings the states into a canonical form to
// speed up equality checks.
- this.initStates.deepNormalize();
+ initStates.deepNormalize();
//
// Start progress report thread.
@@ -240,13 +245,9 @@ public class Simulator {
// Start up multiple simulation worker threads, each with their own unique seed.
final Set<Integer> runningWorkers = new HashSet<>();
- for (int i = 0; i < this.numWorkers; i++) {
- final SimulationWorker worker = new SimulationWorker(i, this.tool, initStates, this.workerResultQueue,
- this.rng.nextLong(), this.traceDepth, this.traceNum, this.checkDeadlock, this.traceFile,
- this.liveCheck, this.numOfGenStates, this.numOfGenTraces);
-
- worker.start();
- workers.add(worker);
+ for (int i = 0; i < this.workers.size(); i++) {
+ SimulationWorker worker = workers.get(i);
+ worker.start(initStates);
runningWorkers.add(i);
}
@@ -402,19 +403,16 @@ public class Simulator {
}
public IValue getLocalValue(int idx) {
- if (idx < this.localValues.length) {
- return this.localValues[idx];
+ for (SimulationWorker w : workers) {
+ return w.getLocalValue(idx);
}
return null;
}
- public void setLocalValue(int idx, IValue val) {
- if (idx >= this.localValues.length) {
- IValue[] vals = new IValue[idx + 1];
- System.arraycopy(this.localValues, 0, vals, 0, this.localValues.length);
- this.localValues = vals;
+ public void setAllValues(int idx, IValue val) {
+ for (SimulationWorker w : workers) {
+ w.setLocalValue(idx, val);
}
- this.localValues[idx] = val;
}
/**
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/StateVec.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/StateVec.java
index b35d9b534226806a9ffa5e452b143b2b15b544f6..de75c3773f5e2f353b8f0f19f272273a3f0fa99a 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/StateVec.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/StateVec.java
@@ -5,8 +5,12 @@
package tlc2.tool;
+import java.util.LinkedList;
+
import tlc2.TLCGlobals;
import tlc2.output.EC;
+import tlc2.value.impl.RecordValue;
+import tlc2.value.impl.Value;
import util.Assert;
/*
@@ -178,4 +182,25 @@ public final class StateVec implements IStateFunctor, INextStateFunctor {
}
return false;
}
+
+ public final Value[] toRecords(final TLCState append) {
+ final Value[] values = new Value[size + 1];
+ for (int i = 0; i < values.length; i++) {
+ values[i] = new RecordValue(v[i]);
+ }
+ values[values.length] = new RecordValue(append);
+ return values;
+ }
+
+ public final Value[] toRecords(final TLCState from, final TLCState append) {
+ final LinkedList<RecordValue> res = new LinkedList<>();
+ res.add(new RecordValue(append));
+ for (int i = size - 1; i >= 0; i--) {
+ res.push(new RecordValue(v[i]));
+ if (from.fingerPrint() == v[i].fingerPrint()) {
+ break;
+ }
+ }
+ return res.toArray(new Value[res.size()]);
+ }
}
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/TLCState.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/TLCState.java
index 24477f02a55ce43b92659829da819af2c93adfc6..1e66db7dc1d732be52c485b24cc392d4a98f4a4f 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/TLCState.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/TLCState.java
@@ -98,6 +98,9 @@ public abstract class TLCState implements Cloneable, Serializable {
}
public final void setPredecessor(final TLCState predecessor) {
+ // This method only keeps the level instead of the predecessor, because a) we
+ // don't need the predecessor and b) keeping predecessors would mean that we
+ // eventually have all states of the state graph in memory.
if (predecessor.getLevel() == Integer.MAX_VALUE) {
Assert.fail(EC.TLC_TRACE_TOO_LONG, this.toString());
}
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/TLCTrace.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/TLCTrace.java
index cb58807a3dcfd9bc1e4d9c35769cca695d9826be..4cd1d64e0cb4258a32beb48ff19bcbc15814c245 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/TLCTrace.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/TLCTrace.java
@@ -27,7 +27,7 @@ import util.FileUtil;
public class TLCTrace {
static final String EXT = ".st";
- private static String filename;
+ protected static String filename;
private final BufferedRandomAccessFile raf;
private long lastPtr;
private TraceApp tool;
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/Worker.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/Worker.java
index c06f9afa0756acd639a22f9c15cf3b8612ef72af..43d76b3320b5157f1d357d52f94591f583c00c31 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/Worker.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/Worker.java
@@ -98,7 +98,7 @@ public final class Worker extends IdThread implements IWorker, INextStateFunctor
final long preNext = this.statesGenerated;
try {
this.tool.getNextStates(this, curState);
- } catch (TLCRuntimeException e) {
+ } catch (TLCRuntimeException | EvalException e) {
// The next-state relation couldn't be evaluated.
this.tlc.doNextFailed(curState, null, e);
}
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/ModelConfig.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/ModelConfig.java
index 01e061447e9f0f514bc1422493867fa6fdc19e19..7f8af9803409c7a2b49c601dea874a17f53d41a6 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/ModelConfig.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/ModelConfig.java
@@ -44,7 +44,8 @@ import util.TLAConstants;
* @author Yuan Yu, Leslie Lamport
*/
public class ModelConfig implements ValueConstants, Serializable {
- // keywords of the configuration file
+ // keywords of the configuration file.
+ // CAREFUL: HAVE TO BE IN CONFIGTBL FOR PARSING TO WORK!
private static final String Constant = TLAConstants.KeyWords.CONSTANT;
private static final String Constants = TLAConstants.KeyWords.CONSTANTS;
private static final String Constraint = "CONSTRAINT";
@@ -125,7 +126,8 @@ public class ModelConfig implements ValueConstants, Serializable {
this.configTbl.put(Props, temp);
this.configTbl.put(Type, "");
this.configTbl.put(TypeConstraint, "");
-
+ this.configTbl.put(CheckDeadlock, "undef");
+
this.modConstants = new Hashtable<>();
this.modOverrides = new Hashtable<>();
this.overrides = new Hashtable<>();
@@ -429,7 +431,7 @@ public class ModelConfig implements ValueConstants, Serializable {
throw new ConfigFileException(EC.CFG_EXPECTED_SYMBOL, new String[] {
String.valueOf(scs.getBeginLine()), "TRUE or FALSE" });
}
- if (previous != null)
+ if (previous != "undef")
{
throw new ConfigFileException(EC.CFG_TWICE_KEYWORD, new String[] { String.valueOf(loc), CheckDeadlock });
}
@@ -601,8 +603,9 @@ public class ModelConfig implements ValueConstants, Serializable {
public synchronized final boolean getCheckDeadlock()
{
- if (this.configTbl.containsKey(CheckDeadlock)) {
- return (boolean) this.configTbl.get(CheckDeadlock);
+ Object object = this.configTbl.get(CheckDeadlock);
+ if (object instanceof Boolean) {
+ return (boolean) object;
}
return true;
}
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java
index 9f3cc4d6d9c71ac456387b483bb0e171c6ee60b6..d2c2030a45df281d9a03039afd5e4c2ccb7090b2 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java
@@ -30,6 +30,7 @@ import tla2sany.semantic.SymbolNode;
import tla2sany.semantic.ThmOrAssumpDefNode;
import tlc2.output.EC;
import tlc2.output.MP;
+import tlc2.output.OutputCollector;
import tlc2.tool.Action;
import tlc2.tool.BuiltInOPs;
import tlc2.tool.EvalControl;
@@ -3097,6 +3098,31 @@ public abstract class Tool
return ((BoolValue)val).val;
}
+ @Override
+ public final int checkAssumptions() {
+ final ExprNode[] assumps = getAssumptions();
+ final boolean[] isAxiom = getAssumptionIsAxiom();
+ int assumptionsError = EC.NO_ERROR;
+ for (int i = 0; i < assumps.length; i++)
+ {
+ try
+ {
+ if ((!isAxiom[i]) && !isValid(assumps[i]))
+ {
+ OutputCollector.addViolatedAssumption(assumps[i]);
+ assumptionsError = MP.printError(EC.TLC_ASSUMPTION_FALSE, assumps[i].toString());
+ }
+ } catch (final Exception e)
+ {
+ // Assert.printStack(e);
+ OutputCollector.addViolatedAssumption(assumps[i]);
+ assumptionsError = MP.printError(EC.TLC_ASSUMPTION_EVALUATION_ERROR,
+ new String[] { assumps[i].toString(), e.getMessage() });
+ }
+ }
+ return assumptionsError;
+ }
+
/* Reconstruct the initial state whose fingerprint is fp. */
@Override
public final TLCStateInfo getState(final long fp) {
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/liveness/LiveCheck1.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/liveness/LiveCheck1.java
index 27a711604be93a68279d2dc52967e6b31526a26e..c4f0811990a1368688b0c8db59f5044d7a3edcb6 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/liveness/LiveCheck1.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/liveness/LiveCheck1.java
@@ -7,7 +7,6 @@ package tlc2.tool.liveness;
import java.io.IOException;
-import tlc2.TLCGlobals;
import tlc2.output.EC;
import tlc2.output.MP;
import tlc2.output.StatePrinter;
@@ -654,13 +653,14 @@ public class LiveCheck1 implements ILiveCheck {
}
// Print the prefix:
- TLCState lastState = null;
+ TLCState cycleState = null;
for (int i = 0; i < stateNum; i++) {
- StatePrinter.printState(states[i], lastState, i + 1);
- lastState = states[i].state;
+ StatePrinter.printState(states[i], cycleState, i + 1);
+ cycleState = states[i].state;
}
// Print the cycle:
+ TLCState lastState = cycleState;
int cyclePos = stateNum;
long[] fps = new long[cycleStack.size()];
int idx = fps.length;
@@ -682,13 +682,12 @@ public class LiveCheck1 implements ILiveCheck {
if (node.stateFP == lastState.fingerPrint()) {
StatePrinter.printStutteringState(stateNum);
} else {
- if (TLCGlobals.tool) {
- // The parser in Tool mode is picky and does not detect the Back to State unless it's printed via MP.printState.
- // See LiveWorker#printTrace(..)
- MP.printState(EC.TLC_BACK_TO_STATE, new String[] { "" + cyclePos }, (TLCState) null, -1);
- } else {
- MP.printMessage(EC.TLC_BACK_TO_STATE, "" + cyclePos);
- }
+ sinfo = myTool.getState(cycleState.fingerPrint(), sinfo);
+ // The print stmts below claim there is a cycle, thus assert that
+ // there is indeed one. Index-based lookup into states array is
+ // reduced by one because cyclePos is human-readable.
+ assert cycleState.equals(sinfo.state);
+ StatePrinter.printBackToState(sinfo, cyclePos);
}
}
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/util/DotStateWriter.java b/tlatools/org.lamport.tlatools/src/tlc2/util/DotStateWriter.java
index 8cb2ca08a3ae87941d0285aa04292035b7736074..73d895881a2db4e6c19b06cc447a01f06aa1da18 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/util/DotStateWriter.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/util/DotStateWriter.java
@@ -295,7 +295,7 @@ public class DotStateWriter extends StateWriter {
sb.append(String.format("node [ labeljust=\"l\",colorscheme=\"%s\",style=filled,shape=record ]\n",
dotColorScheme));
for (String action : actions) {
- String str = String.format("%s [label=\"%s\",fillcolor=%d]", action, action,
+ String str = String.format("%s [label=\"%s\",fillcolor=%d]", action.replaceAll("!", ":"), action,
this.actionToColors.get(action));
sb.append(str);
sb.append("\n");
diff --git a/tlatools/org.lamport.tlatools/test-model/Github358.tla b/tlatools/org.lamport.tlatools/test-model/Github358.tla
new file mode 100644
index 0000000000000000000000000000000000000000..6ff29f99fc11a89475e8cc951347f1fd56c87c33
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/test-model/Github358.tla
@@ -0,0 +1,7 @@
+------------------------------ MODULE Github358 -----------------------------
+(*--algorithm Github358
+begin
+ A::
+ skip;
+end algorithm; *)
+=============================================================================
diff --git a/tlatools/org.lamport.tlatools/test-model/Github461.cfg b/tlatools/org.lamport.tlatools/test-model/Github461.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..e5a3896997d57e27da8ca619e152212920e137d1
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/test-model/Github461.cfg
@@ -0,0 +1,4 @@
+INIT
+Init
+NEXT
+Next
diff --git a/tlatools/org.lamport.tlatools/test-model/Github461.tla b/tlatools/org.lamport.tlatools/test-model/Github461.tla
new file mode 100644
index 0000000000000000000000000000000000000000..58beab5b7e764bbfe3bbae7bf902923eec77a7b8
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/test-model/Github461.tla
@@ -0,0 +1,12 @@
+----------------------------- MODULE Github461 -----------------------------
+EXTENDS Integers, TLC
+
+VARIABLES x
+
+Init == x = 0
+
+Next ==
+ /\ Assert(x < 4, "Failure of assertion at line 8, column 4.")
+ /\ x' = x + 1
+
+====
diff --git a/tlatools/org.lamport.tlatools/test-model/Test4.cfg b/tlatools/org.lamport.tlatools/test-model/Test4.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..81bbfad60f51f7a0061d092d12270f050a4ec618
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/test-model/Test4.cfg
@@ -0,0 +1 @@
+SPECIFICATION Spec
\ No newline at end of file
diff --git a/tlatools/org.lamport.tlatools/test-model/Test4.tla b/tlatools/org.lamport.tlatools/test-model/Test4.tla
new file mode 100644
index 0000000000000000000000000000000000000000..15affe77f9f9ac7f57fda1f6555a7aff3df30cec
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/test-model/Test4.tla
@@ -0,0 +1,8 @@
+---------- MODULE Test4 -----------
+VARIABLE x
+
+ASSUME TRUE = FALSE \* No, it's not!
+
+Spec == x = 0 /\ [][UNCHANGED x]_x
+
+==============================================
diff --git a/tlatools/org.lamport.tlatools/test-model/simulation/NQSpec/NQSpec.tla b/tlatools/org.lamport.tlatools/test-model/simulation/NQSpec/NQSpec.tla
index df9696352aff3633975edc6a91e70401dc27feca..7affcc75a616acf5e1f1fd441f5eb4fbafc2da0d 100644
--- a/tlatools/org.lamport.tlatools/test-model/simulation/NQSpec/NQSpec.tla
+++ b/tlatools/org.lamport.tlatools/test-model/simulation/NQSpec/NQSpec.tla
@@ -1,5 +1,5 @@
------------------------------- MODULE NQSpec -------------------------------
-EXTENDS Integers, Sequences
+EXTENDS Integers, Sequences, TLC
CONSTANTS EnQers, DeQers, Data, InitData, Ids, Busy, NoData
@@ -25,7 +25,9 @@ TypeOK == /\ enq \in [EnQers -> Data \cup {Done}]
/\ after \in [elts -> SUBSET doneElts]
/\ adding \in [EnQers -> Elements \cup {NotAnElement}]
-Init == /\ enq = [e \in EnQers |-> Done]
+Init ==
+ /\ TLCSet(42, 1)
+ /\ enq = [e \in EnQers |-> Done]
/\ deq = [d \in DeQers |-> InitData]
/\ after = << >>
/\ adding = [e \in EnQers |-> NotAnElement]
diff --git a/tlatools/org.lamport.tlatools/test-model/simulation/NQSpec/QSpec.tla b/tlatools/org.lamport.tlatools/test-model/simulation/NQSpec/QSpec.tla
index ad2b1b3b8f3e06053d29ae5eeb5624781c125e67..4d3a7962b5121e4e4d08f855a99c682921f1fad8 100644
--- a/tlatools/org.lamport.tlatools/test-model/simulation/NQSpec/QSpec.tla
+++ b/tlatools/org.lamport.tlatools/test-model/simulation/NQSpec/QSpec.tla
@@ -56,7 +56,9 @@ EndDeq(d) == /\ deq[d] = Busy
/\ deq' = [deq EXCEPT ![d] = deqInner[d]]
/\ UNCHANGED <<enq, queue, enqInner, deqInner>>
-Next == \/ \E e \in EnQers : BeginEnq(e) \/ DoEnq(e) \/ EndEnq(e)
+Next ==
+ /\ TLCSet(42, TLCGet(42))
+ /\ \/ \E e \in EnQers : BeginEnq(e) \/ DoEnq(e) \/ EndEnq(e)
\/ \E d \in DeQers : BeginDeq(d) \/ DoDeq(d) \/ EndDeq(d)
Spec == Init /\ [][Next]_vars
diff --git a/tlatools/org.lamport.tlatools/test/pcal/DivergenceTest.java b/tlatools/org.lamport.tlatools/test/pcal/DivergenceTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..a6db76aebaafc8ba75f24406a93fcb53dfb75a97
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/test/pcal/DivergenceTest.java
@@ -0,0 +1,315 @@
+/*******************************************************************************
+ * Copyright (c) 2020 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 pcal;
+
+import java.io.File;
+import java.io.IOException;
+
+import org.junit.Ignore;
+import org.junit.Test;
+
+import tla2sany.drivers.SANY;
+import util.TestPrintStream;
+import util.ToolIO;
+
+// Plz can haz https://openjdk.java.net/jeps/355 ?
+public class DivergenceTest extends PCalTest {
+ @Test
+ public void divergenceTest00() throws IOException {
+ final String filename = "divergenceTest001" + System.currentTimeMillis();
+ final String absolutePath = writeFile(System.getProperty("java.io.tmpdir") + File.separator + filename,
+ "---- MODULE " + filename + " ----\n" +
+ "\n" +
+ "(*\n" +
+ "--algorithm a\n" +
+ "begin\n" +
+ " skip;\n" +
+ "end algorithm; *)\n" +
+ "\\* BEGIN TRANSLATION\n" +
+ "VARIABLE pc\n" +
+ "\n" +
+ "vars == << pc >>\n" +
+ "\n" +
+ "Init == /\\ pc = \"Lbl_1\"\n" +
+ "\n" +
+ "Lbl_1 == /\\ pc = \"Lbl_1\"\n" +
+ " /\\ TRUE\n" +
+ " /\\ pc' = \"Done\"\n" +
+ "\n" +
+ "(* Allow infinite stuttering to prevent deadlock on termination. *)\n" +
+ "Terminating == pc = \"Done\" /\\ UNCHANGED vars\n" +
+ "\n" +
+ "Next == Lbl_1\n" +
+ " \\/ Terminating\n" +
+ "\n" +
+ "Spec == Init /\\ [][Next]_vars\n" +
+ "\n" +
+ "Termination == <>(pc = \"Done\")\n" +
+ "\n" +
+ "\\* END TRANSLATION\n" +
+ "\n=========================");
+ // Parse with SANY and check for errors (collects parse errors into ToolIO.out)
+ final TestPrintStream testPrintStream = new TestPrintStream();
+ ToolIO.out = testPrintStream;
+ SANY.SANYmain(new String[] { absolutePath });
+ testPrintStream.assertSubstring("Semantic processing of module " + filename);
+ testPrintStream.assertNoSubstring("!! WARNING " + filename);
+ }
+
+ @Test
+ public void divergenceTest01() throws IOException {
+ final String filename = "divergenceTest01" + System.currentTimeMillis();
+ final String absolutePath = writeFile(System.getProperty("java.io.tmpdir") + File.separator + filename,
+ "---- MODULE " + filename + " ----\n" +
+ "\n" +
+ "(*\n" +
+ "--algorithm a\n" +
+ "begin\n" +
+ " skip;\n" +
+ "end algorithm; *)\n" +
+ "\\* BEGIN TRANSLATION (chksum(PCal) \\in STRING /\\ chksum(TLA+) \\in STRING)\n" +
+ "VARIABLE pc\n" +
+ "\n" +
+ "vars == << pc >>\n" +
+ "\n" +
+ "Init == /\\ pc = \"Lbl_1\"\n" +
+ "\n" +
+ "Lbl_1 == /\\ pc = \"Lbl_1\"\n" +
+ " /\\ TRUE\n" +
+ " /\\ pc' = \"Done\"\n" +
+ "\n" +
+ "(* Allow infinite stuttering to prevent deadlock on termination. *)\n" +
+ "Terminating == pc = \"Done\" /\\ UNCHANGED vars\n" +
+ "\n" +
+ "Next == Lbl_1\n" +
+ " \\/ Terminating\n" +
+ "\n" +
+ "Spec == Init /\\ [][Next]_vars\n" +
+ "\n" +
+ "Termination == <>(pc = \"Done\")\n" +
+ "\n" +
+ "\\* END TRANSLATION\n" +
+ "\n=========================");
+ // Parse with SANY and check for errors (collects parse errors into ToolIO.out)
+ final TestPrintStream testPrintStream = new TestPrintStream();
+ ToolIO.out = testPrintStream;
+ SANY.SANYmain(new String[] { absolutePath });
+ testPrintStream.assertSubstring("Semantic processing of module " + filename);
+ testPrintStream.assertNoSubstring("!! WARNING " + filename);
+ }
+
+ @Test
+ public void divergenceTest02() throws IOException {
+ final String filename = "divergenceTest02" + System.currentTimeMillis();
+ final String absolutePath = writeFile(System.getProperty("java.io.tmpdir") + File.separator + filename,
+ "---- MODULE " + filename + " ----\n" +
+ "\n" +
+ "(*\n" +
+ "--algorithm a\n" +
+ "begin\n" +
+ " print \"msg\";\n" + // PlusCal diverged
+ "end algorithm; *)\n" +
+ "\\* BEGIN TRANSLATION (chksum(PCal) = \"4860ac97\" /\\ chksum(TLA+) = \"af3d9146\")\n" +
+ "VARIABLE pc\n" +
+ "\n" +
+ "vars == << pc >>\n" +
+ "\n" +
+ "Init == /\\ pc = \"Lbl_1\"\n" +
+ "\n" +
+ "Lbl_1 == /\\ pc = \"Lbl_1\"\n" +
+ " /\\ TRUE\n" +
+ " /\\ pc' = \"Done\"\n" +
+ "\n" +
+ "(* Allow infinite stuttering to prevent deadlock on termination. *)\n" +
+ "Terminating == pc = \"Done\" /\\ UNCHANGED vars\n" +
+ "\n" +
+ "Next == Lbl_1\n" +
+ " \\/ Terminating\n" +
+ "\n" +
+ "Spec == Init /\\ [][Next]_vars\n" +
+ "\n" +
+ "Termination == <>(pc = \"Done\")\n" +
+ "\n" +
+ "\\* END TRANSLATION\n" +
+ "\n=========================");
+ // Parse with SANY and check for errors (collects parse errors into ToolIO.out)
+ final TestPrintStream testPrintStream = new TestPrintStream();
+ ToolIO.out = testPrintStream;
+ SANY.SANYmain(new String[] { absolutePath });
+ testPrintStream.assertSubstring("Semantic processing of module " + filename);
+ testPrintStream.assertSubstring(String.format(
+ "!! WARNING: The PlusCal algorithm in module %s has changed since its last translation.",
+ filename));
+ }
+
+ @Test
+ public void divergenceTest03() throws IOException {
+ final String filename = "divergenceTest03" + System.currentTimeMillis();
+ final String absolutePath = writeFile(System.getProperty("java.io.tmpdir") + File.separator + filename,
+ "---- MODULE " + filename + " ----\n" +
+ "\n" +
+ "(*\n" +
+ "--algorithm a\n" +
+ "begin\n" +
+ " skip;\n" +
+ "end algorithm; *)\n" +
+ "\\* BEGIN TRANSLATION (checksum(PlusCal) = \"4860ac97\" /\\ ChkSum(tla+) = \"af3d9146\")\n" +
+ "VARIABLE pc\n" +
+ "\n" +
+ "vars == << pc >>\n" +
+ "\n" +
+ "Init == /\\ pc = \"Lbl_1\"\n" +
+ "\n" +
+ "Lbl_1 == /\\ pc = \"Lbl_1\"\n" +
+ " /\\ TRUE\n" +
+ " /\\ pc' = \"Done\"\n" +
+ "\n" +
+ "(* Allow infinite stuttering to prevent deadlock on termination. *)\n" +
+ "Terminating == pc = \"Done\" /\\ UNCHANGED vars\n" +
+ "\n" +
+ "Next == Lbl_1\n" + // TLA+ diverged.
+ "\n" +
+ "Spec == Init /\\ [][Next]_vars\n" +
+ "\n" +
+ "Termination == <>(pc = \"Done\")\n" +
+ "\n" +
+ "\\* END TRANSLATION\n" +
+ "\n=========================");
+ // Parse with SANY and check for errors (collects parse errors into ToolIO.out)
+ final TestPrintStream testPrintStream = new TestPrintStream();
+ ToolIO.out = testPrintStream;
+ SANY.SANYmain(new String[] { absolutePath });
+ testPrintStream.assertSubstring("Semantic processing of module " + filename);
+ testPrintStream.assertSubstring(String.format(
+ "!! WARNING: The TLA+ translation in module %s has changed since its last translation.",
+ filename));
+ }
+
+ @Test
+ public void divergenceTest04() throws IOException {
+ final String filename = "divergenceTest04" + System.currentTimeMillis();
+ final String absolutePath = writeFile(System.getProperty("java.io.tmpdir") + File.separator + filename,
+ "---- MODULE " + filename + " ----\n" +
+ "\n" +
+ "(*\n" +
+ "--algorithm a\n" +
+ "begin\n" +
+ " print \"msg\";\n" + // PlusCal diverged
+ "end algorithm; *)\n" +
+ "\\* BEGIN TRANSLATION (checksum(PlusCal) = \"4860ac97\" /\\ ChkSum(tla+) = \"af3d9146\") \n" +
+ "VARIABLE pc\n" +
+ "\n" +
+ "vars == << pc >>\n" +
+ "\n" +
+ "Init == /\\ pc = \"Lbl_1\"\n" +
+ "\n" +
+ "Lbl_1 == /\\ pc = \"Lbl_1\"\n" +
+ " /\\ TRUE\n" +
+ " /\\ pc' = \"Done\"\n" +
+ "\n" +
+ "(* Allow infinite stuttering to prevent deadlock on termination. *)\n" +
+ "Terminating == pc = \"Done\" /\\ UNCHANGED vars\n" +
+ "\n" +
+ "Next == Lbl_1\n" + // TLA+ diverged.
+ "\n" +
+ "Spec == Init /\\ [][Next]_vars\n" +
+ "\n" +
+ "Termination == <>(pc = \"Done\")\n" +
+ "\n" +
+ "\\* END TRANSLATION\n" +
+ "\n=========================");
+ // Parse with SANY and check for errors (collects parse errors into ToolIO.out)
+ final TestPrintStream testPrintStream = new TestPrintStream();
+ ToolIO.out = testPrintStream;
+ SANY.SANYmain(new String[] { absolutePath });
+ testPrintStream.assertSubstring("Semantic processing of module " + filename);
+ testPrintStream.assertSubstring(String.format(
+ "!! WARNING: The PlusCal algorithm and its TLA+ translation in module %s filename since the last translation.",
+ filename));
+ }
+ @Test
+ public void divergenceTest05() throws IOException {
+ final String filename = "divergenceTest04" + System.currentTimeMillis();
+ final String absolutePath = writeFile(System.getProperty("java.io.tmpdir") + File.separator + filename,
+ "---- MODULE " + filename + " ----\n" +
+ "\n" +
+ "(*\n" +
+ "--algorithm a\n" +
+ "begin\n" +
+ " print \"msg\";\n" + // PlusCal diverged
+ "end algorithm; *)\n" +
+ "\\* BEGIN TRANSLATION (checksum(PlusCal) \\in STRING /\\ ChkSum(tla+) \\in STRING) \n" +
+ "VARIABLE pc\n" +
+ "\n" +
+ "vars == << pc >>\n" +
+ "\n" +
+ "Init == /\\ pc = \"Lbl_1\"\n" +
+ "\n" +
+ "Lbl_1 == /\\ pc = \"Lbl_1\"\n" +
+ " /\\ TRUE\n" +
+ " /\\ pc' = \"Done\"\n" +
+ "\n" +
+ "(* Allow infinite stuttering to prevent deadlock on termination. *)\n" +
+ "Terminating == pc = \"Done\" /\\ UNCHANGED vars\n" +
+ "\n" +
+ "Next == Lbl_1\n" + // TLA+ diverged.
+ "\n" +
+ "Spec == Init /\\ [][Next]_vars\n" +
+ "\n" +
+ "Termination == <>(pc = \"Done\")\n" +
+ "\n" +
+ "\\* END TRANSLATION\n" +
+ "\n=========================");
+ // Parse with SANY and check for errors (collects parse errors into ToolIO.out)
+ final TestPrintStream testPrintStream = new TestPrintStream();
+ ToolIO.out = testPrintStream;
+ SANY.SANYmain(new String[] { absolutePath });
+ testPrintStream.assertSubstring("Semantic processing of module " + filename);
+ testPrintStream.assertNoSubstring(String.format(
+ "!! WARNING:",
+ filename));
+ }
+
+ @Test
+ public void divergenceTest06() throws IOException {
+ final String filename = "divergenceTest05" + System.currentTimeMillis();
+ final String absolutePath = writeFile(System.getProperty("java.io.tmpdir") + File.separator + filename,
+ "---- MODULE " + filename + " ----\n" +
+ "\n" +
+ "(*\n" +
+ "--algorithm a\n" +
+ "begin\n" +
+ " skip;\n" +
+ "end algorithm; *)\n" +
+ "\n=========================");
+ // Parse with SANY and check for errors (collects parse errors into ToolIO.out)
+ final TestPrintStream testPrintStream = new TestPrintStream();
+ ToolIO.out = testPrintStream;
+ SANY.SANYmain(new String[] { absolutePath });
+ testPrintStream.assertSubstring("Semantic processing of module " + filename);
+ testPrintStream.assertNoSubstring("!! WARNING " + filename);
+ }
+}
diff --git a/tlatools/org.lamport.tlatools/test/pcal/Github358.java b/tlatools/org.lamport.tlatools/test/pcal/Github358.java
new file mode 100644
index 0000000000000000000000000000000000000000..c7851681e2c19132e359b4d1a64518eacdd5d602
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/test/pcal/Github358.java
@@ -0,0 +1,51 @@
+/*******************************************************************************
+ * Copyright (c) 2020 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 pcal;
+
+import static org.junit.Assert.assertEquals;
+import static org.junit.Assert.assertTrue;
+
+import org.junit.Test;
+
+import tlc2.tool.CommonTestCase;
+import util.ToolIO;
+
+public class Github358 extends PCalTest {
+
+ @Test
+ public void test() {
+ assertEquals(trans.STATUS_EXIT_WITH_ERRORS,
+ trans.runMe(new String[] {"-nocfg", CommonTestCase.BASE_PATH + "Github358.tla"}));
+
+ final String[] messages = ToolIO.getAllMessages();
+ assertTrue(messages.length == 1);
+
+ final String msg = messages[0];
+ assertEquals("Unrecoverable error:\n" +
+ " -- Expected \":=\" but found \"skip\"\n" +
+ " line 5, column 7.", msg.trim());
+ }
+}
diff --git a/tlatools/org.lamport.tlatools/test/pcal/ValidatorPerformance.java b/tlatools/org.lamport.tlatools/test/pcal/ValidatorPerformance.java
deleted file mode 100644
index a84a6900004255dadcc1d9b9ed5f129a85fe32ee..0000000000000000000000000000000000000000
--- a/tlatools/org.lamport.tlatools/test/pcal/ValidatorPerformance.java
+++ /dev/null
@@ -1,39 +0,0 @@
-package pcal;
-
-import java.io.FileInputStream;
-import java.io.IOException;
-
-import org.junit.Assert;
-import org.junit.Test;
-
-import tlc2.tool.CommonTestCase;
-
-public class ValidatorPerformance {
- private static final String SPEC_FILE = CommonTestCase.BASE_PATH + "PlusCalOptions.tla";
-
- @Test
- public void testTimings() throws IOException {
- final long trimmedStart = System.currentTimeMillis();
- for (int i = 0; i < 1000; i++) {
- try (final FileInputStream fis = new FileInputStream(SPEC_FILE)) {
- Validator.validate(fis);
- }
- }
- final long trimmedEnd = System.currentTimeMillis();
-
- Validator.PRE_TRIM_VALIDATION_CONTENT = false;
- final long untrimmedStart = System.currentTimeMillis();
- for (int i = 0; i < 1000; i++) {
- try (final FileInputStream fis = new FileInputStream(SPEC_FILE)) {
- Validator.validate(fis);
- }
- }
- final long untrimmedEnd = System.currentTimeMillis();
-
- final long trimmedDelta = trimmedEnd - trimmedStart;
- final long untrimmedDelta = untrimmedEnd - untrimmedStart;
- System.out.println("Trimmed run time was " + trimmedDelta + " and untrimmed was " + untrimmedDelta);
- Assert.assertTrue("Untrimmed processing time (" + untrimmedDelta +") ran faster than trimmed (" + trimmedDelta + ").",
- (trimmedDelta < untrimmedDelta));
- }
-}
diff --git a/tlatools/org.lamport.tlatools/test/tlc2/output/SpecTraceExpressionWriterTest.java b/tlatools/org.lamport.tlatools/test/tlc2/output/SpecTraceExpressionWriterTest.java
index f15520973b0e22532159a057d80540e864370321..1f2fb1ddb96c6de2f82b6e0a8c5b0ae79d0a3949 100644
--- a/tlatools/org.lamport.tlatools/test/tlc2/output/SpecTraceExpressionWriterTest.java
+++ b/tlatools/org.lamport.tlatools/test/tlc2/output/SpecTraceExpressionWriterTest.java
@@ -1,5 +1,7 @@
package tlc2.output;
+import static org.junit.Assert.assertTrue;
+
import java.io.File;
import java.io.IOException;
import java.util.ArrayList;
@@ -128,4 +130,31 @@ public class SpecTraceExpressionWriterTest {
concludeTest();
}
+
+
+ @Test
+ public void testMultilineTraceExpression() throws Exception {
+ final List<MCState> trace = generateStatesForDeadlockCondition();
+ writer.addTraceFunction(trace);
+
+ final List<Formula> expressions = new ArrayList<>();
+ expressions.add(new Formula("\n"
+ + "/\\ y # 7\n"
+ + "/\\ \\/ TRUE\n"
+ + " \\* Comment"
+ + " \\/ FALSE"));
+ // Named expression
+ final Formula e = new Formula("namedExpression == \n"
+ + " (* A commend \n over two lines*)"
+ + " /\\ \\/ TRUE\n"
+ + " \\* Comment"
+ + " \\/ FALSE");
+ assertTrue(e.isNamed());
+ expressions.add(e);
+ final TraceExpressionInformationHolder[] traceExpressions
+ = writer.createAndAddVariablesAndDefinitions(expressions, "writerTestTraceExpressions");
+ writer.addInitNext(trace, traceExpressions, "STEWInit", "STEWNext", "STEWAC", TRIVIAL_TWO_STATE_DEADLOCK_NEXT[0]);
+
+ concludeTest();
+ }
}
diff --git a/tlatools/org.lamport.tlatools/test/tlc2/tool/Github461Test.java b/tlatools/org.lamport.tlatools/test/tlc2/tool/Github461Test.java
new file mode 100644
index 0000000000000000000000000000000000000000..1e05070fb0c52ddc02cc9418d49339f7baffd695
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/test/tlc2/tool/Github461Test.java
@@ -0,0 +1,72 @@
+/*******************************************************************************
+ * Copyright (c) 2020 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 java.io.FileNotFoundException;
+import java.io.IOException;
+import java.util.ArrayList;
+import java.util.List;
+
+import org.junit.Test;
+
+import tlc2.output.EC;
+import tlc2.tool.liveness.ModelCheckerTestCase;
+
+public class Github461Test extends ModelCheckerTestCase {
+
+ public Github461Test() {
+ super("Github461", EC.ExitStatus.VIOLATION_ASSERT);
+ }
+
+ @Test
+ public void testSpec() throws FileNotFoundException, IOException {
+ // Assert evaluation error.
+ assertTrue(recorder.recordedWithStringValue(EC.TLC_VALUE_ASSERT_FAILED,
+ "\"Failure of assertion at line 8, column 4.\""));
+
+ // Assert an error trace.
+ assertTrue(recorder.recorded(EC.TLC_STATE_PRINT2));
+
+ // Assert the correct trace.
+ final List<String> expectedTrace = new ArrayList<String>(4);
+ expectedTrace.add("x = 0");
+ expectedTrace.add("x = 1");
+ expectedTrace.add("x = 2");
+ expectedTrace.add("x = 3");
+ expectedTrace.add("x = 4");
+ assertTraceWith(recorder.getRecords(EC.TLC_STATE_PRINT2), expectedTrace);
+
+ // Assert the underlying error message with stack trace.
+ assertTrue(recorder.recordedWithStringValues(EC.TLC_NESTED_EXPRESSION,
+ "0. Line 9, column 5 to line 10, column 17 in Github461\n" +
+ "1. Line 9, column 8 to line 9, column 65 in Github461\n" +
+ "\n"));
+
+ assertZeroUncovered();
+ }
+}
diff --git a/tlatools/org.lamport.tlatools/test/tlc2/tool/liveness/simulation/SimulationTestAssumption.java b/tlatools/org.lamport.tlatools/test/tlc2/tool/liveness/simulation/SimulationTestAssumption.java
new file mode 100644
index 0000000000000000000000000000000000000000..5f2729afb2ce1be36dc18a3d71f4a5e392c38c45
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/test/tlc2/tool/liveness/simulation/SimulationTestAssumption.java
@@ -0,0 +1,46 @@
+/*******************************************************************************
+ * Copyright (c) 2020 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.liveness.simulation;
+
+import static org.junit.Assert.assertTrue;
+
+import org.junit.Test;
+
+import tlc2.output.EC;
+
+public class SimulationTestAssumption extends SuccessfulSimulationTestCase {
+
+ public SimulationTestAssumption() {
+ super("Test4", "/", new String[] { "-simulate", "num=1" }, EC.ExitStatus.VIOLATION_ASSUMPTION);
+ }
+
+ @Test
+ public void testSpec() {
+ assertTrue(recorder.recorded(EC.TLC_ASSUMPTION_FALSE));
+ assertTrue(recorder.recorded(EC.TLC_FINISHED));
+ }
+}
diff --git a/tlatools/org.lamport.tlatools/test/tlc2/tool/liveness/simulation/SuccessfulSimulationTestCase.java b/tlatools/org.lamport.tlatools/test/tlc2/tool/liveness/simulation/SuccessfulSimulationTestCase.java
index 2eb3c22857017d75737719f160977454a0bfde3b..ba1f69f9f0baf3785a86d9186d014f8fb1e9b352 100644
--- a/tlatools/org.lamport.tlatools/test/tlc2/tool/liveness/simulation/SuccessfulSimulationTestCase.java
+++ b/tlatools/org.lamport.tlatools/test/tlc2/tool/liveness/simulation/SuccessfulSimulationTestCase.java
@@ -48,6 +48,10 @@ public abstract class SuccessfulSimulationTestCase extends ModelCheckerTestCase
super(spec, path, extraArguments);
}
+ public SuccessfulSimulationTestCase(String spec, String path, String[] extraArguments, int exitStatus) {
+ super(spec, path, extraArguments, exitStatus);
+ }
+
@Test
public void testSpec() {
// Simulation must *NOT* show a counterexample. Regular model-checking
diff --git a/tlatools/org.lamport.tlatools/test/tlc2/tool/simulation/SimulationWorkerTest.java b/tlatools/org.lamport.tlatools/test/tlc2/tool/simulation/SimulationWorkerTest.java
index f44cd05fd2a33c1accceed3fde0ea344d61a6226..96afcecf19f228ad4f8d340deb3f506e6464fac8 100644
--- a/tlatools/org.lamport.tlatools/test/tlc2/tool/simulation/SimulationWorkerTest.java
+++ b/tlatools/org.lamport.tlatools/test/tlc2/tool/simulation/SimulationWorkerTest.java
@@ -67,9 +67,9 @@ public class SimulationWorkerTest extends CommonTestCase {
ILiveCheck liveCheck = new NoOpLiveCheck(tool, "BasicMultiTrace");
StateVec initStates = tool.getInitStates();
BlockingQueue<SimulationWorkerResult> resultQueue = new LinkedBlockingQueue<>();
- SimulationWorker worker = new SimulationWorker(0, tool, initStates, resultQueue, 0, 100, 1000, false, null,
+ SimulationWorker worker = new SimulationWorker(0, tool, resultQueue, 0, 100, 1000, false, null,
liveCheck, new LongAdder(), new LongAdder());
- worker.start();
+ worker.start(initStates);
SimulationWorkerResult res = resultQueue.take();
assertFalse(res.isError());
worker.join();
@@ -84,9 +84,9 @@ public class SimulationWorkerTest extends CommonTestCase {
StateVec initStates = tool.getInitStates();
BlockingQueue<SimulationWorkerResult> resultQueue = new LinkedBlockingQueue<>();
int maxTraceNum = 3;
- SimulationWorker worker = new SimulationWorker(0, tool, initStates, resultQueue, 0, 100, maxTraceNum, false,
+ SimulationWorker worker = new SimulationWorker(0, tool, resultQueue, 0, 100, maxTraceNum, false,
null, liveCheck, new LongAdder(), new LongAdder());
- worker.start();
+ worker.start(initStates);
SimulationWorkerResult res = resultQueue.take();
assertTrue(res.isError());
@@ -158,9 +158,9 @@ public class SimulationWorkerTest extends CommonTestCase {
StateVec initStates = tool.getInitStates();
ILiveCheck liveCheck = new NoOpLiveCheck(tool, "BasicMultiTrace");
BlockingQueue<SimulationWorkerResult> resultQueue = new LinkedBlockingQueue<>();
- SimulationWorker worker = new SimulationWorker(0, tool, initStates, resultQueue, 0, 100, 100, false, null,
+ SimulationWorker worker = new SimulationWorker(0, tool, resultQueue, 0, 100, 100, false, null,
liveCheck, new LongAdder(), new LongAdder());
- worker.start();
+ worker.start(initStates);
SimulationWorkerResult res = resultQueue.take();
assertTrue(res.isError());
@@ -206,9 +206,9 @@ public class SimulationWorkerTest extends CommonTestCase {
StateVec initStates = tool.getInitStates();
ILiveCheck liveCheck = new NoOpLiveCheck(tool, "BasicMultiTrace");
BlockingQueue<SimulationWorkerResult> resultQueue = new LinkedBlockingQueue<>();
- SimulationWorker worker = new SimulationWorker(0, tool, initStates, resultQueue, 0, 100, 100, false, null,
+ SimulationWorker worker = new SimulationWorker(0, tool, resultQueue, 0, 100, 100, false, null,
liveCheck, new LongAdder(), new LongAdder());
- worker.start();
+ worker.start(initStates);
SimulationWorkerResult res = resultQueue.take();
assertTrue(res.isError());
@@ -234,9 +234,9 @@ public class SimulationWorkerTest extends CommonTestCase {
StateVec initStates = tool.getInitStates();
ILiveCheck liveCheck = new NoOpLiveCheck(tool, "BasicMultiTrace");
BlockingQueue<SimulationWorkerResult> resultQueue = new LinkedBlockingQueue<>();
- SimulationWorker worker = new SimulationWorker(0, tool, initStates, resultQueue, 0, 100, 100, false, null,
+ SimulationWorker worker = new SimulationWorker(0, tool, resultQueue, 0, 100, 100, false, null,
liveCheck, new LongAdder(), new LongAdder());
- worker.start();
+ worker.start(initStates);
SimulationWorkerResult res = resultQueue.take();
@@ -255,9 +255,9 @@ public class SimulationWorkerTest extends CommonTestCase {
StateVec initStates = tool.getInitStates();
ILiveCheck liveCheck = new NoOpLiveCheck(tool, "BasicMultiTrace");
BlockingQueue<SimulationWorkerResult> resultQueue = new LinkedBlockingQueue<>();
- SimulationWorker worker = new SimulationWorker(0, tool, initStates, resultQueue, 0, 100, 100, false, null,
+ SimulationWorker worker = new SimulationWorker(0, tool, resultQueue, 0, 100, 100, false, null,
liveCheck, new LongAdder(), new LongAdder());
- worker.start();
+ worker.start(initStates);
SimulationWorkerResult res = resultQueue.take();
assertTrue(res.isError());
@@ -283,9 +283,9 @@ public class SimulationWorkerTest extends CommonTestCase {
StateVec initStates = tool.getInitStates();
ILiveCheck liveCheck = new NoOpLiveCheck(tool, "BasicMultiTrace");
BlockingQueue<SimulationWorkerResult> resultQueue = new LinkedBlockingQueue<>();
- SimulationWorker worker = new SimulationWorker(0, tool, initStates, resultQueue, 0, 100, 100, true, null,
+ SimulationWorker worker = new SimulationWorker(0, tool, resultQueue, 0, 100, 100, true, null,
liveCheck, new LongAdder(), new LongAdder());
- worker.start();
+ worker.start(initStates);
SimulationWorkerResult res = resultQueue.take();
assertTrue(res.isError());
@@ -328,9 +328,9 @@ public class SimulationWorkerTest extends CommonTestCase {
StateVec initStates = tool.getInitStates();
ILiveCheck liveCheck = new NoOpLiveCheck(tool, "BasicMultiTrace");
BlockingQueue<SimulationWorkerResult> resultQueue = new LinkedBlockingQueue<>();
- SimulationWorker worker = new SimulationWorker(0, tool, initStates, resultQueue, 0, 100, 100, false, null,
+ SimulationWorker worker = new SimulationWorker(0, tool, resultQueue, 0, 100, 100, false, null,
liveCheck, new LongAdder(), new LongAdder());
- worker.start();
+ worker.start(initStates);
SimulationWorkerResult res = resultQueue.take();
assertFalse(res.isError());
worker.join();
@@ -345,9 +345,9 @@ public class SimulationWorkerTest extends CommonTestCase {
StateVec initStates = tool.getInitStates();
ILiveCheck liveCheck = new NoOpLiveCheck(tool, "BasicMultiTrace");
BlockingQueue<SimulationWorkerResult> resultQueue = new LinkedBlockingQueue<>();
- SimulationWorker worker = new SimulationWorker(0, tool, initStates, resultQueue, 0, 100, 100, false, null,
+ SimulationWorker worker = new SimulationWorker(0, tool, resultQueue, 0, 100, 100, false, null,
liveCheck, new LongAdder(), new LongAdder());
- worker.start();
+ worker.start(initStates);
SimulationWorkerResult res = resultQueue.take();
assertFalse(res.isError());
worker.join();
@@ -366,9 +366,9 @@ public class SimulationWorkerTest extends CommonTestCase {
// If we set the trace limit to the max, the worker should effectively run forever. We verify that after it generates
// a result, we can cancel it and the worker will terminate.
long traceNum = Long.MAX_VALUE;
- SimulationWorker worker = new SimulationWorker(0, tool, initStates, resultQueue, 0, 100, traceNum, false, null,
+ SimulationWorker worker = new SimulationWorker(0, tool, resultQueue, 0, 100, traceNum, false, null,
liveCheck, new LongAdder(), new LongAdder());
- worker.start();
+ worker.start(initStates);
// Check one result.
SimulationWorkerResult res = resultQueue.take();
@@ -394,9 +394,9 @@ public class SimulationWorkerTest extends CommonTestCase {
// At this trace depth, the worker should never find the invariant violation.
long traceDepth = 1;
- SimulationWorker worker = new SimulationWorker(0, tool, initStates, resultQueue, 0, traceDepth, 100, false,
+ SimulationWorker worker = new SimulationWorker(0, tool, resultQueue, 0, traceDepth, 100, false,
null, liveCheck, new LongAdder(), new LongAdder());
- worker.start();
+ worker.start(initStates);
SimulationWorkerResult res = resultQueue.take();
assertFalse(res.isError());
@@ -418,10 +418,10 @@ public class SimulationWorkerTest extends CommonTestCase {
LongAdder numOfGenTraces = new LongAdder();
long traceDepth = 5;
long traceNum = 5;
- SimulationWorker worker = new SimulationWorker(0, tool, initStates, resultQueue, 0, traceDepth, traceNum, false,
+ SimulationWorker worker = new SimulationWorker(0, tool, resultQueue, 0, traceDepth, traceNum, false,
null, liveCheck, numOfGenStates, numOfGenTraces);
- worker.start();
+ worker.start(initStates);
worker.join();
assertFalse(worker.isAlive());
assertEquals(70, numOfGenStates.longValue());
diff --git a/tlatools/org.lamport.tlatools/test/util/TestPrintStream.java b/tlatools/org.lamport.tlatools/test/util/TestPrintStream.java
index df6400f37613cff591c72c802319082bd94e3ece..ad12a39b826eba7f167eed3e091692ab88490f98 100644
--- a/tlatools/org.lamport.tlatools/test/util/TestPrintStream.java
+++ b/tlatools/org.lamport.tlatools/test/util/TestPrintStream.java
@@ -68,4 +68,12 @@ public class TestPrintStream extends PrintStream {
}
fail("Substring not found");
}
+
+ public void assertNoSubstring(String substring) {
+ for (String string : strings) {
+ if (string.contains(substring)) {
+ fail("Substring not found");
+ }
+ }
+ }
}
\ No newline at end of file
diff --git a/toolbox/org.lamport.tla.toolbox.doc/META-INF/MANIFEST.MF b/toolbox/org.lamport.tla.toolbox.doc/META-INF/MANIFEST.MF
index b1ec28784e3d81e88b379a5913100f370f3183dd..7e88dd103450fe2661c5f593be32ecbd0e79a4ff 100644
--- a/toolbox/org.lamport.tla.toolbox.doc/META-INF/MANIFEST.MF
+++ b/toolbox/org.lamport.tla.toolbox.doc/META-INF/MANIFEST.MF
@@ -2,7 +2,7 @@ Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: TLA+ Toolbox Help
Bundle-SymbolicName: org.lamport.tla.toolbox.doc; singleton:=true
-Bundle-Version: 1.7.0.qualifier
+Bundle-Version: 1.7.1.qualifier
Bundle-RequiredExecutionEnvironment: J2SE-1.4
Bundle-Vendor: Simon Zambrovski, Leslie Lamport
Bundle-ActivationPolicy: lazy
diff --git a/toolbox/org.lamport.tla.toolbox.doc/pom.xml b/toolbox/org.lamport.tla.toolbox.doc/pom.xml
index dbc49b5232a9ff942d82baeecbabdb45239a135b..a559fc916941797f802a4ebdfaf2882a1b99465f 100644
--- a/toolbox/org.lamport.tla.toolbox.doc/pom.xml
+++ b/toolbox/org.lamport.tla.toolbox.doc/pom.xml
@@ -11,7 +11,7 @@
</parent>
<groupId>tlatoolbox</groupId>
<artifactId>org.lamport.tla.toolbox.doc</artifactId>
- <version>1.7.0-SNAPSHOT</version>
+ <version>1.7.1-SNAPSHOT</version>
<packaging>eclipse-plugin</packaging>
<properties>
<!-- Do not include non-code project in Sonar reporting. -->
diff --git a/toolbox/org.lamport.tla.toolbox.editor.basic/src/org/eclipse/jface/dialogs/ForkedProgressMonitorDialog.java b/toolbox/org.lamport.tla.toolbox.editor.basic/src/org/eclipse/jface/dialogs/ForkedProgressMonitorDialog.java
new file mode 100644
index 0000000000000000000000000000000000000000..c3745378d338328a526284b42c14a2b87125d7c6
--- /dev/null
+++ b/toolbox/org.lamport.tla.toolbox.editor.basic/src/org/eclipse/jface/dialogs/ForkedProgressMonitorDialog.java
@@ -0,0 +1,642 @@
+/*******************************************************************************
+ * Copyright (c) 2000, 2018 IBM Corporation and others.
+ *
+ * This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License 2.0
+ * which accompanies this distribution, and is available at
+ * https://www.eclipse.org/legal/epl-2.0/
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ *
+ * Contributors:
+ * IBM Corporation - initial API and implementation
+ *******************************************************************************/
+package org.eclipse.jface.dialogs;
+
+import java.lang.reflect.InvocationTargetException;
+
+import org.eclipse.core.runtime.IProgressMonitor;
+import org.eclipse.core.runtime.IProgressMonitorWithBlocking;
+import org.eclipse.core.runtime.IStatus;
+import org.eclipse.jface.operation.IRunnableContext;
+import org.eclipse.jface.operation.IRunnableWithProgress;
+import org.eclipse.jface.operation.ModalContext;
+import org.eclipse.jface.resource.JFaceResources;
+import org.eclipse.swt.SWT;
+import org.eclipse.swt.graphics.Cursor;
+import org.eclipse.swt.graphics.Image;
+import org.eclipse.swt.graphics.Point;
+import org.eclipse.swt.layout.GridData;
+import org.eclipse.swt.widgets.Button;
+import org.eclipse.swt.widgets.Composite;
+import org.eclipse.swt.widgets.Control;
+import org.eclipse.swt.widgets.Label;
+import org.eclipse.swt.widgets.Shell;
+
+/**
+ * A modal dialog that displays progress during a long running operation.
+ * <p>
+ * This concrete dialog class can be instantiated as is, or further subclassed
+ * as required.
+ * </p>
+ * <p>
+ * Typical usage is:
+ * </p>
+ * <pre>
+ * try {
+ * IRunnableWithProgress op = ...;
+ * new ProgressMonitorDialog(activeShell).run(true, true, op);
+ * } catch (InvocationTargetException e) {
+ * // handle exception
+ * } catch (InterruptedException e) {
+ * // handle cancelation
+ * }
+ * </pre>
+ *
+ * <p>
+ * Note that the ProgressMonitorDialog is not intended to be used with multiple
+ * runnables - this dialog should be discarded after completion of one
+ * IRunnableWithProgress and a new one instantiated for use by a second or
+ * sebsequent IRunnableWithProgress to ensure proper initialization.
+ * </p>
+ * <p>
+ * Note that not forking the process will result in it running in the UI which
+ * may starve the UI. The most obvious symptom of this problem is non
+ * responsiveness of the cancel button. If you are running within the UI Thread
+ * you should do the bulk of your work in another Thread to prevent starvation.
+ * It is recommended that fork is set to true in most cases.
+ * </p>
+ */
+public class ForkedProgressMonitorDialog extends IconAndMessageDialog implements
+ IRunnableContext {
+ /**
+ * Name to use for task when normal task name is empty string.
+ */
+ private static String DEFAULT_TASKNAME = JFaceResources
+ .getString("ProgressMonitorDialog.message"); //$NON-NLS-1$
+
+ /**
+ * Constants for label and monitor size
+ */
+ private static int LABEL_DLUS = 40;
+
+ private static int BAR_DLUS = 9;
+
+ /**
+ * The progress indicator control.
+ */
+ protected ProgressIndicator progressIndicator;
+
+ /**
+ * The label control for the task. Kept for backwards compatibility.
+ */
+ protected Label taskLabel;
+
+ /**
+ * The label control for the subtask.
+ */
+ protected Label subTaskLabel;
+
+ /**
+ * The Cancel button control.
+ */
+ protected Button cancel;
+
+ /**
+ * Indicates whether the Cancel button is to be shown.
+ */
+ protected boolean operationCancelableState = false;
+
+ /**
+ * Indicates whether the Cancel button is to be enabled.
+ */
+ protected boolean enableCancelButton;
+
+ /**
+ * The progress monitor.
+ */
+ private ProgressMonitor progressMonitor = new ProgressMonitor();
+
+ /**
+ * The name of the current task (used by ProgressMonitor).
+ */
+ private String task;
+
+ /**
+ * The nesting depth of currently running runnables.
+ */
+ private int nestingDepth;
+
+ /**
+ * The cursor used in the cancel button;
+ */
+ protected Cursor arrowCursor;
+
+ /**
+ * Flag indicating whether to open or merely create the dialog before run.
+ */
+ private boolean openOnRun = true;
+
+ /**
+ * Internal progress monitor implementation.
+ */
+ private class ProgressMonitor implements IProgressMonitorWithBlocking {
+ private String fSubTask = "";//$NON-NLS-1$
+
+ private volatile boolean fIsCanceled;
+
+ /**
+ * is the process forked
+ */
+ protected boolean forked = false;
+
+ /**
+ * is locked
+ */
+ protected boolean locked = false;
+
+ @Override
+ public void beginTask(String name, int totalWork) {
+ if (progressIndicator.isDisposed()) {
+ return;
+ }
+ if (name == null) {
+ task = "";//$NON-NLS-1$
+ } else {
+ task = name;
+ }
+ String s = task;
+ if (s.length() <= 0) {
+ s = DEFAULT_TASKNAME;
+ }
+ setMessage(s, false);
+ if (!forked) {
+ update();
+ }
+ if (totalWork == UNKNOWN) {
+ progressIndicator.beginAnimatedTask();
+ } else {
+ progressIndicator.beginTask(totalWork);
+ }
+ }
+
+ @Override
+ public void done() {
+ if (!progressIndicator.isDisposed()) {
+ progressIndicator.sendRemainingWork();
+ progressIndicator.done();
+ }
+ }
+
+ @Override
+ public void setTaskName(String name) {
+ if (name == null) {
+ task = "";//$NON-NLS-1$
+ } else {
+ task = name;
+ }
+ String s = task;
+ if (s.length() <= 0) {
+ s = DEFAULT_TASKNAME;
+ }
+ setMessage(s, false);
+ if (!forked) {
+ update();
+ }
+ }
+
+ @Override
+ public boolean isCanceled() {
+ return fIsCanceled;
+ }
+
+ @Override
+ public void setCanceled(boolean b) {
+ fIsCanceled = b;
+ if (locked) {
+ clearBlocked();
+ }
+ }
+
+ @Override
+ public void subTask(String name) {
+ if (subTaskLabel.isDisposed()) {
+ return;
+ }
+ if (name == null) {
+ fSubTask = "";//$NON-NLS-1$
+ } else {
+ fSubTask = name;
+ }
+// subTaskLabel.setText(shortenText(fSubTask, subTaskLabel));
+ subTaskLabel.setText(fSubTask);
+ if (!forked) {
+ subTaskLabel.update();
+ }
+ }
+
+ @Override
+ public void worked(int work) {
+ internalWorked(work);
+ }
+
+ @Override
+ public void internalWorked(double work) {
+ if (!progressIndicator.isDisposed()) {
+ progressIndicator.worked(work);
+ }
+ }
+
+ @Override
+ public void clearBlocked() {
+ if (getShell() == null || getShell().isDisposed())
+ return;
+ locked = false;
+ updateForClearBlocked();
+ }
+
+ @Override
+ public void setBlocked(IStatus reason) {
+ if (getShell() == null || getShell().isDisposed())
+ return;
+ locked = true;
+ updateForSetBlocked(reason);
+ }
+ }
+
+ /**
+ * Clear blocked state from the receiver.
+ */
+ protected void updateForClearBlocked() {
+ progressIndicator.showNormal();
+ setMessage(task, true);
+ if (imageLabel != null) {
+ imageLabel.setImage(getImage());
+ }
+ }
+
+ /**
+ * Set blocked state from the receiver.
+ *
+ * @param reason
+ * IStatus that gives the details
+ */
+ protected void updateForSetBlocked(IStatus reason) {
+ progressIndicator.showPaused();
+ setMessage(reason.getMessage(), true);
+ if (imageLabel != null) {
+ imageLabel.setImage(getImage());
+ }
+ }
+
+ /**
+ * Creates a progress monitor dialog under the given shell. The dialog has a
+ * standard title and no image. <code>open</code> is non-blocking.
+ *
+ * @param parent
+ * the parent shell, or <code>null</code> to create a top-level
+ * shell
+ */
+ public ForkedProgressMonitorDialog(Shell parent) {
+ super(parent);
+ // no close button on the shell style
+ if (isResizable()) {
+ setShellStyle(getDefaultOrientation() | SWT.BORDER | SWT.TITLE
+ | SWT.APPLICATION_MODAL | SWT.RESIZE | SWT.MAX);
+ } else {
+ setShellStyle(getDefaultOrientation() | SWT.BORDER | SWT.TITLE
+ | SWT.APPLICATION_MODAL);
+ }
+ setBlockOnOpen(false);
+ }
+
+ /**
+ * Enables the cancel button (asynchronously).
+ *
+ * @param b
+ * The state to set the button to.
+ */
+ private void asyncSetOperationCancelButtonEnabled(final boolean b) {
+ if (getShell() != null) {
+ getShell().getDisplay().asyncExec(() -> setOperationCancelButtonEnabled(b));
+ }
+ }
+
+ /**
+ * The cancel button has been pressed.
+ *
+ * @since 3.0
+ */
+ @Override
+ protected void cancelPressed() {
+ // NOTE: this was previously done from a listener installed on the
+ // cancel button. On GTK, the listener installed by
+ // Dialog.createButton is called first and this was throwing an
+ // exception because the cancel button was already disposed
+ cancel.setEnabled(false);
+ progressMonitor.setCanceled(true);
+ super.cancelPressed();
+ }
+
+ /**
+ * The <code>ProgressMonitorDialog</code> implementation of this method
+ * only closes the dialog if there are no currently running runnables.
+ */
+ @Override
+ public boolean close() {
+ if (getNestingDepth() <= 0) {
+ clearCursors();
+ return super.close();
+ }
+ return false;
+ }
+
+ /**
+ * Clear the cursors in the dialog.
+ *
+ * @since 3.0
+ */
+ protected void clearCursors() {
+ if (cancel != null && !cancel.isDisposed()) {
+ cancel.setCursor(null);
+ }
+ Shell shell = getShell();
+ if (shell != null && !shell.isDisposed()) {
+ shell.setCursor(null);
+ }
+ if (arrowCursor != null) {
+ arrowCursor.dispose();
+ }
+ arrowCursor = null;
+ }
+
+ @Override
+ protected void configureShell(final Shell shell) {
+ super.configureShell(shell);
+ shell.setText(JFaceResources.getString("ProgressMonitorDialog.title")); //$NON-NLS-1$
+ shell.setCursor(shell.getDisplay().getSystemCursor(SWT.CURSOR_WAIT));
+ // Add a listener to set the message properly when the dialog becomes
+ // visible
+ shell.addListener(SWT.Show, event -> shell.getDisplay().asyncExec(() -> setMessage(message, true)));
+ }
+
+ @Override
+ protected void createButtonsForButtonBar(Composite parent) {
+ // cancel button
+ createCancelButton(parent);
+ }
+
+ /**
+ * Creates the cancel button.
+ *
+ * @param parent
+ * the parent composite
+ * @since 3.0
+ */
+ protected void createCancelButton(Composite parent) {
+ cancel = createButton(parent, IDialogConstants.CANCEL_ID,
+ IDialogConstants.CANCEL_LABEL, false);
+ if (arrowCursor == null) {
+ arrowCursor = new Cursor(cancel.getDisplay(), SWT.CURSOR_ARROW);
+ }
+ cancel.setCursor(arrowCursor);
+ setOperationCancelButtonEnabled(enableCancelButton);
+ }
+
+ @Override
+ protected Control createDialogArea(Composite parent) {
+ setMessage(DEFAULT_TASKNAME, false);
+ createMessageArea(parent);
+ // Only set for backwards compatibility
+ taskLabel = messageLabel;
+ // progress indicator
+ progressIndicator = new ProgressIndicator(parent);
+ GridData gd = new GridData();
+ gd.heightHint = convertVerticalDLUsToPixels(BAR_DLUS);
+ gd.horizontalAlignment = GridData.FILL;
+ gd.grabExcessHorizontalSpace = true;
+ gd.horizontalSpan = 2;
+ progressIndicator.setLayoutData(gd);
+ // label showing current task
+ subTaskLabel = new Label(parent, SWT.LEFT | SWT.WRAP);
+ gd = new GridData(GridData.FILL_HORIZONTAL);
+ gd.heightHint = convertVerticalDLUsToPixels(LABEL_DLUS);
+ gd.horizontalSpan = 2;
+ subTaskLabel.setLayoutData(gd);
+ subTaskLabel.setFont(parent.getFont());
+ return parent;
+ }
+
+ @Override
+ protected Point getInitialSize() {
+ Point calculatedSize = super.getInitialSize();
+ if (calculatedSize.x < 450) {
+ calculatedSize.x = 450;
+ }
+ return calculatedSize;
+ }
+
+ /**
+ * Returns the progress monitor to use for operations run in this progress
+ * dialog.
+ *
+ * @return the progress monitor
+ */
+ public IProgressMonitor getProgressMonitor() {
+ return progressMonitor;
+ }
+
+ /**
+ * This implementation of IRunnableContext#run(boolean, boolean,
+ * IRunnableWithProgress) runs the given <code>IRunnableWithProgress</code>
+ * using the progress monitor for this progress dialog and blocks until the
+ * runnable has been run, regardless of the value of <code>fork</code>.
+ * The dialog is opened before the runnable is run, and closed after it
+ * completes. It is recommended that <code>fork</code> is set to true in
+ * most cases. If <code>fork</code> is set to <code>false</code>, the
+ * runnable will run in the UI thread and it is the runnable's
+ * responsibility to call <code>Display.readAndDispatch()</code> to ensure
+ * UI responsiveness.
+ */
+ @Override
+ public void run(boolean fork, boolean cancelable,
+ IRunnableWithProgress runnable) throws InvocationTargetException,
+ InterruptedException {
+ setCancelable(cancelable);
+ try {
+ aboutToRun();
+ // Let the progress monitor know if they need to update in UI Thread
+ progressMonitor.forked = fork;
+ ModalContext.run(runnable, fork, getProgressMonitor(), getShell()
+ .getDisplay());
+ } finally {
+ finishedRun();
+ }
+ }
+
+ /**
+ * Returns whether the dialog should be opened before the operation is run.
+ * Defaults to <code>true</code>
+ *
+ * @return <code>true</code> to open the dialog before run,
+ * <code>false</code> to only create the dialog, but not open it
+ * @since 3.0
+ */
+ public boolean getOpenOnRun() {
+ return openOnRun;
+ }
+
+ /**
+ * Sets whether the dialog should be opened before the operation is run.
+ * NOTE: Setting this to false and not forking a process may starve any
+ * asyncExec that tries to open the dialog later.
+ *
+ * @param openOnRun
+ * <code>true</code> to open the dialog before run,
+ * <code>false</code> to only create the dialog, but not open
+ * it
+ * @since 3.0
+ */
+ public void setOpenOnRun(boolean openOnRun) {
+ this.openOnRun = openOnRun;
+ }
+
+ /**
+ * Returns the nesting depth of running operations.
+ *
+ * @return the nesting depth of running operations
+ * @since 3.0
+ */
+ protected int getNestingDepth() {
+ return nestingDepth;
+ }
+
+ /**
+ * Increments the nesting depth of running operations.
+ *
+ * @since 3.0
+ */
+ protected void incrementNestingDepth() {
+ nestingDepth++;
+ }
+
+ /**
+ * Decrements the nesting depth of running operations.
+ *
+ * @since 3.0
+ *
+ */
+ protected void decrementNestingDepth() {
+ nestingDepth--;
+ }
+
+ /**
+ * Called just before the operation is run. Default behaviour is to open or
+ * create the dialog, based on the setting of <code>getOpenOnRun</code>,
+ * and increment the nesting depth.
+ *
+ * @since 3.0
+ */
+ protected void aboutToRun() {
+ if (getOpenOnRun()) {
+ open();
+ } else {
+ create();
+ }
+ incrementNestingDepth();
+ }
+
+ /**
+ * Called just after the operation is run. Default behaviour is to decrement
+ * the nesting depth, and close the dialog.
+ *
+ * @since 3.0
+ */
+ protected void finishedRun() {
+ decrementNestingDepth();
+ close();
+ }
+
+ /**
+ * Sets whether the progress dialog is cancelable or not.
+ *
+ * @param cancelable
+ * <code>true</code> if the end user can cancel this progress
+ * dialog, and <code>false</code> if it cannot be canceled
+ */
+ public void setCancelable(boolean cancelable) {
+ if (cancel == null) {
+ enableCancelButton = cancelable;
+ } else {
+ asyncSetOperationCancelButtonEnabled(cancelable);
+ }
+ }
+
+ /**
+ * Helper to enable/disable Cancel button for this dialog.
+ *
+ * @param b
+ * <code>true</code> to enable the cancel button, and
+ * <code>false</code> to disable it
+ * @since 3.0
+ */
+ protected void setOperationCancelButtonEnabled(boolean b) {
+ operationCancelableState = b;
+ if (cancel != null && !cancel.isDisposed()) {
+ cancel.setEnabled(b);
+ }
+ }
+
+ @Override
+ protected Image getImage() {
+ return getInfoImage();
+ }
+
+ /**
+ * Set the message in the message label.
+ *
+ * @param messageString
+ * The string for the new message.
+ * @param force
+ * If force is true then always set the message text.
+ */
+ private void setMessage(String messageString, boolean force) {
+ // must not set null text in a label
+ message = messageString == null ? "" : messageString; //$NON-NLS-1$
+ if (messageLabel == null || messageLabel.isDisposed()) {
+ return;
+ }
+ if (force || messageLabel.isVisible()) {
+ messageLabel.setToolTipText(message);
+ messageLabel.setText(shortenText(message, messageLabel));
+ }
+ }
+
+ /**
+ * Update the message label. Required if the monitor is forked.
+ */
+ private void update() {
+ if (messageLabel == null || messageLabel.isDisposed()) {
+ return;
+ }
+ messageLabel.update();
+ }
+
+ @Override
+ public int open() {
+ // Check to be sure it is not already done. If it is just return OK.
+ if (!getOpenOnRun()) {
+ if (getNestingDepth() == 0) {
+ return OK;
+ }
+ }
+ int result = super.open();
+ // update message label just in case beginTask() has been invoked
+ // already
+ if (task == null || task.length() == 0)
+ setMessage(DEFAULT_TASKNAME, true);
+ else
+ setMessage(task, true);
+ return result;
+ }
+}
diff --git a/toolbox/org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/pcal/PCalTranslator.java b/toolbox/org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/pcal/PCalTranslator.java
index 0feca318b3392364a8317bed20625fc9bc005747..e0655248913d320c9339485c448764c731c0e789 100644
--- a/toolbox/org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/pcal/PCalTranslator.java
+++ b/toolbox/org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/pcal/PCalTranslator.java
@@ -33,7 +33,6 @@ import java.util.List;
import org.eclipse.core.resources.IFile;
import org.eclipse.core.resources.IMarker;
import org.eclipse.core.runtime.IProgressMonitor;
-import org.eclipse.jface.dialogs.ProgressMonitorDialog;
import org.eclipse.jface.operation.IRunnableContext;
import org.eclipse.jface.operation.IRunnableWithProgress;
import org.eclipse.jface.text.IDocument;
@@ -50,6 +49,7 @@ import org.lamport.tla.toolbox.util.pref.IPreferenceConstants;
import org.lamport.tla.toolbox.util.pref.PreferenceStoreHelper;
import pcal.Translator;
+import pcal.ValidationCallBack;
public class PCalTranslator {
@@ -62,8 +62,8 @@ public class PCalTranslator {
// call to the PlusCal translator call is forked off into a non-UI thread.
// However, we use a ProgressMonitorDialog to lock the UI from further
// modifications.
- final IRunnableContext context = new ProgressMonitorDialog(tlaEditor.getEditorSite().getShell());
- context.run(true, false, new IRunnableWithProgress() {
+ final IRunnableContext context = new ValidationProgressMonitorDialog(tlaEditor.getEditorSite().getShell());
+ context.run(true, true, new IRunnableWithProgress() {
public void run(final IProgressMonitor progressMonitor) throws InvocationTargetException, InterruptedException {
final IEditorInput editorInput = tlaEditor.getEditorInput();
final IDocument doc = tlaEditor.getDocumentProvider().getDocument(editorInput);
@@ -89,7 +89,7 @@ public class PCalTranslator {
// succeed, we know there are parser problems which we will use to marker the
// editor.
final Translator translator = new Translator(doc.get(), asList);
- if (translator.translate()) {
+ if (translator.translate((ValidationCallBack) context)) {
// Update the mapping to/from TLA+ to PlusCal.
spec.setTpMapping(translator.getMapping(), file.getName(), progressMonitor);
diff --git a/toolbox/org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/pcal/ValidationProgressMonitorDialog.java b/toolbox/org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/pcal/ValidationProgressMonitorDialog.java
new file mode 100644
index 0000000000000000000000000000000000000000..0313be1b6cd0bc6e1c38ad07c9e06c76352cadd8
--- /dev/null
+++ b/toolbox/org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/pcal/ValidationProgressMonitorDialog.java
@@ -0,0 +1,149 @@
+/*******************************************************************************
+ * Copyright (c) 2020 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 org.lamport.tla.toolbox.editor.basic.pcal;
+
+import java.util.concurrent.ArrayBlockingQueue;
+import java.util.concurrent.BlockingQueue;
+
+import org.eclipse.jface.dialogs.ForkedProgressMonitorDialog;
+import org.eclipse.jface.dialogs.IDialogConstants;
+import org.eclipse.jface.operation.IRunnableContext;
+import org.eclipse.swt.SWT;
+import org.eclipse.swt.widgets.Button;
+import org.eclipse.swt.widgets.Composite;
+import org.eclipse.swt.widgets.Event;
+import org.eclipse.swt.widgets.Listener;
+import org.eclipse.swt.widgets.Shell;
+
+import pcal.ValidationCallBack;
+
+public class ValidationProgressMonitorDialog extends ForkedProgressMonitorDialog implements IRunnableContext, ValidationCallBack {
+
+ private Button continueButton;
+
+ private Button thirdButton;
+
+ public ValidationProgressMonitorDialog(final Shell parent) {
+ super(parent);
+ }
+
+ @Override
+ protected void configureShell(final Shell shell) {
+ super.configureShell(shell);
+ // Set the title (dialog frame).
+ shell.setText("Translate PlusCal Algorithm.");
+ }
+
+ @Override
+ protected void createButtonsForButtonBar(final Composite parent) {
+ // Create a second button with which the user can chose to continue.
+ thirdButton = createButton(parent, IDialogConstants.OK_ID, "&Overwrite Translation", true);
+ thirdButton.setEnabled(false); // disabled by default unless doIt explicitly called.
+ thirdButton.setVisible(false);
+
+ // Create a second button with which the user can chose to continue.
+ continueButton = createButton(parent, IDialogConstants.OK_ID, "&Overwrite Translation", true);
+ continueButton.setEnabled(false); // disabled by default unless doIt explicitly called.
+
+ // Let superclass create the cancel button to which we attach our listener.
+ super.createButtonsForButtonBar(parent);
+ cancel.setText("&Abort");
+
+ getShell().setDefaultButton(continueButton);
+ }
+
+ @Override
+ public boolean shouldCancel() {
+
+ final Object lock = new Object();
+
+ final Listener listener = new Listener() {
+ public void handleEvent(final Event e) {
+ // Nothing to do here except releasing the latch.
+ synchronized (lock) {
+ lock.notifyAll(); // Technically, notify would suffice.
+ };
+ }
+ };
+
+ // Set the label on the dialog and enable the cancel and
+ // continue buttons.
+ getShell().getDisplay().syncExec(() -> {
+ getProgressMonitor().setTaskName("Overwrite modified TLA+ translation?");
+ getProgressMonitor().subTask(
+ "The TLA+ translation has been manually modified since its last translation (chksum(tla) mismatch). Click the \"Overwrite Translation\" button to replace the TLA+ translation anyway or \"Cancel\" to abort re-translation and keep the modified TLA+ translation.");
+ continueButton.setText("&Overwrite Translation");
+ continueButton.setEnabled(true);
+ continueButton.addListener(SWT.Selection, listener);
+ cancel.setText("&Abort");
+ cancel.setEnabled(true);
+ cancel.addListener(SWT.Selection, listener);
+ });
+
+ // Block this thread until the user presses either the cancel or continue button.
+ try {
+ synchronized (lock) {
+ lock.wait();
+ };
+ } catch (InterruptedException e) {
+ Thread.currentThread().interrupt();
+ return true;
+ }
+
+ // True if the user pressed cancel button, false if continue.
+ return getProgressMonitor().isCanceled();
+ }
+
+ @Override
+ public Generate shouldGenerate() {
+ final BlockingQueue<Generate> q = new ArrayBlockingQueue<>(1);
+
+ // Set the label on the dialog and enable the cancel and
+ // continue buttons.
+ getShell().getDisplay().syncExec(() -> {
+ getProgressMonitor().setTaskName("Add Checksums to TLA+ translation?");
+ getProgressMonitor().subTask(
+ "The PlusCal translator can add checksums to the \\* BEGIN TRANSLATION line of this spec to warn you before model-checking a stale TLA+ translation. Do you want to add checksums, never add checksums, or decide later?");
+ continueButton.setText("&Add Checksums");
+ continueButton.setEnabled(true);
+ continueButton.addListener(SWT.Selection,(e) -> q.offer(Generate.DO_IT));
+ cancel.setText("&Later");
+ cancel.setEnabled(true);
+ cancel.addListener(SWT.Selection,(e) -> q.offer(Generate.NOT_NOW));
+ thirdButton.setText("&Never Add");
+ thirdButton.setEnabled(true);
+ thirdButton.setVisible(true);
+ thirdButton.addListener(SWT.Selection,(e) -> q.offer(Generate.IGNORE));
+ });
+
+ try {
+ return q.take();
+ } catch (InterruptedException e) {
+ Thread.currentThread().interrupt();
+ return Generate.NOT_NOW;
+ }
+ }
+}
diff --git a/toolbox/org.lamport.tla.toolbox.feature.standalone/feature.xml b/toolbox/org.lamport.tla.toolbox.feature.standalone/feature.xml
index 56a805a6e13a216d168b84a9f9c3066c863fbf11..7b295fe909741b7f4256497379f9e4ca7365a502 100644
--- a/toolbox/org.lamport.tla.toolbox.feature.standalone/feature.xml
+++ b/toolbox/org.lamport.tla.toolbox.feature.standalone/feature.xml
@@ -324,7 +324,7 @@
id="org.eclipse.jdt.annotation"
download-size="0"
install-size="0"
- version="1.1.400.v20180921-1416"
+ version="1.1.500.v20200407-1355"
unpack="false"/>
<plugin
@@ -355,4 +355,11 @@
version="0.0.0"
unpack="false"/>
+ <plugin
+ id="org.eclipse.e4.ui.ide"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"
+ unpack="false"/>
+
</feature>
diff --git a/toolbox/org.lamport.tla.toolbox.product.product/TLAToolbox.target b/toolbox/org.lamport.tla.toolbox.product.product/TLAToolbox.target
index ce56b36199c52b3a23fea81aae4d2d49bd93e371..f557ad7de79319e92bfc012164e58ca92de6f760 100644
--- a/toolbox/org.lamport.tla.toolbox.product.product/TLAToolbox.target
+++ b/toolbox/org.lamport.tla.toolbox.product.product/TLAToolbox.target
@@ -3,7 +3,7 @@
<location includeAllPlatforms="false" includeConfigurePhase="false" includeMode="planner" includeSource="true" type="InstallableUnit">
<unit id="org.eclipse.contribution.weaving.feature.group" version="0.0.0"/>
<unit id="org.eclipse.ajdt.feature.group" version="0.0.0"/>
-<repository id="eclipse-ajdt" location="http://download.eclipse.org/tools/ajdt/48/dev/update/ajdt-e48-2.2.4.201908131520/"/>
+<repository id="eclipse-ajdt" location="http://download.eclipse.org/tools/ajdt/410/dev/update/ajdt-e410-2.2.4.202007241909"/>
</location>
<location includeAllPlatforms="false" includeConfigurePhase="false" includeMode="planner" includeSource="true" type="InstallableUnit">
<unit id="org.apache.log4j" version="0.0.0"/>
@@ -41,7 +41,7 @@
<unit id="org.eclipse.core.runtime.feature.feature.group" version="0.0.0"/>
<unit id="org.eclipse.jdt.feature.group" version="0.0.0"/>
<unit id="org.eclipse.pde.source.feature.group" version="0.0.0"/>
-<repository id="eclipse" location="http://download.eclipse.org/eclipse/updates/4.13/R-4.13-201909161045"/>
+<repository id="eclipse" location="http://download.eclipse.org/eclipse/updates/4.16/R-4.16-202006040540/"/>
</location>
<location includeAllPlatforms="false" includeConfigurePhase="false" includeMode="planner" includeSource="true" type="InstallableUnit">
<unit id="org.eclipse.egit.feature.group" version="0.0.0"/>
diff --git a/toolbox/org.lamport.tla.toolbox.product.product/entitlements.plist b/toolbox/org.lamport.tla.toolbox.product.product/entitlements.plist
index afa54db33b9f4537ab2dee65bed8423c35a7e9bf..5b0a42361d4eb3b45b07a7ad0083f4ef335eb9b6 100644
--- a/toolbox/org.lamport.tla.toolbox.product.product/entitlements.plist
+++ b/toolbox/org.lamport.tla.toolbox.product.product/entitlements.plist
@@ -12,5 +12,7 @@
<true/>
<key>com.apple.security.cs.disable-library-validation</key>
<true/>
+ <key>com.apple.security.cs.debugger</key>
+ <true/>
</dict>
</plist>
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 cf8f405108f88e8997fcd4c6e6e12ddbd41050a0..e79ef3fa9372269920d06b4d75113bffcb817287 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,17 +1,17 @@
<?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.0.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.1.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.0 of 20 April 2020 and includes:
+This is Version 1.7.1 of 31 December 2020 and includes:
- SANY Version 2.2 of 20 April 2020
- - TLC Version 2.15 of 20 April 2020
- - PlusCal Version 1.10 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.
@@ -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.0" />
+ <property name="eclipse.buildId" value="1.7.1" />
</configurations>
<repositories>
- <repository location="http://lamport.org/tlatoolbox/branches/1.7.0/toolboxUpdate/" enabled="true" />
+ <repository location="http://lamport.org/tlatoolbox/branches/1.7.1/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 c6efde3da48d005bcf9b9cf6187b42a363f0b632..98d54a174ed9411d1a92667eccad0a4f5fac20ed 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.0 of 20 April 2020 and includes:
 - SANY Version 2.2 of 20 April 2020
 - TLC Version 2.15 of 20 April 2020
 - PlusCal Version 1.10 of 20 April 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.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">
</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 cc83746bfb2d99a158e282ea13cee1992ed111b2..8a8e21c454c87eed26cb8338f85c680c91538165 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.0 of 20 April 2020");
+ lblVersion.setText("Version 1.7.1 of 31 December 2020");
lblVersion.setBackground(backgroundColor);
}
diff --git a/toolbox/org.lamport.tla.toolbox.product.uitest/pom.xml b/toolbox/org.lamport.tla.toolbox.product.uitest/pom.xml
index 62963a225ceebe94d8baea7d9ab3c6514514ece8..fc6c437acd09eb1db7d6b6592f5e933392973697 100644
--- a/toolbox/org.lamport.tla.toolbox.product.uitest/pom.xml
+++ b/toolbox/org.lamport.tla.toolbox.product.uitest/pom.xml
@@ -39,8 +39,8 @@
http://maven.xored.com/nexus/content/repositories/ci4rcptt-releases/org/eclipse/sdk/
-->
<properties>
- <rcptt-maven-version>2.4.3</rcptt-maven-version>
- <rcptt-runner-version>2.4.3</rcptt-runner-version>
+ <rcptt-maven-version>2.5.1</rcptt-maven-version>
+ <rcptt-runner-version>2.5.1</rcptt-runner-version>
<aut-unpack-directory>target/unpack-for-aut/</aut-unpack-directory>
<!--
<jdk-bundle-plugin-prefix>st.theori.openjdk.</jdk-bundle-plugin-prefix>
@@ -181,7 +181,7 @@
DO NOT USE - see above comment WRT truezip
- <explicit>../org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.0-[platform].zip</explicit>
+ <explicit>../org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-[platform].zip</explicit>
-->
<explicit>${aut-unpack-directory}</explicit>
diff --git a/toolbox/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCModelLaunchDataProvider.java b/toolbox/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCModelLaunchDataProvider.java
index 839437ea1a5636f39e447322a47835b419763176..d3bbc1d693ade7c2a7fb786850bb74bdbb2db055 100644
--- a/toolbox/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCModelLaunchDataProvider.java
+++ b/toolbox/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCModelLaunchDataProvider.java
@@ -364,6 +364,18 @@ public class TLCModelLaunchDataProvider implements ITLCOutputListener
break;
case MP.NONE:
+ if (messageCode == EC.TLC_COVERAGE_MISMATCH) {
+ // The Toolbox's error parser expects the error trace 2217 to directly follow
+ // the 2110 error marker. However, when TLC runs with multiple workers, 2217 and
+ // 2110 can be interleaved with 2776 if one or more workers have already started
+ // evaluating the next-state relation again before they receive the violation
+ // signal. See Github issue #538 for more details and in particular
+ // https://github.com/tlaplus/tlaplus/issues/538#issuecomment-751945328
+ // Bugs in the CostModelCreator that cause TCL_COVERAGE_MISMATCH should be fixed
+ // separately.
+ break;
+ }
+
if (lastDetectedError != null)
{
// something is detected which is not an error
diff --git a/toolbox/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCState.java b/toolbox/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCState.java
index d36996433b22f3d9eababe3a404462b48316e484..3d8ff45c0e1ae6995a471cd9e14ca8fc9ce3c858 100644
--- a/toolbox/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCState.java
+++ b/toolbox/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCState.java
@@ -99,7 +99,15 @@ public class TLCState implements IModuleLocatable
{
final TLCState state = BACK_TO_STATE(number, modelName);
// See in MP.java case for EC.TLC_BACK_TO_STATE
- state.setLocation(Location.parseLocation(label.substring((BACK_TO_STATE + ": ").length(), label.length())));
+ if (label.indexOf(BACK_TO_STATE + ": ") < 0) {
+ // LiveCheck1 of simulation mode didn't report the location of the back to
+ // state in a lasso trace. Setting the location to nullLoc here means that
+ // a double-click on "back to state..." in the error-trace explorer doesn't
+ // select and reveal the action in the spec.
+ state.setLocation(Location.nullLoc);
+ } else {
+ state.setLocation(Location.parseLocation(label.substring((BACK_TO_STATE + ": ").length(), label.length())));
+ }
return state;
} else
{
diff --git a/toolbox/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TLCModelLaunchDelegate.java b/toolbox/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TLCModelLaunchDelegate.java
index aebc2f6ddb47e28e2faeb9910cfb96cfb9ca8a52..7b6efd2a011a02f8d1497d5ebe44736d17cc9dab 100644
--- a/toolbox/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TLCModelLaunchDelegate.java
+++ b/toolbox/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TLCModelLaunchDelegate.java
@@ -14,7 +14,6 @@ import java.util.Arrays;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Hashtable;
-import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map;
import java.util.Properties;
@@ -22,7 +21,6 @@ import java.util.Random;
import java.util.Set;
import java.util.Vector;
import java.util.concurrent.atomic.AtomicBoolean;
-import java.util.concurrent.atomic.AtomicInteger;
import java.util.stream.Collectors;
import org.eclipse.core.internal.resources.ResourceException;
@@ -54,12 +52,10 @@ import org.eclipse.debug.core.Launch;
import org.eclipse.debug.core.model.IProcess;
import org.eclipse.debug.core.model.IStreamsProxy;
import org.eclipse.debug.core.model.LaunchConfigurationDelegate;
-import org.eclipse.jface.dialogs.IDialogConstants;
import org.eclipse.jface.dialogs.MessageDialog;
import org.eclipse.jface.dialogs.MessageDialogWithToggle;
import org.eclipse.jface.text.FindReplaceDocumentAdapter;
import org.eclipse.jface.text.IDocument;
-import org.eclipse.swt.SWT;
import org.eclipse.swt.widgets.Display;
import org.eclipse.ui.PartInitException;
import org.eclipse.ui.PlatformUI;
@@ -88,6 +84,7 @@ import org.osgi.framework.FrameworkUtil;
import org.osgi.framework.ServiceReference;
import pcal.Validator;
+import pcal.Validator.ValidationResult;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpDeclNode;
import tlc2.TLCGlobals;
@@ -129,20 +126,6 @@ public class TLCModelLaunchDelegate extends LaunchConfigurationDelegate
* Only generate the models but do not run TLC
*/
public static final String MODE_GENERATE = "generate";
-
- private static final AtomicBoolean PERFORM_VALIDATION_BEFORE_LAUNCH = new AtomicBoolean(true);
-
- private static final Integer DIVERGENCE_CONTINUE_LAUNCH = Integer.valueOf(1);
- private static final Integer DIVERGENCE_SHOW_HISTORY = Integer.valueOf(2);
- private static final LinkedHashMap<String, Integer> DIVERGENCE_DIALOG_BUTTONS;
-
- static {
- DIVERGENCE_DIALOG_BUTTONS = new LinkedHashMap<>();
- DIVERGENCE_DIALOG_BUTTONS.put("&Abort Launch", Integer.valueOf(0));
- DIVERGENCE_DIALOG_BUTTONS.put("Continue &Launch", DIVERGENCE_CONTINUE_LAUNCH);
- DIVERGENCE_DIALOG_BUTTONS.put("Abort Launch && Show &History", DIVERGENCE_SHOW_HISTORY); // "&&" because "&" is mnemonic.
- }
-
// Mutex rule for the following jobs to run after each other
protected MutexRule mutexRule = new MutexRule();
@@ -183,16 +166,16 @@ public class TLCModelLaunchDelegate extends LaunchConfigurationDelegate
return false;
}
+ final AtomicBoolean success = new AtomicBoolean(true);
final int specType = config.getAttribute(MODEL_BEHAVIOR_SPEC_TYPE, MODEL_BEHAVIOR_TYPE_DEFAULT);
if ((specType != MODEL_BEHAVIOR_TYPE_NO_SPEC)
- && PERFORM_VALIDATION_BEFORE_LAUNCH.get()
&& mode.equals(MODE_MODELCHECK)) {
final Model model = config.getAdapter(Model.class);
final IFile rootModule = model.getSpec().toSpec().getRootFile();
- final Validator.ValidationResult result;
+ final Set<Validator.ValidationResult> results;
try (final InputStream is = rootModule.getContents()) {
- result = Validator.validate(is);
+ results = Validator.validate(model.getSpec().toSpec().getRootModule().getRootParseUnit(), is);
} catch (final IOException e) {
monitor.done();
@@ -200,90 +183,110 @@ public class TLCModelLaunchDelegate extends LaunchConfigurationDelegate
}
final Display d = PlatformUI.getWorkbench().getDisplay();
- final AtomicInteger returnCode = new AtomicInteger(-1);
- switch (result) {
- case NO_PLUSCAL_EXISTS:
- case NO_DIVERGENCE:
- break;
- case ERROR_ENCOUNTERED:
- d.syncExec(() -> {
- final MessageDialogWithToggle dialog = MessageDialogWithToggle.openYesNoQuestion(
- d.getActiveShell(), "Error encountered",
- "Something went wrong attempting to detect divergence between PlusCal and its translation, continue anyway?",
- "Do not bug me about PlusCal verification during the rest of my Toolbox session.", false,
- null, null);
-
- if (dialog.getToggleState()) {
- PERFORM_VALIDATION_BEFORE_LAUNCH.set(false);
- }
-
- returnCode.set(dialog.getReturnCode());
- });
-
- if (returnCode.get() == IDialogConstants.NO_ID) {
- return false;
- }
- break;
- case NO_TRANSLATION_EXISTS:
- d.syncExec(() -> {
- final MessageDialogWithToggle dialog = MessageDialogWithToggle.openYesNoQuestion(
- d.getActiveShell(), "Translation missing",
- "Your spec appears to contain PlusCal but no TLA+ translation, are you sure you want to continue?",
- "Do not bug me about PlusCal verification during the rest of my Toolbox session.", false,
- null, null);
-
- if (dialog.getToggleState()) {
- PERFORM_VALIDATION_BEFORE_LAUNCH.set(false);
- }
-
- returnCode.set(dialog.getReturnCode());
- });
-
- if (returnCode.get() == IDialogConstants.NO_ID) {
- return false;
+ if (results.contains(ValidationResult.TLA_DIVERGENCE_EXISTS) && results.contains(ValidationResult.PCAL_DIVERGENCE_EXISTS)) {
+ /* Both hashes are invalid.
+ This is probably a sequel to Case 3, in which the user has decided either
+ (1) she has fixed the bug or (2) wants to change the spec and will later
+ modify the translation.
+ TLC called: By default, a warning should be raised. It should be considered
+ the same as Case 2. */
+ d.syncExec(() -> {
+ final MessageDialog md = new MessageDialog(d.getActiveShell(),
+ "The PlusCal algorithm and its translation have been modified after the last translation.",
+ null,
+ String.format(
+ "The PlusCal algorithm and its translation in module %s have been modified since the last translation (chksums mismatch).\n"
+ + "\nTo permanently disable this warning, change the conjuncts on the \\* BEGIN TRANSLATION line to:\n"
+ + "\n\t\tchksum(pcal) \\in STRING /\\ chksum(tla) \\in STRING\n"
+ + "\nWould you like to abort model-checking?",
+ model.getSpec().getRootModuleName()),
+ MessageDialog.WARNING, new String[] { "&Abort Model-Checking", "Continue &Model-Checking",
+ "Abort && Show Spec &History" },
+ 0);
+ final int open = md.open();
+ if (open != 1) {
+ success.set(false);
+ if (open == 2) {
+ final Module m = new Module(model.getSpec().getRootFile());
+ ShowHistoryHandler.openHistoryForModule(m);
+ }
+ }
+ });
+ } else if (results.contains(ValidationResult.TLA_DIVERGENCE_EXISTS)) {
+ /* The algorithm hash is valid and the translation hash is invalid.
+ There are two reasons: (1) The user is debugging the spec, or
+ (2) She needed to modify the translation because she wants a spec that can't
+ be produced by PlusCal.
+ TLC called: In both cases, no warning should be needed. However,
+ in (1), she might have finished debugging and forgotten to run the
+ translator. To handle case (1), I suggest the default should be to run
+ TLC but raise a transient window with a warning that is easily ignored.
+ For case (2), it should be possible to put something in a translation
+ comment to disable the warning. */
+ /*
+ * Raising a transient, modal dialog doesn't result in a good UX. Instead, it
+ * would be best to annotate the model editor with a warning. Unfortunately,
+ * this is not possible from this non-UI bundle and it's overkill to introduce a
+ * new listener. Thus, we will raise just another non-modal dialog that informs
+ * the user how to silence this warning.
+ */
+ d.syncExec(() -> {
+ final MessageDialog md = new MessageDialog(d.getActiveShell(),
+ "The TLA+ translation has been modified after the last translation.", null,
+ String.format(
+ "The TLA+ translation in module %s has changed since its last translation (chksum(tla) mismatch).\n"
+ + "\nTo permanently disable this warning, change the second conjunct on the \\* BEGIN TRANSLATION line to:\n"
+ + "\n\t\tchksum(tla) \\in STRING\n"
+ + "\nWould you like to abort model-checking?",
+ model.getSpec().getRootModuleName()),
+ MessageDialog.INFORMATION, new String[] { "&Abort Model-Checking",
+ "Continue &Model-Checking", "Abort && Show Spec &History" },
+ 1);
+ final int open = md.open();
+ if (open != 1) {
+ success.set(false);
+ if (open == 2) {
+ final Module m = new Module(model.getSpec().getRootFile());
+ ShowHistoryHandler.openHistoryForModule(m);
+ }
}
- break;
- case NO_CHECKSUMS_EXIST:
- d.syncExec(() -> {
- final MessageDialogWithToggle dialog = MessageDialogWithToggle.openInformation(
- d.getActiveShell(), "A note about your spec",
- "Your spec contains PlusCal and a TLA+ translation - but they have not been verified to "
- + "be in sync; consider re-translating the PlusCal algorithm.",
- "Do not bug me about PlusCal verification during the rest of my Toolbox session.", false,
- null, null);
-
- if (dialog.getToggleState()) {
- PERFORM_VALIDATION_BEFORE_LAUNCH.set(false);
- }
- });
-
- break;
- case DIVERGENCE_EXISTS:
- d.syncExec(() -> {
- final MessageDialogWithToggle dialog = MessageDialogWithToggle.open(MessageDialogWithToggle.QUESTION,
- d.getActiveShell(), "PlusCal out of sync",
- "The PlusCal and TLA+ translation in your spec appear to be out of sync - would you like to"
- + " stop the launch?",
- "Do not bug me about PlusCal verification during the rest of my Toolbox session.", false,
- null, null, SWT.NONE, DIVERGENCE_DIALOG_BUTTONS);
-
- if (dialog.getToggleState()) {
- PERFORM_VALIDATION_BEFORE_LAUNCH.set(false);
- }
-
- returnCode.set(dialog.getReturnCode());
- });
-
- if (returnCode.get() != DIVERGENCE_CONTINUE_LAUNCH.intValue()) {
- if (returnCode.get() == DIVERGENCE_SHOW_HISTORY.intValue()) {
+ });
+ } else if (results.contains(ValidationResult.PCAL_DIVERGENCE_EXISTS)) {
+ /* The algorithm hash is invalid and the translation hash is valid.
+ TLC called: By default, a warning should be generated. I see little reason
+ for not generating the warning. So, it doesn't matter if its inconvenient
+ to turn off the warning, but turning it off should affect only the current
+ spec; and it should be easy to turn back on. */
+ d.syncExec(() -> {
+ final MessageDialog md = new MessageDialog(d.getActiveShell(),
+ "PlusCal algorithm has changed but not re-translated", null,
+ String.format(
+ "The PlusCal algorithm in module %s has changed since its last translation (chksum(pcal) mismatch).\n"
+ + "\nTo permanently disable this warning, change the first conjunct on the \\* BEGIN TRANSLATION line to:\n"
+ + "\n\t\tchksum(pcal) \\in STRING\n"
+ + "\nWould you like to abort model-checking?",
+ model.getSpec().getRootModuleName()),
+ MessageDialog.WARNING, new String[] { "&Abort Model-Checking", "Continue &Model-Checking",
+ "Abort && Show Spec &History" },
+ 0);
+ final int open = md.open();
+ if (open != 1) {
+ success.set(false);
+ if (open == 2) {
final Module m = new Module(model.getSpec().getRootFile());
ShowHistoryHandler.openHistoryForModule(m);
}
-
- return false;
}
- break;
- }
+ });
+ } else if (results.contains(ValidationResult.ERROR_ENCOUNTERED)) {
+ d.syncExec(() -> {
+ MessageDialogWithToggle.openWarning(
+ d.getActiveShell(), "Error encountered",
+ "Something went wrong attempting to detect divergence between PlusCal and its translation, continue anyway?");
+
+ success.set(false);
+ });
+ }
}
try {
@@ -293,7 +296,7 @@ public class TLCModelLaunchDelegate extends LaunchConfigurationDelegate
monitor.done();
}
- return true;
+ return success.get();
}
/**
diff --git a/toolbox/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TraceExplorerDelegate.java b/toolbox/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TraceExplorerDelegate.java
index 76bf6b1b7cd26cceb507e97b852c8e84ea35718e..23aba96c2c6254cf601a3acfdc5f9876671e8a25 100644
--- a/toolbox/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TraceExplorerDelegate.java
+++ b/toolbox/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TraceExplorerDelegate.java
@@ -651,7 +651,7 @@ public class TraceExplorerDelegate extends TLCModelLaunchDelegate implements ILa
writer.addTraceFunction(trace);
// variables declarations for trace explorer expressions
- writer.addVariablesAndDefinitions(traceExpressionData, TLAConstants.TraceExplore.TRACE_EXPLORE_EXPRESSIONS, false);
+ writer.addVariablesAndDefinitions(traceExpressionData, TLAConstants.TraceExplore.TRACE_EXPLORE_EXPRESSIONS, true);
// add init and next
writer.addInitNext(trace, traceExpressionData, initId, nextId, actionConstraintId);
diff --git a/toolbox/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/spec/parser/ModuleParserLauncher.java b/toolbox/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/spec/parser/ModuleParserLauncher.java
index 125f202e343fffe2faa68985c17815c5a133cff6..6f664abc7048ede28561e012f6323662a61e49e2 100644
--- a/toolbox/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/spec/parser/ModuleParserLauncher.java
+++ b/toolbox/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/spec/parser/ModuleParserLauncher.java
@@ -156,7 +156,7 @@ public class ModuleParserLauncher
SANY.frontEndInitialize(moduleSpec, outputStr);
// should cancel?
checkCancel(monitor);
- SANY.frontEndParse(moduleSpec, outputStr);
+ SANY.frontEndParse(moduleSpec, outputStr, false);
// should cancel?
checkCancel(monitor);
SANY.frontEndSemanticAnalysis(moduleSpec, outputStr, true);
diff --git a/toolbox/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/util/RCPNameToFileIStream.java b/toolbox/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/util/RCPNameToFileIStream.java
index 7e28d9ee4011f23c97704169c920a9a037cd9ae0..ba241075001cb4db79c5c7b5f7206b9f0d71ebc4 100644
--- a/toolbox/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/util/RCPNameToFileIStream.java
+++ b/toolbox/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/util/RCPNameToFileIStream.java
@@ -175,7 +175,7 @@ public class RCPNameToFileIStream implements FilenameToStream
private File getFromArchive(String prefix, String name) {
final File outputFile = new TLAFile(TMPDIR + File.separator + name, true, this);
outputFile.deleteOnExit(); // Written to TMPDIR which is likely deleted regularly anyway.
- try (FileSystem fileSystem = FileSystems.newFileSystem(new File(prefix).toPath(), null)) {
+ try (FileSystem fileSystem = FileSystems.newFileSystem(new File(prefix).toPath(), (ClassLoader) null)) {
Path fileToExtract = fileSystem.getPath(name);
Files.copy(fileToExtract, outputFile.toPath(), StandardCopyOption.REPLACE_EXISTING);
return outputFile;