Differences

This shows you the differences between two versions of the page.

--- learning:distributed [2024/09/28 15:58] – created - external edit 127.0.0.1
+++ learning:distributed [2024/10/21 22:19] (current) – fponzi
@@ Line 1: / Line 1: @@
 ====== Distributed mode and Cloud mode ======
+Please Note: this feature is on track to be deprecated. More info can be found here: https://github.com/tlaplus/tlaplus/issues/718
 When we need to model check a model that has a large state space, we can run tlc in distributed mode. In this mode, TLC will run in multiple machines. Cloud mode is distributed mode, but automatically spawns up instances in the supported clouds.
-There have been no reported issues, and nothing is fundamentally broken with either Distributed TLC or Cloud TLC. However, we no longer have sponsored access to AWS to run Cloud TLC as part of our CI testing. Additionally, cloud providers often change their APIs, and the jclouds library [1] that Cloud TLC depends on has not been updated in a while. The dropdown menu for selecting the cloud has been moved in the Toolbox’s nightly build (see attached screenshot). {{distributed-toolbox.png|alt text}}
+There have been no reported issues, and nothing is fundamentally broken with either Distributed TLC or Cloud TLC. However, we no longer have sponsored access to AWS to run Cloud TLC as part of our CI testing. Additionally, cloud providers often change their APIs, and the jclouds library [1] that Cloud TLC depends on has not been updated in a while. The dropdown menu for selecting the cloud has been moved in the Toolbox’s nightly build (see attached screenshot).
+{{ :learning:distributed-toolbox.png?600 |}}
 Distributed TLC can be used from the command line [2], but there is no support in the VSCode extension.