Re: [tlaplus] Re: Scaling up model checking

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

On 13.11.19 18:01, william.schultz via tlaplus wrote:
> From your experience, do you have any intuition on the scalability limit
> (CPU core limit) I should expect for TLC if it has plenty of memory?

This is difficult to answer because it depends on the cost to evaluate
the next-state relation.  For a larger spec where the next-state
relation is expensive to evaluate, TLC will benefit from more CPUs
(contention on the StateQueue won't be the bottleneck).  For a toy spec
that models a simple counter there is no point in using more than a
single CPU though.

M.

-- 
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/4d3c0f8c-313e-0afc-3c6a-8107473e5986%40lemmster.de.