Re: [tlaplus] Scaling up model checking

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

On 27.08.19 10:20, dunlapg@xxxxxxxxx wrote:
> 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.


The cloud feature - dubbed "Cloud TLC" - can be used from the
command-line too.  [1] shows how the TLC performance tests make use of
it.  The initial setup of cloud credentials is discussed in the Toolbox
help.

Best

Markus

[1] https://gist.github.com/lemmy/62c4b6b158187180a5b7c873d08a0f51

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0a0d3681-510c-096c-d33a-3fc2708da415%40lemmster.de.