On Tuesday, August 27, 2019 at 5:41:00 PM UTC+1, Hillel Wayne wrote:
Hi George,
Have you looked into the toolbox's distributed model checking?
You can use it to distribute the model checking to multiple AWS or
Azure compute instances.
When first learning TLA I used the toolbox, and I did notice the "deploy to AWS / Azure" option. But for lots of reasons I prefer using the CLI versions. Anything you do through the toolbox you should be able to do through the CLI, right?
If absolutely necessary, I would consider going that route; but apart from the disadvantage of not being able to use the CLI tools, there's the issue of having to get budget approved for using AWS or Azure. These two test boxes we have are mostly just sitting around at the moment, so it makes sense to see if we can light them up before looking at cloud-based solutions.
Thanks,
-George