Re: [tlaplus] problem in verifying liveness properties

[Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 16.12.2015 13:26, Amira Methni wrote:
> I have a model and I tried to verify a set of liveness properties on it
> (I'm using the TLA toolbox on Ubuntu 12.04 (x86_64bits).
> The problem is that TLC displays the status "Finishing computing initial
> states". And it does not progress (a screenshot is attached), knowing
> that when I verify invariants, TLC works correctly. 
> 
> Is it normal? 

Hi Amira,

no, it's not normal for TLC to show no output. Does the TLC process
produce a significant system load or is it idling?

The screenshot unfortunately doesn't give much insight. Can you share
your spec and model with me? I can then try to diagnose the problem locally.

Thanks
Markus