Support running a cloud specific shutdown command on instances when

running CloudDistributedTLCJob in asynchronous mode (fire and forget).
Needed on Azure to deallocate instances to stop being
charged.

[Feature][Toolbox]

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

@@ -196,4 +196,47 @@ public class AzureCloudTLCInstanceParameters extends CloudTLCInstanceParameters
 		// (similar to EC2CloudTLCInstanceParameters#getHostnameSetup.
 		return "hostname \"$(hostname).cloudapp.net\" && echo \"$(curl -s ifconfig.co) $(hostname)\" >> /etc/hosts";
 	}
+
+	/* (non-Javadoc)
+	 * @see org.lamport.tla.toolbox.jcloud.CloudTLCInstanceParameters#getCleanup()
+	 */
+	@Override
+	public String getCloudAPIShutdown() {
+		final String servicePrincipal = System.getenv("AZURE_COMPUTE_SERVICE_PRINCIPAL");
+		final String password = System.getenv("AZURE_COMPUTE_SERVICE_PRINCIPAL_PASSWORD");
+		final String tenant = System.getenv("AZURE_COMPUTE_SERVICE_PRINCIPAL_TENANT");
+		if (servicePrincipal == null || password == null || tenant == null) {
+			// Missing credentials.
+			return super.getCloudAPIShutdown();
+		}
+		// What we try to accomplish is to purge the complete Azure Resource Group (a RG
+		// combines all Azure resources associated with the VM (storage, networking,
+		// ips, ...).
+		// The way we do it, is to use the azure CLI to deploy the template in
+		// /tmp/rg.json created by the printf statement under the same resource group
+		// identify we wish to purge. The trick is, that the template defines no
+		// resources whatsoever. This effectively purges the old resources in the
+		// resource group. Idea taken from
+		// http://www.codeisahighway.com/effective-ways-to-delete-resources-in-a-resource-group-on-azure/
+		// bash/screen/ssh apparently fiddle with quotes and which is why the json is base64 encoded 
+		// and decoded on the instance:
+		// { "$schema": "https://schema.management.azure.com/schemas/2015-01-01/deploymentTemplate.json#", "contentVersion": "1.0.0.0", "parameters": {}, "variables": {}, "resources": [], "outputs": {} } | base64
+		//
+		// Unfortunately, the azure CLI needs credentials to talk to the Azure API. For
+		// that, one manually creates a service principal once as described in
+		// https://docs.microsoft.com/en-us/cli/azure/create-an-azure-service-principal-azure-cli?view=azure-cli-latest
+		// and uses it to log into Azure as described in
+		// https://docs.microsoft.com/en-us/cli/azure/authenticate-azure-cli?view=azure-cli-latest.
+		// Using AZURE_COMPUTE_CREDENTIALS and AZURE_COMPUTE_IDENTITY to login with azure CLI
+		// would trigger a two-factor auth for Microsoft FTEs. Not something we want.
+		//
+		// An alternative might be to use an auth.properties file, but this doesn't seem
+		// supported by azure CLI yet. Read "File based authentication" at
+		// https://docs.microsoft.com/en-us/java/azure/java-sdk-azure-authenticate#mgmt-file
+		return "echo eyAiJHNjaGVtYSI6ICJodHRwczovL3NjaGVtYS5tYW5hZ2VtZW50LmF6dXJlLmNvbS9zY2hlbWFzLzIwMTUtMDEtMDEvZGVwbG95bWVudFRlbXBsYXRlLmpzb24jIiwgImNvbnRlbnRWZXJzaW9uIjogIjEuMC4wLjAiLCAicGFyYW1ldGVycyI6IHt9LCAidmFyaWFibGVzIjoge30sICJyZXNvdXJjZXMiOiBbXSwgIm91dHB1dHMiOiB7fSB9Cg== | base64 -d > /tmp/rg.json"
+				+ " && " + "az login --service-principal -u \"" + servicePrincipal + "\" -p " + password + " --tenant "
+				// $(hostname -s) only works iff hostname is correctly setup with getHostnameSetup() above.
+				+ tenant + " && " + "az group deployment create --resource-group $(hostname -s)"
+				+ " --template-file /tmp/rg.json --mode Complete";
+	}
 }

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

@@ -348,6 +348,12 @@ public class CloudDistributedTLCJob extends Job {
 						+ "-jar /tmp/tla2tools.jar " 
 						+ params.getTLCParameters() + " "
 						+ "&& "
+					// Run any cloud specific cleanup tasks.
+					// When CloudDistributedTLCJob runs in synchronous CLI mode (isCLI), it will destroy
+					// the VMs (nodes) via the jclouds API. No need to deallocate nodes
+					// via special logic.
+					+ (isCLI ? "/bin/true" : params.getCloudAPIShutdown())
+					+ " && "
 					// Let the machine power down immediately after
 					// finishing model checking to cut costs. However,
 					// do not shut down (hence "&&") when TLC finished
@@ -461,6 +467,9 @@ public class CloudDistributedTLCJob extends Job {
 								// to a NoRouteToHostException when the master
 								// shut down caused by a violation among the
 								// init states.
+					            // Run any cloud specific cleanup tasks.
+					            + params.getCloudAPIShutdown()
+					            + " && "
 								+ "sudo shutdown -h now"
 								+ "\""), 
 						new TemplateOptions().runAsRoot(false).wrapInInitScript(

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

@@ -140,6 +140,10 @@ public abstract class CloudTLCInstanceParameters {
 		return "/bin/true"; // no-op, because concat with && ... && in CDTJ.
 	}
 
+	public String getCloudAPIShutdown() {
+		return "/bin/true"; // no-op, because concat with && ... && in CDTJ.
+	}
+
 	public String getExtraRepositories() {
 		return "/bin/true"; // no-op, because concat with && ... && in CDTJ.
 	}