Merge tag 'v1.5.5'

1.5.5 release

CONTRIBUTING.md

-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.

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.

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.&nbsp;</A>
-
-
-There is a lock icon and a key icon that you click to lock or
-unlock the model.&nbsp;  
-
-Those icons are in the upper-left part of each model-editor page.&nbsp;
-
-
-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>.&nbsp;
-
-This means that you can't view information in sections of a running
-model that are closed.&nbsp;
+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.&nbsp;
 
 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

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>

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.&nbsp;
-
-The model is always locked while it is being run by TLC, and it remains
-locked after TLC completes unless the run was short.&nbsp;
-</p>
-
 <hr> 
 <!-- delete rest of line to comment out --> 
 <dl>

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>
 

org.lamport.tla.toolbox.doc/html/trouble/trouble.html

@@ -148,8 +148,8 @@ The &nbsp; <samp>.log</samp>&nbsp; file is in the
 directory.&nbsp; 
 
 On Windows, you can find out where your home directory is located, by 
-looking at the <samp>%HOMEPATH%</samp> environment variable.&nbsp; On 
-Linux and Mac, check the $HOME variable.&nbsp;
+by entering the command <code>echo %SYSTEMDRIVE%%HOMEPATH%</code> in 
+Command Prompt.&nbsp; On Linux and Mac, check the $HOME variable.&nbsp;
 
 (The log contains enough timestamped entries for you to figure out
 what part of it relates to the problem you are reporting.)&nbsp;

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">&uarr; Updating the Toolbox</a>
 </hr>

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 &quot;The Operators of  TLA+&quot;">
-            <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"

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>

org.lamport.tla.toolbox.feature.uitest/.project

+<?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>

org.lamport.tla.toolbox.feature.uitest/build.properties

+bin.includes = feature.xml

org.lamport.tla.toolbox.feature.uitest/feature.xml

+<?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>

org.lamport.tla.toolbox.feature.uitest/pom.xml

+<?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>

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();

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 

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));

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

org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/EC2PropertyCloudTLCInstanceParameters.java

+/*******************************************************************************
+ * 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());
+	}
+}