Re: [tlaplus] tlc uses only one cpu when enable liveness checking

[Yongqiang Yang <xiaoqiangnk@xxxxxxxxx>]

Thanks. I want to sure whether I express idea or algorithms in tla as in my brain. e.g. the state machine stops at some point and can not go ahead without stuttering, invariants is not violated, I found liveness checking can find errors like this.  However liveness checking is too slow, is there other solution?

Thanks. 

在 2020年3月10日星期二 UTC+8上午10:05:27，Markus Alexander Kuppe写道：

On 09.03.20 18:53, Yongqiang Yang wrote:
> When I enabled liveness checking by adding formula to properties, TLC
> uses only one cpu.  Is this expected?

Yes:
https://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm

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/aa93b3da-034b-41ad-8cb9-e4e4905b2b7c%40googlegroups.com.