[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Re: Scaling up model checking

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.


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.