tlc uses only one cpu when enable liveness checking

[Yongqiang Yang]

When I enabled liveness checking by adding formula to properties, TLC uses only one cpu.  Is this expected?

[Yongqiang Yang]

Where the liveness formula is as follows, it checks that a log is acked by quorum servers eventually would be committed.

<> (\A entry \in {[term |-> Nat, index |-> Nat, value |-> Nat]} : entry \in AllServerQuorumLogs ~> entry \in RANGE(committedLogs)) 

在 2020年3月10日星期二 UTC+8上午9:53:26，Yongqiang Yang写道：

[Yongqiang Yang]

<> (\A entry \in [term: 1..MaxTerm, index: 1..MaxIndex, value: 1..MaxValue] : entry \in AllServerQuorumLogs ~> entry \in RANGE(committedLogs))                                     

MaxTerm, MaxIndex and MaxValue are constants .

在 2020年3月10日星期二 UTC+8上午10:00:51，Yongqiang Yang写道：

[Markus 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.

[Yongqiang Yang]

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写道：