diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index f236d1f6f141982774ec133a2ca61e88de40e30a..dc9368190c43f6820a01bb5c76680d7a3aaf6a6d 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -1,8 +1,11 @@
-Please open issues to discuss your contributions prior to any patch you write. Some parts of the tlaplus repository follow a very strict contribution policy. We do not want to reject your 1k LOC patch because the actual change is not considered sensible by us.
+We welcome contributions from volunteers. A number of [improvements we'd like to see implemented](https://github.com/tlaplus/tlaplus/blob/master/general/docs/contributions.md) are listed at [general/docs/contributions.md](https://github.com/tlaplus/tlaplus/blob/master/general/docs/contributions.md) in addition to the [issues tagged with "helpwanted"](https://github.com/tlaplus/tlaplus/issues?q=is%3Aopen+is%3Aissue+label%3A%22help+wanted%22). But we're happy to consider anything you'd like to contribute. However, some parts of the tlaplus repository follow a very strict contribution policy. So before you start working on anything, please [discuss with us](https://github.com/tlaplus/tlaplus/issues) what you want to do. You can do that on the [issues page](https://github.com/tlaplus/tlaplus/issues). We do not want to reject your 1k LOC patch because the actual change is not considered sensible by us.
+
+
+
+Except for [TLAPS](https://tla.msr-inria.inria.fr/tlaps/content/Home.html), the TLA<sup>+</sup> tools are maintained in Eclipse. [For instructions on how to setup the Eclipse IDE, please go to general/ide/README.md.](https://github.com/tlaplus/tlaplus/tree/master/general/ide).
-[For instructions on how to setup the Eclipse IDE, please go to https://github.com/tlaplus/tlaplus/tree/master/general/ide.](https://github.com/tlaplus/tlaplus/tree/master/general/ide)
Quality Metrics
---------------
-We collect [quality metrics](https://sonarqube.com/organizations/tlaplus/projects). If you want to help out with the project, the reports indicate several low hanging fruits to pick.
+We collect [quality metrics](https://sonarcloud.io/organizations/tlaplus/projects). If you want to help out with the project, the reports indicate several low hanging fruits to pick.
diff --git a/general/docs/contributions.md b/general/docs/contributions.md
index 56831eefe1b0a8d0d29927aa442acf45e4549351..d9a8143dfe1fe085b0c6b1210e158a290385e861 100644
--- a/general/docs/contributions.md
+++ b/general/docs/contributions.md
@@ -6,7 +6,7 @@ Please also consult the [issues tracker](https://github.com/tlaplus/tlaplus/issu
TLC model checker
-----------------
#### Concurrent search for strongly connected components (difficulty: high) (skills: Java, TLA+)
-One part of TLC's procedure to check liveness properties, is to find the liveness graph's [strongly connected components](https://en.wikipedia.org/wiki/Strongly_connected_component) (SCC). TLC's implementation uses [Tarjan's](https://en.wikipedia.org/wiki/Strongly_connected_component) canonical solution to this problem. Tarjan's algorithm is a sequential algorithm that runs in linear time. While the time complexity is acceptable, its sequential nature causes TLC's liveness checking not to scale. Recently, concurrent variants of the algorithm have been proposed and [studied in the scope of other model checkers](https://wwwhome.ewi.utwente.nl/~laarman/papers/scc_ppopp_2016.pdf). This work will require writing a TLA+ specification and ideally a formal proof of the algorithm's correctness.
+One part of TLC's procedure to check liveness properties, is to find the liveness graph's [strongly connected components](https://en.wikipedia.org/wiki/Strongly_connected_component) (SCC). TLC's implementation uses [Tarjan's](https://en.wikipedia.org/wiki/Strongly_connected_component) canonical solution to this problem. Tarjan's algorithm is a sequential algorithm that runs in linear time. While the time complexity is acceptable, its sequential nature causes TLC's liveness checking not to scale. Recently, concurrent variants of the algorithm have been proposed and [studied in the scope of other model checkers](https://github.com/utwente-fmt/ppopp16). This work will require writing a TLA+ specification and ideally a formal proof of the algorithm's correctness.
#### Liveness checking under symmetry (difficulty: high) (skills: Java, TLA+)
[Symmetry reduction](http://www.cs.cmu.edu/~emc/papers/Conference%20Papers/Symmetry%20Reductions%20in%20Model%20Checking.pdf) techniques can significantly reduce the size of the state graph generated and checked by TLC. For safety checking, symmetry reduction is well studied and has long been implemented in TLC. TLC's liveness checking procedure however, can fail to find property violations if symmetry is declared. Yet, there is no reason why symmetry reduction cannot be applied to liveness checking. This work will require writing a TLA+ specification and ideally a formal proof of the algorithm's correctness.
@@ -37,3 +37,11 @@ TLA Toolbox
#### Package Toolbox for Debian and Fedora based Linux distributions (difficulty: easy) (skills: Eclipse, Linux)
The current Toolbox installation requires Linux users to download a zip file, to extract it and manually integrate the Toolbox into the System. Packaging the Toolbox for Debian (.deb) and Fedora (.rpm) based Linux distributions would not only simplify the installation procedure, it would also create more visible for TLA+ within the Linux community.
+#### Add support for Google Compute to Cloud TLC (difficulty: easy) (skills: jclouds, Linux)
+The Toolbox can launch Azure and Amazon EC2 instances to run model checking in the cloud. The Toolbox interfaces with clouds via the [jclouds](https://jclouds.apache.org/) toolkit. jclouds has support for Google Compute, but https://github.com/tlaplus/tlaplus/blob/master/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudDistributedTLCJob.java has to be enhanced to support Google Compute.
+
+#### Add support for x1 instances to jclouds (difficulty: easy) (skills: jclouds)
+We raised an [enhancement request for the jclouds toolkit](https://issues.apache.org/jira/browse/JCLOUDS-1339) to add support for Amazon's largest compute instances [(x1e.32xlarge, x1.32xlarge, x1.16xlarge)](https://aws.amazon.com/ec2/instance-types/x1/).
+
+#### Finish Unicode support (difficulty: easy) (skills: Eclipse, SANY)
+A few [outstanding issues](https://github.com/tlaplus/tlaplus/issues?q=is%3Aissue+is%3Aopen+label%3AUnicode) prevent the integration of the Unicode support into the Toolbox. In addition to the open issues, adding unit tests would be welcomed. A [nightly/ci Jenkins build](https://tla.msr-inria.inria.fr/build/job/M-HEAD-pron-unicode-Toolbox.product.standalone/) is available.
diff --git a/org.lamport.tla.toolbox.doc/html/model/about-models.html b/org.lamport.tla.toolbox.doc/html/model/about-models.html
index 09e709c6d63f9effc1cf2cc2a959df2bb78414b4..fb4ea01ad0106ab9fb5cfde4fb34b87534b9d510 100644
--- a/org.lamport.tla.toolbox.doc/html/model/about-models.html
+++ b/org.lamport.tla.toolbox.doc/html/model/about-models.html
@@ -87,22 +87,8 @@ model </p> <pre>
N=3,Proc={a1,a2,a3}
</pre>
<A name="locking">
-To prevent accidentally running or editing a model, you can lock it. </A>
-
-
-There is a lock icon and a key icon that you click to lock or
-unlock the model.
-
-Those icons are in the upper-left part of each model-editor page.
-
-
-The model is always locked while it is being run by TLC, and it remains
-locked after TLC completes unless the run was shorter
-than the
- <a href="executing-tlc.html#auto-lock-time"><em>TLC Run Auto-Lock Time</em> preference</A>.
-
-This means that you can't view information in sections of a running
-model that are closed.
+The model is always locked while it is being run by TLC. This means that
+you can't view information in sections of a running model that are closed.
It's therefore a good idea to open all sections of the model
that you might want to look at before starting a TLC run that will
diff --git a/org.lamport.tla.toolbox.doc/html/model/advanced-page.html b/org.lamport.tla.toolbox.doc/html/model/advanced-page.html
index e522d7323e7a0ee1cfa429c0fd501aa02c400e03..42f5b0f8525ecc8082f68a91e67c58a5ade906f8 100644
--- a/org.lamport.tla.toolbox.doc/html/model/advanced-page.html
+++ b/org.lamport.tla.toolbox.doc/html/model/advanced-page.html
@@ -275,18 +275,43 @@ contains more than this number of elements.
<h3>Visualize state graph after completion of model checking</h3>
<p>
Visualize the generated state graph graphically after completion of model checking. The
-visualization helps to better understand the the system being specified. Initial states are represented by gray vertices.
+visualization helps to better understand the system being specified. Initial states are represented by gray vertices.
<p><b>Warning: </b>Can reasonably only visualize small state graphs with a few dozen to hundred states.</b></p>
<p>
In order to visualize a state graph, the path to the <em>dot</em> executable of the
-<a href="http://www.graphviz.org/">GraphViz</a> project has to be set on the <em>State Graph</em> preference
-page on the File/Preferences menu. On macOS dot is most easily installed via the ports system. On Windows, can
-be obtained through Cygwin.
+<a href="http://www.graphviz.org/">GraphViz</a> project has to be set under <em>Specify dot command</em> on the <em>PDF viewer</em> preference
+page on the File/Preferences menu. On macOS dot is most easily installed via the ports system. Homebrew has a Graphviz port too.
+On Windows, GraphViz can be obtained through Cygwin or installed standalone. On most Linux derivatives, GraphViz can be installed via the package manager.
+After installation, the the dot binary can usually be found at:
+</p>
+
+<p>
+<table>
+ <tr>
+ <td>OS</td>
+ <td>Default path</td>
+ </tr>
+ <tr>
+ <td>Windows (Cygwin)</td>
+ <td>C:\cygwin\bin\dot.exe</td>
+ <tr>
+ <td>Windows (standalone)</td>
+ <td>C:\Program Files (x86)\Graphviz2.38\bin\dot.exe</td>
+ </tr>
+ <tr>
+ <td>macOS (ports)</td>
+ <td>/opt/local/bin/dot</td>
+ </tr>
+ <tr>
+ <td>Linux</td>
+ <td>/usr/bin/dot</td>
+ </tr>
+<table>
</p>
<p>
On Windows and Linux the state graph will be visualized with either the built-in or standalone PDF viewer
depending on which is selected on the PDF viewer preference page
-(selecting the standalone viewer is advised for best results).
+(selecting a standalone viewer is advised for best results).
</p>
<h3><A name="jvmargs">JVM arguments</A></h3>
diff --git a/org.lamport.tla.toolbox.doc/html/model/creating-model.html b/org.lamport.tla.toolbox.doc/html/model/creating-model.html
index 426e0cd9b469b4152e63eb24577d9d0d89f50a73..c71fc78d0d44ef555ffac0041cc3ca3245106901 100644
--- a/org.lamport.tla.toolbox.doc/html/model/creating-model.html
+++ b/org.lamport.tla.toolbox.doc/html/model/creating-model.html
@@ -43,15 +43,6 @@ in the model, as well as additional definitions entered in the
of the <A href="advanced-page.html">Advanced Options Page</A>.
</p>
-
-<p>
-A model can be locked or unlocked by using the lock icon or the key icon
-in the upper-left part of each model-editor page.
-
-The model is always locked while it is being run by TLC, and it remains
-locked after TLC completes unless the run was short.
-</p>
-
<hr>
<!-- delete rest of line to comment out -->
<dl>
diff --git a/org.lamport.tla.toolbox.doc/html/model/executing-tlc.html b/org.lamport.tla.toolbox.doc/html/model/executing-tlc.html
index 372384bd5af702212a3caff7a0842bf5d285a477..fee8a4a213595b7e864fffbec4556ee7238ac7a7 100644
--- a/org.lamport.tla.toolbox.doc/html/model/executing-tlc.html
+++ b/org.lamport.tla.toolbox.doc/html/model/executing-tlc.html
@@ -224,13 +224,14 @@ The model is automatically saved when you run or validate it, so you will
probably have no reason to save it explicitly.
</p>
-<h3>Take snapshot of model after completion of model checking</h3>
+<h3>Number of model snapshots to keep</h3>
<p>
Re-running a model erases the corresponding model checking results if any. With snapshots
-activate, the Toolbox creates a history of model runs. The history allows one to trace back
-the evolution of the specification and corresponding model.
+activate, the Toolbox maintains a history of the N most recent model runs. The value N is defined
+by <samp>Number of model snapshots to keep</samp> where zero disables snapshots completely.
+The history allows one to trace back the evolution of the specification and corresponding model.
</p>
-<p>Snapshots can be deleted in the Spec Explorer as needed.
+<p>Snapshots can also be deleted in the Spec Explorer as needed.
</p>
<h3>Maximum JVM Heap Size</h3>
@@ -241,15 +242,6 @@ in the <a href="overview-page.html#how-to-run">How to run?</a> section of the
model editor's Overview Page help page.
</p>
-<h3><A name="auto-lock-time">TLC Run Auto-Lock Time</A></h3>
-<p>
-
-If a TLC run completes after executing for at least this number of minutes,
-then the model will remain <A href="about-models.html#locking">locked</A>.
-
-</p>
-
-
<h3><A name="maximum-tail-length">Default number of states shown in error traces</A></h3>
<p>
diff --git a/org.lamport.tla.toolbox.doc/html/trouble/trouble.html b/org.lamport.tla.toolbox.doc/html/trouble/trouble.html
index 72fafe755fd72fe2ff0f44ed39d35bba4116375f..2ec05a5fdba7f3b2f639b1e16aad422a6ec5cf72 100644
--- a/org.lamport.tla.toolbox.doc/html/trouble/trouble.html
+++ b/org.lamport.tla.toolbox.doc/html/trouble/trouble.html
@@ -148,8 +148,8 @@ The <samp>.log</samp> file is in the
directory.
On Windows, you can find out where your home directory is located, by
-looking at the <samp>%HOMEPATH%</samp> environment variable. On
-Linux and Mac, check the $HOME variable.
+by entering the command <code>echo %SYSTEMDRIVE%%HOMEPATH%</code> in
+Command Prompt. On Linux and Mac, check the $HOME variable.
(The log contains enough timestamped entries for you to figure out
what part of it relates to the problem you are reporting.)
diff --git a/org.lamport.tla.toolbox.doc/html/update/update-preferences.html b/org.lamport.tla.toolbox.doc/html/update/update-preferences.html
index ed6a6a28598e7e8f3a4154a685835f26a6c2894c..d6b74f34b7d769922f9f126d3edcdb8390c8eb83 100644
--- a/org.lamport.tla.toolbox.doc/html/update/update-preferences.html
+++ b/org.lamport.tla.toolbox.doc/html/update/update-preferences.html
@@ -42,7 +42,7 @@ scheduled time, the search will be done when the Toolbox is next started.
</p>
<h3>Download options</h3>
-<p>If you schedules for updates to be checked, you can choose whether or not
+<p>If you schedule for updates to be checked, you can choose whether or not
to download (but not install) the new updates before notifying you.
</p>
@@ -53,6 +53,34 @@ scheduled time, the search will be done when the Toolbox is next started.
If you defer the update, a preference determines if the notification pops up
again and, if so, when.
+<!-- Some content reused from https://help.eclipse.org/oxygen/index.jsp?topic=%2Forg.eclipse.platform.doc.user%2Freference%2Fref-net-preferences.htm -->
+
+<h3>Network Connections</h3>
+If your network environment requires you to setup proxy servers to connect to the internet, you can do so on the
+Network Connections preference page found under <strong>General > Network Connections</strong>.
+
+The <i>Active Provider</i> instructs the Toolbox to use no proxy server (Direct), use the system's proxy server
+(Native) or the manually defined ones (Manual).
+
+<ul>
+ <li>Choosing the <i>Direct</i> provider causes all the connections to be opened without the use of a proxy server.</li>
+ <li><i>Native</i> causes settings that were discovered in the operating system to be used (does not work on macOS).</li>
+ <li>Selecting <i>Manual</i> causes settings defined in the <i>Proxy entries</i> table below to be used.</li>
+</ul>
+
+<p>
+When using the Manual provider there are three predefined schemas to set settings for: HTTP, HTTPS and SOCKS.
+Configuration for each schema is displayed in the <i>Proxy entries</i> table. To edit settings for a particular
+schema double-click the entry or select the entry and click Edit... button.
+</p>
+
+<p>
+The <i>Proxy bypass</i> table is only relevant for advanced use cases when different proxies need to be configured
+to access different computers on the internet. Most users can ignore the <i>Proxy bypass</i> table.
+</p>
+
+Please ask your network administrator if the Toolbox fails to access the internet and you do not know what to enter.
+
<hr>
<a href="run-update.html">↑ Updating the Toolbox</a>
</hr>
diff --git a/org.lamport.tla.toolbox.doc/pdfs/SRC-TN-1997-006A.pdf b/org.lamport.tla.toolbox.doc/pdfs/SRC-TN-1997-006A.pdf
deleted file mode 100644
index 75e9f60a6f84b80c404b3e8fe579b59f8b6d69f4..0000000000000000000000000000000000000000
Binary files a/org.lamport.tla.toolbox.doc/pdfs/SRC-TN-1997-006A.pdf and /dev/null differ
diff --git a/org.lamport.tla.toolbox.doc/plugin.xml b/org.lamport.tla.toolbox.doc/plugin.xml
index 8ce134611eb40298ac32e6f8cec01bc624c33dea..a43cad181545e30b6386d0b395132e8f535d09b0 100644
--- a/org.lamport.tla.toolbox.doc/plugin.xml
+++ b/org.lamport.tla.toolbox.doc/plugin.xml
@@ -72,27 +72,6 @@
tooltip="Opens Table of Contents">
</command>
</menuContribution>
- <!-- The Operators of TLA+ -->
- <menuContribution
- allPopups="false"
- locationURI="menu:toolbox.menu.help?after=toolbox.command.help.tlaplus">
- <command
- commandId="org.lamport.tla.toolbox.doc.pdf"
- label="The Operators of TLA+"
- mnemonic="O"
- mode="FORCE_TEXT"
- style="push"
- tooltip="Opens the paper "The Operators of TLA+"">
- <parameter
- name="org.lamport.tla.toolbox.doc.pdf.file"
- value="SRC-TN-1997-006A.pdf">
- </parameter>
- <parameter
- name="org.lamport.tla.toolbox.doc.pdf.name"
- value="Operators of TLA+">
- </parameter>
- </command>
- </menuContribution>
<!-- The TLA+ Cheat Sheet: -->
<menuContribution
allPopups="false"
diff --git a/org.lamport.tla.toolbox.feature.standalone/feature.xml b/org.lamport.tla.toolbox.feature.standalone/feature.xml
index 70b72b5268e83a1dfb121a29bba70a6321129827..5913e4911e890fac5d85c1507d524941dc3c0fbe 100644
--- a/org.lamport.tla.toolbox.feature.standalone/feature.xml
+++ b/org.lamport.tla.toolbox.feature.standalone/feature.xml
@@ -215,4 +215,65 @@
version="0.0.0"
unpack="false"/>
+ <plugin
+ id="org.eclipse.ui.net"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"
+ unpack="false"/>
+
+ <plugin
+ id="org.eclipse.core.net.linux.x86_64"
+ os="linux"
+ arch="x86_64"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"
+ fragment="true"
+ unpack="false"/>
+
+ <plugin
+ id="org.eclipse.core.net.linux.x86"
+ os="linux"
+ arch="x86"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"
+ fragment="true"
+ unpack="false"/>
+
+ <plugin
+ id="org.eclipse.core.net.win32.x86_64"
+ os="win32"
+ arch="x86_64"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"
+ fragment="true"
+ unpack="false"/>
+
+ <plugin
+ id="org.eclipse.core.net.win32.x86"
+ os="win32"
+ arch="x86"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"
+ fragment="true"
+ unpack="false"/>
+
+ <plugin
+ id="org.eclipse.equinox.p2.director"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"
+ unpack="false"/>
+
+ <plugin
+ id="org.eclipse.equinox.p2.director.app"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"
+ unpack="false"/>
+
</feature>
diff --git a/org.lamport.tla.toolbox.feature.uitest/.project b/org.lamport.tla.toolbox.feature.uitest/.project
new file mode 100644
index 0000000000000000000000000000000000000000..c05f540f012b8a10a43edb46ca516021b52f60cd
--- /dev/null
+++ b/org.lamport.tla.toolbox.feature.uitest/.project
@@ -0,0 +1,17 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+ <name>org.lamport.tla.toolbox.feature.uitest</name>
+ <comment></comment>
+ <projects>
+ </projects>
+ <buildSpec>
+ <buildCommand>
+ <name>org.eclipse.pde.FeatureBuilder</name>
+ <arguments>
+ </arguments>
+ </buildCommand>
+ </buildSpec>
+ <natures>
+ <nature>org.eclipse.pde.FeatureNature</nature>
+ </natures>
+</projectDescription>
diff --git a/org.lamport.tla.toolbox.feature.uitest/build.properties b/org.lamport.tla.toolbox.feature.uitest/build.properties
new file mode 100644
index 0000000000000000000000000000000000000000..82ab19c62d182db3688b1af6e6f465a74265ac92
--- /dev/null
+++ b/org.lamport.tla.toolbox.feature.uitest/build.properties
@@ -0,0 +1 @@
+bin.includes = feature.xml
diff --git a/org.lamport.tla.toolbox.feature.uitest/feature.xml b/org.lamport.tla.toolbox.feature.uitest/feature.xml
new file mode 100644
index 0000000000000000000000000000000000000000..56396d7c85322ae077ea53cdded9a6776dc1774d
--- /dev/null
+++ b/org.lamport.tla.toolbox.feature.uitest/feature.xml
@@ -0,0 +1,78 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<feature
+ id="org.lamport.tla.toolbox.feature.uitest"
+ label="TLA+ Toolbox UI test Feature"
+ version="1.0.0.qualifier"
+ provider-name="Markus Kuppe"
+ license-feature="org.lamport.tla.toolbox.feature.branding"
+ license-feature-version="1.0.0.qualifier">
+
+ <description>
+ This feature contains all UI tests.
+ </description>
+
+ <includes
+ id="org.eclipse.swtbot"
+ version="0.0.0"/>
+
+ <includes
+ id="org.eclipse.swtbot.eclipse"
+ version="0.0.0"/>
+
+ <includes
+ id="org.eclipse.swtbot.eclipse.test.junit"
+ version="0.0.0"/>
+
+ <includes
+ id="org.eclipse.swtbot.forms"
+ version="0.0.0"/>
+
+ <plugin
+ id="org.lamport.tla.toolbox.uitest"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"
+ unpack="false"/>
+
+ <plugin
+ id="org.lamport.tla.toolbox.tool.tlc.ui.uitest"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"
+ unpack="false"/>
+
+ <plugin
+ id="org.lamport.tla.toolbox.tool.tla2tex.uitest"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"
+ unpack="false"/>
+
+ <plugin
+ id="org.apache.log4j"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"
+ unpack="false"/>
+
+ <plugin
+ id="org.hamcrest.library"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"
+ unpack="false"/>
+
+ <plugin
+ id="org.eclipse.jdt.junit.runtime"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"
+ unpack="false"/>
+
+ <plugin
+ id="org.apache.ant"
+ download-size="0"
+ install-size="0"
+ version="0.0.0"/>
+
+</feature>
diff --git a/org.lamport.tla.toolbox.feature.uitest/pom.xml b/org.lamport.tla.toolbox.feature.uitest/pom.xml
new file mode 100644
index 0000000000000000000000000000000000000000..aa8d5b4b53a15e7466426449147ef4819c7ba087
--- /dev/null
+++ b/org.lamport.tla.toolbox.feature.uitest/pom.xml
@@ -0,0 +1,20 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project
+ xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd"
+ xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
+ <modelVersion>4.0.0</modelVersion>
+ <parent>
+ <artifactId>parent</artifactId>
+ <groupId>tlatoolbox</groupId>
+ <version>0.0.1-SNAPSHOT</version>
+ <relativePath>../pom.xml</relativePath>
+ </parent>
+ <groupId>tlatoolbox</groupId>
+ <artifactId>org.lamport.tla.toolbox.feature.uitest</artifactId>
+ <version>1.0.0-SNAPSHOT</version>
+ <packaging>eclipse-feature</packaging>
+ <properties>
+ <!-- Do not include non-code project in Sonar reporting. -->
+ <sonar.skip>true</sonar.skip>
+ </properties>
+</project>
diff --git a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/Application.java b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/Application.java
index dfa4e6baadbff97e82fd45b53469bb53a0977bb7..85e30988980c22dc64b20157e64e120a62f35a4c 100644
--- a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/Application.java
+++ b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/Application.java
@@ -90,6 +90,14 @@ public class Application implements IApplication {
boolean checkDeadlock = false;
if (!checkDeadlock) {
tlcParams.append("-deadlock");
+ tlcParams.append(" ");
+ }
+
+ // https://github.com/tlaplus/tlaplus/issues/92#issuecomment-339989087
+ final int coverage = Integer.getInteger("coverage", 0);
+ if (coverage > 0) {
+ tlcParams.append("-coverage ");
+ tlcParams.append(String.valueOf(coverage));
}
final TLCJobFactory factory = new CloudTLCJobFactory();
diff --git a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudDistributedTLCJob.java b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudDistributedTLCJob.java
index b66caf888dff68e00142d56b4212d75fdb085688..b609a25b42cf66297098e41d6b8f4e8830ddbacb 100644
--- a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudDistributedTLCJob.java
+++ b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudDistributedTLCJob.java
@@ -307,13 +307,16 @@ public class CloudDistributedTLCJob extends Job {
// world-readable. It is cloud-readable already through the RMI api.
monitor.subTask("Copying tla2tools.jar to master node at " + hostname);
SshClient sshClient = context.utils().sshForNode().apply(master);
- sshClient.put("/tmp/tla2tools.jar", jarPayLoad);
+ sshClient.put("/tmp/tla2tools.pack.gz", jarPayLoad);
monitor.worked(10);
if (monitor.isCanceled()) {
return Status.CANCEL_STATUS;
}
final String tlcMasterCommand = " cd /mnt/tlc/ && "
+ // Decompress tla2tools.pack.gz
+ + "unpack200 /tmp/tla2tools.pack.gz /tmp/tla2tools.jar"
+ + " && "
// Execute TLC (java) process inside screen
// and shutdown on TLC's completion. But
// detach from screen directly. Name screen
diff --git a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudTLCJobFactory.java b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudTLCJobFactory.java
index 71ceb25ce0cc856990095538f1881e874efbdb7c..18713d4585f12967fd7c04a13b7804454c3c4183 100644
--- a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudTLCJobFactory.java
+++ b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudTLCJobFactory.java
@@ -37,6 +37,7 @@ public class CloudTLCJobFactory implements TLCJobFactory {
private static final String AZURECOMPUTE = "Azure";
private static final String AWS_EC2 = "aws-ec2";
+ private static final String AWS_EC2_VM_PROPERTIES = "aws-ec2-props";
@Override
public Job getTLCJob(String aName, File aModelFolder, int numberOfWorkers, final Properties props, String tlcparams) {
@@ -45,6 +46,9 @@ public class CloudTLCJobFactory implements TLCJobFactory {
if (AWS_EC2.equals(aName)) {
return new CloudDistributedTLCJob(aName, aModelFolder, numberOfWorkers, props,
new EC2CloudTLCInstanceParameters(tlcparams, numberOfWorkers));
+ } else if (AWS_EC2_VM_PROPERTIES.equals(aName)) {
+ return new CloudDistributedTLCJob(aName, aModelFolder, numberOfWorkers, props,
+ new EC2PropertyCloudTLCInstanceParameters(tlcparams, numberOfWorkers));
} else if (AZURECOMPUTE.equals(aName)) {
return new CloudDistributedTLCJob(aName, aModelFolder, numberOfWorkers, props,
new AzureCloudTLCInstanceParameters(tlcparams, numberOfWorkers));
diff --git a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/EC2CloudTLCInstanceParameters.java b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/EC2CloudTLCInstanceParameters.java
index b1ec2c097f8f0fb446cc2eb39db5c0ab492e42f3..bec45e175813361387a36414fac961808e3b2623 100644
--- a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/EC2CloudTLCInstanceParameters.java
+++ b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/EC2CloudTLCInstanceParameters.java
@@ -55,7 +55,7 @@ public class EC2CloudTLCInstanceParameters extends CloudTLCInstanceParameters {
// http://cloud-images.ubuntu.com/locator/ec2/
// See http://aws.amazon.com/amazon-linux-ami/instance-type-matrix/
// for paravirtual vs. hvm
- return getRegion() + "/ami-84a048fe"; // "xenial,amd64,hvm:instance-store"
+ return getRegion() + "/ami-2931b953"; // "us-east-1,xenial,amd64,hvm:instance-store"
}
@Override
diff --git a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/EC2PropertyCloudTLCInstanceParameters.java b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/EC2PropertyCloudTLCInstanceParameters.java
new file mode 100644
index 0000000000000000000000000000000000000000..ab82f89ca01e666defb162293c50cf28ed8e87a3
--- /dev/null
+++ b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/EC2PropertyCloudTLCInstanceParameters.java
@@ -0,0 +1,67 @@
+/*******************************************************************************
+ * Copyright (c) 2017 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.jcloud;
+
+public class EC2PropertyCloudTLCInstanceParameters extends EC2CloudTLCInstanceParameters {
+
+ public EC2PropertyCloudTLCInstanceParameters(final String tlcParams, int numberOfWorkers) {
+ super(tlcParams.trim(), numberOfWorkers);
+ }
+
+ @Override
+ public String getImageId() {
+ final String imageId = System.getProperty("aws-ec2.image");
+ if (imageId == null) {
+ return super.getImageId();
+ }
+ return getRegion() + "/" + imageId;
+ }
+
+ @Override
+ public String getRegion() {
+ return System.getProperty("aws-ec2.region", super.getRegion());
+ }
+
+ @Override
+ public String getHardwareId() {
+ return System.getProperty("aws-ec2.instanceType", super.getHardwareId());
+ }
+
+ @Override
+ public String getOSFilesystemTuning() {
+ return System.getProperty("aws-ec2.tuning", super.getOSFilesystemTuning());
+ }
+
+ @Override
+ public String getJavaVMArgs() {
+ return System.getProperty("aws-ec2.vmargs", super.getJavaVMArgs());
+ }
+
+ @Override
+ public String getTLCParameters() {
+ return System.getProperty("aws-ec2.tlcparams", super.getTLCParameters());
+ }
+}
diff --git a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/PayloadHelper.java b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/PayloadHelper.java
index 19374157798a689081f63ebaccdb6da6ffeded4d..ad9f09ba58260e1b24f9629eabbe0d15e835e16e 100644
--- a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/PayloadHelper.java
+++ b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/PayloadHelper.java
@@ -46,7 +46,11 @@ import java.util.HashMap;
import java.util.Map;
import java.util.Properties;
import java.util.jar.Attributes;
+import java.util.jar.JarFile;
import java.util.jar.Manifest;
+import java.util.jar.Pack200;
+import java.util.jar.Pack200.Packer;
+import java.util.zip.GZIPOutputStream;
import org.apache.commons.io.IOUtils;
import org.eclipse.core.runtime.IProgressMonitor;
@@ -133,22 +137,53 @@ public class PayloadHelper {
final Path to = fs.getPath("/model/generated.properties");
Files.copy(f.toPath(), to, StandardCopyOption.REPLACE_EXISTING);
} catch (final IOException e1) {
- throw new RuntimeException("No model directory found to deploy");
+ throw new RuntimeException("No model directory found to deploy", e1);
}
/*
- * Convert the customized tla2tools.jar into a jClouds payload object. This
- * is the format it will be transfered on the wire. This is handled by
- * jClouds though.
+ * Compress archive with pack200 to achieve a much higher compression rate. We
+ * are going to send the file on the wire after all:
+ *
+ * effort: take more time choosing codings for better compression segment: use
+ * largest-possible archive segments (>10% better compression) mod time: smear
+ * modification times to a single value deflate: ignore all JAR deflation hints
+ * in original archive
+ */
+ final Packer packer = Pack200.newPacker();
+ final Map<String, String> p = packer.properties();
+ p.put(Packer.EFFORT, "9");
+ p.put(Packer.SEGMENT_LIMIT, "-1");
+ p.put(Packer.MODIFICATION_TIME, Packer.LATEST);
+ p.put(Packer.DEFLATE_HINT, Packer.FALSE);
+
+ // Do not reorder which changes package names. Pkg name changes e.g. break
+ // SimpleFilenameToStream.
+ p.put(Packer.KEEP_FILE_ORDER, Packer.TRUE);
+
+ // Throw an error if any of the above attributes is unrecognized.
+ p.put(Packer.UNKNOWN_ATTRIBUTE, Packer.ERROR);
+
+ final File packTempFile = File.createTempFile("tla2tools", ".pack.gz");
+ try (final JarFile jarFile = new JarFile(tempFile);
+ final GZIPOutputStream fos = new GZIPOutputStream(new FileOutputStream(packTempFile));) {
+ packer.pack(jarFile, fos);
+ } catch (IOException ioe) {
+ throw new RuntimeException("Failed to pack200 the tla2tools.jar file", ioe);
+ }
+
+ /*
+ * Convert the customized tla2tools.jar into a jClouds payload object. This is
+ * the format it will be transfered on the wire. This is handled by jClouds
+ * though.
*/
Payload jarPayLoad = null;
try {
- final InputStream openStream = new FileInputStream(tempFile);
+ final InputStream openStream = new FileInputStream(packTempFile);
jarPayLoad = Payloads.newInputStreamPayload(openStream);
// manually set length of content to prevent a NPE bug
jarPayLoad.getContentMetadata().setContentLength(Long.valueOf(openStream.available()));
} catch (final IOException e1) {
- throw new RuntimeException("No tlatools.jar to deploy");
+ throw new RuntimeException("No tlatools.jar to deploy", e1);
} finally {
monitor.worked(5);
}
diff --git a/org.lamport.tla.toolbox.p2repository/category.xml b/org.lamport.tla.toolbox.p2repository/category.xml
index 404145aecb8709a308317116490902784c984504..20ccac2970cde71c507b0d47428ba6591c2fc7c1 100644
--- a/org.lamport.tla.toolbox.p2repository/category.xml
+++ b/org.lamport.tla.toolbox.p2repository/category.xml
@@ -1,5 +1,8 @@
<?xml version="1.0" encoding="UTF-8"?>
<site>
+ <feature url="features/org.lamport.tla.toolbox.feature.uitest_1.0.0.qualifier.jar" id="org.lamport.tla.toolbox.feature.uitest" version="1.0.0.qualifier">
+ <category name="tychotest.category"/>
+ </feature>
<feature url="features/org.lamport.tla.toolbox.feature.standalone_1.0.0.qualifier.jar" id="org.lamport.tla.toolbox.feature.standalone" version="1.0.0.qualifier">
<category name="tychodemo.category"/>
</feature>
@@ -11,4 +14,9 @@
TLA+ Toolbox Category
</description>
</category-def>
+ <category-def name="tychotest.category" label="Test Category - please ignore">
+ <description>
+ Please ignore this category which is only relevant for Toolbox testing!
+ </description>
+ </category-def>
</site>
diff --git a/org.lamport.tla.toolbox.product.product/TLAToolbox.target b/org.lamport.tla.toolbox.product.product/TLAToolbox.target
index 52b6e3ce81b05d03170815220ea0822a85395c09..a1554e902856f6bb685dc157fe26396e87c9afec 100644
--- a/org.lamport.tla.toolbox.product.product/TLAToolbox.target
+++ b/org.lamport.tla.toolbox.product.product/TLAToolbox.target
@@ -45,7 +45,7 @@
<unit id="org.eclipse.equinox.sdk.feature.group" version="3.13.0.v20170531-1133"/>
<unit id="org.eclipse.core.runtime.feature.feature.group" version="1.2.0.v20170518-1049"/>
<unit id="org.eclipse.sdk.ide" version="4.7.0.I20170612-0950"/>
-<repository location="http://download.eclipse.org/eclipse/updates/4.7/"/>
+<repository location="http://download.eclipse.org/eclipse/updates/4.7/" id="eclipse"/>
</location>
<location includeAllPlatforms="false" includeConfigurePhase="false" includeMode="planner" includeSource="true" type="InstallableUnit">
<unit id="de.vonloesch.pdf4eclipse.feature.feature.group" version="0.0.0"/>
diff --git a/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product b/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product
index f608beb1b6ac6648921b7bbf425006ac7e304c5b..edf28a51befd047507bfcbac901059a307cb111c 100644
--- a/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product
+++ b/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product
@@ -1,16 +1,16 @@
<?xml version="1.0" encoding="UTF-8"?>
<?pde version="3.5"?>
-<product name="TLA+ Toolbox" uid="org.lamport.tla.toolbox.product.product" id="org.lamport.tla.toolbox.product.standalone.product" application="org.lamport.tla.toolbox.application" version="1.5.4" 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.5.5.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.5.4 of 06 October 2017 and includes:
+This is Version 1.5.5 of 05 January 2018 and includes:
- SANY Version 2.1 of 23 July 2017
- - TLC Version 2.10 of 28 September 2017
+ - TLC Version 2.11 of 05 January 2018
- PlusCal Version 1.8 of 07 December 2015
- TLATeX Version 1.0 of 20 September 2017
@@ -80,12 +80,16 @@ openFile
<plugin id="org.eclipse.equinox.http.registry" autoStart="true" startLevel="3" />
<plugin id="org.lamport.tla.toolbox.jclouds" autoStart="true" startLevel="4" />
<plugin id="sts" autoStart="true" startLevel="4" />
- <property name="eclipse.buildId" value="1.5.4" />
+ <property name="eclipse.buildId" value="1.5.5" />
</configurations>
<repositories>
<repository location="http://lamport.org/tlatoolbox/toolboxUpdate/" enabled="true" />
<repository location="http://lamport.org/tlatoolbox/ci/toolboxUpdate/" enabled="false" />
+ <repository location="http://lamport.org/tlatoolbox/toolboxUpdate/" enabled="true" />
+ <repository location="http://lamport.org/tlatoolbox/ci/toolboxUpdate/" enabled="false" />
+ <repository location="http://lamport.org/tlatoolbox/toolboxUpdate/" enabled="true" />
+ <repository location="http://lamport.org/tlatoolbox/ci/toolboxUpdate/" enabled="false" />
</repositories>
<preferencesInfo>
diff --git a/org.lamport.tla.toolbox.product.product/pom.xml b/org.lamport.tla.toolbox.product.product/pom.xml
index 309be7b6fdc959493bc5c1bb86ed6229536b0418..6e6620fbc72313c159012f715944da293dd50ec3 100644
--- a/org.lamport.tla.toolbox.product.product/pom.xml
+++ b/org.lamport.tla.toolbox.product.product/pom.xml
@@ -19,7 +19,7 @@
<!-- Align product.version with the version in
org.lamport.tla.toolbox.product.product.product
product.version. -->
- <product.version>1.5.4</product.version>
+ <product.version>1.5.5</product.version>
<!-- Format build timestamp to adhere to the Debian package guidelines -->
<maven.build.timestamp.format>yyyyMMdd-HHmm</maven.build.timestamp.format>
<product.build>${maven.build.timestamp}</product.build>
diff --git a/org.lamport.tla.toolbox.product.standalone/plugin.xml b/org.lamport.tla.toolbox.product.standalone/plugin.xml
index 239b8d7cc281d7dea969e76b33ae06b6ea312815..c923097f13130ae81093a68d26fffad6659448e7 100644
--- a/org.lamport.tla.toolbox.product.standalone/plugin.xml
+++ b/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.5.4 of 06 October 2017 and includes:
 - SANY Version 2.1 of 23 July 2017
 - TLC Version 2.10 of 28 September 2017
 - PlusCal Version 1.8 of 07 December 2015
 - 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 .">
+ value="TLA+ Toolbox provides a user interface for TLA+ Tools. 

This is Version 1.5.5 of 05 January 2018 and includes:
 - SANY Version 2.1 of 23 July 2017
 - TLC Version 2.11 of 05 January 2018
 - PlusCal Version 1.8 of 07 December 2015
 - 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 .">
</property>
<property
name="aboutImage"
diff --git a/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ApplicationWorkbenchWindowAdvisor.java b/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ApplicationWorkbenchWindowAdvisor.java
index c3bfe9203483632ad607fdb4848a4f789a5649ca..22cc7378d8001a37a8d0ce5e602a904e4bec8bb1 100644
--- a/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ApplicationWorkbenchWindowAdvisor.java
+++ b/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ApplicationWorkbenchWindowAdvisor.java
@@ -67,7 +67,6 @@ public class ApplicationWorkbenchWindowAdvisor extends WorkbenchWindowAdvisor
filters.add("de.vonloesch.pdf4Eclipse");
// Filter out GraphViz
- //TODO Move its configuration (path to dot) into Toolbox specific preference page.
filters.add("com.abstratt.graphviz.ui");
// Clean the preferences
diff --git a/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java b/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java
index a1e55c43b35dfd33664e0b2b4a26e9880fd71bf5..1f53e15fd813e0d9f4e409992bae15279ea2e5a8 100644
--- a/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java
+++ b/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java
@@ -175,7 +175,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.5.4 of 06 October 2017");
+ lblVersion.setText("Version 1.5.5 of 05 January 2018");
lblVersion.setBackground(backgroundColor);
}
diff --git a/org.lamport.tla.toolbox.tool.tla2tex.uitest/pom.xml b/org.lamport.tla.toolbox.tool.tla2tex.uitest/pom.xml
index 4fe11a57f0d3479c4cbd68b9409487b13e71fba0..fcab171009279160ba1cbd4b6a8a93a6c58564aa 100644
--- a/org.lamport.tla.toolbox.tool.tla2tex.uitest/pom.xml
+++ b/org.lamport.tla.toolbox.tool.tla2tex.uitest/pom.xml
@@ -101,7 +101,7 @@
<dependency>
<type>p2-installable-unit</type>
<artifactId>org.eclipse.equinox.weaving.hook</artifactId>
- <version>1.1.100.v20140821-1915</version>
+ <version>1.2.0.v20160929-1449</version>
</dependency>
<dependency>
<type>p2-installable-unit</type>
@@ -115,7 +115,7 @@
<frameworkExtension>
<groupId>p2.osgi.bundle</groupId>
<artifactId>org.eclipse.equinox.weaving.hook</artifactId>
- <version>1.1.100.v20140821-1915</version>
+ <version>1.2.0.v20160929-1449</version>
</frameworkExtension>
</frameworkExtensions>
diff --git a/org.lamport.tla.toolbox.tool.tla2tex.uitest/src/org/lamport/tla/toolbox/tool/tla2tex/PDFHandlerThreadingTest.java b/org.lamport.tla.toolbox.tool.tla2tex.uitest/src/org/lamport/tla/toolbox/tool/tla2tex/PDFHandlerThreadingTest.java
index c691c080fc1fa938ed9bb42b59b53bc382537f7e..c140079a03b8fb0a7177a618c3ca42db5809be6a 100644
--- a/org.lamport.tla.toolbox.tool.tla2tex.uitest/src/org/lamport/tla/toolbox/tool/tla2tex/PDFHandlerThreadingTest.java
+++ b/org.lamport.tla.toolbox.tool.tla2tex.uitest/src/org/lamport/tla/toolbox/tool/tla2tex/PDFHandlerThreadingTest.java
@@ -2,8 +2,6 @@ package org.lamport.tla.toolbox.tool.tla2tex;
import java.io.File;
-import junit.framework.Assert;
-
import org.eclipse.swtbot.eclipse.finder.SWTWorkbenchBot;
import org.eclipse.swtbot.eclipse.finder.widgets.SWTBotEditor;
import org.eclipse.swtbot.swt.finder.junit.SWTBotJunit4ClassRunner;
@@ -16,15 +14,18 @@ import org.lamport.tla.toolbox.test.RCPTestSetupHelper;
import org.lamport.tla.toolbox.test.threading.MonitorAdaptor;
import org.lamport.tla.toolbox.ui.handler.OpenSpecHandler;
+import org.junit.Assert;
+
@RunWith(SWTBotJunit4ClassRunner.class)
public class PDFHandlerThreadingTest {
private static SWTWorkbenchBot bot;
- private static final String specA = System
- .getProperty("org.lamport.tla.toolbox.tool.tlc.ui.test.PathToSpecA");
- private static final String specB = System
- .getProperty("org.lamport.tla.toolbox.tool.tlc.ui.test.PathToSpecB");
+ private static final String specA = System.getProperty("org.lamport.tla.toolbox.tool.tlc.ui.test.PathToSpecA",
+ RCPTestSetupHelper.getAbsolutePath("org.lamport.tla.toolbox.uitest",
+ "farsite/DistributedSystemModule.tla"));
+ private static final String specB = System.getProperty("org.lamport.tla.toolbox.tool.tlc.ui.test.PathToSpecB",
+ RCPTestSetupHelper.getAbsolutePath("org.lamport.tla.toolbox.uitest", "DieHard/DieHard.tla"));
@BeforeClass
public static void beforeClass() throws Exception {
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui.uitest/pom.xml b/org.lamport.tla.toolbox.tool.tlc.ui.uitest/pom.xml
index a6c08a6606f7fefaac7119ffffca318e2e904fc3..8e015c4f7c789ecd09d06ab52efbf86f4966f0c0 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui.uitest/pom.xml
+++ b/org.lamport.tla.toolbox.tool.tlc.ui.uitest/pom.xml
@@ -102,7 +102,7 @@
<dependency>
<type>p2-installable-unit</type>
<artifactId>org.eclipse.equinox.weaving.hook</artifactId>
- <version>1.1.100.v20140821-1915</version>
+ <version>1.2.0.v20160929-1449</version>
</dependency>
<dependency>
<type>p2-installable-unit</type>
@@ -116,7 +116,7 @@
<frameworkExtension>
<groupId>p2.osgi.bundle</groupId>
<artifactId>org.eclipse.equinox.weaving.hook</artifactId>
- <version>1.1.100.v20140821-1915</version>
+ <version>1.2.0.v20160929-1449</version>
</frameworkExtension>
</frameworkExtensions>
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui.uitest/src/org/lamport/tla/toolbox/SmokeTests.java b/org.lamport.tla.toolbox.tool.tlc.ui.uitest/src/org/lamport/tla/toolbox/SmokeTests.java
new file mode 100644
index 0000000000000000000000000000000000000000..585f5609d216328e854e7f160845d7de92616804
--- /dev/null
+++ b/org.lamport.tla.toolbox.tool.tlc.ui.uitest/src/org/lamport/tla/toolbox/SmokeTests.java
@@ -0,0 +1,17 @@
+package org.lamport.tla.toolbox;
+
+import org.junit.runner.RunWith;
+import org.junit.runners.Suite;
+import org.junit.runners.Suite.SuiteClasses;
+import org.lamport.tla.toolbox.tool.tlc.ui.test.ModelCheckerTest;
+import org.lamport.tla.toolbox.ui.handler.CloneModelTest;
+import org.lamport.tla.toolbox.ui.handler.RenameSpecHandlerTest;
+
+@RunWith(Suite.class)
+@SuiteClasses({
+ ModelCheckerTest.class,
+ CloneModelTest.class,
+ RenameSpecHandlerTest.class
+})
+
+public class SmokeTests {}
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui.uitest/src/org/lamport/tla/toolbox/tool/tlc/ui/test/AbstractTest.java b/org.lamport.tla.toolbox.tool.tlc.ui.uitest/src/org/lamport/tla/toolbox/tool/tlc/ui/test/AbstractTest.java
index 2df881c61892784ed2eb464173f14c4247d5e3f1..7fa147f8c268f7369777050b535c73ffa77f130a 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui.uitest/src/org/lamport/tla/toolbox/tool/tlc/ui/test/AbstractTest.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui.uitest/src/org/lamport/tla/toolbox/tool/tlc/ui/test/AbstractTest.java
@@ -32,9 +32,10 @@ public abstract class AbstractTest {
/**
* Full qualified spec name
*/
- protected static final String specA = System
- .getProperty("org.lamport.tla.toolbox.tool.tlc.ui.test.PathToSpecA");
-
+ protected static String specA = System.getProperty("org.lamport.tla.toolbox.tool.tlc.ui.test.PathToSpecA",
+ RCPTestSetupHelper.getAbsolutePath("org.lamport.tla.toolbox.uitest",
+ "DieHard/DieHard.tla"));
+
/**
* Pre flight checks (run once for each test _class_)
*/
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui.uitest/src/org/lamport/tla/toolbox/tool/tlc/ui/test/threading/HandlerThreadingTest.java b/org.lamport.tla.toolbox.tool.tlc.ui.uitest/src/org/lamport/tla/toolbox/tool/tlc/ui/test/threading/HandlerThreadingTest.java
index 67bf0378d90cb783487f1402e770c6915161f19d..82b8cb77ae04ca27c4622be4ab0c3055f3b612ea 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui.uitest/src/org/lamport/tla/toolbox/tool/tlc/ui/test/threading/HandlerThreadingTest.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui.uitest/src/org/lamport/tla/toolbox/tool/tlc/ui/test/threading/HandlerThreadingTest.java
@@ -15,6 +15,7 @@ import org.junit.Before;
import org.junit.BeforeClass;
import org.junit.Test;
import org.junit.runner.RunWith;
+import org.lamport.tla.toolbox.test.RCPTestSetupHelper;
import org.lamport.tla.toolbox.test.threading.MonitorAdaptor;
import org.lamport.tla.toolbox.tool.tlc.ui.test.AbstractTest;
@@ -28,7 +29,8 @@ import org.lamport.tla.toolbox.tool.tlc.ui.test.AbstractTest;
@RunWith(SWTBotJunit4ClassRunner.class)
public class HandlerThreadingTest extends AbstractTest {
- private static final String specB = System.getProperty("org.lamport.tla.toolbox.tool.tlc.ui.test.PathToSpecB");
+ private static final String specB = System.getProperty("org.lamport.tla.toolbox.tool.tlc.ui.test.PathToSpecB",
+ RCPTestSetupHelper.getAbsolutePath("org.lamport.tla.toolbox.uitest", "farsite/DistributedSystemModule.tla"));
@BeforeClass
public static void beforeClass() {
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/.classpath b/org.lamport.tla.toolbox.tool.tlc.ui/.classpath
index bbd8b304fcf5fc337804d99b0c1f49e77d817c48..1f88b32b86a4988f8a32bf10abcd8d0c15e1182f 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/.classpath
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/.classpath
@@ -1,6 +1,6 @@
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
- <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.7"/>
+ <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="src" path="src"/>
<classpathentry kind="output" path="class"/>
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/.settings/org.eclipse.jdt.core.prefs b/org.lamport.tla.toolbox.tool.tlc.ui/.settings/org.eclipse.jdt.core.prefs
index b1513f02a112a1e4efcea3b1013570093e4c79e1..aa8d6f1cb02d3ed8670a9eb027bf36664fc9802a 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/.settings/org.eclipse.jdt.core.prefs
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/.settings/org.eclipse.jdt.core.prefs
@@ -1,8 +1,8 @@
eclipse.preferences.version=1
org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
-org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.7
+org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8
org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve
-org.eclipse.jdt.core.compiler.compliance=1.7
+org.eclipse.jdt.core.compiler.compliance=1.8
org.eclipse.jdt.core.compiler.debug.lineNumber=generate
org.eclipse.jdt.core.compiler.debug.localVariable=generate
org.eclipse.jdt.core.compiler.debug.sourceFile=generate
@@ -70,4 +70,4 @@ org.eclipse.jdt.core.compiler.problem.unusedParameterWhenOverridingConcrete=disa
org.eclipse.jdt.core.compiler.problem.unusedPrivateMember=warning
org.eclipse.jdt.core.compiler.problem.unusedWarningToken=warning
org.eclipse.jdt.core.compiler.problem.varargsArgumentNeedCast=warning
-org.eclipse.jdt.core.compiler.source=1.7
+org.eclipse.jdt.core.compiler.source=1.8
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/META-INF/MANIFEST.MF b/org.lamport.tla.toolbox.tool.tlc.ui/META-INF/MANIFEST.MF
index f30093583fc2492dcd09da2d03e6f1d1db25fd75..e59dad9f58775066800b7186ce1284666353fc3b 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/META-INF/MANIFEST.MF
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/META-INF/MANIFEST.MF
@@ -20,7 +20,7 @@ Require-Bundle: org.eclipse.core.runtime,
javax.mail;bundle-version="1.4.0",
com.abstratt.graphviz;bundle-version="2.1.201501",
com.abstratt.graphviz.ui;bundle-version="2.1.201501"
-Bundle-RequiredExecutionEnvironment: JavaSE-1.7
+Bundle-RequiredExecutionEnvironment: JavaSE-1.8
Bundle-ActivationPolicy: lazy
Import-Package: org.lamport.tla.toolbox.editor.basic
Export-Package: org.lamport.tla.toolbox.tool.tlc.output;x-friends:="org.lamport.tla.toolbox.tool.tlc.ui.test",
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/icons/full/lockedstate.gif b/org.lamport.tla.toolbox.tool.tlc.ui/icons/full/lockedstate.gif
deleted file mode 100644
index e6379511e95ba6c8e0c71b45d8336755d97b3a7e..0000000000000000000000000000000000000000
Binary files a/org.lamport.tla.toolbox.tool.tlc.ui/icons/full/lockedstate.gif and /dev/null differ
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/icons/full/owned_monitor_obj.gif b/org.lamport.tla.toolbox.tool.tlc.ui/icons/full/owned_monitor_obj.gif
deleted file mode 100644
index 57fb95edc3fe1e6cafc9f7bdc17e6bf886057030..0000000000000000000000000000000000000000
Binary files a/org.lamport.tla.toolbox.tool.tlc.ui/icons/full/owned_monitor_obj.gif and /dev/null differ
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/plugin.xml b/org.lamport.tla.toolbox.tool.tlc.ui/plugin.xml
index d1d1faaf92d1e32ffa5caa9a9e58f67852df7064..fcd694f4dc868de975dea1387897871856265d52 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/plugin.xml
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/plugin.xml
@@ -445,6 +445,15 @@
name="TLC Models"
priority="normal"
providesSaveables="false">
+ <commonSorter
+ id="toolbox.content.ModelSnapshotSorter"
+ class="org.lamport.tla.toolbox.tool.tlc.ui.modelexplorer.ModelSnapshotSorter">
+ <parentExpression>
+ <or>
+ <instanceof value="org.lamport.tla.toolbox.tool.tlc.model.Model" />
+ </or>
+ </parentExpression>
+ </commonSorter>
<possibleChildren>
<or>
<instanceof
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/handlers/DeleteModelHandler.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/handlers/DeleteModelHandler.java
index 0380a2a5659ab9534b74cbed489d766691d4fdb2..96a9747462a5959a0c03463d9b13fa9153c2a63f 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/handlers/DeleteModelHandler.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/handlers/DeleteModelHandler.java
@@ -1,6 +1,12 @@
package org.lamport.tla.toolbox.tool.tlc.handlers;
+import java.text.SimpleDateFormat;
+import java.util.Collection;
import java.util.Iterator;
+import java.util.List;
+import java.util.Set;
+import java.util.function.Predicate;
+import java.util.stream.Collectors;
import org.eclipse.core.commands.AbstractHandler;
import org.eclipse.core.commands.ExecutionEvent;
@@ -24,6 +30,7 @@ import org.lamport.tla.toolbox.util.UIHelper;
public class DeleteModelHandler extends AbstractHandler implements IHandler
{
+ private static final SimpleDateFormat sdf = new SimpleDateFormat("MMM dd,yyyy HH:mm:ss");
/**
* @see org.eclipse.core.commands.IHandler#execute(org.eclipse.core.commands.ExecutionEvent)
@@ -40,11 +47,9 @@ public class DeleteModelHandler extends AbstractHandler implements IHandler
// 1.) get confirmation from the user to delete all files/models
// if user cancels, just return
- int amountOfModels = iss.size();
boolean userConfirmedDeletion = MessageDialog.openQuestion(
UIHelper.getShell(), "Confirm Delete",
- "Are you sure you want to delete " + amountOfModels
- + " model(s)?");
+ getLabel(iss));
if(!userConfirmedDeletion) {
return null;
}
@@ -67,16 +72,6 @@ public class DeleteModelHandler extends AbstractHandler implements IHandler
+ ", because it is being model checked.");
return null;
}
- if(model.isLocked()) {
- MessageDialog
- .openError(
- UIHelper.getShell(),
- "Could not delete a model",
- "Could not delete the model "
- + model.getName()
- + ", because it is currently locked.");
- return null;
- }
}
// 3.) at this point, we are safe to delete all models (user has
@@ -130,4 +125,64 @@ public class DeleteModelHandler extends AbstractHandler implements IHandler
}
return null;
}
+
+ private String getLabel(final IStructuredSelection iss) {
+ if (iss.size() > 1) {
+ // The selected models.
+ @SuppressWarnings("unchecked")
+ final List<Model> list = (List<Model>) iss.toList();
+ final Predicate<Model> p = Model::isSnapshot;
+ final Set<Model> models = list.stream().filter(p.negate()).collect(Collectors.toSet());
+
+ if (models.isEmpty()) {
+ // Only Snapshots are selected.
+ return String.format("Are you sure you want to delete the %s selected snapshots?", iss.size());
+ } else {
+ // The set of snapshots (either explicitly selected or implicit via parent
+ // model) to be deleted.
+ final Set<Model> allSnapshots = list.stream().map(Model::getSnapshots).flatMap(c -> c.stream())
+ .collect(Collectors.toSet());
+
+ if (models.size() > 1 && allSnapshots.isEmpty()) {
+ return String.format("Are you sure you want to delete the %s selected models?", iss.size());
+ } else {
+ // The set of selected snapshots to be deleted.
+ final Set<Model> selectedSnapshots = list.stream().filter(Model::isSnapshot)
+ .collect(Collectors.toSet());
+
+ if (models.size() == 1) {
+ // 1 Model with its snapshots and selected snapshots.
+ allSnapshots.addAll(selectedSnapshots);
+ return String.format("Are you sure you want to delete the select model '%s' and %s snapshot%s?",
+ models.iterator().next().getName(), allSnapshots.size(),
+ isPlural(allSnapshots));
+ } else {
+ // N models with M snapshots
+ allSnapshots.addAll(selectedSnapshots);
+ return String.format("Are you sure you want to delete %s models and %s snapshot%s?",
+ models.size(), allSnapshots.size(), isPlural(allSnapshots));
+ }
+ }
+ }
+ }
+ return getLabel((Model) iss.getFirstElement());
+ }
+
+ private String getLabel(Model model) {
+ final Model snapshotFor = model.getSnapshotFor();
+ if (snapshotFor != model) {
+ return String.format("Are you sure you want to delete the snapshot of %s of model '%s'?",
+ sdf.format(model.getSnapshotTimeStamp()), snapshotFor.getName());
+ }
+ final Collection<Model> snapshots = model.getSnapshots();
+ if (!snapshots.isEmpty()) {
+ return String.format("Are you sure you want to delete the model '%s' and its %s snapshot%s?", model.getName(),
+ snapshots.size(), isPlural(snapshots));
+ }
+ return String.format("Are you sure you want to delete the model '%s'?", model.getName());
+ }
+
+ private static String isPlural(final Collection<?> col) {
+ return col.size() > 1 ? "s" : "";
+ }
}
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/handlers/RenameModelHandlerDelegate.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/handlers/RenameModelHandlerDelegate.java
index aac3c051ace7ad503f15fd62fb3be6015795e622..36089f89aefd00954cebb44e06c9c1e603c749d3 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/handlers/RenameModelHandlerDelegate.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/handlers/RenameModelHandlerDelegate.java
@@ -47,11 +47,11 @@ public class RenameModelHandlerDelegate extends AbstractHandler implements IHand
// model file
final Model model = (Model) ((IStructuredSelection) selection).getFirstElement();
- // a) fail if model is in use or locked
- if (model.isRunning() || model.isLocked()) {
+ // a) fail if model is in use
+ if (model.isRunning()) {
MessageDialog.openError(UIHelper.getShellProvider().getShell(), "Could not rename models",
"Could not rename the model " + model.getName()
- + ", because it is being model checked or is locked.");
+ + ", because it is being model checked.");
return null;
}
if (model.isSnapshot()) {
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/handlers/StartLaunchHandler.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/handlers/StartLaunchHandler.java
index a1edfe06e31370df42fc3e3e66ff4ee7bf1d7a98..86f364186270df2ca8f3a22132add8259c50aed0 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/handlers/StartLaunchHandler.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/handlers/StartLaunchHandler.java
@@ -98,19 +98,7 @@ public class StartLaunchHandler extends AbstractHandler {
modelEditor.doSaveWithoutValidating(new NullProgressMonitor());
}
- // 2) model might be locked
- if (model.isLocked()) {
- boolean unlock = MessageDialog
- .openQuestion(shell, "Unlock model?",
- "The current model is locked, but has to be unlocked prior to launching. Should the model be unlocked?");
- if (unlock) {
- model.setLocked(false);
- } else {
- return null;
- }
- }
-
- // 3) model might be stale
+ // 2) model might be stale
if (model.isStale()) {
boolean unlock = MessageDialog
.openQuestion(shell, "Repair model?",
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/ModelEditor.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/ModelEditor.java
index e5557023b3a2f9e7397055a49aa070886c3d240d..14b3f28c275e5b84ad2e97e90f57220030d87494 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/ModelEditor.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/ModelEditor.java
@@ -152,11 +152,11 @@ public class ModelEditor extends FormEditor
public void run()
{
- // Re-validate the pages, iff the model is not running
- // and is not locked. Also check if the model is nulled by now which
+ // Re-validate the pages, iff the model is not running.
+ // Also check if the model is nulled by now which
// happens if the ModelEditor disposed before a scheduled run gets
// executed.
- if (model != null && !model.isRunning() && !model.isLocked())
+ if (model != null && !model.isRunning())
{
/*
* Note that all pages are not necessarily
@@ -819,16 +819,6 @@ public class ModelEditor extends FormEditor
}
} else {
// launching the config
- if (mode.equals(TLCModelLaunchDelegate.MODE_MODELCHECK)) {
- // if model checking, the length of time that
- // tlc
- // should run before the model is automatically
- // locked
- // must be saved from the preferences
- int autoLockTime = TLCUIActivator.getDefault().getPreferenceStore()
- .getInt(ITLCPreferenceConstants.I_TLC_AUTO_LOCK_MODEL_TIME);
- model.setAutoLockTime(autoLockTime);
- }
model.launch(mode, new SubProgressMonitor(monitor, 1), true);
/*
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/BasicFormPage.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/BasicFormPage.java
index 5540d9432e90f8896a476a4eb57907d1df2edf61..2a170482dac5be31ecfd9e771476fba5c5ca093b 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/BasicFormPage.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/BasicFormPage.java
@@ -6,12 +6,10 @@ import java.util.List;
import org.eclipse.core.runtime.CoreException;
import org.eclipse.core.runtime.ListenerList;
-import org.eclipse.core.runtime.NullProgressMonitor;
import org.eclipse.jface.action.Action;
import org.eclipse.jface.action.IToolBarManager;
import org.eclipse.jface.action.ToolBarManager;
import org.eclipse.jface.dialogs.IMessageProvider;
-import org.eclipse.jface.dialogs.MessageDialog;
import org.eclipse.jface.resource.ImageDescriptor;
import org.eclipse.swt.SWT;
import org.eclipse.swt.events.FocusEvent;
@@ -47,6 +45,7 @@ import org.lamport.tla.toolbox.tool.tlc.ui.contribution.DynamicContributionItem;
import org.lamport.tla.toolbox.tool.tlc.ui.editor.DataBindingManager;
import org.lamport.tla.toolbox.tool.tlc.ui.editor.ISectionConstants;
import org.lamport.tla.toolbox.tool.tlc.ui.editor.ModelEditor;
+import org.lamport.tla.toolbox.tool.tlc.ui.util.DirtyMarkingListener;
import org.lamport.tla.toolbox.tool.tlc.ui.util.FormHelper;
import org.lamport.tla.toolbox.tool.tlc.ui.util.IgnoringListener;
import org.lamport.tla.toolbox.tool.tlc.ui.util.SemanticHelper;
@@ -89,13 +88,12 @@ public abstract class BasicFormPage extends FormPage implements IModelConfigurat
{
public static final String CRASHED_TITLE = " ( model checking has crashed )";
public static final String RUNNING_TITLE = " ( model checking is in progress )";
- public static final String LOCKED_TITLE = " ( model is locked )";
private static final String TLC_ERROR_STRING = "TLC Error";
/**
* a list of dirty part listeners, which marks parts as dirty on input and cause the re-validation of the input
*/
- protected ListenerList dirtyPartListeners = new ListenerList();
+ protected ListenerList<DirtyMarkingListener> dirtyPartListeners = new ListenerList<DirtyMarkingListener>();
/**
* the initialization status. Becomes true, after the {@link BasicFormPage#pageInitializationComplete()} method is executed
*/
@@ -257,10 +255,6 @@ public abstract class BasicFormPage extends FormPage implements IModelConfigurat
toolbarManager.add(new DynamicContributionItem(new GenerateAction()));
// stop button
toolbarManager.add(new DynamicContributionItem(new StopAction()));
- // lock button
- toolbarManager.add(new DynamicContributionItem(new LockModelAction()));
- // unlock button
- toolbarManager.add(new DynamicContributionItem(new UnlockModelAction()));
// refresh the tool-bar
toolbarManager.update(true);
@@ -280,10 +274,6 @@ public abstract class BasicFormPage extends FormPage implements IModelConfigurat
headClientTBM.add(new DynamicContributionItem(new GenerateAction()));
// stop button
headClientTBM.add(new DynamicContributionItem(new StopAction()));
- // lock button
- headClientTBM.add(new DynamicContributionItem(new LockModelAction()));
- // unlock button
- headClientTBM.add(new DynamicContributionItem(new UnlockModelAction()));
// refresh the head client toolbar
headClientTBM.update(true);
@@ -556,8 +546,7 @@ public abstract class BasicFormPage extends FormPage implements IModelConfigurat
// refresh the title
String title = mForm.getForm().getText();
- int titleIndex = Math.max(Math.max(title.indexOf(RUNNING_TITLE), title.indexOf(CRASHED_TITLE)), title
- .indexOf(LOCKED_TITLE));
+ int titleIndex = Math.max(title.indexOf(RUNNING_TITLE), title.indexOf(CRASHED_TITLE));
// restore the title
if (titleIndex != -1)
{
@@ -574,9 +563,6 @@ public abstract class BasicFormPage extends FormPage implements IModelConfigurat
mForm.getForm().setText(title + RUNNING_TITLE);
}
- } else if (getModel().isLocked())
- {
- mForm.getForm().setText(title + LOCKED_TITLE);
} else
{
// restore the title, only if we need
@@ -596,7 +582,7 @@ public abstract class BasicFormPage extends FormPage implements IModelConfigurat
}
// refresh enablement status
- setEnabled(!modelRunning && !getModel().isLocked());
+ setEnabled(!modelRunning);
mForm.getForm().update();
}
@@ -842,8 +828,7 @@ public abstract class BasicFormPage extends FormPage implements IModelConfigurat
*/
public boolean isEnabled()
{
- final Model model = getModel();
- return !model.isRunning() && !model.isLocked();
+ return !getModel().isRunning();
}
}
@@ -870,7 +855,7 @@ public abstract class BasicFormPage extends FormPage implements IModelConfigurat
*/
public boolean isEnabled()
{
- return !getModel().isRunning() && !getModel().isLocked();
+ return !getModel().isRunning();
}
}
@@ -925,64 +910,4 @@ public abstract class BasicFormPage extends FormPage implements IModelConfigurat
}
}
- class UnlockModelAction extends Action
- {
- UnlockModelAction()
- {
- super("Unlock model", TLCUIActivator.imageDescriptorFromPlugin(TLCUIActivator.PLUGIN_ID,
- "icons/full/owned_monitor_obj.gif"));
- setDescription("Unlocks the model");
- setToolTipText("Unlocks the model so that changes are possible.");
- }
-
- public void run()
- {
- ((ModelEditor) getEditor()).getModel().setLocked(false);
- }
-
- public boolean isEnabled()
- {
- return !getModel().isRunning() && getModel().isLocked();
- }
- }
-
- class LockModelAction extends Action
- {
- LockModelAction()
- {
- super("Lock model", TLCUIActivator.imageDescriptorFromPlugin(TLCUIActivator.PLUGIN_ID,
- "icons/full/lockedstate.gif"));
- setDescription("Locks the model");
- setToolTipText("Locks the model so that no changes are possible.");
- }
-
- public void run()
- {
- if (getEditor().isDirty())
- {
- // allow the user to save or cancel
- // it is not allowed to not save and lock the model
- boolean save = MessageDialog.open(MessageDialog.CONFIRM, UIHelper.getShellProvider().getShell(),
- "Model Modified", "The model has been modified. Do you want to save the changes?", SWT.NONE);
- if (save)
- {
- ModelEditor editor = (ModelEditor) getEditor();
- editor.doSave(new NullProgressMonitor());
- // The changes may result in an error, but validation
- // can only be run on an unlocked model, so the validation
- // must be run synchronously before the model is locked.
- UIHelper.runUISync(editor.getValidateRunnable());
- } else
- {
- return;
- }
- }
- getModel().setLocked(true);
- }
-
- public boolean isEnabled()
- {
- return !getModel().isLocked();
- }
- }
}
\ No newline at end of file
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/ResultPage.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/ResultPage.java
index 6c48bf3c8651fef488438bf7007c8ea4311e616a..c167881362d87e2904b8840b58f8c5a45083c815 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/ResultPage.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/ResultPage.java
@@ -721,7 +721,7 @@ public class ResultPage extends BasicFormPage implements ITLCModelLaunchDataPres
* @see org.eclipse.jface.action.Action#isEnabled()
*/
public boolean isEnabled() {
- if (getModel().isLocked() || getModel().isRunning()) {
+ if (getModel().isRunning()) {
return false;
}
return super.isEnabled();
@@ -781,7 +781,7 @@ public class ResultPage extends BasicFormPage implements ITLCModelLaunchDataPres
{
if (inputElement != null && inputElement instanceof List)
{
- return ((List) inputElement).toArray(new Object[((List) inputElement).size()]);
+ return ((List<?>) inputElement).toArray(new Object[((List<?>) inputElement).size()]);
}
return null;
}
@@ -844,7 +844,7 @@ public class ResultPage extends BasicFormPage implements ITLCModelLaunchDataPres
{
if (inputElement != null && inputElement instanceof List)
{
- return ((List) inputElement).toArray(new Object[((List) inputElement).size()]);
+ return ((List<?>) inputElement).toArray(new Object[((List<?>) inputElement).size()]);
}
return null;
}
@@ -864,6 +864,7 @@ public class ResultPage extends BasicFormPage implements ITLCModelLaunchDataPres
*
* @return
*/
+ @SuppressWarnings("unchecked") // generics cast
public StateSpaceInformationItem[] getStateSpaceInformation()
{
List<StateSpaceInformationItem> infoList = (List<StateSpaceInformationItem>) stateSpace.getInput();
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/part/ValidateableConstantSectionPart.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/part/ValidateableConstantSectionPart.java
index 764a56c1b36170b3e4a1f3042657eaa5e6224ba4..8d231553445026bf62fea9cd33ee391f9e4228a1 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/part/ValidateableConstantSectionPart.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/part/ValidateableConstantSectionPart.java
@@ -37,8 +37,7 @@ public class ValidateableConstantSectionPart extends ValidateableTableSectionPar
// Create the wizard
AssignmentWizard wizard = new AssignmentWizard(getSection().getText(), getSection().getDescription(),
- (Assignment) formula, AssignmentWizard.SHOW_OPTION, AssignmentWizardPage.CONSTANT_WIZARD_ID,
- AssignmentWizardPage.CONSTANT_TYPING_WIZARD_ID);
+ (Assignment) formula, AssignmentWizard.SHOW_OPTION, AssignmentWizardPage.CONSTANT_WIZARD_ID);
// Create the wizard dialog
WizardDialog dialog = new WizardDialog(getTableViewer().getTable().getShell(), wizard);
wizard.setWizardDialog(dialog);
@@ -58,6 +57,8 @@ public class ValidateableConstantSectionPart extends ValidateableTableSectionPar
* Add assignment to the list -- Despite Simon's comments, this is actually called when clicking on ADD
* for Definition Override
*/
+ @Override
+ @SuppressWarnings("unchecked") // Generic casting...
protected void doAdd()
{
Assignment formula = doEditFormula((Assignment) null);
@@ -65,7 +66,7 @@ public class ValidateableConstantSectionPart extends ValidateableTableSectionPar
// add a formula
if (formula != null)
{
- Vector input = ((Vector) tableViewer.getInput()); // this seems to be the place to check for duplicate overrides.
+ Vector<Assignment> input = ((Vector<Assignment>) tableViewer.getInput()); // this seems to be the place to check for duplicate overrides.
input.add(formula);
tableViewer.setInput(input);
this.doMakeDirty();
@@ -73,6 +74,7 @@ public class ValidateableConstantSectionPart extends ValidateableTableSectionPar
}
// This is called when hitting EDIT or double clicking to enter a Constant's value or to change a Definition override.
+ @Override
protected void doEdit()
{
IStructuredSelection selection = (IStructuredSelection) tableViewer.getSelection();
@@ -94,6 +96,7 @@ public class ValidateableConstantSectionPart extends ValidateableTableSectionPar
/**
* create the viewer
*/
+ @Override
protected TableViewer createTableViewer(Table table)
{
// create
@@ -116,6 +119,7 @@ public class ValidateableConstantSectionPart extends ValidateableTableSectionPar
/**
* create the table (no check boxes)
*/
+ @Override
protected Table createTable(Composite sectionArea, FormToolkit toolkit)
{
Table table = toolkit.createTable(sectionArea, SWT.MULTI | SWT.V_SCROLL | SWT.H_SCROLL | SWT.FULL_SELECTION);
@@ -127,6 +131,7 @@ public class ValidateableConstantSectionPart extends ValidateableTableSectionPar
/**
* Only create the edit button
*/
+ @Override
protected void createButtons(Composite sectionArea, FormToolkit toolkit, boolean add, boolean edit, boolean remove)
{
doCreateButtons(sectionArea, toolkit, false, true, false);
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/part/ValidateableOverridesSectionPart.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/part/ValidateableOverridesSectionPart.java
index ab0349658c50b53695e83e60f2209df73da63f58..433793ca9c9bd8bba67a1a5769827d4f2a5eb69a 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/part/ValidateableOverridesSectionPart.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/part/ValidateableOverridesSectionPart.java
@@ -34,6 +34,8 @@ public class ValidateableOverridesSectionPart extends ValidateableConstantSectio
super(composite, title, description, toolkit, flags, page, DataBindingManager.SEC_DEFINITION_OVERRIDE);
}
+ @Override
+ @SuppressWarnings("unchecked") // Generic casting...
protected Assignment doEditFormula(Assignment formula)
{
// add -> let the user select the definition to override
@@ -49,7 +51,7 @@ public class ValidateableOverridesSectionPart extends ValidateableConstantSectio
// If I'm wrong, we just set names[] to a zero-length array.
if ((input != null) && (input instanceof Vector))
{
- Vector inputVec = (Vector) input;
+ Vector<Object> inputVec = (Vector<Object>) input;
names = new String[inputVec.size()];
for (int i = 0; i < names.length; i++)
{
@@ -114,7 +116,7 @@ public class ValidateableOverridesSectionPart extends ValidateableConstantSectio
// Create the wizard
AssignmentWizard wizard = new AssignmentWizard(getSection().getText(), getSection().getDescription(),
(Assignment) formula, AssignmentWizard.SHOW_MODEL_VALUE_OPTION,
- AssignmentWizardPage.DEF_OVERRIDE_WIZARD_ID, "");
+ AssignmentWizardPage.DEF_OVERRIDE_WIZARD_ID);
// Create the wizard dialog
WizardDialog dialog = new WizardDialog(getTableViewer().getTable().getShell(), wizard);
wizard.setWizardDialog(dialog);
@@ -134,6 +136,7 @@ public class ValidateableOverridesSectionPart extends ValidateableConstantSectio
/**
* create the buttons
*/
+ @Override
protected void createButtons(Composite sectionArea, FormToolkit toolkit, boolean add, boolean edit, boolean remove)
{
doCreateButtons(sectionArea, toolkit, true, true, true);
@@ -143,6 +146,7 @@ public class ValidateableOverridesSectionPart extends ValidateableConstantSectio
* Overrides the method in ValidateableConstantSectionPart in order
* to add a label provider for displaying definition overrides properly.
*/
+ @Override
protected TableViewer createTableViewer(Table table)
{
TableViewer tableViewer = super.createTableViewer(table);
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/modelexplorer/ModelContentProvider.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/modelexplorer/ModelContentProvider.java
index 7bb15da476d43889877f245ee1ba94c6a6a2869d..c09e6532346e096c1eab5790268d3cc01e95adf6 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/modelexplorer/ModelContentProvider.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/modelexplorer/ModelContentProvider.java
@@ -59,15 +59,15 @@ public class ModelContentProvider implements ITreeContentProvider {
UIHelper.runUISync(new Runnable() {
@Override
public void run() {
- final Model snapshot = event.getModel();
- final Model parent = snapshot.getSnapshotFor();
- // The CommonViewer is stupid in that it accesses an element (snapshot) even
+ final Model model = event.getModel();
+ final TLCSpec parent = model.getSpec();
+ // The CommonViewer is stupid in that it accesses an element (model) even
// after it has been removed in order to update the viewer's current selection.
// Since we have to prevent this access to avoid a null pointer, we explicitly
// reset the selection.
getViewer().setSelection(new StructuredSelection(parent));
// ...still remove the element from the tree.
- getViewer().remove(parent, new Object[] {snapshot});
+ getViewer().remove(parent, new Object[] {model});
}
});
}
@@ -84,7 +84,13 @@ public class ModelContentProvider implements ITreeContentProvider {
return new Group[] {new Group((Spec) parentElement, models.toArray(new Model[models.size()]))};
}
} else if (parentElement instanceof Group) {
- return ((Group) parentElement).getModels();
+ // Attach the model listener above to each model instance to be notified of
+ // state changes, especially model deletion (see comment above).
+ final Model[] models = ((Group) parentElement).getModels();
+ for (Model model : models) {
+ model.add(modelChangeListener);
+ }
+ return models;
} else if (parentElement instanceof Model) {
final Collection<Model> snapshots = ((Model) parentElement).getSnapshots();
for (final Model model : snapshots) {
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/modelexplorer/ModelSnapshotSorter.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/modelexplorer/ModelSnapshotSorter.java
new file mode 100644
index 0000000000000000000000000000000000000000..43a37fa19abbb92afac9948249b30ecd38d79aca
--- /dev/null
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/modelexplorer/ModelSnapshotSorter.java
@@ -0,0 +1,36 @@
+package org.lamport.tla.toolbox.tool.tlc.ui.modelexplorer;
+
+import org.eclipse.jface.viewers.Viewer;
+import org.eclipse.jface.viewers.ViewerComparator;
+
+import org.lamport.tla.toolbox.tool.tlc.model.Model;
+
+/**
+ * Our snapshots were displayed in a funky order due to the default comparator
+ * (which did String comparsion of the label strings.) They are now sorted in
+ * descending (reverse chronological) order.
+ *
+ * @see org.eclipse.jface.util.Policy#getDefaultComparator()
+ */
+public class ModelSnapshotSorter extends ViewerComparator {
+
+ @Override
+ public int compare(final Viewer viewer, final Object e1, final Object e2) {
+ if ((!(e1 instanceof Model)) || (!(e2 instanceof Model))) {
+ return super.compare(viewer, e1, e2);
+ } else {
+ final Model m1 = (Model) e1;
+ final Model m2 = (Model) e2;
+ final long t1 = m1.getSnapshotTimeStamp();
+ final long t2 = m2.getSnapshotTimeStamp();
+
+ if (t1 < t2) {
+ return 1;
+ } else if (t1 > t2) {
+ return -1;
+ }
+
+ return 0;
+ }
+ }
+}
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/preference/ITLCPreferenceConstants.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/preference/ITLCPreferenceConstants.java
index a9461f270e9b22106a775e9e8e752db92e50de8c..bb4fe333c10a20440991af7e7f2605a8d99ab432 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/preference/ITLCPreferenceConstants.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/preference/ITLCPreferenceConstants.java
@@ -31,10 +31,6 @@ public interface ITLCPreferenceConstants
public static final String I_TLC_FPBITS_DEFAULT = "fpBitsDefault";
public static final String I_TLC_MAXSETSIZE_DEFAULT = "maxSetSizeDefault";
- /**
- * Automatically lock model after TLC exceeds given length of time.
- */
- public static final String I_TLC_AUTO_LOCK_MODEL_TIME = "autoLockModelTime";
/**
* font used for text in the error viewer at the top of the TLC error
* view, the User Output field on the results page, and the Progress
@@ -48,5 +44,10 @@ public interface ITLCPreferenceConstants
* Implementation of {@link FPSet} to use during model checking
*/
public static final String I_TLC_FPSETIMPL_DEFAULT = "fpSetImpl";
-
+ /**
+ * If set, the Toolbox will open a modal progress dialog to indicate TLC
+ * startup. A user can opt to subsequently suppress the dialog. This returns the
+ * old behavior prior to the change in https://bugs.eclipse.org/146205#c10.
+ */
+ public static final String I_TLC_SHOW_MODAL_PROGRESS = "showModalProgress";
}
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/preference/TLCPreferenceInitializer.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/preference/TLCPreferenceInitializer.java
index e3e512a92b4ac995f20c645463ecb46a2cbdb776..a7c8e57d6b85cb9f46a57b3ae2039437ca946d5f 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/preference/TLCPreferenceInitializer.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/preference/TLCPreferenceInitializer.java
@@ -1,10 +1,14 @@
package org.lamport.tla.toolbox.tool.tlc.ui.preference;
import org.eclipse.core.runtime.preferences.AbstractPreferenceInitializer;
+import org.eclipse.core.runtime.preferences.IEclipsePreferences;
+import org.eclipse.core.runtime.preferences.InstanceScope;
import org.eclipse.jface.preference.IPreferenceStore;
+import org.eclipse.ui.internal.IPreferenceConstants;
+import org.eclipse.ui.internal.WorkbenchPlugin;
import org.lamport.tla.toolbox.tool.tlc.TLCActivator;
-import org.lamport.tla.toolbox.tool.tlc.launch.IModelConfigurationDefaults;
import org.lamport.tla.toolbox.tool.tlc.ui.TLCUIActivator;
+import org.osgi.service.prefs.BackingStoreException;
import tlc2.TLCGlobals;
import tlc2.tool.fp.FPSetFactory;
@@ -12,6 +16,7 @@ import tlc2.tool.fp.FPSetFactory;
/**
* Class used to initialize default TLC preference values.
*/
+@SuppressWarnings("restriction")
public class TLCPreferenceInitializer extends AbstractPreferenceInitializer
{
@@ -22,18 +27,38 @@ public class TLCPreferenceInitializer extends AbstractPreferenceInitializer
*/
public void initializeDefaultPreferences()
{
+ final IPreferenceStore uiPreferencesStore = TLCUIActivator.getDefault().getPreferenceStore();
+ final IPreferenceStore tlcPreferencesStore = TLCActivator.getDefault().getPreferenceStore();
- IPreferenceStore store = TLCUIActivator.getDefault().getPreferenceStore();
- store.setDefault(ITLCPreferenceConstants.I_TLC_TRACE_MAX_SHOW_ERRORS, 10000);
- store.setDefault(ITLCPreferenceConstants.I_TLC_POPUP_ERRORS, true);
- store.setDefault(ITLCPreferenceConstants.I_TLC_REVALIDATE_ON_MODIFY, true);
- store.setDefault(TLCActivator.I_TLC_SNAPSHOT_PREFERENCE, true);
- store.setDefault(ITLCPreferenceConstants.I_TLC_MAXIMUM_HEAP_SIZE_DEFAULT, MAX_HEAP_SIZE_DEFAULT);
- store.setDefault(ITLCPreferenceConstants.I_TLC_MAXSETSIZE_DEFAULT, TLCGlobals.setBound);
- store.setDefault(ITLCPreferenceConstants.I_TLC_FPBITS_DEFAULT, 1);
- store.setDefault(ITLCPreferenceConstants.I_TLC_FPSETIMPL_DEFAULT, FPSetFactory.getImplementationDefault());
- store.setDefault(ITLCPreferenceConstants.I_TLC_AUTO_LOCK_MODEL_TIME,
- IModelConfigurationDefaults.MODEL_AUTO_LOCK_TIME_DEFAULT);
+ tlcPreferencesStore.setDefault(TLCActivator.I_TLC_SNAPSHOT_KEEP_COUNT, 10);
+
+ // This is so bad.. we store them in parallel because one is needed by plugin relied upon the PreferencePage
+ // and the other by a plugin which is on the opposite side of the dependency. (TLCModelLaunchDelegate)
+ uiPreferencesStore.setDefault(TLCActivator.I_TLC_SNAPSHOT_KEEP_COUNT, 10);
+
+ uiPreferencesStore.setDefault(ITLCPreferenceConstants.I_TLC_TRACE_MAX_SHOW_ERRORS, 10000);
+ uiPreferencesStore.setDefault(ITLCPreferenceConstants.I_TLC_POPUP_ERRORS, true);
+ uiPreferencesStore.setDefault(ITLCPreferenceConstants.I_TLC_REVALIDATE_ON_MODIFY, true);
+ uiPreferencesStore.setDefault(ITLCPreferenceConstants.I_TLC_MAXIMUM_HEAP_SIZE_DEFAULT, MAX_HEAP_SIZE_DEFAULT);
+ uiPreferencesStore.setDefault(ITLCPreferenceConstants.I_TLC_MAXSETSIZE_DEFAULT, TLCGlobals.setBound);
+ uiPreferencesStore.setDefault(ITLCPreferenceConstants.I_TLC_FPBITS_DEFAULT, 1);
+ uiPreferencesStore.setDefault(ITLCPreferenceConstants.I_TLC_FPSETIMPL_DEFAULT, FPSetFactory.getImplementationDefault());
// store.setDefault(ITLCPreferenceConstants.I_TLC_DELETE_PREVIOUS_FILES, true);
+
+ // By default we want the Toolbox to show a modal progress dialog upon TLC
+ // startup. A user can opt to subsequently suppress the dialog.
+ // This restores the behavior prior to https://bugs.eclipse.org/146205#c10.
+ if (!uiPreferencesStore.contains(ITLCPreferenceConstants.I_TLC_SHOW_MODAL_PROGRESS)) {
+ final IEclipsePreferences node = InstanceScope.INSTANCE
+ .getNode(WorkbenchPlugin.getDefault().getBundle().getSymbolicName());
+ node.putBoolean(IPreferenceConstants.RUN_IN_BACKGROUND, false);
+ try {
+ node.flush();
+ } catch (final BackingStoreException e) {
+ TLCUIActivator.getDefault().logError("Error trying to flush the workbench plugin preferences store.",
+ e);
+ }
+ uiPreferencesStore.setValue(ITLCPreferenceConstants.I_TLC_SHOW_MODAL_PROGRESS, true);
+ }
}
}
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/preference/TLCPreferencePage.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/preference/TLCPreferencePage.java
index 99d34cfec051d572a5602910f1e3261ae84b9da3..db5554a4821f92befc409f7c7e6b2734e8fe824b 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/preference/TLCPreferencePage.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/preference/TLCPreferencePage.java
@@ -33,8 +33,8 @@ public class TLCPreferencePage extends FieldEditorPreferencePage implements IWor
@Override
public void propertyChange(PropertyChangeEvent event) {
final IPreferenceStore store = TLCActivator.getDefault().getPreferenceStore();
- if (TLCActivator.I_TLC_SNAPSHOT_PREFERENCE.equals(event.getProperty())) {
- store.setValue(TLCActivator.I_TLC_SNAPSHOT_PREFERENCE, (boolean) event.getNewValue());
+ if (TLCActivator.I_TLC_SNAPSHOT_KEEP_COUNT.equals(event.getProperty())) {
+ store.setValue(TLCActivator.I_TLC_SNAPSHOT_KEEP_COUNT, (int)event.getNewValue());
}
}
});
@@ -59,15 +59,19 @@ public class TLCPreferencePage extends FieldEditorPreferencePage implements IWor
addField(new BooleanFieldEditor(ITLCPreferenceConstants.I_TLC_REVALIDATE_ON_MODIFY,
"&Re-validate model on save", getFieldEditorParent()));
- addField(new BooleanFieldEditor(TLCActivator.I_TLC_SNAPSHOT_PREFERENCE,
- "Take &snapshot of model after completion of model checking", getFieldEditorParent()));
+
+ IntegerFieldEditor integerFieldEditor = new IntegerFieldEditor(TLCActivator.I_TLC_SNAPSHOT_KEEP_COUNT,
+ "Number of model &snapshots to keep",
+ getFieldEditorParent());
+ integerFieldEditor.setValidRange(0, Integer.MAX_VALUE);
+ addField(integerFieldEditor);
+
// addField(new BooleanFieldEditor(ITLCPreferenceConstants.I_TLC_DELETE_PREVIOUS_FILES,
// "&Automatically delete unused data from previous model run", getFieldEditorParent()));
addField(new IntegerFieldEditor(ITLCPreferenceConstants.I_TLC_MAXIMUM_HEAP_SIZE_DEFAULT,
"Maximum JVM Heap Size default in % of physical system memory", getFieldEditorParent()));
- addField(new IntegerFieldEditor(ITLCPreferenceConstants.I_TLC_AUTO_LOCK_MODEL_TIME, "TLC run auto-lock time (in minutes)",
- getFieldEditorParent()));
- IntegerFieldEditor integerFieldEditor = new IntegerFieldEditor(ITLCPreferenceConstants.I_TLC_TRACE_MAX_SHOW_ERRORS,
+
+ integerFieldEditor = new IntegerFieldEditor(ITLCPreferenceConstants.I_TLC_TRACE_MAX_SHOW_ERRORS,
"Default number of states shown in error traces", getFieldEditorParent());
integerFieldEditor.setValidRange(1, Integer.MAX_VALUE);
addField(integerFieldEditor);
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/util/FormHelper.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/util/FormHelper.java
index 7df26d48079c7a66f8f131852a770f5217f4f528..865847dba64ec71ef4bf7f3429a8eded6d5b1d0a 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/util/FormHelper.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/util/FormHelper.java
@@ -372,7 +372,7 @@ public class FormHelper
gd.horizontalIndent = 30;
gd.verticalAlignment = SWT.TOP;
gd.horizontalAlignment = SWT.RIGHT;
- gd.minimumWidth = 150;
+ gd.minimumWidth = 300;
hyperlink.setLayoutData(gd);
return hyperlink;
@@ -397,7 +397,7 @@ public class FormHelper
gd.horizontalIndent = 30;
gd.verticalAlignment = SWT.TOP;
gd.horizontalAlignment = SWT.RIGHT;
- gd.minimumWidth = 200;
+ gd.minimumWidth = 400;
text.setLayoutData(gd);
return text;
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/wizard/AssignmentWizard.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/wizard/AssignmentWizard.java
index a41d3e2df4c6a0a8bec33581c4296e81c2239573..740052597bc214a00ca930c3d2ec3cd14e7c5052 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/wizard/AssignmentWizard.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/wizard/AssignmentWizard.java
@@ -7,7 +7,6 @@ import org.lamport.tla.toolbox.tool.tlc.model.Assignment;
/**
* Wizard for editing a constant assignement
* @author Simon Zambrovski
- * @version $Id$
*/
public class AssignmentWizard extends Wizard
{
@@ -31,31 +30,26 @@ public class AssignmentWizard extends Wizard
private Assignment assignment;
private AssignmentWizardPage assignmentPage;
- private TypingWizardPage typePage;
- private WizardDialog WizardDialog;
+ private WizardDialog wizardDialog;
/**
* Constructs the wizard that assigns values to constants,
* I believe it also constructs the wizard that overrides definitions. (LL)
- * The last argument is meaningful only for the wizard that assigns values
- * to constants.
* @param fieldFlags bit mask determining fields that are visible
* @see {@link AssignmentWizard} constants
*/
- public AssignmentWizard(String action, String description, Assignment assignment, int fieldFlags, String helpId,
- String pageTwoHelpId)
+ public AssignmentWizard(String action, String description, Assignment assignment, int fieldFlags, String helpId)
{
super();
this.assignment = assignment;
- assignmentPage = new AssignmentWizardPage(action, description, fieldFlags, helpId);
- typePage = new TypingWizardPage(action, description, pageTwoHelpId);
+ this.assignmentPage = new AssignmentWizardPage(action, description, fieldFlags, helpId);
}
+ @Override
public void addPages()
{
- addPage(assignmentPage);
- addPage(typePage);
+ addPage(this.assignmentPage);
}
/**
@@ -78,20 +72,16 @@ public class AssignmentWizard extends Wizard
* text field which calls updateButtons() whenever
* the input text is modified.
*/
+ @Override
public boolean canFinish()
{
- String inputText = assignmentPage.getInputText();
+ String inputText = this.assignmentPage.getInputText();
// either on the first page, but no typing of MV set is possible, or on the second page
// also, if on the first page, there must be an input that is not only white space
// Modified by LL on 5 Nov 2009 to return true regardless of inputText if the model value
// option is selected.
- return ( assignmentPage.isCurrentPage()
- && !assignmentPage.isTypeInputPossible()
- && ( (inputText != null && inputText.trim().length() != 0)
- || assignmentPage.modelValueSelected()
- )
- )
- || !assignmentPage.isCurrentPage();
+ return ((inputText != null && inputText.trim().length() != 0)
+ || this.assignmentPage.modelValueSelected());
}
/* (non-Javadoc)
@@ -103,10 +93,10 @@ public class AssignmentWizard extends Wizard
}
public void setWizardDialog(WizardDialog dialog) {
- WizardDialog = dialog;
+ this.wizardDialog = dialog;
}
public int getWizardDialogReturnCode() {
- return WizardDialog.getReturnCode();
+ return this.wizardDialog.getReturnCode();
}
}
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/wizard/AssignmentWizardPage.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/wizard/AssignmentWizardPage.java
index 979a2459df4c8edb360e7c3513ab00789ef710a7..82adf0df88537ce7bd77e826bc4f0a314174835a 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/wizard/AssignmentWizardPage.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/wizard/AssignmentWizardPage.java
@@ -2,7 +2,6 @@ package org.lamport.tla.toolbox.tool.tlc.ui.wizard;
import org.eclipse.jface.text.Document;
import org.eclipse.jface.text.source.SourceViewer;
-import org.eclipse.jface.wizard.IWizardPage;
import org.eclipse.jface.wizard.WizardPage;
import org.eclipse.swt.SWT;
import org.eclipse.swt.custom.StyledText;
@@ -14,6 +13,7 @@ import org.eclipse.swt.events.SelectionListener;
import org.eclipse.swt.layout.GridData;
import org.eclipse.swt.layout.GridLayout;
import org.eclipse.swt.widgets.Button;
+import org.eclipse.swt.widgets.Combo;
import org.eclipse.swt.widgets.Composite;
import org.eclipse.swt.widgets.Display;
import org.eclipse.swt.widgets.Label;
@@ -32,18 +32,34 @@ import tla2sany.semantic.OpDefNode;
public class AssignmentWizardPage extends WizardPage
{
public static final String CONSTANT_WIZARD_ID = "constant_assignment_wizard";
- public static final String CONSTANT_TYPING_WIZARD_ID = "constant_assignment_typing_wizard";
public static final String DEF_OVERRIDE_WIZARD_ID = "definition_override_wizard";
private LabeledListComposite paramComposite;
private SourceViewer source;
- private Button optionModelValue = null;
private final int fieldFlags;
private final String helpId; // The id of the help context for this wizard page
+
+ private Button optionOrdinaryValue;
+
+ private Button optionModelValue = null;
+
private Button optionSetModelValues;
private Button flagSymmetricalSet;
- private Button optionOrdinaryValue;
+ private Combo smvTypeCombo;
+ private Button optionSMVUntyped;
+
+ // selection adapter reacting to set of value typing radio choice
+ final private SelectionListener typingOptionSelectionAdapter = new SelectionAdapter() {
+ @Override
+ public void widgetSelected(SelectionEvent e)
+ {
+ smvTypeCombo.setEnabled(optionSMVUntyped.getSelection());
+ }
+ };
+
+
// selection adapter reacting on the choice
- private SelectionListener optionSelectionAdapter = new SelectionAdapter() {
+ final private SelectionListener optionSelectionAdapter = new SelectionAdapter() {
+ @Override
public void widgetSelected(SelectionEvent e)
{
boolean modelValueSelected = optionModelValue.getSelection();
@@ -61,7 +77,9 @@ public class AssignmentWizardPage extends WizardPage
{
boolean modelValueSetSelected = optionSetModelValues.getSelection();
flagSymmetricalSet.setEnabled(modelValueSetSelected);
- }
+ smvTypeCombo.setEnabled(modelValueSetSelected);
+ optionSMVUntyped.setEnabled(modelValueSetSelected);
+ }
getContainer().updateButtons();
}
};
@@ -86,15 +104,15 @@ public class AssignmentWizardPage extends WizardPage
container.setLayout(layout);
GridData gd;
- paramComposite = new LabeledListComposite(container, getAssignment().getLabel().substring(
- getAssignment().getLabel().lastIndexOf("!") + 1), getAssignment().getParams());
+ final Assignment assignment = getAssignment();
+ paramComposite = new LabeledListComposite(container, assignment.getLocalLabel(), assignment.getParams());
gd = new GridData(SWT.LEFT, SWT.TOP, false, true);
paramComposite.setLayoutData(gd);
source = FormHelper.createSourceViewer(container, SWT.BORDER | SWT.MULTI | SWT.H_SCROLL | SWT.V_SCROLL);
// set data
- source.setDocument(new Document(getAssignment().getRight()));
+ source.setDocument(new Document(assignment.getRight()));
StyledText styledText = source.getTextWidget();
styledText.addModifyListener(new ModifyListener() {
@@ -116,7 +134,7 @@ public class AssignmentWizardPage extends WizardPage
styledText.setLayoutData(gd);
// display source name and originally defined in module
- OpDefNode node = ModelHelper.getOpDefNode(getAssignment().getLabel());
+ OpDefNode node = ModelHelper.getOpDefNode(assignment.getLabel());
if (node != null && node.getSource() != node)
{
GridData labelGridData = new GridData();
@@ -133,35 +151,65 @@ public class AssignmentWizardPage extends WizardPage
// both bits set, make a radio list
if (fieldFlags == AssignmentWizard.SHOW_OPTION)
{
+ Composite leftContainer = new Composite(container, SWT.NULL);
+ gd = new GridData(SWT.LEFT, SWT.TOP, false, false);
+ leftContainer.setLayoutData(gd);
+ leftContainer.setLayout(new GridLayout(1, false));
+
// ordinary value option
- optionOrdinaryValue = new Button(container, SWT.RADIO);
+ optionOrdinaryValue = new Button(leftContainer, SWT.RADIO);
optionOrdinaryValue.setText("Ordinary assignment");
gd = new GridData(SWT.LEFT, SWT.TOP, false, false);
- gd.horizontalSpan = 2;
optionOrdinaryValue.setLayoutData(gd);
// make a model value
- optionModelValue = new Button(container, SWT.RADIO);
+ optionModelValue = new Button(leftContainer, SWT.RADIO);
optionModelValue.setText("Model value");
gd = new GridData(SWT.LEFT, SWT.TOP, false, false);
- gd.horizontalSpan = 2;
optionModelValue.setLayoutData(gd);
// make a set of model values
- optionSetModelValues = new Button(container, SWT.RADIO);
+ optionSetModelValues = new Button(leftContainer, SWT.RADIO);
optionSetModelValues.setText("Set of model values");
gd = new GridData(SWT.LEFT, SWT.TOP, false, false);
- gd.horizontalSpan = 2;
optionSetModelValues.setLayoutData(gd);
- // option to make a set symmetrical
- flagSymmetricalSet = new Button(container, SWT.CHECK);
+ // option to make a set of model values symmetrical
+ flagSymmetricalSet = new Button(leftContainer, SWT.CHECK);
flagSymmetricalSet.setText("Symmetry set");
gd = new GridData(SWT.LEFT, SWT.TOP, false, false);
- gd.horizontalSpan = 2;
- gd.horizontalIndent = 10;
- flagSymmetricalSet.setLayoutData(gd);
+ gd.horizontalIndent = 10;
+ flagSymmetricalSet.setLayoutData(gd);
+
+ final Composite rightContainer = new Composite(leftContainer, SWT.NONE);
+ gd = new GridData(SWT.LEFT, SWT.TOP, false, false);
+ rightContainer.setLayoutData(gd);
+ rightContainer.setLayout(new GridLayout(2, false));
+
+ // untyped set of model values option
+ optionSMVUntyped = new Button(rightContainer, SWT.CHECK);
+ optionSMVUntyped.setText("Type:");
+ optionSMVUntyped.addSelectionListener(typingOptionSelectionAdapter);
+ gd = new GridData(SWT.LEFT, SWT.TOP, true, false);
+ gd.horizontalIndent = 5;
+ optionSMVUntyped.setLayoutData(gd);
+
+ // type combo box
+ smvTypeCombo = new Combo(rightContainer, SWT.BORDER);
+
+ // add letters (assumes A-Z...a-z)
+ for (char i = 'A'; i < 'z'; i++)
+ {
+ if (Character.isLetter(i))
+ {
+ smvTypeCombo.add("" + i);
+ }
+ }
+ gd = new GridData(SWT.LEFT, SWT.TOP, false, false);
+ smvTypeCombo.setLayoutData(gd);
+ smvTypeCombo.setText("A");
+ smvTypeCombo.setEnabled(false);
// install listeners
optionOrdinaryValue.addSelectionListener(optionSelectionAdapter);
@@ -169,23 +217,36 @@ public class AssignmentWizardPage extends WizardPage
optionSetModelValues.addSelectionListener(optionSelectionAdapter);
// set the value from the assignment object
- if (getAssignment().isModelValue())
+ if (assignment.isModelValue())
{
// single model value
- if (!getAssignment().isSetOfModelValues())
+ if (!assignment.isSetOfModelValues())
{
flagSymmetricalSet.setEnabled(false);
- optionModelValue.setSelection(getAssignment().isModelValue());
+ smvTypeCombo.setEnabled(false);
+ optionSMVUntyped.setEnabled(false);
+ optionModelValue.setSelection(assignment.isModelValue());
source.getTextWidget().setBackground(container.getBackground());
// set of model values
} else
{
- optionSetModelValues.setSelection(getAssignment().isModelValue());
- flagSymmetricalSet.setSelection(getAssignment().isSymmetricalSet());
+ optionSetModelValues.setSelection(assignment.isModelValue());
+ flagSymmetricalSet.setSelection(assignment.isSymmetricalSet());
+
+ final TypedSet set = TypedSet.parseSet(this.getAssignment().getRight());
+ final boolean hasType = set.hasType();
+
+ optionSMVUntyped.setSelection(hasType);
+ if (hasType) {
+ smvTypeCombo.setText(set.getType());
+ smvTypeCombo.setEnabled(true);
+ }
}
} else
{
flagSymmetricalSet.setEnabled(false);
+ smvTypeCombo.setEnabled(false);
+ optionSMVUntyped.setEnabled(false);
optionOrdinaryValue.setSelection(true);
}
@@ -211,12 +272,12 @@ public class AssignmentWizardPage extends WizardPage
optionModelValue.addSelectionListener(optionSelectionAdapter);
// set the value from the assignment object
- if (getAssignment().isModelValue())
+ if (assignment.isModelValue())
{
// single model value
- if (!getAssignment().isSetOfModelValues())
+ if (!assignment.isSetOfModelValues())
{
- optionModelValue.setSelection(getAssignment().isModelValue());
+ optionModelValue.setSelection(assignment.isModelValue());
source.getTextWidget().setBackground(container.getBackground());
// set of model values
}
@@ -244,13 +305,9 @@ public class AssignmentWizardPage extends WizardPage
return ((AssignmentWizard) getWizard()).getFormula();
}
- public boolean finish()
- {
- return false;
- }
-
// this method sets up the Assignment object when the user
// clicks Finish or Cancel
+ @Override
public void dispose()
{
// cancel should not update any model values
@@ -279,6 +336,19 @@ public class AssignmentWizardPage extends WizardPage
TypedSet set = TypedSet.parseSet(rightSide);
this.getAssignment().setSymmetric(flagSymmetricalSet.getSelection());
this.getAssignment().setRight(set.toString());
+
+ // evaluate the selected option and change the MVs as appropriate
+ set = TypedSet.parseSet(this.getAssignment().getRight());
+ if (optionSMVUntyped.getSelection())
+ {
+ // retrieve the type letter
+ final String type = smvTypeCombo.getText();
+ set.setType(type);
+ } else {
+ set.unsetType();
+ }
+ // set the content back
+ this.getAssignment().setRight(set.toString());
} else
{
// ordinary assignment (with no parameters)
@@ -312,37 +382,6 @@ public class AssignmentWizardPage extends WizardPage
super.dispose();
}
- /*
- * Show the next page ( for typing of model values sets )
- * @see org.eclipse.jface.wizard.WizardPage#getNextPage()
- */
- public IWizardPage getNextPage()
- {
- if (isTypeInputPossible())
- {
- return super.getNextPage();
- }
- return null;
- }
-
- protected boolean isTypeInputPossible()
- {
- // only a set of model values can be typed
- if (optionSetModelValues == null || !optionSetModelValues.getSelection())
- {
- return false;
- }
- String set = FormHelper.trimTrailingSpaces(source.getDocument().get());
- TypedSet parsedSet = TypedSet.parseSet(set);
-
- return (parsedSet.getType() == null);
- }
-
- public boolean isCurrentPage()
- {
- return super.isCurrentPage();
- }
-
/**
* Returns the unmodified text entered into this pages
* source text field.
diff --git a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/TLCActivator.java b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/TLCActivator.java
index 81011a59786b973f60dfc015464b94ee52d9a6f4..d93f07100c370bd5189c03b0b3b692fdb6202129 100644
--- a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/TLCActivator.java
+++ b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/TLCActivator.java
@@ -9,10 +9,16 @@ import org.osgi.framework.BundleContext;
*/
public class TLCActivator extends AbstractUIPlugin {
+ // TODO This is the only constant used in our Preferences that is not declared in ITLCPreferenceConstants
+ // because of package dependency issues. We should do something about that because this scattering
+ // feels meh.
/**
- * Take a model snapshot when model checking finishes to create a history of model runs.
+ * This preference is exposed through the Toolbox preference pane and allows the
+ * user to dictate how many snapshots are kept (with the oldest being pruned as
+ * this value is reached or exceeded.) A value of 0 here means that no snapshot
+ * is taken as part of the pre-launch of TLC.
*/
- public static final String I_TLC_SNAPSHOT_PREFERENCE = "takeModelSnapshot";
+ public static final String I_TLC_SNAPSHOT_KEEP_COUNT = "numberOfSnapshotsToKeep";
// The plug-in ID
public static final String PLUGIN_ID = "org.lamport.tla.toolbox.tool.tlc";
@@ -34,7 +40,6 @@ public class TLCActivator extends AbstractUIPlugin {
public void start(BundleContext context) throws Exception {
super.start(context);
plugin = this;
- plugin.getPreferenceStore().setDefault(I_TLC_SNAPSHOT_PREFERENCE, true);
}
/*
diff --git a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/job/TLAModelFilesCreationOperation.java b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/job/TLAModelFilesCreationOperation.java
deleted file mode 100644
index 82dd3a59828f915d7c014e068ca93c3298520188..0000000000000000000000000000000000000000
--- a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/job/TLAModelFilesCreationOperation.java
+++ /dev/null
@@ -1,72 +0,0 @@
-package org.lamport.tla.toolbox.tool.tlc.job;
-
-import java.io.ByteArrayInputStream;
-
-import org.eclipse.core.resources.IFile;
-import org.eclipse.core.resources.IProject;
-import org.eclipse.core.resources.IWorkspaceRunnable;
-import org.eclipse.core.runtime.CoreException;
-import org.eclipse.core.runtime.IPath;
-import org.eclipse.core.runtime.IProgressMonitor;
-import org.eclipse.core.runtime.SubProgressMonitor;
-import org.lamport.tla.toolbox.util.ResourceHelper;
-
-/**
- * Creates the stub for modelecking, extending the specification root module
- * @author Simon Zambrovski
- * @version $Id$
- */
-public class TLAModelFilesCreationOperation implements IWorkspaceRunnable
-{
- // project to create files in
- private IProject project;
- // path to the root module, which name will be added after EXTEND keyword
- // the .tla and .cfg files will be createed in the same directory
- // as the rootModule
- private IPath rootModulePath;
-
- /**
- * Construct an operation for creation of the files for model checking
- * @param project project to link files into
- * @param rootModulePath root module to be extended
- */
- public TLAModelFilesCreationOperation(IProject project, IPath rootModulePath)
- {
- this.rootModulePath = rootModulePath;
- this.project = project;
- }
-
- /* (non-Javadoc)
- * @see org.eclipse.core.resources.IWorkspaceRunnable#run(org.eclipse.core.runtime.IProgressMonitor)
- */
- public void run(IProgressMonitor monitor) throws CoreException
- {
- monitor.beginTask("Creating files", 2);
- // foo.tla
- String rootModuleFilename = this.rootModulePath.lastSegment();
- // foo
- String rootModuleName = ResourceHelper.getModuleName(rootModuleFilename);
-
- String tlaModuleName = "MC";
-
- IPath tlaPath = this.rootModulePath.removeLastSegments(1).append(tlaModuleName).addFileExtension("tla");
- IPath cfgPath = this.rootModulePath.removeLastSegments(1).append(tlaModuleName).addFileExtension("cfg");
-
- byte[] content = ResourceHelper.getExtendingModuleContent(tlaModuleName, rootModuleName).append(
- ResourceHelper.getModuleClosingTag()).toString().getBytes();
-
- try
- {
-
- IFile tlaFile = project.getFile(tlaPath);
- tlaFile.create(new ByteArrayInputStream(content), false /* force*/, new SubProgressMonitor(monitor, 1));
-
- IFile cfgFile = project.getFile(cfgPath);
- cfgFile.create(new ByteArrayInputStream("".getBytes()), false /* force*/, new SubProgressMonitor(monitor, 1));
-
- } finally {
- monitor.done();
- }
- }
-
-}
diff --git a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/IConfigurationConstants.java b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/IConfigurationConstants.java
index 7302a70b2caf3e049d8350b6448db6ad056be6ed..f5bb35f8bb2b1aaa11df346376ad1f023ffc4543 100644
--- a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/IConfigurationConstants.java
+++ b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/IConfigurationConstants.java
@@ -124,11 +124,4 @@ public interface IConfigurationConstants
*/
public static final String LAUNCH_FPSET_IMPL = "fpSetImpl";
- /**
- * Length of time in minutes the TLC must run
- * before the model is automatically locked at the termination
- * of the run.
- */
- public static final String LAUNCH_AUTO_LOCK_MODEL_TIME = "autoLockTime";
-
}
diff --git a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/IModelConfigurationDefaults.java b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/IModelConfigurationDefaults.java
index f0f1cc8aa0471f7f7a4df9855e2ff434e0e21444..a2a7b891a181fd5d2e43dfb9545fd992a404b145 100644
--- a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/IModelConfigurationDefaults.java
+++ b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/IModelConfigurationDefaults.java
@@ -33,10 +33,4 @@ public interface IModelConfigurationDefaults extends IConfigurationDefaults
*/
public static final boolean MODEL_CORRECTNESS_CHECK_DEADLOCK_DEFAULT = true;
- /**
- * Default length of time TLC must run for the model
- * to be automatically locked when tlc terminates
- */
- public static final int MODEL_AUTO_LOCK_TIME_DEFAULT = 15;
-
}
diff --git a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TLCModelLaunchDelegate.java b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TLCModelLaunchDelegate.java
index ea23d94cba836a527d9647ee91b97f66f8f0633f..d2dcdf1046590c7df43e04ccfd8fe662615b7912 100644
--- a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TLCModelLaunchDelegate.java
+++ b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TLCModelLaunchDelegate.java
@@ -49,6 +49,7 @@ import org.lamport.tla.toolbox.tool.tlc.job.DistributedTLCJob;
import org.lamport.tla.toolbox.tool.tlc.job.ITLCJobStatus;
import org.lamport.tla.toolbox.tool.tlc.job.TLCJobFactory;
import org.lamport.tla.toolbox.tool.tlc.job.TLCProcessJob;
+import org.lamport.tla.toolbox.tool.tlc.model.Assignment;
import org.lamport.tla.toolbox.tool.tlc.model.Model;
import org.lamport.tla.toolbox.tool.tlc.model.ModelWriter;
import org.lamport.tla.toolbox.tool.tlc.model.TypedSet;
@@ -127,27 +128,6 @@ public class TLCModelLaunchDelegate extends LaunchConfigurationDelegate implemen
return false;
}
- // check and lock the model
- final Model model = config.getAdapter(Model.class);
- synchronized (config)
- {
- // read out the running attribute
- if (/*model.isRunning() || */model.isLocked())
- {
- // previous run has not been completed
- // exit
- throw new CoreException(
- new Status(
- IStatus.ERROR,
- TLCActivator.PLUGIN_ID,
- "The running attribute for "
- + model.getName()
- + " has been set to true or that model is locked. "
- + "Another TLC is possible running on the same model, has been terminated non-gracefully "
- + "or you tried to run TLC on a locked model. Running TLC on a locked model is not possible."));
- }
- }
-
try
{
monitor.beginTask("Reading model parameters", 1);
@@ -362,8 +342,8 @@ public class TLCModelLaunchDelegate extends LaunchConfigurationDelegate implemen
writer.addPrimer(ModelHelper.MC_MODEL_NAME, model.getSpec().getRootModuleName());
// Sets constants to a Vector of the substitutions for the CONSTANT substitutions
- List constants = ModelHelper.deserializeAssignmentList(config.getAttribute(MODEL_PARAMETER_CONSTANTS,
- new Vector()));
+ List<Assignment> constants = ModelHelper.deserializeAssignmentList(config.getAttribute(MODEL_PARAMETER_CONSTANTS,
+ new Vector<String>()));
// Sets modelValues to a TypedSet object whose value is a String array containing
// the names of the model values declared on the Advanced model page.
@@ -389,8 +369,8 @@ public class TLCModelLaunchDelegate extends LaunchConfigurationDelegate implemen
writer.addConstantsBis(constants, MODEL_PARAMETER_CONSTANTS);
// Sets overrides to the Vector of definition overrides.
- List overrides = ModelHelper.deserializeAssignmentList(config.getAttribute(MODEL_PARAMETER_DEFINITIONS,
- new Vector()));
+ List<Assignment> overrides = ModelHelper.deserializeAssignmentList(config.getAttribute(MODEL_PARAMETER_DEFINITIONS,
+ new Vector<String>()));
// For the definition overrides, it adds the definitions to the MC.tla file and the
// overriding CONSTANT statements to the MC.cfg file.
@@ -474,12 +454,12 @@ public class TLCModelLaunchDelegate extends LaunchConfigurationDelegate implemen
{
// invariants
writer.addFormulaList(ModelWriter.createFormulaListContent(config.getAttribute(
- MODEL_CORRECTNESS_INVARIANTS, new Vector()), ModelWriter.INVARIANT_SCHEME), "INVARIANT",
+ MODEL_CORRECTNESS_INVARIANTS, new Vector<String>()), ModelWriter.INVARIANT_SCHEME), "INVARIANT",
MODEL_CORRECTNESS_INVARIANTS);
// properties
writer.addFormulaList(ModelWriter.createFormulaListContent(config.getAttribute(
- MODEL_CORRECTNESS_PROPERTIES, new Vector()), ModelWriter.PROP_SCHEME), "PROPERTY",
+ MODEL_CORRECTNESS_PROPERTIES, new Vector<String>()), ModelWriter.PROP_SCHEME), "PROPERTY",
MODEL_CORRECTNESS_PROPERTIES);
}
@@ -585,7 +565,7 @@ public class TLCModelLaunchDelegate extends LaunchConfigurationDelegate implemen
// find the error cause and install the error marker on the corresponding
// field
- Hashtable props = ModelHelper.createMarkerDescription(document, searchAdapter,
+ Hashtable<String, Object> props = ModelHelper.createMarkerDescription(document, searchAdapter,
message, severity, coordinates);
if (props != null)
{
@@ -864,7 +844,6 @@ public class TLCModelLaunchDelegate extends LaunchConfigurationDelegate implemen
// TLC models seem to require some clean-up
- model.setLocked(false);
model.setRunning(false);
model.recover();
@@ -963,18 +942,7 @@ public class TLCModelLaunchDelegate extends LaunchConfigurationDelegate implemen
Assert.isTrue(event.getJob() instanceof TLCProcessJob);
Assert.isNotNull(event.getResult());
TLCProcessJob tlcJob = (TLCProcessJob) event.getJob();
- if (event.getResult().isOK())
- {
- int autoLockTime = model.getAutoLockTime();
- // auto lock time is in minutes, getTLCStartTime() and getTLCEndTime()
- // are in milliseconds
- if (tlcJob.getTlcEndTime() - tlcJob.getTlcStartTime() > autoLockTime * 60 * 1000)
- {
- // length of job execution exceeded a certain length of time
- // should lock
- model.setLocked(true);
- }
- }
+
if (!Status.CANCEL_STATUS.equals(event.getJob().getResult()) && tlcJob.getExitValue() > 0) {
// if TLC crashed with exit value > 0 and the user did *not*
// click cancel, mark the job as crashed.
@@ -989,9 +957,8 @@ public class TLCModelLaunchDelegate extends LaunchConfigurationDelegate implemen
* suffix to identify it as a snapshot. The model for which it is a snapshot is identified by the
* prefix of the snapshot's model name.
*/
- final boolean takeSnapshot = TLCActivator.getDefault().getPreferenceStore()
- .getBoolean(TLCActivator.I_TLC_SNAPSHOT_PREFERENCE);
- if (!takeSnapshot || model.isSnapshot()) {
+ final int snapshotKeepCount = TLCActivator.getDefault().getPreferenceStore().getInt(TLCActivator.I_TLC_SNAPSHOT_KEEP_COUNT);
+ if (!(snapshotKeepCount > 0) || model.isSnapshot()) {
return;
}
refreshJob = new WorkspaceJob("Taking snapshot of " + model.getName() + "...") {
diff --git a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TraceExplorerDelegate.java b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TraceExplorerDelegate.java
index bd84e66712f9228a2576cb30877fb108a9793cbe..4382b591c025eac4bf61c5b2487e4c7b68b42414 100644
--- a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TraceExplorerDelegate.java
+++ b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TraceExplorerDelegate.java
@@ -286,119 +286,111 @@ public class TraceExplorerDelegate extends TLCModelLaunchDelegate implements ILa
IFile[] files = new IFile[] { tlaFile, cfgFile, outFile };
- /*
- * We want to copy spec files to the model folder only if
- * the model is not locked. Before copying, the previous spec
- * files must be deleted.
- */
- if (!model.isLocked())
+
+ /******************************************************************
+ * This code deletes all existing files in the model folder except*
+ * for the checkpoint folder, if it exists. *
+ ******************************************************************/
+ final IResource[] members = modelFolder.members();
+ // erase everything inside
+ if (members.length == 0)
{
+ monitor.worked(STEP);
+ } else
+ {
+ // Get the checkpoint folder in order to avoid
+ // deleting that folder.
+ // This ModelHelper method should return an array of
+ // size one because there should only be one checkpoint
+ // folder.
+ final IResource[] checkpoints = model.getCheckpoints(false);
- /******************************************************************
- * This code deletes all existing files in the model folder except*
- * for the checkpoint folder, if it exists. *
- ******************************************************************/
- final IResource[] members = modelFolder.members();
- // erase everything inside
- if (members.length == 0)
- {
- monitor.worked(STEP);
- } else
- {
- // Get the checkpoint folder in order to avoid
- // deleting that folder.
- // This ModelHelper method should return an array of
- // size one because there should only be one checkpoint
- // folder.
- final IResource[] checkpoints = model.getCheckpoints(false);
+ ISchedulingRule deleteRule = ResourceHelper.getDeleteRule(members);
- ISchedulingRule deleteRule = ResourceHelper.getDeleteRule(members);
+ // delete files
+ ResourcesPlugin.getWorkspace().run(new IWorkspaceRunnable() {
- // delete files
- ResourcesPlugin.getWorkspace().run(new IWorkspaceRunnable() {
+ public void run(IProgressMonitor monitor) throws CoreException
+ {
- public void run(IProgressMonitor monitor) throws CoreException
+ monitor.beginTask("Deleting files", members.length);
+ // delete the members of the target
+ // directory
+ for (int i = 0; i < members.length; i++)
{
-
- monitor.beginTask("Deleting files", members.length);
- // delete the members of the target
- // directory
- for (int i = 0; i < members.length; i++)
+ try
{
- try
- {
- if ((checkpoints.length > 0 && checkpoints[0].equals(members[i]))
- || members[i].getName().equals(ModelHelper.FILE_CFG)
- || members[i].getName().equals(ModelHelper.FILE_TLA)
- || members[i].getName().equals(ModelHelper.FILE_OUT)
- || members[i].getName().equals(ModelHelper.TE_TRACE_SOURCE)
- // Iff the model has been run with a module
- // override, then there is a .class (and
- // optionally a .java) file in the folder.
- // We must not delete the .class file.
- // The TraceExplorer won't work unless
- // the module overrides also come with a
- // pure TLA+ implementation.
- || members[i].getName().endsWith(".class")
- || members[i].getName().endsWith(".java"))
- {
- // We don't want to delete the checkpoints folder
- // or any of the MC files or the MC_TE.out file.
- continue;
- }
- members[i].delete(IResource.FORCE, new SubProgressMonitor(monitor, 1));
- } catch (CoreException e)
+ if ((checkpoints.length > 0 && checkpoints[0].equals(members[i]))
+ || members[i].getName().equals(ModelHelper.FILE_CFG)
+ || members[i].getName().equals(ModelHelper.FILE_TLA)
+ || members[i].getName().equals(ModelHelper.FILE_OUT)
+ || members[i].getName().equals(ModelHelper.TE_TRACE_SOURCE)
+ // Iff the model has been run with a module
+ // override, then there is a .class (and
+ // optionally a .java) file in the folder.
+ // We must not delete the .class file.
+ // The TraceExplorer won't work unless
+ // the module overrides also come with a
+ // pure TLA+ implementation.
+ || members[i].getName().endsWith(".class")
+ || members[i].getName().endsWith(".java"))
{
- // catch the exception if
- // deletion failed, and just
- // ignore this fact
- // FIXME this should be fixed at
- // some later point in time
- TLCActivator.logError("Error deleting a file " + members[i].getLocation(), e);
+ // We don't want to delete the checkpoints folder
+ // or any of the MC files or the MC_TE.out file.
+ continue;
}
+ members[i].delete(IResource.FORCE, new SubProgressMonitor(monitor, 1));
+ } catch (CoreException e)
+ {
+ // catch the exception if
+ // deletion failed, and just
+ // ignore this fact
+ // FIXME this should be fixed at
+ // some later point in time
+ TLCActivator.logError("Error deleting a file " + members[i].getLocation(), e);
}
- monitor.done();
}
- }, deleteRule, IWorkspace.AVOID_UPDATE, new SubProgressMonitor(monitor, STEP));
- }
- /******************************************************************
- * Finished deleting files. *
- ******************************************************************/
-
- /******************************************************************
- * This code copies all spec module files to the model folder. *
- ******************************************************************/
- monitor.subTask("Copying files");
-
- // retrieve the root file
- final IFile specRootFile = model.getSpec().getRootFile();
- if (specRootFile == null)
- {
- // root module file not found
- throw new CoreException(new Status(IStatus.ERROR, TLCActivator.PLUGIN_ID,
- "Error accessing the root module " + model.getSpec().getRootFilename()));
- }
+ monitor.done();
+ }
+ }, deleteRule, IWorkspace.AVOID_UPDATE, new SubProgressMonitor(monitor, STEP));
+ }
+ /******************************************************************
+ * Finished deleting files. *
+ ******************************************************************/
+
+ /******************************************************************
+ * This code copies all spec module files to the model folder. *
+ ******************************************************************/
+ monitor.subTask("Copying files");
+
+ // retrieve the root file
+ final IFile specRootFile = model.getSpec().getRootFile();
+ if (specRootFile == null)
+ {
+ // root module file not found
+ throw new CoreException(new Status(IStatus.ERROR, TLCActivator.PLUGIN_ID,
+ "Error accessing the root module " + model.getSpec().getRootFilename()));
+ }
- // copy
- specRootFile.copy(targetFolderPath.append(specRootFile.getProjectRelativePath()), IResource.DERIVED
- | IResource.FORCE, new SubProgressMonitor(monitor, 1));
- // find the result
- IResource specRootFileCopy = modelFolder.findMember(specRootFile.getProjectRelativePath());
+ // copy
+ specRootFile.copy(targetFolderPath.append(specRootFile.getProjectRelativePath()), IResource.DERIVED
+ | IResource.FORCE, new SubProgressMonitor(monitor, 1));
+ // find the result
+ IResource specRootFileCopy = modelFolder.findMember(specRootFile.getProjectRelativePath());
- // react if no result
- if (specRootFileCopy == null)
- {
- throw new CoreException(new Status(IStatus.ERROR, TLCActivator.PLUGIN_ID, "Error copying "
- + model.getSpec().getRootFilename() + " into " + targetFolderPath.toOSString()));
- }
+ // react if no result
+ if (specRootFileCopy == null)
+ {
+ throw new CoreException(new Status(IStatus.ERROR, TLCActivator.PLUGIN_ID, "Error copying "
+ + model.getSpec().getRootFilename() + " into " + targetFolderPath.toOSString()));
+ }
- ModelHelper.copyExtendedModuleFiles(specRootFile, targetFolderPath, monitor, STEP, project);
+ ModelHelper.copyExtendedModuleFiles(specRootFile, targetFolderPath, monitor, STEP, project);
- /******************************************************************
- * Finished copying files. *
- ******************************************************************/
+ /******************************************************************
+ * Finished copying files. *
+ ******************************************************************/
- }
/***************************************************************************
* Create the TE.tla, TE.cfg, and TE.out files if they don't exist and set *
diff --git a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/Assignment.java b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/Assignment.java
index 4583567da78e1c0dba5669fcc6374e52f4c9848a..71c7954451b72a237d504604521addb86a5b5ce4 100644
--- a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/Assignment.java
+++ b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/Assignment.java
@@ -144,6 +144,14 @@ public class Assignment extends Formula
return label;
}
+ /**
+ * @return "bar" for a assignment "frob!bar"
+ */
+ public String getLocalLabel() {
+ final int beginIndex = label.lastIndexOf("!") + 1;
+ return label.substring(beginIndex);
+ }
+
/**
* Retrieve the right part
* @return the right side of the assignment, can be <code>null</code>
diff --git a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/Model.java b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/Model.java
index 183ac571ba5cd96ad7bca7428fe335f1331c1cfa..e62fee95bc847918c7af6feeb8cdde337223ed00 100644
--- a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/Model.java
+++ b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/Model.java
@@ -29,8 +29,10 @@ package org.lamport.tla.toolbox.tool.tlc.model;
import java.io.File;
import java.io.IOException;
import java.io.InputStream;
+import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
+import java.util.Collections;
import java.util.Comparator;
import java.util.List;
import java.util.Map;
@@ -59,7 +61,7 @@ import org.eclipse.core.runtime.IProgressMonitor;
import org.eclipse.core.runtime.NullProgressMonitor;
import org.eclipse.core.runtime.Platform;
import org.eclipse.core.runtime.Status;
-import org.eclipse.core.runtime.SubProgressMonitor;
+import org.eclipse.core.runtime.SubMonitor;
import org.eclipse.core.runtime.jobs.ISchedulingRule;
import org.eclipse.debug.core.DebugPlugin;
import org.eclipse.debug.core.ILaunch;
@@ -75,9 +77,7 @@ import org.eclipse.ui.part.FileEditorInput;
import org.lamport.tla.toolbox.spec.Spec;
import org.lamport.tla.toolbox.tool.ToolboxHandle;
import org.lamport.tla.toolbox.tool.tlc.TLCActivator;
-import org.lamport.tla.toolbox.tool.tlc.launch.IConfigurationConstants;
import org.lamport.tla.toolbox.tool.tlc.launch.IModelConfigurationConstants;
-import org.lamport.tla.toolbox.tool.tlc.launch.IModelConfigurationDefaults;
import org.lamport.tla.toolbox.tool.tlc.model.Model.StateChangeListener.ChangeEvent;
import org.lamport.tla.toolbox.tool.tlc.model.Model.StateChangeListener.ChangeEvent.State;
import org.lamport.tla.toolbox.tool.tlc.traceexplorer.SimpleTLCState;
@@ -100,17 +100,13 @@ public class Model implements IModelConfigurationConstants, IAdaptable {
*/
private static final String IS_ORIGINAL_TRACE_SHOWN = "isOriginalTraceShown";
/**
- * marker on .launch file with boolean attribute modelIsRunning
+ * marker on .launch file with boolean attribute modelIsRunning; only used for historic clean-ups as of 1.5.5
*/
private static final String TLC_MODEL_IN_USE_MARKER = "org.lamport.tla.toolbox.tlc.modelMarker";
/**
* marker on .launch file, binary semantics
*/
private static final String TLC_CRASHED_MARKER = "org.lamport.tla.toolbox.tlc.crashedModelMarker";
- /**
- * model is locked by a user lock
- */
- private static final String MODEL_IS_LOCKED = "modelIsLocked";
/**
* marker on .launch file, with boolean attribute isOriginalTraceShown
*/
@@ -310,25 +306,6 @@ public class Model implements IModelConfigurationConstants, IAdaptable {
}
}
- public int getAutoLockTime() {
- try {
- return this.launchConfig.getAttribute(IConfigurationConstants.LAUNCH_AUTO_LOCK_MODEL_TIME,
- IModelConfigurationDefaults.MODEL_AUTO_LOCK_TIME_DEFAULT);
- } catch (CoreException shouldNotHappen) {
- TLCActivator.logError(shouldNotHappen.getMessage(), shouldNotHappen);
- }
- return 0;
- }
-
- public void setAutoLockTime(int autoLockTime) {
- try {
- this.launchConfig.getWorkingCopy().setAttribute(IConfigurationConstants.LAUNCH_AUTO_LOCK_MODEL_TIME,
- autoLockTime);
- } catch (CoreException shouldNotHappen) {
- TLCActivator.logError(shouldNotHappen.getMessage(), shouldNotHappen);
- }
- }
-
public String getName() {
try {
return this.launchConfig.getAttribute(ModelHelper.MODEL_NAME, (String) null);
@@ -371,14 +348,6 @@ public class Model implements IModelConfigurationConstants, IAdaptable {
notifyListener(new StateChangeListener.ChangeEvent(this, isRunning ? State.RUNNING : State.NOT_RUNNING));
}
- public boolean isLocked() {
- return isMarkerSet(TLC_MODEL_IN_USE_MARKER, MODEL_IS_LOCKED);
- }
-
- public void setLocked(boolean isLocked) {
- setMarker(TLC_MODEL_IN_USE_MARKER, MODEL_IS_LOCKED, isLocked);
- }
-
/**
* Looks up if the model has a stale marker. The stale marker is installed
* when the TLC process crashed (terminated with exit code > 0).
@@ -426,7 +395,7 @@ public class Model implements IModelConfigurationConstants, IAdaptable {
public long getSnapshotTimeStamp() {
final int idx = getName().lastIndexOf(SNAP_SHOT) + 10;
- return Long.valueOf(getName().substring(idx, getName().length()));
+ return Long.valueOf(getName().substring(idx));
}
public Collection<Model> getSnapshots() {
@@ -481,6 +450,11 @@ public class Model implements IModelConfigurationConstants, IAdaptable {
.getFolder(snapshot.getName() + File.separator + snapshot.getName() + ".dot").getLocation();
FileUtils.moveFile(oldDotFile.toFile(), newDotFile.toFile());
}
+
+ // Now that we've had a successful save, prune any snapshots, starting with the oldest, in order to assure the
+ // cardinality no greater than snapshotKeepCount.
+ pruneOldestSnapshots();
+
// Refresh the snapshot folder after having copied files without using the
// Eclipse resource API. Otherwise, the resource API does not see the files
// which e.g. results in an incomplete model deletion or hasStateGraphDump
@@ -493,6 +467,26 @@ public class Model implements IModelConfigurationConstants, IAdaptable {
return snapshot;
}
+ private void pruneOldestSnapshots() throws CoreException {
+ // Sort model by snapshot timestamp and remove oldest ones.
+ final int snapshotKeepCount = TLCActivator.getDefault().getPreferenceStore().getInt(TLCActivator.I_TLC_SNAPSHOT_KEEP_COUNT);
+ final List<Model> snapshotModels = new ArrayList<>(getSnapshots());
+ if (snapshotModels.size() > snapshotKeepCount) {
+ final int pruneCount = snapshotModels.size() - snapshotKeepCount;
+ Collections.sort(snapshotModels, new Comparator<Model>() {
+ public int compare (final Model model1, final Model model2) {
+ final long ts1 = model1.getSnapshotTimeStamp();
+ final long ts2 = model2.getSnapshotTimeStamp();
+ return Long.compare(ts1, ts2);
+ }
+ });
+ for (int i = 0; i < pruneCount; i++) {
+ final Model model = snapshotModels.get(i);
+ model.delete(new NullProgressMonitor());
+ }
+ }
+ }
+
/*
* End of snapshot related methods.
*/
@@ -672,6 +666,14 @@ public class Model implements IModelConfigurationConstants, IAdaptable {
}
public void delete(IProgressMonitor monitor) throws CoreException {
+
+ // First delete the Model's snapshots. If left undelete, they disappear from the
+ // Toolbox have to be deleted manually.
+ final Collection<Model> snapshots = getSnapshots();
+ for (Model model : snapshots) {
+ model.delete(SubMonitor.convert(monitor));
+ }
+
notifyListener(new ChangeEvent(this, State.DELETED));
final IResource[] members;
@@ -704,7 +706,7 @@ public class Model implements IModelConfigurationConstants, IAdaptable {
try {
for (int i = 0; i < members.length; i++) {
members[i].delete(IResource.FORCE,
- new SubProgressMonitor(subMonitor, 1));
+ SubMonitor.convert(subMonitor, 1));
}
} catch (CoreException e) {
TLCActivator.logError("Error deleting a file "
@@ -715,7 +717,7 @@ public class Model implements IModelConfigurationConstants, IAdaptable {
subMonitor.done();
}
}, deleteRule, IWorkspace.AVOID_UPDATE,
- new SubProgressMonitor(monitor, members.length));
+ SubMonitor.convert(monitor, members.length));
}
/**
diff --git a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/TypedSet.java b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/TypedSet.java
index 8b6bfb1f07f0c70c862d70a164821664d25fcc6f..00c183d4c6c9d2d6acbbb4ab817cd7e8ee4363d5 100644
--- a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/TypedSet.java
+++ b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/TypedSet.java
@@ -157,6 +157,10 @@ public class TypedSet
{
this.type = type;
}
+
+ public void unsetType() {
+ setType(null);
+ }
public String[] getValues()
{
diff --git a/org.lamport.tla.toolbox.uitest/META-INF/MANIFEST.MF b/org.lamport.tla.toolbox.uitest/META-INF/MANIFEST.MF
index 039a173c1b91f593f062aa74711ea86399acfd2e..e02cdafc7fb1deaa64f188e81650d972f4fac051 100644
--- a/org.lamport.tla.toolbox.uitest/META-INF/MANIFEST.MF
+++ b/org.lamport.tla.toolbox.uitest/META-INF/MANIFEST.MF
@@ -15,6 +15,7 @@ Require-Bundle: org.eclipse.swt;bundle-version="3.5.0";visibility:=reexport,
org.apache.log4j;visibility:=reexport,
org.eclipse.ui.editors;bundle-version="3.9.0",
org.eclipse.ui.forms;bundle-version="3.6.200"
+Eclipse-BundleShape: dir
Eclipse-RegisterBuddy: org.apache.log4j
Eclipse-SupplementBundle: org.lamport.tla.toolbox*
Export-Package: org.lamport.tla.toolbox.test,
diff --git a/org.lamport.tla.toolbox.uitest/build.properties b/org.lamport.tla.toolbox.uitest/build.properties
index 34d2e4d2dad529ceaeb953bfcdb63c51d69ffed2..c86a1eb2d9f308e8744d51124a7272afbbbdf55d 100644
--- a/org.lamport.tla.toolbox.uitest/build.properties
+++ b/org.lamport.tla.toolbox.uitest/build.properties
@@ -1,4 +1,6 @@
source.. = src/
output.. = bin/
bin.includes = META-INF/,\
- .
+ .,\
+ farsite/,\
+ DieHard/
diff --git a/org.lamport.tla.toolbox.uitest/src/org/lamport/tla/toolbox/test/RCPTestSetupHelper.java b/org.lamport.tla.toolbox.uitest/src/org/lamport/tla/toolbox/test/RCPTestSetupHelper.java
index b841e6d05fb420916ead7c617f496769c3309e37..4ec242ca3cebd0b02a5809ca2026fddd2f804a58 100644
--- a/org.lamport.tla.toolbox.uitest/src/org/lamport/tla/toolbox/test/RCPTestSetupHelper.java
+++ b/org.lamport.tla.toolbox.uitest/src/org/lamport/tla/toolbox/test/RCPTestSetupHelper.java
@@ -1,6 +1,13 @@
package org.lamport.tla.toolbox.test;
+import java.io.File;
+import java.io.IOException;
+import java.net.URISyntaxException;
+import java.net.URL;
+
+import org.eclipse.core.runtime.FileLocator;
import org.eclipse.core.runtime.NullProgressMonitor;
+import org.eclipse.core.runtime.Platform;
import org.eclipse.swt.widgets.Display;
import org.eclipse.swt.widgets.Shell;
import org.eclipse.swtbot.eclipse.finder.SWTWorkbenchBot;
@@ -16,11 +23,27 @@ import org.eclipse.ui.WorkbenchException;
import org.lamport.tla.toolbox.Activator;
import org.lamport.tla.toolbox.spec.Spec;
import org.lamport.tla.toolbox.spec.manager.WorkspaceSpecManager;
+import org.osgi.framework.Bundle;
/**
* @see http://www.ralfebert.de/articles/swtbot/
*/
public abstract class RCPTestSetupHelper {
+
+ public static String getAbsolutePath(final String bundle, final String fileInBundle) {
+ final Bundle b = Platform.getBundle(bundle);
+ final URL url = b.getEntry(fileInBundle);
+ try {
+ final URL resolved = FileLocator.resolve(url);
+ final File f = new File(resolved.toURI());
+ return f.getAbsolutePath();
+ } catch (final IOException e) {
+ e.printStackTrace();
+ } catch (URISyntaxException e) {
+ e.printStackTrace();
+ }
+ return null;
+ }
public static void beforeClass() {
UIThreadRunnable.syncExec(new VoidResult() {
diff --git a/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/ui/handler/OpenSpecHandler.java b/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/ui/handler/OpenSpecHandler.java
index 51bff5f682291821bcbee8830d6dea852957f363..f610ed934497d3ec68eb7f3f712f07569a0a0279 100644
--- a/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/ui/handler/OpenSpecHandler.java
+++ b/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/ui/handler/OpenSpecHandler.java
@@ -8,7 +8,6 @@ import org.eclipse.core.runtime.IProgressMonitor;
import org.eclipse.core.runtime.IStatus;
import org.eclipse.core.runtime.Status;
import org.eclipse.core.runtime.jobs.Job;
-import org.eclipse.jface.viewers.AbstractTreeViewer;
import org.eclipse.ui.part.FileEditorInput;
import org.eclipse.ui.progress.UIJob;
import org.lamport.tla.toolbox.Activator;
@@ -81,8 +80,7 @@ public class OpenSpecHandler extends AbstractHandler implements IHandler
// Expand the spec's subitems (modules & models group and their subitems).
// getViewer() cannot return null here. After all, this listener
// is handling its double-click event.
- ToolboxExplorer.getViewer().expandToLevel(spec, AbstractTreeViewer.ALL_LEVELS);
-
+ ToolboxExplorer.getViewer().expandToLevel(spec, ToolboxExplorer.DEFAULT_EXPAND_LEVEL);
return Status.OK_STATUS;
}
};
diff --git a/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/ui/navigator/ToolboxExplorer.java b/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/ui/navigator/ToolboxExplorer.java
index cf3277a5e42ca465313f7700ecc91999e8c2cc09..d2dae9682ee12c779b67e61e845b65546cd71f14 100644
--- a/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/ui/navigator/ToolboxExplorer.java
+++ b/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/ui/navigator/ToolboxExplorer.java
@@ -28,7 +28,6 @@ package org.lamport.tla.toolbox.ui.navigator;
import java.util.HashMap;
import java.util.Map;
-import org.eclipse.jface.viewers.AbstractTreeViewer;
import org.eclipse.jface.viewers.DoubleClickEvent;
import org.eclipse.jface.viewers.IStructuredSelection;
import org.eclipse.ui.IViewPart;
@@ -50,6 +49,10 @@ public class ToolboxExplorer extends CommonNavigator
public final static String VIEW_ID = "toolbox.view.ToolboxExplorer";
public static final String COMMAND_ID = "toolbox.command.cnf.open.delegate";
+ // first level is spec and model group, second level actual specs and models,
+ // third level are model snapshots which we hide by default.
+ public static final int DEFAULT_EXPAND_LEVEL = 2;
+
/**
* Override the method to deliver the root object for the NCE activation
*/
@@ -111,7 +114,7 @@ public class ToolboxExplorer extends CommonNavigator
if (navigator != null)
{
final CommonViewer commonViewer = navigator.getCommonViewer();
- commonViewer.setAutoExpandLevel(AbstractTreeViewer.ALL_LEVELS);
+ commonViewer.setAutoExpandLevel(DEFAULT_EXPAND_LEVEL);
return commonViewer;
}
diff --git a/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/ui/navigator/ToolboxExplorerResourceListener.java b/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/ui/navigator/ToolboxExplorerResourceListener.java
index cb5322012d60418a881fc4f60f688e13f53f9df5..eafb76dc3ad39f97728f32c151c20edd48262852 100644
--- a/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/ui/navigator/ToolboxExplorerResourceListener.java
+++ b/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/ui/navigator/ToolboxExplorerResourceListener.java
@@ -29,7 +29,6 @@ import org.eclipse.core.resources.IResourceChangeEvent;
import org.eclipse.core.resources.IResourceChangeListener;
import org.eclipse.core.resources.IWorkspace;
import org.eclipse.core.resources.ResourcesPlugin;
-import org.eclipse.jface.viewers.AbstractTreeViewer;
import org.eclipse.ui.navigator.CommonViewer;
import org.lamport.tla.toolbox.Activator;
import org.lamport.tla.toolbox.lifecycle.ToolboxLifecycleParticipant;
@@ -62,8 +61,7 @@ public class ToolboxExplorerResourceListener extends ToolboxLifecycleParticipant
// Afterwards, the users expanded states is preserved.
if (event == null && viewer != null) { // viewer might already be disposed which happens when the Toolbox shuts down.
final Spec specLoaded = Activator.getSpecManager().getSpecLoaded();
- viewer.expandToLevel(specLoaded,
- AbstractTreeViewer.ALL_LEVELS);
+ viewer.expandToLevel(specLoaded, ToolboxExplorer.DEFAULT_EXPAND_LEVEL);
}
}
});
diff --git a/pom.xml b/pom.xml
index 5d0673f2f11b0ae74c5dac57558c5c1ac901134c..473967c499e40f8ec44595b1cef7d61754b7d822 100644
--- a/pom.xml
+++ b/pom.xml
@@ -66,6 +66,7 @@
<module>org.lamport.tla.toolbox.feature.prover</module>
<module>org.lamport.tla.toolbox.feature.tla2tex</module>
<module>org.lamport.tla.toolbox.feature.tlc</module>
+ <module>org.lamport.tla.toolbox.feature.uitest</module>
<module>org.lamport.tla.toolbox.feature.branding</module>
<module>org.lamport.tla.toolbox.feature.standalone</module>
@@ -125,8 +126,41 @@
<version>${tycho-version}</version>
<extensions>true</extensions>
</plugin>
- <plugin>
- <groupId>org.eclipse.tycho</groupId>
+ <!-- Compress Toolbox plugins -->
+ <plugin>
+ <groupId>org.eclipse.tycho.extras</groupId>
+ <artifactId>tycho-pack200b-plugin</artifactId>
+ <version>${tycho-version}</version>
+ <executions>
+ <execution>
+ <id>pack200-pack</id>
+ <goals>
+ <goal>pack</goal>
+ </goals>
+ </execution>
+ </executions>
+ </plugin>
+ <!-- Then, alter p2-metadata to make the .pack.gz
+ artifact visible from other modules -->
+ <plugin>
+ <groupId>org.eclipse.tycho</groupId>
+ <artifactId>tycho-p2-plugin</artifactId>
+ <version>${tycho-version}</version>
+ <executions>
+ <execution>
+ <id>p2-metadata</id>
+ <goals>
+ <goal>p2-metadata</goal>
+ </goals>
+ <phase>package</phase>
+ </execution>
+ </executions>
+ <configuration>
+ <defaultP2Metadata>false</defaultP2Metadata>
+ </configuration>
+ </plugin>
+ <plugin>
+ <groupId>org.eclipse.tycho</groupId>
<artifactId>tycho-compiler-plugin</artifactId>
<version>${tycho-version}</version>
<configuration>
@@ -173,7 +207,7 @@
</execution>
</executions>
</plugin>
- <plugin>
+ <plugin>
<groupId>org.eclipse.tycho</groupId>
<artifactId>target-platform-configuration</artifactId>
<version>${tycho-version}</version>
@@ -181,6 +215,10 @@
<!-- recommended: use p2-based target platform resolver -->
<resolver>p2</resolver>
<ignoreTychoRepositories>true</ignoreTychoRepositories>
+ <!-- Include the pack200 artifacts in the p2 repository. This increases
+ the size of the p2 repository (jars + pack.gz), but reduces the load on the
+ server hosting the repository as clients download the compressed pack.gz files. -->
+ <includePackedArtifacts>true</includePackedArtifacts>
<!-- use existing target platform definition -->
<target>
<artifact>
diff --git a/tlatools/customBuild.xml b/tlatools/customBuild.xml
index eca525a62ab7ff4dc0f0547f5a6fe95afcf8aa97..5da1c0ff2a7263c8f87cb22efcb85c4c0b86a43e 100644
--- a/tlatools/customBuild.xml
+++ b/tlatools/customBuild.xml
@@ -193,8 +193,23 @@
<!-- create a JAR file for the users -->
<mkdir dir="${dist.dir}" />
- <jar destfile="${dist.file}">
- <fileset dir="${class.dir}" includes="**/*" />
+ <jar destfile="${dist.file}" level="9">
+ <fileset dir="${class.dir}" includes="**/*" excludes="
+ **/*.jpg,
+ tlc2/tool/fp/*.tla,
+ pcal/*.tla,
+ META-INF/maven/,
+ src/tla2sany/parser/ParseException.09-09-07,
+ src/tla2sany/parser/TLAplusParser.09-07-02,
+ src/tla2sany/parser/TLAplusParser.11-02-10,
+ src/tla2sany/parser/TLAplusParserConstants.09-07-02,
+ src/tla2sany/parser/TLAplusParserConstants.09-09-07,
+ src/tla2sany/parser/TLAplusParserConstants.11-02-10,
+ src/tla2sany/parser/TLAplusParserTokenManager.09-07-02,
+ src/tla2sany/parser/TLAplusParserTokenManager.09-09-07,
+ src/tla2sany/parser/TLAplusParserTokenManager.11-02-10,
+ src/tla2sany/parser/Token.09-09-07,
+ src/tla2sany/parser/TokenMgrError.09-09-07"/>
<manifest>
<attribute name="Built-By" value="${user.name}" />
<attribute name="Build-Tag" value="${env.BUILD_TAG}" />
diff --git a/tlatools/src/tla2sany/explorer/ExploreNode.java b/tlatools/src/tla2sany/explorer/ExploreNode.java
index 81df5d3aa8594d943c39ab8434fb432b3b61331e..8598632c5381e3d4f9bc67516e1052dd4dbf05d9 100644
--- a/tlatools/src/tla2sany/explorer/ExploreNode.java
+++ b/tlatools/src/tla2sany/explorer/ExploreNode.java
@@ -21,7 +21,8 @@ public interface ExploreNode {
* descendant foo. *
***********************************************************************/
public String levelDataToString();
- public void walkGraph(Hashtable semNodesTable);
+
+ public void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable);
/***********************************************************************
* This method is apparently supposed to insert an entry in *
* semNodesTable for itself and every descendant in the semantic tree *
diff --git a/tlatools/src/tla2sany/semantic/APSubstInNode.java b/tlatools/src/tla2sany/semantic/APSubstInNode.java
index f8af1db14f9bf1adb4ed13681d5b42f25f48e0f1..eb9a2dc6339fa8779a18e648e34ec97a61a47dda 100644
--- a/tlatools/src/tla2sany/semantic/APSubstInNode.java
+++ b/tlatools/src/tla2sany/semantic/APSubstInNode.java
@@ -21,9 +21,11 @@ import java.util.HashSet;
import java.util.Hashtable;
import java.util.Iterator;
+import tla2sany.explorer.ExploreNode;
import tla2sany.st.TreeNode;
import tla2sany.utilities.Strings;
import tla2sany.utilities.Vector;
+import tla2sany.xml.SymbolContext;
import util.UniqueString;
import org.w3c.dom.Document;
@@ -193,7 +195,8 @@ public class APSubstInNode extends LevelNode {
* to this method can contain a mixture of explicit and implicit
* substitutions
*/
- final void addExplicitSubstitute(Context instanceeCtxt, UniqueString lhs,
+ @SuppressWarnings("unused") // TODO final else block is dead code
+ final void addExplicitSubstitute(Context instanceCtxt, UniqueString lhs,
TreeNode stn, ExprOrOpArgNode sub) {
int index;
for (index = 0; index < this.substs.length; index++) {
@@ -221,7 +224,7 @@ public class APSubstInNode extends LevelNode {
// the instancee context
// look up the lhs symbol in the instancee context
- SymbolNode lhsSymbol = instanceeCtxt.getSymbol(lhs);
+ SymbolNode lhsSymbol = instanceCtxt.getSymbol(lhs);
// lhs must be an OpDeclNode; if not just return, as this error
// will have been earlier, though semantic analysis was allowed
@@ -288,6 +291,7 @@ public class APSubstInNode extends LevelNode {
// private SetOfArgLevelConstraints argLevelConstraints;
// private HashSet argLevelParams;
+ @Override
public final boolean levelCheck(int itr) {
if (this.levelChecked >= itr) return this.levelCorrect;
this.levelChecked = itr ;
@@ -308,7 +312,7 @@ public class APSubstInNode extends LevelNode {
// Calculate the level information
this.level = this.body.getLevel();
- HashSet lpSet = this.body.getLevelParams();
+ HashSet<SymbolNode> lpSet = this.body.getLevelParams();
for (int i = 0; i < this.substs.length; i++) {
if (lpSet.contains(this.getSubFor(i))) {
this.level = Math.max(level, this.getSubWith(i).getLevel());
@@ -316,10 +320,9 @@ public class APSubstInNode extends LevelNode {
}
// this.levelParams = new HashSet();
- Iterator iter = lpSet.iterator();
+ Iterator<SymbolNode> iter = lpSet.iterator();
while (iter.hasNext()) {
- Object param = iter.next();
- this.levelParams.addAll(Subst.paramSet(param, this.substs));
+ this.levelParams.addAll(Subst.paramSet(iter.next(), this.substs));
/*******************************************************************
* At this point, levelCheck(itr) has been invoked on *
* this.substs[i].getExpr() (which equals this.getSubWith(i)). *
@@ -331,11 +334,10 @@ public class APSubstInNode extends LevelNode {
* this.levelParams to compute this.allParams, except using *
* Subst.allParamSet instead of Subst.paramSet. *
***********************************************************************/
- HashSet apSet = this.body.getAllParams();
+ HashSet<SymbolNode> apSet = this.body.getAllParams();
iter = apSet.iterator();
while (iter.hasNext()) {
- Object param = iter.next();
- this.allParams.addAll(Subst.allParamSet(param, this.substs));
+ this.allParams.addAll(Subst.allParamSet(iter.next(), this.substs));
/*******************************************************************
* At this point, levelCheck(itr) has been invoked on *
* this.substs[i].getExpr() (which equals this.getSubWith(i)). *
@@ -392,6 +394,7 @@ public class APSubstInNode extends LevelNode {
// "ArgLevelParams: " + this.argLevelParams + "\n" ;
// }
+ @Override
public final String toString(int depth) {
if (depth <= 0) return "";
@@ -421,6 +424,7 @@ public class APSubstInNode extends LevelNode {
* The children of this node are the body and the expressions
* being substituted for symbols.
*/
+ @Override
public SemanticNode[] getChildren() {
SemanticNode[] res = new SemanticNode[this.substs.length + 1];
res[0] = this.body;
@@ -430,11 +434,12 @@ public class APSubstInNode extends LevelNode {
return res;
}
- public final void walkGraph(Hashtable semNodesTable) {
+ @Override
+ public final void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
- semNodesTable.put(new Integer(myUID), this);
+ semNodesTable.put(uid, this);
if (this.substs != null) {
for (int i = 0; i < this.substs.length; i++) {
@@ -445,16 +450,29 @@ public class APSubstInNode extends LevelNode {
return;
}
- protected Element getLevelElement(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ protected Element getLevelElement(Document doc, SymbolContext context) {
Element sbts = doc.createElement("substs");
for (int i=0; i<substs.length; i++) {
sbts.appendChild(substs[i].export(doc, context));
}
Element bdy = doc.createElement("body");
bdy.appendChild(body.export(doc,context));
+
+ Element from = doc.createElement("instFrom");
+ Element fromchild = this.instantiatingModule.export(doc, context);
+ from.appendChild(fromchild);
+
+ Element to = doc.createElement("instTo");
+ Element tochild = instantiatedModule.export(doc,context);
+ to.appendChild(tochild);
+
+
Element ret = doc.createElement("APSubstInNode");
ret.appendChild(sbts);
ret.appendChild(bdy);
+ ret.appendChild(from);
+ ret.appendChild(to);
// at the end, we append the context of the symbols used in this node
//ret.appendChild(context.export(doc));
diff --git a/tlatools/src/tla2sany/semantic/AnyDefNode.java b/tlatools/src/tla2sany/semantic/AnyDefNode.java
index 490c3d56262dd6f61cb63afa21766a9e55c503a8..fe0201b3a7fff9a755e529facf31227e33144c74 100644
--- a/tlatools/src/tla2sany/semantic/AnyDefNode.java
+++ b/tlatools/src/tla2sany/semantic/AnyDefNode.java
@@ -39,14 +39,14 @@ public interface AnyDefNode {
public boolean getOpLevelCond(int i, int j, int k) ;
public int getLevel() ;
public int getWeight(int i) ;
- public HashSet getLevelParams() ;
- public HashSet getAllParams() ;
- public HashSet getNonLeibnizParams() ;
+ public HashSet<SymbolNode> getLevelParams() ;
+ public HashSet<SymbolNode> getAllParams() ;
+ public HashSet<SymbolNode> getNonLeibnizParams() ;
public int getArity() ;
public boolean[] getIsLeibnizArg() ;
public boolean getIsLeibniz() ;
public SetOfLevelConstraints getLevelConstraints() ;
- public HashSet getArgLevelParams() ;
+ public HashSet<ArgLevelParam> getArgLevelParams() ;
public SetOfArgLevelConstraints getArgLevelConstraints() ;
public FormalParamNode[] getParams() ;
}
diff --git a/tlatools/src/tla2sany/semantic/AssumeNode.java b/tlatools/src/tla2sany/semantic/AssumeNode.java
index 6077e82931eb3b86c9f84d74dc8799866b49ce95..040ff65ca1fee049a605b83ceacf5d27c0c281f6 100644
--- a/tlatools/src/tla2sany/semantic/AssumeNode.java
+++ b/tlatools/src/tla2sany/semantic/AssumeNode.java
@@ -5,11 +5,10 @@ package tla2sany.semantic;
import java.util.HashSet;
import java.util.Hashtable;
+import tla2sany.explorer.ExploreNode;
import tla2sany.st.TreeNode;
import tla2sany.utilities.Strings;
-
-import tla2sany.xml.XMLExportable;
-import org.w3c.dom.Attr;
+import tla2sany.xml.SymbolContext;
import org.w3c.dom.Document;
import org.w3c.dom.Element;
import org.w3c.dom.Node;
@@ -81,6 +80,7 @@ public AssumeNode(TreeNode stn, ExprNode expr, ModuleNode mn,
/* Level checking */
int levelChecked = 0 ;
+ @Override
public final boolean levelCheck(int iter) {
if (levelChecked >= iter) {return true ;} ;
levelChecked = iter;
@@ -103,33 +103,40 @@ public AssumeNode(TreeNode stn, ExprNode expr, ModuleNode mn,
return res;
}
+ @Override
public final int getLevel() {
return this.assumeExpr.getLevel();
}
- public final HashSet getLevelParams() {
+ @Override
+ public final HashSet<SymbolNode> getLevelParams() {
return this.assumeExpr.getLevelParams();
}
- public final HashSet getAllParams() {
+ @Override
+ public final HashSet<SymbolNode> getAllParams() {
return this.assumeExpr.getAllParams();
}
+ @Override
public final SetOfLevelConstraints getLevelConstraints() {
return this.assumeExpr.getLevelConstraints();
}
+ @Override
public final SetOfArgLevelConstraints getArgLevelConstraints() {
return this.assumeExpr.getArgLevelConstraints();
}
- public final HashSet getArgLevelParams() {
+ @Override
+ public final HashSet<ArgLevelParam> getArgLevelParams() {
return this.assumeExpr.getArgLevelParams();
}
/**
* toString(), levelDataToString(), and walkGraph() methods
*/
+ @Override
public final String levelDataToString() {
return "Level: " + getLevel() + "\n" +
"LevelParameters: " + getLevelParams() + "\n" +
@@ -143,6 +150,7 @@ public AssumeNode(TreeNode stn, ExprNode expr, ModuleNode mn,
* interface; depth parameter is a bound on the depth of the portion
* of the tree that is displayed.
*/
+ @Override
public final String toString (int depth) {
if (depth <= 0) return "";
String res =
@@ -165,6 +173,7 @@ public AssumeNode(TreeNode stn, ExprNode expr, ModuleNode mn,
* The assume expression is the node's only child.
*/
+ @Override
public SemanticNode[] getChildren() {
return new SemanticNode[] {this.assumeExpr};
}
@@ -174,7 +183,8 @@ public AssumeNode(TreeNode stn, ExprNode expr, ModuleNode mn,
* inserts them in the Hashtable semNodesTable for use by the
* Explorer tool.
*/
- public final void walkGraph (Hashtable semNodesTable) {
+ @Override
+ public final void walkGraph (Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
@@ -185,7 +195,7 @@ public AssumeNode(TreeNode stn, ExprNode expr, ModuleNode mn,
/* MR: This is the same as SymbolNode.exportDefinition. Exports the actual theorem content, not only a reference.
*/
- public Element exportDefinition(Document doc, tla2sany.xml.SymbolContext context) {
+ public Element exportDefinition(Document doc, SymbolContext context) {
if (!context.isTop_level_entry())
throw new IllegalArgumentException("Exporting theorem ref "+getNodeRef()+" twice!");
context.resetTop_level_entry();
@@ -226,7 +236,8 @@ public AssumeNode(TreeNode stn, ExprNode expr, ModuleNode mn,
// return getDef().export(doc,context);
// }
- protected Element getLevelElement(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ protected Element getLevelElement(Document doc, SymbolContext context) {
Element e = doc.createElement("AssumeNode");
if (def != null) {
//if there is a definition, export it too
@@ -242,7 +253,8 @@ public AssumeNode(TreeNode stn, ExprNode expr, ModuleNode mn,
}
/* overrides LevelNode.export and exports a UID reference instad of the full version*/
- public Element export(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ public Element export(Document doc, SymbolContext context) {
// first add symbol to context
context.put(this, doc);
Element e = doc.createElement(getNodeRef());
diff --git a/tlatools/src/tla2sany/semantic/AssumeProveNode.java b/tlatools/src/tla2sany/semantic/AssumeProveNode.java
index d2fd8dda8d60b187a9cdc605566843412d6abec3..fda59621bcd30291d4d4e0e800c1ad1c321c179e 100644
--- a/tlatools/src/tla2sany/semantic/AssumeProveNode.java
+++ b/tlatools/src/tla2sany/semantic/AssumeProveNode.java
@@ -6,8 +6,10 @@ package tla2sany.semantic;
import java.util.Hashtable;
+import tla2sany.explorer.ExploreNode;
import tla2sany.st.TreeNode;
import tla2sany.utilities.Strings;
+import tla2sany.xml.SymbolContext;
import org.w3c.dom.Document;
import org.w3c.dom.Element;
@@ -191,6 +193,7 @@ public class AssumeProveNode extends LevelNode {
* compute the level-related fields for an OpApplNode. This seems *
* reasonable, but I don't know if it's really correct. - LL *
*************************************************************************/
+ @Override
public boolean levelCheck(int iter) {
/***********************************************************************
* Return immediately if this this.levelCheck(i) has already been *
@@ -337,6 +340,7 @@ public class AssumeProveNode extends LevelNode {
/**
* The children of this node are the assumes and prove expressions.
*/
+ @Override
public SemanticNode[] getChildren() {
SemanticNode[] res = new SemanticNode[this.assumes.length + 1];
res[assumes.length] = this.prove;
@@ -346,7 +350,8 @@ public class AssumeProveNode extends LevelNode {
return res;
}
- public final void walkGraph(Hashtable h) {
+ @Override
+ public final void walkGraph(Hashtable<Integer, ExploreNode> h) {
Integer uid = new Integer(myUID);
if (h.get(uid) != null) return;
h.put(uid, this);
@@ -363,6 +368,7 @@ public class AssumeProveNode extends LevelNode {
* Displays this node as a String, implementing ExploreNode interface; depth
* parameter is a bound on the depth of the portion of the tree that is displayed.
*/
+ @Override
public final String toString(int depth) {
if (depth <= 0) return "";
String assumeStr = "" ;
@@ -385,7 +391,8 @@ public class AssumeProveNode extends LevelNode {
* End fields and methods implementing the ExplorerNode interface: *
*************************************************************************/
- public Element getLevelElement(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ public Element getLevelElement(Document doc, SymbolContext context) {
Element e = doc.createElement("AssumeProveNode");
Element antecedent = doc.createElement("assumes");
Element succedent = doc.createElement("prove");
diff --git a/tlatools/src/tla2sany/semantic/AtNode.java b/tlatools/src/tla2sany/semantic/AtNode.java
index 8c9d253caa9c63ec715a356ba0e78584b9365821..90aee12b081063bf0607ac581c4411d0033e8658 100644
--- a/tlatools/src/tla2sany/semantic/AtNode.java
+++ b/tlatools/src/tla2sany/semantic/AtNode.java
@@ -4,7 +4,9 @@ package tla2sany.semantic;
import java.util.Hashtable;
+import tla2sany.explorer.ExploreNode;
import tla2sany.utilities.Strings;
+import tla2sany.xml.SymbolContext;
import org.w3c.dom.Document;
import org.w3c.dom.Element;
@@ -72,6 +74,7 @@ public class AtNode extends ExprNode {
// private SetOfArgLevelConstraints argLevelConstraints;
// private HashSet argLevelParams;
+ @Override
public final boolean levelCheck(int iter) {
if (this.levelChecked >= iter) return true;
this.levelChecked = iter;
@@ -147,7 +150,8 @@ public class AtNode extends ExprNode {
* walkGraph finds all reachable nodes in the semantic graph
* and inserts them in the Hashtable semNodesTable for use by the Explorer tool.
*/
- public final void walkGraph(Hashtable h) {
+ @Override
+ public final void walkGraph(Hashtable<Integer, ExploreNode> h) {
// Empty because there are no nodes reachable through an AtNode that are not
// reachable by other paths through the semantic graph.
} // end walkGraph()
@@ -157,6 +161,7 @@ public class AtNode extends ExprNode {
* Displays this node as a String, implementing ExploreNode interface; depth
* parameter is a bound on the depth of the portion of the tree that is displayed.
*/
+ @Override
public final String toString(int depth) {
if (depth <= 0) return "";
return "\n*AtNode: " + super.toString(depth) +
@@ -164,7 +169,8 @@ public class AtNode extends ExprNode {
"\nExceptComponent: " + exceptComponentRef.getUid());
}
- protected Element getLevelElement(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ protected Element getLevelElement(Document doc, SymbolContext context) {
Element e = doc.createElement("AtNode");
SemanticNode exceptObj = exceptRef.getArgs()[0];
SemanticNode exceptComponents = exceptComponentRef.getArgs()[0];
diff --git a/tlatools/src/tla2sany/semantic/Context.java b/tlatools/src/tla2sany/semantic/Context.java
index c0a321ad7f5c5cb721add5ec47e89bcd43fb0f73..0f7f8e3e538574cc617b40af71230e776f80c271 100644
--- a/tlatools/src/tla2sany/semantic/Context.java
+++ b/tlatools/src/tla2sany/semantic/Context.java
@@ -506,11 +506,11 @@ public class Context implements ExploreNode {
return ctxtEntries;
}
- public void walkGraph(Hashtable semNodesTable) {
+ public void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
UniqueString key;
- Enumeration Enum = table.keys();
+ Enumeration<?> e = table.keys();
- while (Enum.hasMoreElements()) {
+ while (e.hasMoreElements()) {
/*********************************************************************
* Bug fix attempted by LL on 19 Apr 2007. *
* *
@@ -524,7 +524,7 @@ public class Context implements ExploreNode {
* getContextEntryStringVector later on. I decided to stop wasting *
* time on this. *
*********************************************************************/
- Object next = Enum.nextElement();
+ Object next = e.nextElement();
if (next instanceof SymbolTable.ModuleName) {
key = ((SymbolTable.ModuleName) next).name ;
System.out.println("Bug in debugging caused by inner module " +
diff --git a/tlatools/src/tla2sany/semantic/DecimalNode.java b/tlatools/src/tla2sany/semantic/DecimalNode.java
index 61995d1146a709ba0e0ae972a5ef84c906465120..b767ee0850624aec769bf0cc4989333f9c7e0639 100644
--- a/tlatools/src/tla2sany/semantic/DecimalNode.java
+++ b/tlatools/src/tla2sany/semantic/DecimalNode.java
@@ -5,7 +5,9 @@ package tla2sany.semantic;
import java.math.BigDecimal;
import java.util.Hashtable;
+import tla2sany.explorer.ExploreNode;
import tla2sany.st.TreeNode;
+import tla2sany.xml.SymbolContext;
import org.w3c.dom.Document;
import org.w3c.dom.Element;
@@ -67,9 +69,11 @@ public class DecimalNode extends ExprNode {
* Returns the value as a string, exactly the way the user typed it--e.g.,
* without any normalization, removal of leading or trailing zero's, etc.
*/
+ @Override
public final String toString() { return this.image; }
/* Level checking */
+ @Override
public final boolean levelCheck(int iter) {
levelChecked = iter;
/*********************************************************************
@@ -109,11 +113,12 @@ public class DecimalNode extends ExprNode {
* inserts them in the Hashtable semNodesTable for use by the
* Explorer tool.
*/
- public final void walkGraph(Hashtable semNodesTable) {
+ @Override
+ public final void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
- semNodesTable.put(new Integer(myUID), this);
+ semNodesTable.put(uid, this);
}
/**
@@ -121,6 +126,7 @@ public class DecimalNode extends ExprNode {
* interface; depth parameter is a bound on the depth of the portion
* of the tree that is displayed.
*/
+ @Override
public final String toString(int depth) {
if (depth <= 0) return "";
return( "\n*DecimalNode" + super.toString(depth) + "Mantissa: "
@@ -130,7 +136,8 @@ public class DecimalNode extends ExprNode {
);
}
- protected Element getLevelElement(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ protected Element getLevelElement(Document doc, SymbolContext context) {
Element e = doc.createElement("DecimalNode");
if (bigVal != null) {
e.appendChild(appendText(doc,"mantissa",bigVal.unscaledValue().toString()));
diff --git a/tlatools/src/tla2sany/semantic/DefStepNode.java b/tlatools/src/tla2sany/semantic/DefStepNode.java
index 05bb98e47b2480241f41e61331ed9448dfcccb76..a17463c1da92f06e85058c41dbedde45a6001fde 100644
--- a/tlatools/src/tla2sany/semantic/DefStepNode.java
+++ b/tlatools/src/tla2sany/semantic/DefStepNode.java
@@ -3,8 +3,10 @@ package tla2sany.semantic;
import java.util.Hashtable;
+import tla2sany.explorer.ExploreNode;
import tla2sany.st.TreeNode;
import tla2sany.utilities.Strings;
+import tla2sany.xml.SymbolContext;
import util.UniqueString;
import org.w3c.dom.Document;
@@ -47,6 +49,7 @@ public class DefStepNode extends LevelNode {
public UniqueString getStepNumber() {return stepNumber ;}
public OpDefNode[] getDefs() {return defs;}
+ @Override
public boolean levelCheck(int iter) {
/***********************************************************************
* Level check the steps and the instantiated modules coming from *
@@ -55,15 +58,17 @@ public class DefStepNode extends LevelNode {
return this.levelCheckSubnodes(iter, defs) ;
}
- public void walkGraph(Hashtable semNodesTable) {
+ @Override
+ public void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
- semNodesTable.put(new Integer(myUID), this);
+ semNodesTable.put(uid, this);
for (int i = 0; i < defs.length; i++) {
defs[i].walkGraph(semNodesTable);
} ;
}
+ @Override
public SemanticNode[] getChildren() {
SemanticNode[] res = new SemanticNode[defs.length];
for (int i = 0; i < defs.length; i++) {
@@ -71,6 +76,8 @@ public class DefStepNode extends LevelNode {
}
return res;
}
+
+ @Override
public String toString(int depth) {
if (depth <= 0) return "";
String ret = "\n*DefStepNode:\n"
@@ -82,7 +89,8 @@ public class DefStepNode extends LevelNode {
return ret;
}
- protected Element getLevelElement(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ protected Element getLevelElement(Document doc, SymbolContext context) {
Element e = doc.createElement("DefStepNode");
for (int i=0; i<defs.length;i++) {
e.appendChild(defs[i].export(doc,context));
diff --git a/tlatools/src/tla2sany/semantic/ExternalModuleTable.java b/tlatools/src/tla2sany/semantic/ExternalModuleTable.java
index 4a208f93b33d48482cf21d56aee097a5bfdbd56b..446c1f086955827aca0247c9d8e32bc8b0f562a0 100644
--- a/tlatools/src/tla2sany/semantic/ExternalModuleTable.java
+++ b/tlatools/src/tla2sany/semantic/ExternalModuleTable.java
@@ -49,7 +49,7 @@ public class ExternalModuleTable implements ExploreNode {
*/
public String levelDataToString() { return "Dummy level string"; }
- public void walkGraph(Hashtable moduleNodesTable) {
+ public void walkGraph(Hashtable<Integer, ExploreNode> moduleNodesTable) {
if (moduleNode != null) moduleNode.walkGraph(moduleNodesTable);
if (ctxt != null) ctxt.walkGraph(moduleNodesTable);
} // end walkGraph()
@@ -137,6 +137,7 @@ public class ExternalModuleTable implements ExploreNode {
}
}
+ @Override
public String toString() {
Enumeration Enum = moduleHashTable.elements();
String ret = "";
@@ -186,7 +187,7 @@ public class ExternalModuleTable implements ExploreNode {
return ret;
}
- public void walkGraph(Hashtable moduleNodesTable) {
+ public void walkGraph(Hashtable<Integer, ExploreNode> moduleNodesTable) {
Enumeration Enum = moduleHashTable.elements();
while ( Enum.hasMoreElements() ) {
diff --git a/tlatools/src/tla2sany/semantic/FormalParamNode.java b/tlatools/src/tla2sany/semantic/FormalParamNode.java
index 262db8715291eb8d6af6fda8daf56c58e00112ba..eff6a45af42ad5c7637c520541b8f8031132d795 100644
--- a/tlatools/src/tla2sany/semantic/FormalParamNode.java
+++ b/tlatools/src/tla2sany/semantic/FormalParamNode.java
@@ -4,7 +4,9 @@ package tla2sany.semantic;
import java.util.Hashtable;
+import tla2sany.explorer.ExploreNode;
import tla2sany.st.TreeNode;
+import tla2sany.xml.SymbolContext;
import util.UniqueString;
import org.w3c.dom.Document;
@@ -67,6 +69,7 @@ public class FormalParamNode extends SymbolNode {
/* Level checking */
// private HashSet levelParams;
+ @Override
public final boolean levelCheck(int iter) {
if (levelChecked == 0) {
/*********************************************************************
@@ -111,13 +114,15 @@ public class FormalParamNode extends SymbolNode {
// "ArgLevelParams: " + this.getArgLevelParams() + "\n" ;
// }
- public final void walkGraph(Hashtable semNodesTable) {
+ @Override
+ public final void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
- semNodesTable.put(new Integer(myUID), this);
+ semNodesTable.put(uid, this);
}
+ @Override
public final String toString(int depth) {
if (depth <= 0) return "";
return ("\n*FormalParamNode: " + this.getName().toString() +
@@ -128,7 +133,7 @@ public class FormalParamNode extends SymbolNode {
return "FormalParamNodeRef";
}
- protected Element getSymbolElement(Document doc, tla2sany.xml.SymbolContext context) {
+ protected Element getSymbolElement(Document doc, SymbolContext context) {
Element e = doc.createElement("FormalParamNode");
e.appendChild(appendText(doc,"uniquename",getName().toString()));
e.appendChild(appendText(doc,"arity",Integer.toString(getArity())));
diff --git a/tlatools/src/tla2sany/semantic/LabelNode.java b/tlatools/src/tla2sany/semantic/LabelNode.java
index 38c6c0db179f194bca9206f6d248a7237def82b4..e5aed3b70f9f9b2b9d45841dbef39b6bceb2999b 100644
--- a/tlatools/src/tla2sany/semantic/LabelNode.java
+++ b/tlatools/src/tla2sany/semantic/LabelNode.java
@@ -46,6 +46,7 @@ import tla2sany.parser.SyntaxTreeNode;
import tla2sany.st.TreeNode;
import tla2sany.utilities.Strings;
import tla2sany.utilities.Vector;
+import tla2sany.xml.SymbolContext;
import util.UniqueString;
import util.WrongInvocationException;
@@ -214,6 +215,7 @@ public class LabelNode extends ExprNode
/*************************************************************************
* Level-Checking. *
*************************************************************************/
+ @Override
public final boolean levelCheck(int iter) {
if (levelChecked >= iter) {return true ;} ;
levelChecked = iter;
@@ -224,37 +226,43 @@ public class LabelNode extends ExprNode
return this.body.levelCheck(iter) && retVal ;
}
+ @Override
public final int getLevel() {
if (levelChecked == 0)
{throw new WrongInvocationException("getLevel called for TheoremNode before levelCheck");};
return this.body.getLevel();
}
- public final HashSet getLevelParams() {
+ @Override
+ public final HashSet<SymbolNode> getLevelParams() {
if (levelChecked == 0)
{throw new WrongInvocationException("getLevelParams called for ThmNode before levelCheck");};
return this.body.getLevelParams();
}
- public final HashSet getAllParams() {
+ @Override
+ public final HashSet<SymbolNode> getAllParams() {
if (levelChecked == 0)
{throw new WrongInvocationException("getAllParams called for ThmNode before levelCheck");};
return this.body.getAllParams();
}
+ @Override
public final SetOfLevelConstraints getLevelConstraints() {
if (levelChecked == 0)
{throw new WrongInvocationException("getLevelConstraints called for ThmNode before levelCheck");};
return this.body.getLevelConstraints();
}
+ @Override
public final SetOfArgLevelConstraints getArgLevelConstraints() {
if (levelChecked == 0)
{throw new WrongInvocationException("getArgLevelConstraints called for ThmNode before levelCheck");};
return this.body.getArgLevelConstraints();
}
- public final HashSet getArgLevelParams() {
+ @Override
+ public final HashSet<ArgLevelParam> getArgLevelParams() {
if (levelChecked == 0)
{throw new WrongInvocationException("getArgLevelParams called for ThmNode before levelCheck");};
return this.body.getArgLevelParams();
@@ -266,22 +274,25 @@ public class LabelNode extends ExprNode
*
* @see tla2sany.semantic.SemanticNode#getChildren()
*/
+ @Override
public SemanticNode[] getChildren() {
return new SemanticNode[] { this.body };
}
/*************************************************************************
* The methods for implementing the ExploreNode interface. *
*************************************************************************/
- public final void walkGraph(Hashtable semNodesTable) {
+ @Override
+ public final void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
- semNodesTable.put(new Integer(myUID), this);
+ semNodesTable.put(uid, this);
if (body != null) body.walkGraph(semNodesTable);
for (int i = 0 ; i < params.length; i++) {
params[i].walkGraph(semNodesTable);
} ;
}
+ @Override
public final String toString(int depth) {
if (depth <= 0) return "";
String ret = "\n*LabelNode: " + super.toString(depth);
@@ -319,7 +330,8 @@ public class LabelNode extends ExprNode
return ret;
}
- protected Element getLevelElement(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ protected Element getLevelElement(Document doc, SymbolContext context) {
Element ret = doc.createElement("LabelNode");
ret.appendChild(appendText(doc,"uniquename",getName().toString()));
ret.appendChild(appendText(doc,"arity",Integer.toString(getArity())));
diff --git a/tlatools/src/tla2sany/semantic/LeafProofNode.java b/tlatools/src/tla2sany/semantic/LeafProofNode.java
index 798b27373dfa3121e17c046d40220a8e21194ba8..b87ad1d5637b767244f2a590d870025c3aa0dd9f 100644
--- a/tlatools/src/tla2sany/semantic/LeafProofNode.java
+++ b/tlatools/src/tla2sany/semantic/LeafProofNode.java
@@ -3,8 +3,10 @@ package tla2sany.semantic;
import java.util.Hashtable;
+import tla2sany.explorer.ExploreNode;
import tla2sany.st.TreeNode;
import tla2sany.utilities.Strings;
+import tla2sany.xml.SymbolContext;
import org.w3c.dom.Document;
import org.w3c.dom.Element;
@@ -70,6 +72,7 @@ public class LeafProofNode extends ProofNode {
public boolean getOmitted() {return omitted ;} ;
public boolean getOnlyFlag() {return isOnly ;} ;
+ @Override
public boolean levelCheck(int iter) {
/***********************************************************************
* Level checking is performed by level-checking the facts. Since the *
@@ -84,6 +87,7 @@ public class LeafProofNode extends ProofNode {
* The children are the facts.
* @see tla2sany.semantic.SemanticNode#getChildren()
*/
+ @Override
public SemanticNode[] getChildren() {
if (this.facts == null || this.facts.length == 0) {
return null;
@@ -95,10 +99,11 @@ public class LeafProofNode extends ProofNode {
return res;
}
- public void walkGraph(Hashtable semNodesTable) {
+ @Override
+ public void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
- semNodesTable.put(new Integer(myUID), this);
+ semNodesTable.put(uid, this);
for (int i = 0; i < facts.length; i++) {
facts[i].walkGraph(semNodesTable);
} ;
@@ -108,6 +113,7 @@ public class LeafProofNode extends ProofNode {
***********************************************************************/
}
+ @Override
public String toString(int depth) {
if (depth <= 0) return "";
String ret = "\n*LeafProofNode:\n"
@@ -125,7 +131,8 @@ public class LeafProofNode extends ProofNode {
return ret;
}
- protected Element getLevelElement(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ protected Element getLevelElement(Document doc, SymbolContext context) {
Element e;
if (getOmitted()) {
diff --git a/tlatools/src/tla2sany/semantic/LetInNode.java b/tlatools/src/tla2sany/semantic/LetInNode.java
index 22345cbc902cab6d0ba450d74e4373fde1b772ae..2e619f490649b5f1a3b1bf417b4e9edf1bdc3d61 100644
--- a/tlatools/src/tla2sany/semantic/LetInNode.java
+++ b/tlatools/src/tla2sany/semantic/LetInNode.java
@@ -10,6 +10,7 @@ import tla2sany.explorer.ExploreNode;
import tla2sany.st.TreeNode;
import tla2sany.utilities.Strings;
import tla2sany.utilities.Vector;
+import tla2sany.xml.SymbolContext;
import org.w3c.dom.Document;
import org.w3c.dom.Element;
@@ -106,6 +107,8 @@ implements ExploreNode, LevelConstants {
// private SetOfArgLevelConstraints argLevelConstraints;
// private HashSet argLevelParams;
+ @Override
+ @SuppressWarnings("unchecked")
public final boolean levelCheck(int itr) {
if (this.levelChecked >= itr) return this.levelCorrect;
levelChecked = itr ;
@@ -141,8 +144,8 @@ implements ExploreNode, LevelConstants {
* the aliasing of the levelParams and allParams fields of this node *
* and its body to the same HashSets, but it doesn't hurt to be safe. *
***********************************************************************/
- this.levelParams = (HashSet) this.body.getLevelParams().clone();
- this.allParams = (HashSet) this.body.getAllParams().clone();
+ this.levelParams = (HashSet<SymbolNode>)this.body.getLevelParams().clone();
+ this.allParams = (HashSet<SymbolNode>) this.body.getAllParams().clone();
// this.levelConstraints = new SetOfLevelConstraints();
this.levelConstraints.putAll(this.body.getLevelConstraints());
@@ -173,9 +176,9 @@ implements ExploreNode, LevelConstants {
if (this.opDefs[i].getKind() != ThmOrAssumpDefKind){
params = ((OpDefNode) this.opDefs[i]).getParams();
} ;
- Iterator iter = this.opDefs[i].getArgLevelParams().iterator();
+ Iterator<ArgLevelParam> iter = this.opDefs[i].getArgLevelParams().iterator();
while (iter.hasNext()) {
- ArgLevelParam alp = (ArgLevelParam)iter.next();
+ ArgLevelParam alp = iter.next();
if (!alp.occur(params)) {
this.argLevelParams.add(alp);
}
@@ -219,6 +222,7 @@ implements ExploreNode, LevelConstants {
// "ArgLevelParams: " + this.argLevelParams + "\n" ;
// }
+ @Override
public SemanticNode[] getChildren() {
SemanticNode[] res =
new SemanticNode[this.opDefs.length + this.insts.length + 1];
@@ -233,12 +237,13 @@ implements ExploreNode, LevelConstants {
return res;
}
- public final void walkGraph(Hashtable semNodesTable) {
+ @Override
+ public final void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
- semNodesTable.put(new Integer(myUID), this);
+ semNodesTable.put(uid, this);
/***********************************************************************
* Can now walk LET nodes from context, don't need to use opDefs *
@@ -253,6 +258,7 @@ implements ExploreNode, LevelConstants {
if (body != null) body.walkGraph(semNodesTable);
}
+ @Override
public final String toString(int depth) {
if (depth <= 0) return "";
@@ -286,8 +292,8 @@ implements ExploreNode, LevelConstants {
return ret;
}
-
- protected Element getLevelElement(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ protected Element getLevelElement(Document doc, SymbolContext context) {
Element ret = doc.createElement("LetInNode");
ret.appendChild(appendElement(doc,"body",body.export(doc,context)));
Element arguments = doc.createElement("opDefs");
diff --git a/tlatools/src/tla2sany/semantic/LevelNode.java b/tlatools/src/tla2sany/semantic/LevelNode.java
index 986dfbbdef5a679017917ec7228ef7132853d5b5..eb8ab78bb2b43b45e17c6f8e81373c1b117ea783 100644
--- a/tlatools/src/tla2sany/semantic/LevelNode.java
+++ b/tlatools/src/tla2sany/semantic/LevelNode.java
@@ -5,6 +5,7 @@ import java.util.HashSet;
import java.util.Iterator;
import tla2sany.st.TreeNode;
+import tla2sany.xml.SymbolContext;
import util.WrongInvocationException;
import org.w3c.dom.Document;
@@ -63,10 +64,10 @@ public class LevelNode extends SemanticNode {
***************************************************************************/
public boolean levelCorrect = true ;
public int level = ConstantLevel ;
-public HashSet levelParams = new HashSet() ;
+public HashSet<SymbolNode> levelParams = new HashSet<>() ;
public SetOfLevelConstraints levelConstraints = new SetOfLevelConstraints();
public SetOfArgLevelConstraints argLevelConstraints = new SetOfArgLevelConstraints();
-public HashSet argLevelParams = new HashSet() ;
+public HashSet<ArgLevelParam> argLevelParams = new HashSet<>() ;
/***************************************************************************
* The following HashSets are used in computing Leibnizity. *
@@ -80,8 +81,8 @@ public HashSet argLevelParams = new HashSet() ;
* See the file leibniz-checking.txt, appended below, for an explanation *
* of Leibnizity and Leibniz checking. *
***************************************************************************/
-public HashSet allParams = new HashSet() ;
-public HashSet nonLeibnizParams = new HashSet() ;
+public HashSet<SymbolNode> allParams = new HashSet<>() ;
+public HashSet<SymbolNode> nonLeibnizParams = new HashSet<>() ;
public int levelChecked = 0 ;
/*************************************************************************
@@ -178,11 +179,11 @@ public int levelChecked = 0 ;
* instantiated by a temporal formula. Added by LL on 1 Mar 2009 *
*************************************************************************/
static void addTemporalLevelConstraintToConstants(
- HashSet params,
+ HashSet<SymbolNode> params,
SetOfLevelConstraints constrs ) {
- Iterator iter = params.iterator();
+ Iterator<SymbolNode> iter = params.iterator();
while (iter.hasNext()) {
- LevelNode node = (LevelNode) iter.next() ;
+ SymbolNode node = iter.next() ;
if (node.getKind() == ConstantDeclKind) {
constrs.put(node, Levels[ActionLevel]);
};
@@ -198,7 +199,7 @@ public int levelChecked = 0 ;
return this.level;
}
- public HashSet getLevelParams(){
+ public HashSet<SymbolNode> getLevelParams(){
/***********************************************************************
* Seems to return a HashSet of OpDeclNode objects. Presumably, these *
* are the parameters from the local context that contribute to the *
@@ -209,7 +210,7 @@ public int levelChecked = 0 ;
return this.levelParams;
}
- public HashSet getAllParams(){
+ public HashSet<SymbolNode> getAllParams(){
/***********************************************************************
* Returns a HashSet of OpDeclNode objects, which are the parameters *
* from the local context that appear within the object. *
@@ -219,7 +220,7 @@ public int levelChecked = 0 ;
return this.allParams;
}
- public HashSet getNonLeibnizParams(){
+ public HashSet<SymbolNode> getNonLeibnizParams(){
/***********************************************************************
* Returns a HashSet of OpDeclNode objects, which is the subset of *
* parameters returned by getAllParams() that appear within a *
@@ -254,7 +255,7 @@ public int levelChecked = 0 ;
return this.argLevelConstraints;
}
- public HashSet getArgLevelParams(){
+ public HashSet<ArgLevelParam> getArgLevelParams(){
/***********************************************************************
* Seems to return a HashSet of ArgLevelParam objects. (See *
* ArgLevelParam.java for an explanation of those objects.) *
@@ -278,32 +279,32 @@ public int levelChecked = 0 ;
"NonLeibnizParams: " + HashSetToString(this.getNonLeibnizParams()) ;
}
- public static String HashSetToString(HashSet hs) {
+ public static String HashSetToString(HashSet<SymbolNode> hs) {
/***********************************************************************
* Converts a HashSet of SymbolNodes to a printable string. *
***********************************************************************/
String rval = "{" ;
boolean first = true ;
- Iterator iter = hs.iterator();
+ Iterator<SymbolNode> iter = hs.iterator();
while (iter.hasNext()) {
if (! first) {rval = rval + ", ";} ;
- rval = rval + ((SymbolNode) iter.next()).getName() ;
+ rval = rval + iter.next().getName() ;
first = false ;
} ;
rval = rval + "}" ;
return rval ;
}
- public static String ALPHashSetToString(HashSet hs) {
+ public static String ALPHashSetToString(HashSet<ArgLevelParam> hs) {
/***********************************************************************
* Converts a HashSet of ArgLevelParam objects to a printable string. *
***********************************************************************/
String rval = "{" ;
boolean first = true ;
- Iterator iter = hs.iterator();
+ Iterator<ArgLevelParam> iter = hs.iterator();
while (iter.hasNext()) {
if (! first) {rval = rval + ", ";} ;
- ArgLevelParam alp = (ArgLevelParam) iter.next();
+ ArgLevelParam alp = iter.next();
rval = rval + "<" + alp.op.getName() + ", " + alp.i + ", " +
alp.param.getName() + ">" ;
first = false;
@@ -322,7 +323,8 @@ public int levelChecked = 0 ;
return this.defaultLevelDataToString() ;}
- protected Element getSemanticElement(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ protected Element getSemanticElement(Document doc, SymbolContext context) {
// T.L. abstract method used to add data from subclasses
Element e = getLevelElement(doc, context); //SymbolElement.getLevelElement is not supposed to be called
try {
@@ -338,7 +340,7 @@ public int levelChecked = 0 ;
* T.L. October 2014
* Abstract method for subclasses of LevelNode to add their information
* */
- protected Element getLevelElement(Document doc, tla2sany.xml.SymbolContext context) {
+ protected Element getLevelElement(Document doc, SymbolContext context) {
throw new UnsupportedOperationException("xml export is not yet supported for: " + getClass() + " with toString: " + toString(100));
}
diff --git a/tlatools/src/tla2sany/semantic/ModuleNode.java b/tlatools/src/tla2sany/semantic/ModuleNode.java
index 8c7b6fedacdb53095df8f604584a78abc6265fa2..ee1ec7a711b669fb9ce839cd8502bb9e1910b545 100644
--- a/tlatools/src/tla2sany/semantic/ModuleNode.java
+++ b/tlatools/src/tla2sany/semantic/ModuleNode.java
@@ -16,9 +16,11 @@ import java.util.HashSet;
import java.util.Hashtable;
import java.util.Iterator;
+import tla2sany.explorer.ExploreNode;
import tla2sany.st.TreeNode;
import tla2sany.utilities.Strings;
import tla2sany.utilities.Vector;
+import tla2sany.xml.SymbolContext;
import util.UniqueString;
import util.WrongInvocationException;
@@ -680,6 +682,7 @@ final void addAssumption(TreeNode stn, ExprNode ass, SymbolTable st,
// private SetOfArgLevelConstraints argLevelConstraints;
// private HashSet argLevelParams;
+ @Override
public final boolean levelCheck(int itr) {
if (levelChecked >= itr) return this.levelCorrect;
@@ -948,6 +951,7 @@ final void addAssumption(TreeNode stn, ExprNode ass, SymbolTable st,
return this.levelCorrect;
}
+ @Override
public final int getLevel() {
throw new WrongInvocationException("Internal Error: Should never call ModuleNode.getLevel()");
}
@@ -1023,6 +1027,7 @@ final void addAssumption(TreeNode stn, ExprNode ass, SymbolTable st,
* walkGraph, levelDataToString, and toString methods to implement
* ExploreNode interface
*/
+ @Override
public final String levelDataToString() {
return "LevelParams: " + getLevelParams() + "\n" +
"LevelConstraints: " + getLevelConstraints() + "\n" +
@@ -1031,6 +1036,7 @@ final void addAssumption(TreeNode stn, ExprNode ass, SymbolTable st,
}
private SemanticNode[] children = null;
+ @Override
public SemanticNode[] getChildren() {
if (children != null) {
return children;
@@ -1047,7 +1053,8 @@ final void addAssumption(TreeNode stn, ExprNode ass, SymbolTable st,
return children;
}
- public final void walkGraph (Hashtable semNodesTable) {
+ @Override
+ public final void walkGraph (Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
@@ -1087,6 +1094,7 @@ final void addAssumption(TreeNode stn, ExprNode ass, SymbolTable st,
}
}
+ @Override
public final String toString(int depth) {
if (depth <= 0) return "";
@@ -1149,7 +1157,7 @@ final void addAssumption(TreeNode stn, ExprNode ass, SymbolTable st,
return "ModuleNodeRef";
}
- protected Element getSymbolElement(Document doc, tla2sany.xml.SymbolContext context) {
+ protected Element getSymbolElement(Document doc, SymbolContext context) {
Element ret = doc.createElement("ModuleNode");
ret.appendChild(appendText(doc, "uniquename", getName().toString()));
diff --git a/tlatools/src/tla2sany/semantic/NewSymbNode.java b/tlatools/src/tla2sany/semantic/NewSymbNode.java
index 944e574aee944ddb254a13ca69591c854bafa2be..6ca5ac858845a72ba821b352b35830716b072761 100644
--- a/tlatools/src/tla2sany/semantic/NewSymbNode.java
+++ b/tlatools/src/tla2sany/semantic/NewSymbNode.java
@@ -21,8 +21,10 @@ package tla2sany.semantic;
import java.util.Hashtable;
+import tla2sany.explorer.ExploreNode;
import tla2sany.st.TreeNode;
import tla2sany.utilities.Strings;
+import tla2sany.xml.SymbolContext;
import org.w3c.dom.Document;
import org.w3c.dom.Element;
@@ -84,6 +86,7 @@ public class NewSymbNode extends LevelNode {
* level of the `set' expression, if it's non-null. Any other level *
* information comes from the `set' expression. *
*************************************************************************/
+ @Override
public boolean levelCheck(int iter) {
if (levelChecked < iter) {
@@ -157,6 +160,7 @@ public class NewSymbNode extends LevelNode {
* The body is the node's only child.
*/
+ @Override
public SemanticNode[] getChildren() {
if (this.set == null) {
return null;
@@ -165,13 +169,15 @@ public class NewSymbNode extends LevelNode {
}
}
- public final void walkGraph(Hashtable semNodesTable) {
+ @Override
+ public final void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
- semNodesTable.put(new Integer(myUID), this);
+ semNodesTable.put(uid, this);
if (set != null) { set.walkGraph(semNodesTable); } ;
}
+ @Override
public final String toString(int depth) {
if (depth <= 0) return "";
String setString = "" ;
@@ -187,7 +193,8 @@ public class NewSymbNode extends LevelNode {
setString);
}
- protected Element getLevelElement(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ protected Element getLevelElement(Document doc, SymbolContext context) {
Element e = doc.createElement("NewSymbNode");
e.appendChild(getOpDeclNode().export(doc,context));
if (getSet() != null) {
diff --git a/tlatools/src/tla2sany/semantic/NonLeafProofNode.java b/tlatools/src/tla2sany/semantic/NonLeafProofNode.java
index 67544148b12faed67054ed5fb8718396971a97c1..6f36da65ae40d13df9f33cbf89970d0943629eec 100644
--- a/tlatools/src/tla2sany/semantic/NonLeafProofNode.java
+++ b/tlatools/src/tla2sany/semantic/NonLeafProofNode.java
@@ -3,9 +3,11 @@ package tla2sany.semantic;
import java.util.Hashtable;
+import tla2sany.explorer.ExploreNode;
import tla2sany.st.TreeNode;
import tla2sany.utilities.Strings;
import tla2sany.utilities.Vector;
+import tla2sany.xml.SymbolContext;
import org.w3c.dom.Document;
import org.w3c.dom.Element;
@@ -141,6 +143,7 @@ public class NonLeafProofNode extends ProofNode {
public LevelNode[] getSteps() {return steps ;}
public Context getContext() {return context ;}
+ @Override
public boolean levelCheck(int iter) {
/***********************************************************************
* Level check the steps and the instantiated modules coming from *
@@ -157,6 +160,7 @@ public class NonLeafProofNode extends ProofNode {
* The children are the steps.
* @see tla2sany.semantic.SemanticNode#getChildren()
*/
+ @Override
public SemanticNode[] getChildren() {
if (this.steps == null || this.steps.length == 0) {
return null;
@@ -168,10 +172,11 @@ public class NonLeafProofNode extends ProofNode {
return res;
}
- public void walkGraph(Hashtable semNodesTable) {
+ @Override
+ public void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
- semNodesTable.put(new Integer(myUID), this);
+ semNodesTable.put(uid, this);
for (int i = 0; i < steps.length; i++) {
steps[i].walkGraph(semNodesTable);
} ;
@@ -186,6 +191,7 @@ public class NonLeafProofNode extends ProofNode {
*********************************************************************/
}
+ @Override
public String toString(int depth) {
if (depth <= 0) return "";
String ret = "\n*ProofNode:\n"
@@ -211,7 +217,8 @@ public class NonLeafProofNode extends ProofNode {
return ret;
}
- protected Element getLevelElement(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ protected Element getLevelElement(Document doc, SymbolContext context) {
Element e = doc.createElement("steps");
for (int i=0; i< steps.length; i++) {
diff --git a/tlatools/src/tla2sany/semantic/NumeralNode.java b/tlatools/src/tla2sany/semantic/NumeralNode.java
index 89bce398f95dcef2a5b4dffb8f054873c8f05f31..bd62e9206df6300d2a5f881778718592affb9845 100644
--- a/tlatools/src/tla2sany/semantic/NumeralNode.java
+++ b/tlatools/src/tla2sany/semantic/NumeralNode.java
@@ -5,7 +5,9 @@ package tla2sany.semantic;
import java.math.BigInteger;
import java.util.Hashtable;
+import tla2sany.explorer.ExploreNode;
import tla2sany.st.TreeNode;
+import tla2sany.xml.SymbolContext;
import org.w3c.dom.Document;
import org.w3c.dom.Element;
@@ -70,9 +72,11 @@ public class NumeralNode extends ExprNode {
* reflects how the value appeared in the input, so it should be
* "\O7777" if that's what appears in the source.
*/
+ @Override
public final String toString() { return this.image; }
/* Level Checking */
+ @Override
public final boolean levelCheck(int iter) {
levelChecked = iter;
/*********************************************************************
@@ -107,13 +111,15 @@ public class NumeralNode extends ExprNode {
// "ArgLevelParams: " + this.getArgLevelParams() + "\n" ;
// }
- public final void walkGraph(Hashtable semNodesTable) {
+ @Override
+ public final void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
- semNodesTable.put(new Integer(myUID), this);
+ semNodesTable.put(uid, this);
}
+ @Override
public final String toString(int depth) {
if (depth <= 0) return "";
@@ -122,7 +128,8 @@ public class NumeralNode extends ExprNode {
"; image: " + image);
}
- protected Element getLevelElement(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ protected Element getLevelElement(Document doc, SymbolContext context) {
String v = (bigValue != null) ? bigValue.toString() : (Integer.toString(value));
Element e = doc.createElement("IntValue");
Node n = doc.createTextNode(v);
diff --git a/tlatools/src/tla2sany/semantic/OpApplNode.java b/tlatools/src/tla2sany/semantic/OpApplNode.java
index c97e23ec5bc9e00af9f0197e5bd2f68557a598c3..905354a747d9be24e7450af621fda67c3216e140 100644
--- a/tlatools/src/tla2sany/semantic/OpApplNode.java
+++ b/tlatools/src/tla2sany/semantic/OpApplNode.java
@@ -24,6 +24,7 @@ import tla2sany.explorer.ExploreNode;
import tla2sany.parser.SyntaxTreeNode;
import tla2sany.st.TreeNode;
import tla2sany.utilities.Strings;
+import tla2sany.xml.SymbolContext;
import util.UniqueString;
import org.w3c.dom.Document;
@@ -398,6 +399,7 @@ public class OpApplNode extends ExprNode implements ExploreNode {
// }
// }
+ @Override
public final boolean levelCheck(int itr) {
if (this.levelChecked >= itr) return this.levelCorrect;
this.levelChecked = itr ;
@@ -492,6 +494,7 @@ public class OpApplNode extends ExprNode implements ExploreNode {
if (opd instanceof OpArgNode &&
((OpArgNode)opd).getOp() instanceof AnyDefNode) {
AnyDefNode opdDef = (AnyDefNode)((OpArgNode)opd).getOp();
+ @SuppressWarnings("unused") // See below comment block
boolean opdDefLevelCheck = opdDef.levelCheck(itr) ;
/*************************************************************
* Need to call opdDef.levelCheck before using its level *
@@ -599,7 +602,7 @@ public class OpApplNode extends ExprNode implements ExploreNode {
* Set allBoundSymbols to a hashset containing all the *
* FormalParamNodes of the bound symbols. *
*********************************************************************/
- HashSet allBoundSymbols = new HashSet() ;
+ HashSet<FormalParamNode> allBoundSymbols = new HashSet<>() ;
if (this.unboundedBoundSymbols != null) {
for (int i = 0 ; i < this.unboundedBoundSymbols.length; i++){
allBoundSymbols.add(this.unboundedBoundSymbols[i]);
@@ -619,9 +622,9 @@ public class OpApplNode extends ExprNode implements ExploreNode {
* Remove bound identifiers from levelParams, allParams, and *
* nonLeibnizParams. *
*********************************************************************/
- Iterator absIter = allBoundSymbols.iterator() ;
+ Iterator<FormalParamNode> absIter = allBoundSymbols.iterator() ;
while (absIter.hasNext()) {
- Object nextBoundSymbol = absIter.next() ;
+ FormalParamNode nextBoundSymbol = absIter.next() ;
this.levelParams.remove(nextBoundSymbol) ;
this.allParams.remove(nextBoundSymbol) ;
this.nonLeibnizParams.remove(nextBoundSymbol) ;
@@ -650,9 +653,9 @@ public class OpApplNode extends ExprNode implements ExploreNode {
***************************************************************/
SetOfLevelConstraints lcons =
this.operands[i].getLevelConstraints() ;
- Iterator iter = lcons.keySet().iterator();
+ Iterator<SymbolNode> iter = lcons.keySet().iterator();
while (iter.hasNext()) {
- SymbolNode param = (SymbolNode) iter.next() ;
+ SymbolNode param = iter.next() ;
if (! allBoundSymbols.contains(param)) {
this.levelConstraints.put(param, lcons.get(param)) ;
}
@@ -666,7 +669,7 @@ public class OpApplNode extends ExprNode implements ExploreNode {
for (int i = 0; i < this.operands.length; i++) {
Integer mlevel = new Integer(opDef.getMaxLevel(i));
if (this.operands[i] != null) {
- Iterator iter = this.operands[i].getLevelParams().iterator();
+ Iterator<SymbolNode> iter = this.operands[i].getLevelParams().iterator();
while (iter.hasNext()) {
this.levelConstraints.put(iter.next(), mlevel);
}
@@ -696,7 +699,7 @@ public class OpApplNode extends ExprNode implements ExploreNode {
for (int k = 0; k < alen; k++) {
if (opDef.getOpLevelCond(i, j, k)) {
Integer mlevel = new Integer(argDef.getMaxLevel(k));
- Iterator iter = this.operands[j].getLevelParams().iterator();
+ Iterator<SymbolNode> iter = this.operands[j].getLevelParams().iterator();
while (iter.hasNext()) {
this.levelConstraints.put(iter.next(), mlevel);
}
@@ -723,10 +726,10 @@ public class OpApplNode extends ExprNode implements ExploreNode {
} ; // if (! argDef.isLeibniz)
} // if (opdi != null && ...)
} // for i
- HashSet alpSet = opDef.getArgLevelParams();
- Iterator iter = alpSet.iterator();
+ HashSet<ArgLevelParam> alpSet = opDef.getArgLevelParams();
+ Iterator<ArgLevelParam> iter = alpSet.iterator();
while (iter.hasNext()) {
- ArgLevelParam alp = (ArgLevelParam)iter.next();
+ ArgLevelParam alp = iter.next();
ExprOrOpArgNode arg = this.getArg(alp.op);
// LL changed OpDefNode -> AnyDefNode in the following.
// See comments in AnyDefNode.java. (It is only in the
@@ -784,7 +787,7 @@ public class OpApplNode extends ExprNode implements ExploreNode {
} // for i
iter = alpSet.iterator();
while (iter.hasNext()) {
- ArgLevelParam alp = (ArgLevelParam)iter.next();
+ ArgLevelParam alp = iter.next();
ExprOrOpArgNode arg = this.getArg(alp.op);
if (arg != null) {
arg.levelCheck(itr) ;
@@ -799,7 +802,7 @@ public class OpApplNode extends ExprNode implements ExploreNode {
/*********************************************************************
* Compute this.argLevelParams. *
*********************************************************************/
- this.argLevelParams = new HashSet();
+ this.argLevelParams = new HashSet<>();
for (int i = 0; i < this.operands.length; i++) {
if (this.operands[i] != null) {
if (allBoundSymbols.size() == 0) {
@@ -813,9 +816,9 @@ public class OpApplNode extends ExprNode implements ExploreNode {
* argLevelConstraints the element implied as described above *
* if alp.param IS a bound identifier. *
***************************************************************/
- Iterator alpiter = this.operands[i].getArgLevelParams().iterator();
- while (alpiter.hasNext()) {
- ArgLevelParam alp = (ArgLevelParam) alpiter.next() ;
+ Iterator<ArgLevelParam> alpIter = this.operands[i].getArgLevelParams().iterator();
+ while (alpIter.hasNext()) {
+ ArgLevelParam alp = alpIter.next() ;
if (!allBoundSymbols.contains(alp.param)) {
this.argLevelParams.add(alp) ;
}
@@ -840,9 +843,9 @@ public class OpApplNode extends ExprNode implements ExploreNode {
/*************************************************************
* Need to invoke levelCheck before invoking getLevelParams. *
*************************************************************/
- Iterator iter1 = arg.getLevelParams().iterator();
+ Iterator<SymbolNode> iter1 = arg.getLevelParams().iterator();
while (iter1.hasNext()) {
- SymbolNode param = (SymbolNode)iter1.next();
+ SymbolNode param = iter1.next();
this.argLevelParams.add(new ArgLevelParam(alp.op, alp.i, param));
}
}
@@ -869,9 +872,9 @@ public class OpApplNode extends ExprNode implements ExploreNode {
for (int j = 0; j < this.operands.length; j++) {
for (int k = 0; k < alen; k++) {
if (opDef.getOpLevelCond(i, j, k)) {
- Iterator iter1 = this.operands[j].getLevelParams().iterator();
+ Iterator<SymbolNode> iter1 = this.operands[j].getLevelParams().iterator();
while (iter1.hasNext()) {
- SymbolNode param = (SymbolNode)iter1.next();
+ SymbolNode param = iter1.next();
this.argLevelParams.add(new ArgLevelParam(opArg, k, param));
}
}
@@ -892,7 +895,7 @@ public class OpApplNode extends ExprNode implements ExploreNode {
this.level = Math.max(this.level, this.operands[i].getLevel());
} // for
- this.levelParams = new HashSet();
+ this.levelParams = new HashSet<>();
/*********************************************************************
* We only add this.operator to the levelParams and allParams. *
*********************************************************************/
@@ -936,17 +939,17 @@ public class OpApplNode extends ExprNode implements ExploreNode {
this.operands[i].getArgLevelConstraints());
}
- this.argLevelParams = new HashSet();
+ this.argLevelParams = new HashSet<>();
for (int i = 0; i < this.operands.length; i++) {
/*******************************************************************
* For every levelParam p of the i-th operand, add to *
* argLevelParams an entry asserting that p appears within an i-th *
* operand of this.operator. *
*******************************************************************/
- HashSet lpSet = this.operands[i].getLevelParams();
- Iterator iter = lpSet.iterator();
+ HashSet<SymbolNode> lpSet = this.operands[i].getLevelParams();
+ Iterator<SymbolNode> iter = lpSet.iterator();
while (iter.hasNext()) {
- SymbolNode param = (SymbolNode)iter.next();
+ SymbolNode param = iter.next();
this.argLevelParams.add(
new ArgLevelParam(this.operator, i, param));
}; // end while
@@ -1097,6 +1100,7 @@ public class OpApplNode extends ExprNode implements ExploreNode {
// "ArgLevelParams: " + this.argLevelParams + "\n" ;
// }
+ @Override
public SemanticNode[] getChildren() {
SemanticNode[] res =
new SemanticNode[this.ranges.length + this.operands.length];
@@ -1114,7 +1118,8 @@ public class OpApplNode extends ExprNode implements ExploreNode {
* walkGraph finds all reachable nodes in the semantic graph
* and inserts them in the Hashtable semNodesTable for use by the Explorer tool.
*/
- public void walkGraph(Hashtable semNodesTable) {
+ @Override
+ public void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
@@ -1217,6 +1222,7 @@ public class OpApplNode extends ExprNode implements ExploreNode {
* Displays this node as a String, implementing ExploreNode interface; depth
* parameter is a bound on the depth of the portion of the tree that is displayed.
*/
+ @Override
public String toString(int depth) {
if (depth <= 0) return "";
String sEO = "" ;
@@ -1229,7 +1235,8 @@ public class OpApplNode extends ExprNode implements ExploreNode {
+ toStringBody(depth) + sEO ;
}
- protected Element getLevelElement(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ protected Element getLevelElement(Document doc, SymbolContext context) {
Element e = doc.createElement("OpApplNode");
// TL 2014 - A fix for detecting null representing OTHER inside a case (please refrain from using null as a semantical object),
@@ -1243,8 +1250,8 @@ public class OpApplNode extends ExprNode implements ExploreNode {
// indeed the OTHER case
if (other.getOperator().getName().toString().equals("$Pair") && other.getArgs()[0] == null) {
// we pass a flag that tells any future OpApplNode that a null operand in 0 position should be replaced by the string $Other
- context = new tla2sany.xml.SymbolContext(context);
- context.setFlag(tla2sany.xml.SymbolContext.OTHER_BUG);
+ context = new SymbolContext(context);
+ context.setFlag(SymbolContext.OTHER_BUG);
}
}
@@ -1259,7 +1266,7 @@ public class OpApplNode extends ExprNode implements ExploreNode {
Element ope = doc.createElement("operands");
for (int i=0; i< operands.length; i++) {
// dealing with the $Case OTHER null bug
- if (i == 0 && operands[0] == null && context.hasFlag(tla2sany.xml.SymbolContext.OTHER_BUG)) {
+ if (i == 0 && operands[0] == null && context.hasFlag(SymbolContext.OTHER_BUG)) {
ope.appendChild(appendText(doc,"StringNode","$Other"));
}
else {
diff --git a/tlatools/src/tla2sany/semantic/OpArgNode.java b/tlatools/src/tla2sany/semantic/OpArgNode.java
index 2fc49eaab6ac23e00e36b9e6d873ac58b22f5b08..b93e2fa1fa9f2812ed19cdad08bb55acd76d3c8b 100644
--- a/tlatools/src/tla2sany/semantic/OpArgNode.java
+++ b/tlatools/src/tla2sany/semantic/OpArgNode.java
@@ -7,13 +7,14 @@ package tla2sany.semantic;
import java.util.Hashtable;
+import tla2sany.explorer.ExploreNode;
import tla2sany.parser.SyntaxTreeNode;
import tla2sany.st.TreeNode;
+import tla2sany.xml.SymbolContext;
import util.UniqueString;
import org.w3c.dom.Document;
import org.w3c.dom.Element;
-import org.w3c.dom.Node;
/**
* This class represents operators of arity > 0 used as arguments to
@@ -66,6 +67,7 @@ public class OpArgNode extends ExprOrOpArgNode {
public final ModuleNode getModule() { return this.mn; }
/* Level check */
+ @Override
public final boolean levelCheck(int iter) {
if (levelChecked >= iter) {return this.levelCorrect; } ;
levelChecked = iter ;
@@ -109,11 +111,12 @@ public class OpArgNode extends ExprOrOpArgNode {
// "ArgLevelParams: " + this.getArgLevelParams() + "\n" ;
// }
- public final void walkGraph(Hashtable semNodesTable) {
+ @Override
+ public final void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
- semNodesTable.put(new Integer(myUID), this);
+ semNodesTable.put(uid, this);
/***********************************************************************
* Modified on 28 Mar 2007 by LL to walk the operator node of the *
@@ -126,6 +129,7 @@ public class OpArgNode extends ExprOrOpArgNode {
if (op != null) {op.walkGraph(semNodesTable) ;} ;
}
+ @Override
public final String toString(int depth) {
if (depth <= 0) return "";
@@ -135,7 +139,8 @@ public class OpArgNode extends ExprOrOpArgNode {
" op: " + (op != null ? "" + ((SemanticNode)op).getUid() : "null" );
}
- protected Element getLevelElement(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ protected Element getLevelElement(Document doc, SymbolContext context) {
Element e = doc.createElement("OpArgNode");
Element n = doc.createElement("argument");
//Element ope = op.getSymbolElement(doc, context);
diff --git a/tlatools/src/tla2sany/semantic/OpDeclNode.java b/tlatools/src/tla2sany/semantic/OpDeclNode.java
index a0cb9c0c9b7c2262fd5eb9d3f9a2505c303bde24..e516b459dcbeece5638d47e0f6e8b897b8ffa26c 100644
--- a/tlatools/src/tla2sany/semantic/OpDeclNode.java
+++ b/tlatools/src/tla2sany/semantic/OpDeclNode.java
@@ -7,7 +7,9 @@ package tla2sany.semantic;
import java.util.Hashtable;
+import tla2sany.explorer.ExploreNode;
import tla2sany.st.TreeNode;
+import tla2sany.xml.SymbolContext;
import util.UniqueString;
import org.w3c.dom.Document;
@@ -85,6 +87,7 @@ public class OpDeclNode extends OpDefOrDeclNode {
// private HashSet levelParams;
+ @Override
public final boolean levelCheck(int iter) {
/***********************************************************************
* Level information set by constructor. *
@@ -136,12 +139,14 @@ public class OpDeclNode extends OpDefOrDeclNode {
// "ArgLevelParams: " + this.getArgLevelParams() + "\n";
// }
- public final void walkGraph(Hashtable semNodesTable) {
+ @Override
+ public final void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
- semNodesTable.put(new Integer(myUID), this);
+ semNodesTable.put(uid, this);
}
+ @Override
public final String toString (int depth) {
if (depth <= 0) return "";
return "\n*OpDeclNode: " + this.getName() + " " + super.toString(depth)
@@ -156,7 +161,7 @@ public class OpDeclNode extends OpDefOrDeclNode {
return "OpDeclNodeRef";
}
- protected Element getSymbolElement(Document doc, tla2sany.xml.SymbolContext context) {
+ protected Element getSymbolElement(Document doc, SymbolContext context) {
Element e = doc.createElement("OpDeclNode");
e.appendChild(appendText(doc,"uniquename",getName().toString()));
e.appendChild(appendText(doc,"arity",Integer.toString(getArity())));
diff --git a/tlatools/src/tla2sany/semantic/OpDefNode.java b/tlatools/src/tla2sany/semantic/OpDefNode.java
index 3966402f9abcff8d0878b71df1092dd58a31bbae..0d94c1baa5ce84f347e9b47913445763da2bca59 100644
--- a/tlatools/src/tla2sany/semantic/OpDefNode.java
+++ b/tlatools/src/tla2sany/semantic/OpDefNode.java
@@ -35,11 +35,13 @@ import java.util.HashSet;
import java.util.Hashtable;
import java.util.Iterator;
+import tla2sany.explorer.ExploreNode;
import tla2sany.parser.SyntaxTreeNode;
import tla2sany.st.Location;
import tla2sany.st.TreeNode;
import tla2sany.utilities.Strings;
import tla2sany.utilities.Vector;
+import tla2sany.xml.SymbolContext;
import util.UniqueString;
import util.WrongInvocationException;
@@ -945,6 +947,7 @@ public class OpDefNode extends OpDefOrDeclNode
// this.argLevelParams = EmptySet;
}
+ @Override
public final boolean levelCheck(int itr) {
if ( (this.levelChecked >= itr)
|| ( (! inRecursiveSection)
@@ -1144,6 +1147,7 @@ public class OpDefNode extends OpDefOrDeclNode
* toString, levelDataToString, and walkGraph methods to implement
* ExploreNode interface
*/
+ @Override
public final String levelDataToString() {
if ( (this.getKind() == ModuleInstanceKind)
|| (this.getKind() == NumberedProofStepKind)) {return "";} ;
@@ -1210,6 +1214,7 @@ public class OpDefNode extends OpDefOrDeclNode
* The body is the node's only child.
*/
+ @Override
public SemanticNode[] getChildren() {
return new SemanticNode[] {this.body};
}
@@ -1219,7 +1224,8 @@ public class OpDefNode extends OpDefOrDeclNode
* and inserts them in the Hashtable semNodesTable for use by
* the Explorer tool.
*/
- public final void walkGraph(Hashtable semNodesTable) {
+ @Override
+ public final void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
semNodesTable.put(uid, this);
@@ -1237,6 +1243,7 @@ public class OpDefNode extends OpDefOrDeclNode
* interface; depth parameter is a bound on the depth of the portion
* of the tree that is displayed.
*/
+ @Override
public final String toString(int depth) {
if (depth <= 0) return "";
@@ -1323,7 +1330,7 @@ public class OpDefNode extends OpDefOrDeclNode
}
}
- protected Element getSymbolElement(Document doc, tla2sany.xml.SymbolContext context) {
+ protected Element getSymbolElement(Document doc, SymbolContext context) {
Element ret = null;
switch (getKind()) {
case UserDefinedOpKind:
diff --git a/tlatools/src/tla2sany/semantic/OpDefOrLabelNode.java b/tlatools/src/tla2sany/semantic/OpDefOrLabelNode.java
index b82c507eb4cd333dcc95ee35a709efb8973cb024..fe64c21a815c930ee0c6f34705b675da139afb6b 100644
--- a/tlatools/src/tla2sany/semantic/OpDefOrLabelNode.java
+++ b/tlatools/src/tla2sany/semantic/OpDefOrLabelNode.java
@@ -35,7 +35,7 @@ import util.UniqueString;
interface OpDefOrLabelNode {
-public abstract void setLabels(Hashtable ht) ;
+public abstract void setLabels(Hashtable<UniqueString, LabelNode> ht) ;
/*************************************************************************
* Set the set of labels to ht. *
*************************************************************************/
diff --git a/tlatools/src/tla2sany/semantic/SemanticNode.java b/tlatools/src/tla2sany/semantic/SemanticNode.java
index e7cd4d39c1c4e45768ad24683dda0c782fc47e85..a421bdfd3aade8b8cdff42053afc3a27d321234b 100644
--- a/tlatools/src/tla2sany/semantic/SemanticNode.java
+++ b/tlatools/src/tla2sany/semantic/SemanticNode.java
@@ -25,7 +25,7 @@ import util.ToolIO;
* used to check for equality.
*/
public abstract class SemanticNode
- implements ASTConstants, ExploreNode, LevelConstants, Comparable, XMLExportable /* interface for exporting into XML */ {
+ implements ASTConstants, ExploreNode, LevelConstants, Comparable<SemanticNode>, XMLExportable /* interface for exporting into XML */ {
private static final Object[] EmptyArr = new Object[0];
@@ -176,10 +176,10 @@ public abstract class SemanticNode
* of walkgraph is to find all reachable nodes in the semantic graph
* and insert them in a Hashtable for use by the Explorer tool.
*/
- public void walkGraph(Hashtable semNodesTable) {
+ public void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
- semNodesTable.put(new Integer(myUID), this);
+ semNodesTable.put(uid, this);
}
/**
@@ -211,9 +211,9 @@ public abstract class SemanticNode
* @param s2
* @return
*/
- public int compareTo(Object s) {
+ public int compareTo(SemanticNode s) {
Location loc1 = this.stn.getLocation();
- Location loc2 = ((SemanticNode) s).stn.getLocation();
+ Location loc2 = s.stn.getLocation();
if (loc1.beginLine() < loc2.beginLine())
{
return -1;
@@ -242,6 +242,7 @@ public abstract class SemanticNode
}
}
+ @Override
public String toString() {
TreeNode treeNode = getTreeNode();
if (treeNode instanceof SyntaxTreeNode
diff --git a/tlatools/src/tla2sany/semantic/SetOfArgLevelConstraints.java b/tlatools/src/tla2sany/semantic/SetOfArgLevelConstraints.java
index 08d295e3f3a10f7c4586626d3806c51f969bec08..edafe574a290a855dbd488667f1fdcc38fe32c7e 100644
--- a/tlatools/src/tla2sany/semantic/SetOfArgLevelConstraints.java
+++ b/tlatools/src/tla2sany/semantic/SetOfArgLevelConstraints.java
@@ -6,7 +6,7 @@ import java.util.HashMap;
import java.util.Iterator;
import java.util.Map;
-class SetOfArgLevelConstraints extends HashMap implements LevelConstants {
+class SetOfArgLevelConstraints extends HashMap<ParamAndPosition, Integer> implements LevelConstants {
// Implements a map mapping arg-level parameters (ParamAndPosition)
// to levels (Integer). An entry <pap,x> means that the argument
// pap.position of the operator pap.param must have a level >= x.
@@ -23,16 +23,17 @@ class SetOfArgLevelConstraints extends HashMap implements LevelConstants {
* it with another one for the same parameter if one is there, or
* ignoring the constraint if it is vacuous.
*/
- public final Object put(Object pap, Object level) {
- int newLevel = ((Integer)level).intValue();
- Object old = this.get(pap);
+ @Override
+ public final Integer put(ParamAndPosition pap, Integer level) {
+ int newLevel = level.intValue();
+ Integer old = this.get(pap);
- int oldLevel = (old == null) ? MinLevel : ((Integer)old).intValue();
+ int oldLevel = (old == null) ? MinLevel : old.intValue();
super.put(pap, new Integer(Math.max(newLevel, oldLevel)));
return old;
}
- public final Object put(SymbolNode param, int position, int level) {
+ public final Integer put(SymbolNode param, int position, int level) {
ParamAndPosition pap = new ParamAndPosition(param, position);
return this.put(pap, new Integer(level));
}
@@ -42,17 +43,19 @@ class SetOfArgLevelConstraints extends HashMap implements LevelConstants {
* map, in each case "subsuming" it with any constraint already
* present for the same parameter if one is there.
*/
- public final void putAll(Map s) {
- for (Iterator iter = s.keySet().iterator(); iter.hasNext(); ) {
- Object key = iter.next();
- put(key, s.get(key));
+ @Override
+ public final void putAll(Map<? extends ParamAndPosition, ? extends Integer> s) {
+ for (Iterator<? extends ParamAndPosition> iter = s.keySet().iterator(); iter.hasNext(); ) {
+ ParamAndPosition key = iter.next();
+ this.put(key, s.get(key));
}
}
+ @Override
public final String toString() {
StringBuffer sb = new StringBuffer("{ ");
- for (Iterator iter = this.keySet().iterator(); iter.hasNext(); ) {
- Object pap = iter.next();
+ for (Iterator<ParamAndPosition> iter = this.keySet().iterator(); iter.hasNext(); ) {
+ ParamAndPosition pap = iter.next();
sb.append(pap.toString() + " -> " + this.get(pap));
if (iter.hasNext()) sb.append(", ");
}
diff --git a/tlatools/src/tla2sany/semantic/SetOfLevelConstraints.java b/tlatools/src/tla2sany/semantic/SetOfLevelConstraints.java
index 8f3c4dfec2ce722c8523218d25068c643d7a0265..676bb196cb14fb49f9aea86788468a4939f8e261 100644
--- a/tlatools/src/tla2sany/semantic/SetOfLevelConstraints.java
+++ b/tlatools/src/tla2sany/semantic/SetOfLevelConstraints.java
@@ -6,7 +6,7 @@ import java.util.HashMap;
import java.util.Iterator;
import java.util.Map;
-class SetOfLevelConstraints extends HashMap implements LevelConstants {
+class SetOfLevelConstraints extends HashMap<SymbolNode, Integer> implements LevelConstants {
// Implements a map mapping parameters to levels. An entry <p,x> in
// the set means that p must have a level <= x.
/*************************************************************************
@@ -15,17 +15,16 @@ class SetOfLevelConstraints extends HashMap implements LevelConstants {
* that the key/parameter must have a level <= the value/int. *
*************************************************************************/
-
-
/**
* This method adds <param, level> into this map. It subsumes
* any existing one.
*/
- public final Object put(Object param, Object level) {
- int newLevel = ((Integer)level).intValue();
- Object old = this.get(param);
+ @Override
+ public final Integer put(SymbolNode param, Integer level) {
+ int newLevel = level.intValue();
+ Integer old = this.get(param);
- int oldLevel = (old == null) ? MaxLevel : ((Integer)old).intValue();
+ int oldLevel = (old == null) ? MaxLevel : old.intValue();
super.put(param, new Integer(Math.min(newLevel, oldLevel)));
return old;
}
@@ -35,17 +34,19 @@ class SetOfLevelConstraints extends HashMap implements LevelConstants {
* map, in each case "subsuming" it with any constraint already
* present for the same parameter if one is there.
*/
- public final void putAll(Map s) {
- for (Iterator iter = s.keySet().iterator(); iter.hasNext(); ) {
- Object key = iter.next();
+ @Override
+ public final void putAll(Map<? extends SymbolNode, ? extends Integer> s) {
+ for (Iterator<? extends SymbolNode> iter = s.keySet().iterator(); iter.hasNext(); ) {
+ SymbolNode key = iter.next();
this.put(key, s.get(key));
}
}
+ @Override
public final String toString() {
StringBuffer sb = new StringBuffer("{ ");
- for (Iterator iter = this.keySet().iterator(); iter.hasNext(); ) {
- SymbolNode param = (SymbolNode)iter.next();
+ for (Iterator<SymbolNode> iter = this.keySet().iterator(); iter.hasNext(); ) {
+ SymbolNode param = iter.next();
sb.append(param.getName() + " -> " + this.get(param));
if (iter.hasNext()) sb.append(", ");
}
diff --git a/tlatools/src/tla2sany/semantic/StringNode.java b/tlatools/src/tla2sany/semantic/StringNode.java
index 054c5077b397d17aebf4683d9b247cc0f49f9c50..89ca90d926a2804e11b6750cdc1381d2013de5c6 100644
--- a/tlatools/src/tla2sany/semantic/StringNode.java
+++ b/tlatools/src/tla2sany/semantic/StringNode.java
@@ -6,6 +6,7 @@ import java.util.Hashtable;
import tla2sany.explorer.ExploreNode;
import tla2sany.st.TreeNode;
+import tla2sany.xml.SymbolContext;
import util.UniqueString;
import org.w3c.dom.Document;
@@ -47,6 +48,7 @@ public class StringNode extends ExprNode implements ExploreNode {
public final UniqueString getRep() { return this.value; }
/* Level Checking */
+ @Override
public final boolean levelCheck(int iter) {
levelChecked = iter;
/*********************************************************************
@@ -81,11 +83,12 @@ public class StringNode extends ExprNode implements ExploreNode {
// "ArgLevelParams: " + this.getArgLevelParams() + "\n" ;
// }
- public final void walkGraph(Hashtable semNodesTable) {
+ @Override
+ public final void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
- semNodesTable.put(new Integer(myUID), this);
+ semNodesTable.put(uid, this);
}
final String PrintVersion(String str) {
@@ -118,6 +121,7 @@ public class StringNode extends ExprNode implements ExploreNode {
return buf.toString();
}
+ @Override
public final String toString(int depth) {
if (depth <= 0) return "";
return "\n*StringNode: " + super.toString(depth)
@@ -125,7 +129,8 @@ public class StringNode extends ExprNode implements ExploreNode {
"'" + " Length: " + value.length();
}
- protected Element getLevelElement(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ protected Element getLevelElement(Document doc, SymbolContext context) {
Element e = doc.createElement("StringValue");
Node n = doc.createTextNode(value.toString());
e.appendChild(n);
diff --git a/tlatools/src/tla2sany/semantic/Subst.java b/tlatools/src/tla2sany/semantic/Subst.java
index 4e91afb6866dbb8c81e954b5644973b6999e83e8..5cf6e9fd761f769b6b37211f25713532888b2788 100644
--- a/tlatools/src/tla2sany/semantic/Subst.java
+++ b/tlatools/src/tla2sany/semantic/Subst.java
@@ -9,7 +9,7 @@ import java.util.Iterator;
import tla2sany.explorer.ExploreNode;
import tla2sany.st.TreeNode;
import tla2sany.utilities.Strings;
-
+import tla2sany.xml.SymbolContext;
import tla2sany.xml.XMLExportable;
import org.w3c.dom.Document;
import org.w3c.dom.Element;
@@ -59,7 +59,7 @@ public class Subst implements LevelConstants, ASTConstants, ExploreNode, XMLExpo
return null;
}
- public static HashSet paramSet(Object param, Subst[] subs) {
+ public static HashSet<SymbolNode> paramSet(SymbolNode param, Subst[] subs) {
/***********************************************************************
* If subs[i] is of the form `parm <- expr', then it returns the *
* expr.levelParams. Otherwise, it returns the HashSet containing *
@@ -76,12 +76,12 @@ public class Subst implements LevelConstants, ASTConstants, ExploreNode, XMLExpo
return subs[idx].getExpr().getLevelParams();
}
- HashSet res = new HashSet();
+ HashSet<SymbolNode> res = new HashSet<>();
res.add(param);
return res;
}
- public static HashSet allParamSet(Object param, Subst[] subs) {
+ public static HashSet<SymbolNode> allParamSet(SymbolNode param, Subst[] subs) {
/***********************************************************************
* This is exactly like paramSet, except it returns the allParams *
* HashSet instead of levelParams. *
@@ -94,7 +94,7 @@ public class Subst implements LevelConstants, ASTConstants, ExploreNode, XMLExpo
return subs[idx].getExpr().getAllParams();
}
- HashSet res = new HashSet();
+ HashSet<SymbolNode> res = new HashSet<>();
res.add(param);
return res;
}
@@ -110,10 +110,10 @@ public class Subst implements LevelConstants, ASTConstants, ExploreNode, XMLExpo
***********************************************************************/
SetOfLevelConstraints res = new SetOfLevelConstraints();
SetOfLevelConstraints lcSet = body.getLevelConstraints();
- Iterator iter = lcSet.keySet().iterator();
+ Iterator<SymbolNode> iter = lcSet.keySet().iterator();
while (iter.hasNext()) {
- SymbolNode param = (SymbolNode)iter.next();
- Object plevel = lcSet.get(param);
+ SymbolNode param = iter.next();
+ Integer plevel = lcSet.get(param);
if (!isConstant) {
if (param.getKind() == ConstantDeclKind) {
plevel = Levels[ConstantLevel];
@@ -122,15 +122,15 @@ public class Subst implements LevelConstants, ASTConstants, ExploreNode, XMLExpo
plevel = Levels[VariableLevel];
}
}
- Iterator iter1 = paramSet(param, subs).iterator();
+ Iterator<SymbolNode> iter1 = paramSet(param, subs).iterator();
while (iter1.hasNext()) {
res.put(iter1.next(), plevel);
}
}
- HashSet alpSet = body.getArgLevelParams();
- iter = alpSet.iterator();
- while (iter.hasNext()) {
- ArgLevelParam alp = (ArgLevelParam)iter.next();
+ HashSet<ArgLevelParam> alpSet = body.getArgLevelParams();
+ Iterator<ArgLevelParam> alpIter = alpSet.iterator();
+ while (alpIter.hasNext()) {
+ ArgLevelParam alp = alpIter.next();
OpArgNode sub = (OpArgNode)getSub(alp.op, subs);
if (sub != null &&
sub.getOp() instanceof OpDefNode) {
@@ -145,7 +145,7 @@ public class Subst implements LevelConstants, ASTConstants, ExploreNode, XMLExpo
* argument of this method. *
*****************************************************************/
Integer mlevel = new Integer(subDef.getMaxLevel(alp.i));
- Iterator iter1 = paramSet(alp.param, subs).iterator();
+ Iterator<SymbolNode> iter1 = paramSet(alp.param, subs).iterator();
while (iter1.hasNext()) {
res.put(iter1.next(), mlevel);
}
@@ -162,10 +162,10 @@ public class Subst implements LevelConstants, ASTConstants, ExploreNode, XMLExpo
***********************************************************************/
SetOfArgLevelConstraints res = new SetOfArgLevelConstraints();
SetOfArgLevelConstraints alcSet = body.getArgLevelConstraints();
- Iterator iter = alcSet.keySet().iterator();
+ Iterator<ParamAndPosition> iter = alcSet.keySet().iterator();
while (iter.hasNext()) {
- ParamAndPosition pap = (ParamAndPosition)iter.next();
- Object plevel = alcSet.get(pap);
+ ParamAndPosition pap = iter.next();
+ Integer plevel = alcSet.get(pap);
ExprOrOpArgNode sub = getSub(pap.param, subs);
if (sub == null) {
res.put(pap, plevel);
@@ -178,10 +178,10 @@ public class Subst implements LevelConstants, ASTConstants, ExploreNode, XMLExpo
}
}
}
- HashSet alpSet = body.getArgLevelParams();
- iter = alpSet.iterator();
- while (iter.hasNext()) {
- ArgLevelParam alp = (ArgLevelParam)iter.next();
+ HashSet<ArgLevelParam> alpSet = body.getArgLevelParams();
+ Iterator<ArgLevelParam> alpIter = alpSet.iterator();
+ while (alpIter.hasNext()) {
+ ArgLevelParam alp = alpIter.next();
ExprOrOpArgNode subParam = getSub(alp.param, subs);
if (subParam != null) {
ExprOrOpArgNode subOp = getSub(alp.op, subs);
@@ -200,16 +200,16 @@ public class Subst implements LevelConstants, ASTConstants, ExploreNode, XMLExpo
return res;
}
- public static HashSet getSubALPSet(LevelNode body, Subst[] subs) {
+ public static HashSet<ArgLevelParam> getSubALPSet(LevelNode body, Subst[] subs) {
/***********************************************************************
* This should only be called after level checking has been called on *
* body and on all subs[i].getExpr(). *
***********************************************************************/
- HashSet res = new HashSet();
- HashSet alpSet = body.getArgLevelParams();
- Iterator iter = alpSet.iterator();
+ HashSet<ArgLevelParam> res = new HashSet<>();
+ HashSet<ArgLevelParam> alpSet = body.getArgLevelParams();
+ Iterator<ArgLevelParam> iter = alpSet.iterator();
while (iter.hasNext()) {
- ArgLevelParam alp = (ArgLevelParam)iter.next();
+ ArgLevelParam alp = iter.next();
ExprOrOpArgNode sub = getSub(alp.op, subs);
if (sub == null) {
res.add(alp);
@@ -217,9 +217,9 @@ public class Subst implements LevelConstants, ASTConstants, ExploreNode, XMLExpo
else {
SymbolNode subOp = ((OpArgNode)sub).getOp();
if (subOp.isParam()) {
- Iterator iter1 = paramSet(alp.param, subs).iterator();
+ Iterator<SymbolNode> iter1 = paramSet(alp.param, subs).iterator();
while (iter1.hasNext()) {
- res.add(new ArgLevelParam(subOp, alp.i, (SymbolNode)iter1.next()));
+ res.add(new ArgLevelParam(subOp, alp.i, iter1.next()));
}
}
}
@@ -229,7 +229,7 @@ public class Subst implements LevelConstants, ASTConstants, ExploreNode, XMLExpo
public final String levelDataToString() { return "Dummy level string"; }
- public final void walkGraph(Hashtable semNodesTable) {
+ public final void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
if (op != null) op.walkGraph(semNodesTable);
if (expr != null) expr.walkGraph(semNodesTable);
}
@@ -240,7 +240,7 @@ public class Subst implements LevelConstants, ASTConstants, ExploreNode, XMLExpo
"\nExpr: " + Strings.indent(2,(expr!=null ? expr.toString(depth-1) : "<null>"));
}
- public Element export(Document doc, tla2sany.xml.SymbolContext context) {
+ public Element export(Document doc, SymbolContext context) {
Element ret = doc.createElement("Subst");
ret.appendChild(op.export(doc,context));
ret.appendChild(expr.export(doc,context));
diff --git a/tlatools/src/tla2sany/semantic/SubstInNode.java b/tlatools/src/tla2sany/semantic/SubstInNode.java
index 07230da85a00f4a1062a90e26390665170f0c78f..8d8c757e8312784ada75834420d758c823e3e10b 100644
--- a/tlatools/src/tla2sany/semantic/SubstInNode.java
+++ b/tlatools/src/tla2sany/semantic/SubstInNode.java
@@ -24,9 +24,11 @@ import java.util.HashSet;
import java.util.Hashtable;
import java.util.Iterator;
+import tla2sany.explorer.ExploreNode;
import tla2sany.st.TreeNode;
import tla2sany.utilities.Strings;
import tla2sany.utilities.Vector;
+import tla2sany.xml.SymbolContext;
import util.UniqueString;
import org.w3c.dom.Document;
@@ -196,7 +198,8 @@ public class SubstInNode extends ExprNode {
* to this method can contain a mixture of explicit and implicit
* substitutions
*/
- final void addExplicitSubstitute(Context instanceeCtxt, UniqueString lhs,
+ @SuppressWarnings("unused") // TODO final else block is dead code
+ final void addExplicitSubstitute(Context instanceCtxt, UniqueString lhs,
TreeNode stn, ExprOrOpArgNode sub) {
int index;
for (index = 0; index < this.substs.length; index++) {
@@ -224,7 +227,7 @@ public class SubstInNode extends ExprNode {
// the instancee context
// look up the lhs symbol in the instancee context
- SymbolNode lhsSymbol = instanceeCtxt.getSymbol(lhs);
+ SymbolNode lhsSymbol = instanceCtxt.getSymbol(lhs);
// lhs must be an OpDeclNode; if not just return, as this error
// will have been earlier, though semantic analysis was allowed
@@ -291,6 +294,8 @@ public class SubstInNode extends ExprNode {
// private SetOfArgLevelConstraints argLevelConstraints;
// private HashSet argLevelParams;
+ @Override
+ @SuppressWarnings("unchecked")
public final boolean levelCheck(int itr) {
if (this.levelChecked >= itr) return this.levelCorrect;
this.levelChecked = itr ;
@@ -311,7 +316,7 @@ public class SubstInNode extends ExprNode {
// Calculate the level information
this.level = this.body.getLevel();
- HashSet lpSet = this.body.getLevelParams();
+ HashSet<SymbolNode> lpSet = this.body.getLevelParams();
for (int i = 0; i < this.substs.length; i++) {
if (lpSet.contains(this.getSubFor(i))) {
this.level = Math.max(level, this.getSubWith(i).getLevel());
@@ -319,10 +324,9 @@ public class SubstInNode extends ExprNode {
}
// this.levelParams = new HashSet();
- Iterator iter = lpSet.iterator();
+ Iterator<SymbolNode> iter = lpSet.iterator();
while (iter.hasNext()) {
- Object param = iter.next();
- this.levelParams.addAll(Subst.paramSet(param, this.substs));
+ this.levelParams.addAll(Subst.paramSet(iter.next(), this.substs));
/*******************************************************************
* At this point, levelCheck(itr) has been invoked on *
* this.substs[i].getExpr() (which equals this.getSubWith(i)). *
@@ -353,8 +357,8 @@ public class SubstInNode extends ExprNode {
* 23 February 2009: Added ".clone" to the following statements to fix *
* bug. *
***********************************************************************/
- this.allParams = (HashSet) this.body.getAllParams().clone() ;
- this.nonLeibnizParams = (HashSet) this.body.getNonLeibnizParams().clone() ;
+ this.allParams = (HashSet<SymbolNode>)this.body.getAllParams().clone() ;
+ this.nonLeibnizParams = (HashSet<SymbolNode>)this.body.getNonLeibnizParams().clone() ;
for (int i = 0 ; i < this.substs.length ; i++) {
OpDeclNode param = substs[i].getOp() ;
if (this.allParams.contains(param)) {
@@ -460,6 +464,7 @@ public class SubstInNode extends ExprNode {
// "ArgLevelParams: " + this.argLevelParams + "\n" ;
// }
+ @Override
public final String toString(int depth) {
if (depth <= 0) return "";
@@ -489,6 +494,7 @@ public class SubstInNode extends ExprNode {
* The children of this node are the body and the expressions
* being substituted for symbols.
*/
+ @Override
public SemanticNode[] getChildren() {
SemanticNode[] res = new SemanticNode[this.substs.length + 1];
res[0] = this.body;
@@ -498,11 +504,12 @@ public class SubstInNode extends ExprNode {
return res;
}
- public final void walkGraph(Hashtable semNodesTable) {
+ @Override
+ public final void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
- semNodesTable.put(new Integer(myUID), this);
+ semNodesTable.put(uid, this);
if (this.substs != null) {
for (int i = 0; i < this.substs.length; i++) {
@@ -513,16 +520,28 @@ public class SubstInNode extends ExprNode {
return;
}
- protected Element getLevelElement(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ protected Element getLevelElement(Document doc, SymbolContext context) {
Element sbts = doc.createElement("substs");
for (int i=0; i<substs.length; i++) {
sbts.appendChild(substs[i].export(doc,context));
}
Element bdy = doc.createElement("body");
bdy.appendChild(body.export(doc,context));
+
+ Element from = doc.createElement("instFrom");
+ Element fromchild = this.instantiatingModule.export(doc, context);
+ from.appendChild(fromchild);
+
+ Element to = doc.createElement("instTo");
+ Element tochild = instantiatedModule.export(doc,context);
+ to.appendChild(tochild);
+
Element ret = doc.createElement("SubstInNode");
ret.appendChild(sbts);
ret.appendChild(bdy);
+ ret.appendChild(from);
+ ret.appendChild(to);
// at the end, we append the context of the symbols used in this node
//ret.appendChild(instanceeCtxt.export(doc));
diff --git a/tlatools/src/tla2sany/semantic/TheoremNode.java b/tlatools/src/tla2sany/semantic/TheoremNode.java
index a9373f030a3d047bf43e6c2a3f9cddad42cf133b..c50b3591c660ff1fc9e0e85291d1eb98cc5c6a1e 100644
--- a/tlatools/src/tla2sany/semantic/TheoremNode.java
+++ b/tlatools/src/tla2sany/semantic/TheoremNode.java
@@ -15,8 +15,10 @@ package tla2sany.semantic;
import java.util.Hashtable;
+import tla2sany.explorer.ExploreNode;
import tla2sany.st.TreeNode;
import tla2sany.utilities.Strings;
+import tla2sany.xml.SymbolContext;
import util.UniqueString;
import org.w3c.dom.Document;
@@ -112,7 +114,8 @@ public class TheoremNode extends LevelNode {
/* (non-Javadoc)
* @see tla2sany.semantic.LevelNode#levelCheck(int)
*/
-public final boolean levelCheck(int iter) {
+ @Override
+ public final boolean levelCheck(int iter) {
if (levelChecked >= iter) {return true ;} ;
levelChecked = iter;
LevelNode sub[] ;
@@ -318,6 +321,7 @@ public final boolean levelCheck(int iter) {
* toString, levelDataToString, and walkGraph methods to implement
* ExploreNode interface
*/
+ @Override
public final String levelDataToString() {
return "Level: " + this.getLevel() + "\n" +
"LevelParameters: " + this.getLevelParams() + "\n" +
@@ -326,6 +330,7 @@ public final boolean levelCheck(int iter) {
"ArgLevelParams: " + this.getArgLevelParams() + "\n";
}
+ @Override
public final String toString(int depth) {
if (depth <= 0) return "";
String res =
@@ -358,6 +363,7 @@ public final boolean levelCheck(int iter) {
* The children are the statement and the proof (if there is one).
*/
+ @Override
public SemanticNode[] getChildren() {
if (this.proof == null) {
return new SemanticNode[] {this.theoremExprOrAssumeProve};
@@ -366,7 +372,8 @@ public final boolean levelCheck(int iter) {
this.proof};
}
- public final void walkGraph(Hashtable semNodesTable) {
+ @Override
+ public final void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
semNodesTable.put(uid, this);
@@ -384,7 +391,7 @@ public final boolean levelCheck(int iter) {
/* MR: This is the same as SymbolNode.exportDefinition. Exports the actual theorem content, not only a reference.
*/
- public Element exportDefinition(Document doc, tla2sany.xml.SymbolContext context) {
+ public Element exportDefinition(Document doc, SymbolContext context) {
//makes sure that the we are creating an entry in the database
if (!context.isTop_level_entry())
throw new IllegalArgumentException("Exporting theorem ref "+getNodeRef()+" twice!");
@@ -440,7 +447,8 @@ public final boolean levelCheck(int iter) {
}
/* overrides LevelNode.export and exports a UID reference instad of the full version*/
- public Element export(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ public Element export(Document doc, SymbolContext context) {
// first add symbol to context
context.put(this, doc);
Element e = doc.createElement(getNodeRef());
diff --git a/tlatools/src/tla2sany/semantic/ThmOrAssumpDefNode.java b/tlatools/src/tla2sany/semantic/ThmOrAssumpDefNode.java
index 9df5b8be650ffd0a21d0e02f0e89b79cbc34ec35..c0dad86488d61413b3e844dd5d34110ef2c1b8d1 100644
--- a/tlatools/src/tla2sany/semantic/ThmOrAssumpDefNode.java
+++ b/tlatools/src/tla2sany/semantic/ThmOrAssumpDefNode.java
@@ -27,15 +27,16 @@ import java.util.HashSet;
import java.util.Hashtable;
import java.util.Iterator;
+import tla2sany.explorer.ExploreNode;
import tla2sany.st.TreeNode;
import tla2sany.utilities.Strings;
import tla2sany.utilities.Vector;
+import tla2sany.xml.SymbolContext;
import util.UniqueString;
import util.WrongInvocationException;
import org.w3c.dom.Document;
import org.w3c.dom.Element;
-import org.w3c.dom.Node;
/***************************************************************************
* This node represents the definition of Foo in *
@@ -85,8 +86,8 @@ public class ThmOrAssumpDefNode extends SymbolNode
* the body that are not within the scope of an inner label or LET *
* definition. *
*************************************************************************/
- private Hashtable labels = null ;
- public Hashtable getLabelsHT() {
+ private Hashtable<UniqueString, LabelNode> labels = null ;
+ public Hashtable<UniqueString, LabelNode> getLabelsHT() {
/***********************************************************************
* Return the labels field. Used to "clone" an OpDefNode for module *
* instantiation. *
@@ -292,7 +293,7 @@ public class ThmOrAssumpDefNode extends SymbolNode
* There doesn't seem to be any easy way to write these methods only *
* once. *
*************************************************************************/
- public void setLabels(Hashtable ht) {labels = ht; }
+ public void setLabels(Hashtable<UniqueString, LabelNode> ht) {labels = ht; }
/***********************************************************************
* Sets the set of labels. *
***********************************************************************/
@@ -312,8 +313,8 @@ public class ThmOrAssumpDefNode extends SymbolNode
* as odn, then odn is added to the set and true is return; else the *
* set is unchanged and false is returned. *
***********************************************************************/
- if (labels == null) {labels = new Hashtable(); } ;
- if (labels.containsKey(odn)) {return false ;} ;
+ if (labels == null) {labels = new Hashtable<>(); } ;
+ if (labels.containsKey(odn.getName())) {return false ;} ;
labels.put(odn.getName(), odn) ;
return true;
}
@@ -324,12 +325,12 @@ public class ThmOrAssumpDefNode extends SymbolNode
* `labels'. *
***********************************************************************/
if (labels == null) {return new LabelNode[0];} ;
- Vector v = new Vector() ;
- Enumeration e = labels.elements() ;
+ Vector<LabelNode> v = new Vector<>() ;
+ Enumeration<LabelNode> e = labels.elements() ;
while (e.hasMoreElements()) { v.addElement(e.nextElement()); } ;
LabelNode[] retVal = new LabelNode[v.size()] ;
for (int i = 0 ; i < v.size() ; i++)
- {retVal[i] = (LabelNode) v.elementAt(i); } ;
+ {retVal[i] = v.elementAt(i); } ;
return retVal ;
}
@@ -417,6 +418,7 @@ public class ThmOrAssumpDefNode extends SymbolNode
* parameter of the definition of op appears within the k-th argument *
* of opArg. *
***********************************************************************/
+ @Override
public final boolean levelCheck(int itr) {
if (this.levelChecked >= itr) { return this.levelCorrect; }
this.levelChecked = itr ;
@@ -573,17 +575,20 @@ public class ThmOrAssumpDefNode extends SymbolNode
/**
* The body is the node's only child.
*/
+ @Override
public SemanticNode[] getChildren() {
return new SemanticNode[] {this.body};
}
- public final void walkGraph(Hashtable semNodesTable) {
+ @Override
+ public final void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
- semNodesTable.put(new Integer(myUID), this);
+ semNodesTable.put(uid, this);
if(this.body != null) {this.body.walkGraph(semNodesTable) ;} ;
}
+ @Override
public final String toString(int depth) {
if (depth <= 0) return "";
String ret =
@@ -617,9 +622,9 @@ public class ThmOrAssumpDefNode extends SymbolNode
***********************************************************************/
if (labels != null) {
ret += "\n Labels: " ;
- Enumeration list = labels.keys() ;
+ Enumeration<UniqueString> list = labels.keys() ;
while (list.hasMoreElements()) {
- ret += ((UniqueString) list.nextElement()).toString() + " " ;
+ ret += list.nextElement().toString() + " " ;
} ;
}
else {ret += "\n Labels: null";};
@@ -657,7 +662,8 @@ public class ThmOrAssumpDefNode extends SymbolNode
}
/* overrides LevelNode.export and exports a UID reference instad of the full version*/
- public Element export(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ public Element export(Document doc, SymbolContext context) {
// first add symbol to context
context.put(this, doc);
Element e = doc.createElement(getNodeRef());
diff --git a/tlatools/src/tla2sany/semantic/UseOrHideNode.java b/tlatools/src/tla2sany/semantic/UseOrHideNode.java
index 2c5198c6000a90aa24634b6be4c14e1552a6141b..7fb248d776c140ed4d69963e98bcb2b47c2bc305 100644
--- a/tlatools/src/tla2sany/semantic/UseOrHideNode.java
+++ b/tlatools/src/tla2sany/semantic/UseOrHideNode.java
@@ -4,8 +4,10 @@ package tla2sany.semantic;
import java.util.Hashtable;
+import tla2sany.explorer.ExploreNode;
import tla2sany.st.TreeNode;
import tla2sany.utilities.Strings;
+import tla2sany.xml.SymbolContext;
import util.UniqueString;
import org.w3c.dom.Document;
@@ -101,6 +103,7 @@ public class UseOrHideNode extends LevelNode {
} // for
}
+ @Override
public boolean levelCheck(int iter) {
/***********************************************************************
* Level checking is performed by level-checking the facts. Since the *
@@ -111,10 +114,11 @@ public class UseOrHideNode extends LevelNode {
return this.levelCheckSubnodes(iter, facts) ;
}
- public void walkGraph(Hashtable semNodesTable) {
+ @Override
+ public void walkGraph(Hashtable<Integer, ExploreNode> semNodesTable) {
Integer uid = new Integer(myUID);
if (semNodesTable.get(uid) != null) return;
- semNodesTable.put(new Integer(myUID), this);
+ semNodesTable.put(uid, this);
for (int i = 0; i < facts.length; i++) {
facts[i].walkGraph(semNodesTable);
} ;
@@ -128,6 +132,7 @@ public class UseOrHideNode extends LevelNode {
* The children are the facts.
* @see tla2sany.semantic.SemanticNode#getChildren()
*/
+ @Override
public SemanticNode[] getChildren() {
if (this.facts == null || this.facts.length == 0) {
return null;
@@ -139,6 +144,7 @@ public class UseOrHideNode extends LevelNode {
return res;
}
+ @Override
public String toString(int depth) {
if (depth <= 0) return "";
String ret = "\n*UseOrHideNode:\n"
@@ -155,7 +161,8 @@ public class UseOrHideNode extends LevelNode {
return ret;
}
- protected Element getLevelElement(Document doc, tla2sany.xml.SymbolContext context) {
+ @Override
+ protected Element getLevelElement(Document doc, SymbolContext context) {
//SemanticNode.SymbolContext context = new SemanticNode.SymbolContext(context2);
Element e = doc.createElement("UseOrHideNode");
diff --git a/tlatools/src/tla2sany/st/Location.java b/tlatools/src/tla2sany/st/Location.java
index beb23da1221988e279612e478a6a02565447798c..8daad5cd8b11c203e27580acfae969306fe19eb9 100644
--- a/tlatools/src/tla2sany/st/Location.java
+++ b/tlatools/src/tla2sany/st/Location.java
@@ -36,7 +36,7 @@ public final class Location
private static final String NATURAL = "([0-9]+)";
private static final String MODULE_ID = "([A-Za-z_0-9]+)";
private static final String CLOSE_ACTION = ">";
- private static final String OPEN_ACTION = "<Action ";
+ private static final String OPEN_ACTION = "<[A-Za-z_0-9]+ "; // The regex used to just be "Action" but the most recent TLC prints the name of the action instead of just the location.
private static final UniqueString unknown = UniqueString.uniqueStringOf("--unknown--");
diff --git a/tlatools/src/tla2sany/utilities/Vector.java b/tlatools/src/tla2sany/utilities/Vector.java
index f22e094a477f634a421763319b4c0c72d2d9a8ab..21705a210ab01b86b225f8d3f642441d2e33c96d 100644
--- a/tlatools/src/tla2sany/utilities/Vector.java
+++ b/tlatools/src/tla2sany/utilities/Vector.java
@@ -2,7 +2,7 @@
package tla2sany.utilities;
import java.util.Enumeration;
-public class Vector {
+public class Vector<E> {
static int defaultSize = 10;
protected Object info[];
@@ -38,7 +38,7 @@ public class Vector {
}
*/
- public final void addElement( Object obj ) {
+ public final void addElement( E obj ) {
if (size == capacity) {
Object next[] = new Object[ capacity + increment ];
System.arraycopy( info, 0, next, 0, capacity );
@@ -49,19 +49,22 @@ public class Vector {
size++;
}
- public final Object firstElement() {
- return info[0];
+ @SuppressWarnings("unchecked")
+ public final E firstElement() {
+ return (E)info[0];
}
- public final Object lastElement() {
- return info[ size-1 ];
+ @SuppressWarnings("unchecked")
+ public final E lastElement() {
+ return (E)info[ size-1 ];
}
- public final Object elementAt(int i) {
+ @SuppressWarnings("unchecked")
+ public final E elementAt(int i) {
if (i < 0 || i >= size )
throw new ArrayIndexOutOfBoundsException();
else
- return info[ i ];
+ return (E)info[ i ];
}
public final void removeAllElements() {
@@ -82,7 +85,7 @@ public class Vector {
}
}
- public final void insertElementAt( Object obj, int i ) {
+ public final void insertElementAt( E obj, int i ) {
if (i < 0 || i >= size )
throw new ArrayIndexOutOfBoundsException();
else if (size == capacity) {
@@ -100,25 +103,25 @@ public class Vector {
size++;
}
- public final void setElementAt( Object obj, int i ) {
+ public final void setElementAt( E obj, int i ) {
if (i < 0 || i >= size )
throw new ArrayIndexOutOfBoundsException();
else
info[ i ] = obj;
}
- public final boolean contains (Object obj) {
+ public final boolean contains (E obj) {
for (int i = 0; i < size; i++) {
if ( info[ i ] == obj ) return true;
}
return false;
}
- public final Enumeration elements() {
- return new VectorEnumeration( info, size );
+ public final Enumeration<E> elements() {
+ return new VectorEnumeration<E>( info, size );
}
- public final void append( Vector v ) {
+ public final void append( Vector<E> v ) {
if ( v.size + size > capacity ) {
Object neo[] = new Object[ capacity + v.capacity ];
capacity += v.capacity;
@@ -132,12 +135,13 @@ public class Vector {
// Like the append method above, but elements of v will not be added to THIS Vector
// if they are already present at least once; repeated elements already in
// THIS Vector, however, will not be removed.
- public final void appendNoRepeats(Vector v) {
+ public final void appendNoRepeats(Vector<E> v) {
for (int i = 0; i < v.size(); i++) {
if ( ! this.contains(v.elementAt(i)) ) this.addElement(v.elementAt(i));
}
}
+ @Override
public final String toString() {
String ret;
ret = "[ ";
diff --git a/tlatools/src/tla2sany/utilities/VectorEnumeration.java b/tlatools/src/tla2sany/utilities/VectorEnumeration.java
index 2d3dbe35010cce11f6471d1155fd19069c8f8002..9ab1fe506cc05ac61276392df4f6fae3dd457890 100644
--- a/tlatools/src/tla2sany/utilities/VectorEnumeration.java
+++ b/tlatools/src/tla2sany/utilities/VectorEnumeration.java
@@ -2,7 +2,7 @@
package tla2sany.utilities;
import java.util.Enumeration;
-final class VectorEnumeration implements Enumeration {
+final class VectorEnumeration<E> implements Enumeration<E> {
int index = 0;
Object data[];
@@ -15,9 +15,10 @@ final class VectorEnumeration implements Enumeration {
return index < data.length;
}
- public final Object nextElement() {
+ @SuppressWarnings("unchecked")
+ public final E nextElement() {
if (index < data.length)
- return data[index++];
+ return (E)data[index++];
else
throw new java.util.NoSuchElementException();
}
diff --git a/tlatools/src/tla2sany/xml/sany.xsd b/tlatools/src/tla2sany/xml/sany.xsd
index 09d9687e8f58fa01890b09fead54018c40f26957..6201603de0c611cf2ca2301f97aa0bdecdadafff 100644
--- a/tlatools/src/tla2sany/xml/sany.xsd
+++ b/tlatools/src/tla2sany/xml/sany.xsd
@@ -230,6 +230,20 @@
</xs:choice>
</xs:complexType>
</xs:element>
+ <xs:element name="instFrom">
+ <xs:complexType>
+ <xs:sequence>
+ <xs:element ref="ModuleNodeRef"/>
+ </xs:sequence>
+ </xs:complexType>
+ </xs:element>
+ <xs:element name="instTo">
+ <xs:complexType>
+ <xs:sequence>
+ <xs:element ref="ModuleNodeRef"/>
+ </xs:sequence>
+ </xs:complexType>
+ </xs:element>
</xs:sequence>
</xs:complexType>
</xs:element>
@@ -254,6 +268,20 @@
</xs:sequence>
</xs:complexType>
</xs:element>
+ <xs:element name="instFrom">
+ <xs:complexType>
+ <xs:sequence>
+ <xs:element ref="ModuleNodeRef"/>
+ </xs:sequence>
+ </xs:complexType>
+ </xs:element>
+ <xs:element name="instTo">
+ <xs:complexType>
+ <xs:sequence>
+ <xs:element ref="ModuleNodeRef"/>
+ </xs:sequence>
+ </xs:complexType>
+ </xs:element>
</xs:sequence>
</xs:complexType>
</xs:element>
diff --git a/tlatools/src/tlc2/TLCGlobals.java b/tlatools/src/tlc2/TLCGlobals.java
index 1c05c17461d08af16d8f8108805fbccca03f78f6..0780ec0f071f42b04b6ddf212faeff200e474416 100644
--- a/tlatools/src/tlc2/TLCGlobals.java
+++ b/tlatools/src/tlc2/TLCGlobals.java
@@ -22,7 +22,7 @@ public class TLCGlobals
{
// The current version of TLC
- public static String versionOfTLC = "Version 2.10 of 28 September 2017";
+ public static String versionOfTLC = "Version 2.11 of 05 January 2018";
// The bound for set enumeration, used for pretty printing
public static int enumBound = 2000;
diff --git a/tlatools/src/tlc2/tool/Action.java b/tlatools/src/tlc2/tool/Action.java
index ba497238ed2933ab19af1d30d32c3b17f4b0984d..621fc27fabf7d490e80764b6947877e8a4946400 100644
--- a/tlatools/src/tlc2/tool/Action.java
+++ b/tlatools/src/tlc2/tool/Action.java
@@ -7,6 +7,7 @@ import java.io.Serializable;
import tla2sany.semantic.SemanticNode;
import tlc2.util.Context;
+import util.UniqueString;
public final class Action implements ToolGlobals, Serializable {
/* A TLA+ action. */
@@ -14,19 +15,29 @@ public final class Action implements ToolGlobals, Serializable {
/* Fields */
public final SemanticNode pred; // Expression of the action
public final Context con; // Context of the action
+ private final UniqueString actionName;
/* Constructors */
public Action(SemanticNode pred, Context con) {
- this.pred = pred;
- this.con = con;
+ this(pred, con, (UniqueString) null);
}
- /* Returns a string representation of this action. */
+ public Action(SemanticNode pred, Context con, UniqueString actionName) {
+ this.pred = pred;
+ this.con = con;
+ this.actionName = actionName;
+ }
+
+/* Returns a string representation of this action. */
public final String toString() {
return "<Action " + pred.toString() + ">";
}
public final String getLocation() {
- return "<Action " + pred.getLocation() + ">";
+ if (actionName != null && !"".equals(actionName.toString())) {
+ // If known, print the action name instead of the generic string "Action".
+ return "<" + actionName + " " + pred.getLocation() + ">";
+ }
+ return "<Action " + pred.getLocation() + ">";
}
}
diff --git a/tlatools/src/tlc2/tool/Tool.java b/tlatools/src/tlc2/tool/Tool.java
index b5005e352a2eba1b48c0f02a3ce231d79ed99cd1..ad239434093d26e76378a92a5c58a158f4223cb1 100644
--- a/tlatools/src/tlc2/tool/Tool.java
+++ b/tlatools/src/tlc2/tool/Tool.java
@@ -163,20 +163,22 @@ public class Tool
return this.actions;
}
-
-
private final void getActions(SemanticNode next, Context con) {
+ this.getActions(next, con, null);
+ }
+
+ private final void getActions(SemanticNode next, Context con, final UniqueString actionName) {
switch (next.getKind()) {
case OpApplKind:
{
OpApplNode next1 = (OpApplNode)next;
- this.getActionsAppl(next1, con);
+ this.getActionsAppl(next1, con, actionName);
return;
}
case LetInKind:
{
LetInNode next1 = (LetInNode)next;
- this.getActions(next1.getBody(), con);
+ this.getActions(next1.getBody(), con, actionName);
return;
}
case SubstInKind:
@@ -184,10 +186,10 @@ public class Tool
SubstInNode next1 = (SubstInNode)next;
Subst[] substs = next1.getSubsts();
if (substs.length == 0) {
- this.getActions(next1.getBody(), con);
+ this.getActions(next1.getBody(), con, actionName);
}
else {
- Action action = new Action(next1, con);
+ Action action = new Action(next1, con, actionName);
this.actionVec.addElement(action);
}
return;
@@ -199,10 +201,10 @@ public class Tool
APSubstInNode next1 = (APSubstInNode)next;
Subst[] substs = next1.getSubsts();
if (substs.length == 0) {
- this.getActions(next1.getBody(), con);
+ this.getActions(next1.getBody(), con, actionName);
}
else {
- Action action = new Action(next1, con);
+ Action action = new Action(next1, con, actionName);
this.actionVec.addElement(action);
}
return;
@@ -214,7 +216,7 @@ public class Tool
case LabelKind:
{
LabelNode next1 = (LabelNode)next;
- this.getActions(next1.getBody(), con);
+ this.getActions(next1.getBody(), con, actionName);
return;
}
default:
@@ -224,7 +226,7 @@ public class Tool
}
}
- private final void getActionsAppl(OpApplNode next, Context con) {
+ private final void getActionsAppl(OpApplNode next, Context con, final UniqueString actionName) {
ExprOrOpArgNode[] args = next.getArgs();
SymbolNode opNode = next.getOperator();
int opcode = BuiltInOPs.getOpCode(opNode.getName());
@@ -250,7 +252,7 @@ public class Tool
Value aval = this.eval(args[i], con, TLCState.Empty);
con1 = con1.cons(formals[i], aval);
}
- this.getActions(opDef.getBody(), con1);
+ this.getActions(opDef.getBody(), con1, opDef.getName());
return;
}
}
@@ -258,7 +260,7 @@ public class Tool
}
}
if (opcode == 0) {
- Action action = new Action(next, con);
+ Action action = new Action(next, con, opNode.getName());
this.actionVec.addElement(action);
return;
}
@@ -273,11 +275,11 @@ public class Tool
this.contexts(next, con, TLCState.Empty, TLCState.Empty, EvalControl.Clear);
Context econ;
while ((econ = Enum.nextElement()) != null) {
- this.getActions(args[0], econ);
+ this.getActions(args[0], econ, actionName);
}
}
catch (Throwable e) {
- Action action = new Action(next, con);
+ Action action = new Action(next, con, actionName);
this.actionVec.removeAll(cnt);
this.actionVec.addElement(action);
}
@@ -287,14 +289,14 @@ public class Tool
case OPCODE_lor:
{
for (int i = 0; i < args.length; i++) {
- this.getActions(args[i], con);
+ this.getActions(args[i], con, actionName);
}
return;
}
default:
{
// We handle all the other builtin operators here.
- Action action = new Action(next, con);
+ Action action = new Action(next, con, actionName);
this.actionVec.addElement(action);
return;
}
@@ -480,7 +482,49 @@ public class Tool
Value[] argVals = new Value[alen];
// evaluate the actuals:
for (int i = 0; i < alen; i++) {
- argVals[i] = this.eval(args[i], c, ps);
+ /*
+ * MAK 12/2017: Effectively disable LazyValues by passing null to this.eval(..).
+ * This has the same effect as calling LazyValue#setUncachable upon the creation
+ * of a LV. However, at this stack level, the LV has long been created. It can
+ * not be set to be uncachable anymore. This changes fixes Github issue 113:
+ * "TLC fails to find initial states with bounded exists"
+ * https://github.com/tlaplus/tlaplus/issues/113. The corresponding unit test is
+ * tlc2.tool.AssignmentInitTest.
+ *
+ * The bug to fix is, that a the use of an LV breaks evaluation of expressions
+ * such as:
+ *
+ * Op(var) == var \in {0,1} /\ var > 0
+ *
+ * Op2(var) == \E val \in {0,1} : var = val /\ var > 0
+ *
+ * The "var" is represented by an instance of a LazyValue which only gets
+ * evaluated once. In the two examples above, the LV statically evaluates to "0"
+ * even when it should evaluate to "1".
+ *
+ * If the init predicate is defined to such that:
+ *
+ * VARIABLE s Init == Op2(s) ...
+ *
+ * TLC won't generate the initial state s=1. Likewise, the following expression
+ * causes TLC to generate two initial states (s=0 and s=1). Again, because the
+ * predicate "var < 1" is both times evaluated with "var=0".
+ *
+ * Init(var) == \E val \in 0..1: var = val /\ var < 1
+ *
+ * Unfortunately, this disables LazyValues for _all_ operators. It affects all
+ * operators such as IF THEN ELSE, Print, ... Disabling LV only for affected
+ * operators appears impossible at this stack level. We would somehow have to
+ * pass along the call context. Alternatively, an attempt could be made to call
+ * LazyValue#setUncachable upon creation of the LV. However, the LV gets created
+ * before the call stack "sees" the actual operator.
+ *
+ * If similar expressions are evaluated in the context of the next-state
+ * relation, line ~921 is responsible. It boils down to line 2059 (opcode prime)
+ * to disable LV by passing null to tlc2.tool.Tool.evalAppl(...) effectively
+ * disabling LVs.
+ */
+ argVals[i] = this.eval(args[i], c, ps, null, EvalControl.Clear);
}
// apply the operator:
bval = opVal.apply(argVals, EvalControl.Clear);
diff --git a/tlatools/src/tlc2/util/Context.java b/tlatools/src/tlc2/util/Context.java
index a3bf18284b112f9895972cf8fd2388f144f44fe8..bfa4c8847e93d5594cd9fea26e910d5fa3434e18 100644
--- a/tlatools/src/tlc2/util/Context.java
+++ b/tlatools/src/tlc2/util/Context.java
@@ -33,9 +33,6 @@ public final class Context {
private final Object value;
private final Context next;
- public int CNT = 1;
-
-
public final static Context Empty = new Context(null, null, null);
private final static Context BaseBranch = new Context(null, null, Empty);
diff --git a/tlatools/test-model/AssignmentInit.cfg b/tlatools/test-model/AssignmentInit.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..cea554fa6375ea5fbb9074b946f867a1bd02ac99
--- /dev/null
+++ b/tlatools/test-model/AssignmentInit.cfg
@@ -0,0 +1,7 @@
+SPECIFICATION
+Spec
+CONSTANT
+N = 42
+M = 42
+\*INVARIANT
+\*Inv
\ No newline at end of file
diff --git a/tlatools/test-model/AssignmentInit.tla b/tlatools/test-model/AssignmentInit.tla
new file mode 100644
index 0000000000000000000000000000000000000000..e8919f6eb8854a86274513e433499dab2638dbe7
--- /dev/null
+++ b/tlatools/test-model/AssignmentInit.tla
@@ -0,0 +1,23 @@
+--------------------------- MODULE AssignmentInit ---------------------------
+EXTENDS Integers
+VARIABLE s
+
+min(S) == CHOOSE e \in S: \A a \in S: e <= a
+
+InitExit(var, S) == \E val \in S: (var = val /\ var > min(S))
+
+InitAll(var, S) == \A val \in S: (var = val /\ var \in S)
+
+InitIn(var, S) == var \in S /\ var > min(S)
+
+\* With this Init(var), the test does not fail without its fix.
+\*Init(ignored) == \E val \in {0,1}: (s = val /\ s > 0)
+
+\* Init1 one state + Init3 one state
+Spec == /\ \/ InitExit(s, {0,1}) \* 1 unique state
+ \/ InitAll(s, {2}) \* 1 unique state
+ \/ InitIn(s, {4,5}) \* 1 unique state
+ \/ InitAll(s, {6,7}) \* 0 unique states
+ /\ [][UNCHANGED s]_s
+
+=============================================================================
diff --git a/tlatools/test-model/AssignmentInitExpensive.cfg b/tlatools/test-model/AssignmentInitExpensive.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..cea554fa6375ea5fbb9074b946f867a1bd02ac99
--- /dev/null
+++ b/tlatools/test-model/AssignmentInitExpensive.cfg
@@ -0,0 +1,7 @@
+SPECIFICATION
+Spec
+CONSTANT
+N = 42
+M = 42
+\*INVARIANT
+\*Inv
\ No newline at end of file
diff --git a/tlatools/test-model/AssignmentInitExpensive.tla b/tlatools/test-model/AssignmentInitExpensive.tla
new file mode 100644
index 0000000000000000000000000000000000000000..dc4091521a568de4fa2872183761c4392cdedc83
--- /dev/null
+++ b/tlatools/test-model/AssignmentInitExpensive.tla
@@ -0,0 +1,17 @@
+--------------------------- MODULE AssignmentInitExpensive ---------------------------
+EXTENDS Integers
+VARIABLE s
+
+\* expensiveOp takes ~10 seconds wallclock time on a modern day machine.
+\* The point is, that doing 10k times will make the test time out.
+expensiveOp == CHOOSE e \in SUBSET (1..18) : TRUE
+
+\* This variant (with an unused parameter) causes TLC to reevaluate
+\* CHOOSE ... SUBSET 10k times.
+\*expensiveOpParam(ignored) == CHOOSE e \in SUBSET (1..18) : TRUE
+
+Init(var) == \E val \in 0..10000: var = expensiveOp
+
+Spec == Init(s) /\ [][UNCHANGED s]_s
+
+=============================================================================
diff --git a/tlatools/test-model/AssignmentInitNeg.cfg b/tlatools/test-model/AssignmentInitNeg.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..c8cffbe64c3dcc8bce148218f2e7b66a7537f573
--- /dev/null
+++ b/tlatools/test-model/AssignmentInitNeg.cfg
@@ -0,0 +1,4 @@
+SPECIFICATION
+Spec
+INVARIANT
+Inv
\ No newline at end of file
diff --git a/tlatools/test-model/AssignmentInitNeg.tla b/tlatools/test-model/AssignmentInitNeg.tla
new file mode 100644
index 0000000000000000000000000000000000000000..8269be1a94fed8c333f1d2ee3e9bdb95ac0545b6
--- /dev/null
+++ b/tlatools/test-model/AssignmentInitNeg.tla
@@ -0,0 +1,10 @@
+--------------------------- MODULE AssignmentInitNeg ---------------------------
+EXTENDS Integers
+VARIABLE s
+
+Init(var) == \E val \in 0..1: (var = val /\ var < 1)
+
+Spec == Init(s) /\ [][UNCHANGED s]_s
+
+Inv == (s < 1)
+=============================================================================
diff --git a/tlatools/test-model/AssignmentNext.cfg b/tlatools/test-model/AssignmentNext.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..bc224b9def594b0819de3f0b45ede63ea8213c7b
--- /dev/null
+++ b/tlatools/test-model/AssignmentNext.cfg
@@ -0,0 +1,2 @@
+SPECIFICATION
+Spec
diff --git a/tlatools/test-model/AssignmentNext.tla b/tlatools/test-model/AssignmentNext.tla
new file mode 100644
index 0000000000000000000000000000000000000000..94574a5ebf9567f6050a745894ab80eac1a569b6
--- /dev/null
+++ b/tlatools/test-model/AssignmentNext.tla
@@ -0,0 +1,9 @@
+--------------------------- MODULE AssignmentNext ---------------------------
+EXTENDS Integers
+VARIABLE s
+
+Next(var) == \E val \in 0..1: (var' = val /\ var' > 0)
+
+Spec == s = "" /\ [][Next(s)]_s
+
+=============================================================================
diff --git a/tlatools/test/tlc2/tool/AssignmentInitExpensiveTest.java b/tlatools/test/tlc2/tool/AssignmentInitExpensiveTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..51f7fb0e5c305936edac8ade3aad5942286eec3a
--- /dev/null
+++ b/tlatools/test/tlc2/tool/AssignmentInitExpensiveTest.java
@@ -0,0 +1,48 @@
+/*******************************************************************************
+ * Copyright (c) 2017 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.assertFalse;
+import static org.junit.Assert.assertTrue;
+
+import org.junit.Test;
+
+import tlc2.output.EC;
+import tlc2.tool.liveness.ModelCheckerTestCase;
+
+public class AssignmentInitExpensiveTest extends ModelCheckerTestCase {
+
+ public AssignmentInitExpensiveTest() {
+ super("AssignmentInitExpensive");
+ }
+
+ @Test
+ public void test() {
+ assertTrue(recorder.recorded(EC.TLC_FINISHED));
+ assertFalse(recorder.recorded(EC.GENERAL));
+ assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, "10002", "1", "0"));
+ }
+}
diff --git a/tlatools/test/tlc2/tool/AssignmentInitNegTest.java b/tlatools/test/tlc2/tool/AssignmentInitNegTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..efe3d70b403ce0070707514fd6de3d1e9707db56
--- /dev/null
+++ b/tlatools/test/tlc2/tool/AssignmentInitNegTest.java
@@ -0,0 +1,48 @@
+/*******************************************************************************
+ * Copyright (c) 2017 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.assertFalse;
+import static org.junit.Assert.assertTrue;
+
+import org.junit.Test;
+
+import tlc2.output.EC;
+import tlc2.tool.liveness.ModelCheckerTestCase;
+
+public class AssignmentInitNegTest extends ModelCheckerTestCase {
+
+ public AssignmentInitNegTest() {
+ super("AssignmentInitNeg");
+ }
+
+ @Test
+ public void test() {
+ assertTrue(recorder.recorded(EC.TLC_FINISHED));
+ assertFalse(recorder.recorded(EC.GENERAL));
+ assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, "2", "1", "0"));
+ }
+}
diff --git a/tlatools/test/tlc2/tool/AssignmentInitTest.java b/tlatools/test/tlc2/tool/AssignmentInitTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..b6d75e72740aec382347fd4b124477eb342b4b60
--- /dev/null
+++ b/tlatools/test/tlc2/tool/AssignmentInitTest.java
@@ -0,0 +1,48 @@
+/*******************************************************************************
+ * Copyright (c) 2017 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.assertFalse;
+import static org.junit.Assert.assertTrue;
+
+import org.junit.Test;
+
+import tlc2.output.EC;
+import tlc2.tool.liveness.ModelCheckerTestCase;
+
+public class AssignmentInitTest extends ModelCheckerTestCase {
+
+ public AssignmentInitTest() {
+ super("AssignmentInit");
+ }
+
+ @Test
+ public void test() {
+ assertTrue(recorder.recorded(EC.TLC_FINISHED));
+ assertFalse(recorder.recorded(EC.GENERAL));
+ assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, "6", "3", "0"));
+ }
+}
diff --git a/tlatools/test/tlc2/tool/AssignmentNextTest.java b/tlatools/test/tlc2/tool/AssignmentNextTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..ba6798bdc40b2349a475505dcce7641d300ac76d
--- /dev/null
+++ b/tlatools/test/tlc2/tool/AssignmentNextTest.java
@@ -0,0 +1,48 @@
+/*******************************************************************************
+ * Copyright (c) 2017 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.assertFalse;
+import static org.junit.Assert.assertTrue;
+
+import org.junit.Test;
+
+import tlc2.output.EC;
+import tlc2.tool.liveness.ModelCheckerTestCase;
+
+public class AssignmentNextTest extends ModelCheckerTestCase {
+
+ public AssignmentNextTest() {
+ super("AssignmentNext");
+ }
+
+ @Test
+ public void test() {
+ assertTrue(recorder.recorded(EC.TLC_FINISHED));
+ assertFalse(recorder.recorded(EC.GENERAL));
+ assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, "3", "1", "0"));
+ }
+}
diff --git a/tlatools/test/tlc2/tool/liveness/ChooseTableauSymmetryTestA.java b/tlatools/test/tlc2/tool/liveness/ChooseTableauSymmetryTestA.java
index 048abf054cb1087b7e5bce0745d091680ba93572..b3a2fdd1e057f2b167943490d79051e5b28a78e0 100644
--- a/tlatools/test/tlc2/tool/liveness/ChooseTableauSymmetryTestA.java
+++ b/tlatools/test/tlc2/tool/liveness/ChooseTableauSymmetryTestA.java
@@ -61,6 +61,6 @@ public class ChooseTableauSymmetryTestA extends ModelCheckerTestCase {
expectedTrace.add("arr = (a :> \"ready\" @@ b :> \"busy\")");
assertTraceWith(recorder.getRecords(EC.TLC_STATE_PRINT2), expectedTrace);
- assertBackToState(3, "<Action line 7, col 13 to line 8, col 47 of module ChooseTableauSymmetry>");
+ assertBackToState(3, "<Ready line 7, col 13 to line 8, col 47 of module ChooseTableauSymmetry>");
}
}
diff --git a/tlatools/test/tlc2/tool/liveness/ErrorTraceConstructionTest.java b/tlatools/test/tlc2/tool/liveness/ErrorTraceConstructionTest.java
index 5bd535ed4abb8153a033286bcfd92b02975c68a2..abd430a752ddc873036e3f63f948c2a865f5a3fe 100644
--- a/tlatools/test/tlc2/tool/liveness/ErrorTraceConstructionTest.java
+++ b/tlatools/test/tlc2/tool/liveness/ErrorTraceConstructionTest.java
@@ -66,6 +66,6 @@ public class ErrorTraceConstructionTest extends ModelCheckerTestCase {
expectedTrace.add("/\\ x = 0\n/\\ y = 7");
assertTraceWith(recorder.getRecords(EC.TLC_STATE_PRINT2), expectedTrace);
- assertBackToState(4, "<Action line 32, col 7 to line 34, col 19 of module ErrorTraceConstruction>");
+ assertBackToState(4, "<N7 line 32, col 7 to line 34, col 19 of module ErrorTraceConstruction>");
}
}
diff --git a/tlatools/test/tlc2/tool/liveness/OneBitMutexNoSymmetryTest.java b/tlatools/test/tlc2/tool/liveness/OneBitMutexNoSymmetryTest.java
index a441bfd8f925cee1dad70207b17f1366393c63f2..a928797343bec7faa9d561903cb6a8085cd99e3f 100644
--- a/tlatools/test/tlc2/tool/liveness/OneBitMutexNoSymmetryTest.java
+++ b/tlatools/test/tlc2/tool/liveness/OneBitMutexNoSymmetryTest.java
@@ -158,6 +158,6 @@ public class OneBitMutexNoSymmetryTest extends ModelCheckerTestCase {
+ "/\\ pc = (A :> \"e3\" @@ B :> \"e2\")");
assertTraceWith(recorder.getRecords(EC.TLC_STATE_PRINT2), expectedTrace);
- assertBackToState(9, "<Action line 66, col 13 to line 74, col 21 of module OneBitMutex>");
+ assertBackToState(9, "<e2 line 66, col 13 to line 74, col 21 of module OneBitMutex>");
}
}