Cloud based distributed TLC

1 Motivation

2 Warning

Using cloud based TLC launches compute instances at your cloud provider which may incur costs. While the cloud based distributed TLC tries to minimize costs by terminating instances as soon as possible, do not rely on it. Always check if cloud instances have been correctly terminated.

3 Limitation

4 Usage

Additionally to the instructions below, you can watch a eight minutes introductory video online.
  1. Set AWS access key and secret as environment variables prior to launching the Toolbox. See the example with dummy keys below. 
    • export AWS_ACCESS_KEY_ID=AKIA7D89HCLJKHZASD7F
export AWS_SECRET_ACCESS_KEY=6FDASAIG7DAS976TYDKHCGQAS5D\FA77
    • Alternatively for Azure (assuming you already have an Azure subscription), please follow Use the portal to create an Azure AD application and service principal that can access resources.
      As Sign-on URL you can choose the TLA+ GitHub URL: https://github.com/tlaplus/tlaplus
    • Finally configure the Azure specific environment variables as shown below for Command Prompt and PowerShell. 
      ## Called "Application ID" in the Azure manual
export AZURE_COMPUTE_SERVICE_PRINCIPAL=TheAzureApplicationID
## Called "Value" in the Azure manual
export AZURE_COMPUTE_SERVICE_PRINCIPAL_PASSWORD=TheAzureApplicationKeyValue
## Called "Directory ID" in the Azure manual
export AZURE_COMPUTE_TENANT=TheAzureDirectoryId

## The "Subscription ID" shown in the overview section of "Cost Management + Billing" in Azure Portal
export AZURE_COMPUTE_SUBSCRIPTION=YourAzureSubscriptionId
    • On Windows in the Command Prompt, set the environment variable with: 
      set AZURE_COMPUTE_SERVICE_PRINCIPAL=TheAzureApplicationID
set AZURE_COMPUTE_SERVICE_PRINCIPAL_PASSWORD=TheAzureApplicationKey
set AZURE_COMPUTE_TENANT=TheAzureDirectoryId
set AZURE_COMPUTE_SUBSCRIPTION=YourAzureSubscriptionId
      If you prefer PowerShell, do (notice the quotes): 
      $env:AZURE_COMPUTE_SERVICE_PRINCIPAL="ThePasswordUsedForTheCertificate"
$env:AZURE_COMPUTE_SERVICE_PRINCIPAL_PASSWORD="TheAzureApplicationKey"
$env:AZURE_COMPUTE_TENANT="TheAzureDirectoryId"
$env:AZURE_COMPUTE_SUBSCRIPTION="YourAzureSubscriptionId"
      To set the variables permanently, use the setx command.

      DO NOT use Cygwin shell to set the environment variables and launch the Toolbox. It will lead to obscure exceptions at runtime.

    • Besides AWS and Azure, packet.net's t1.small.x86 baremetal instances provide a budget environment to run Cloud TLC. 
      ## Called "API Key" in app.packet.net
export PACKET_NET_APIKEY=YourPacketNetAPIKey
## Called "Organization ID" in app.packet.net
export PACKET_NET_PROJECT_ID=YourOrganizationId
  2. Create a specification and a model
  3. Open your model in the model editor
    figure ModelEditorA.png
    Figure 1 Model Editor
  4. Expand the “How to run” section of the “Model Overview” page
    figure ModelEditorB.png
    Figure 2 How to run section
  5. Select “aws-ec2” from the “Run in distributed mode” drop down
    figure ModelEditorC.png
    Figure 3 Select your cloud provider
  6. Enter an email address into “Result mailto address” at which you want to receive the model checking result
    figure ModelEditorD.png
    Figure 4 Enter your email address
  7. Click “Run TLC” to start model checking in the cloud and wait for the start-up to finish (it takes approximately five minutes to set-up the cloud instance)
    1. The Toolbox switches to the “Model checking results” page and opens a progress dialog indicating the state of cloud instance provisioning
      figure ProgressBar.png
      Figure 5 Progress Dialog
    2. After provisioning the cloud instance, the Toolbox prompts the user to open a website in a browser.
      figure ProgressBarFinal.png
      Figure 6 Progress Dialog Final
      This website is hosted on the cloud instance and shows the TLC process output as well as runtime statistics similar to Toolbox stats
      figure MCoutInBrowser.png
      Figure 7 TLC runtime statistics in your browser
  8. Walk out and enjoy the weekend while TLC is busy checking
  9. On Monday expect to find an email in your inbox
    figure EMailResult.png
    Figure 8 Email Result
  10. Save MC.out file somewhere to disc
  11. Switch back to the Toolbox and open the model editor
  12. Open the “Model Checking Results” page
    figure LoadResultIntoToolbox.png
    Figure 9 Load result into Toolbox
  13. Import the MC.out from disc
    figure LoadIntoResultPageB.png
    Figure 10 Load into results page
  14. Voilá
    figure FinalResultLoaded.png
    Figure 11 Final result loaded

5 Common problems

↑ Model Overview Page