Hi,
I was unable to get a solution to my problem (first message). If anyone could help me out, I'd really appreciate it
Markus has figure out the source of the problem, which is caused by Lazy eval which has terrible performance when liveness checked because TLC does not cache the result by re-evaluates it over and over again, as I make use of recrusive operators.
I tried to decrease the number of recursive calls, I also tried using TLCEval (as described on
this page, page6), but the problem still there.
Is there any tips that I can apply to verifty liveness on my model??
Could you tell me how TLC checks liveness (I didn't find a reference that describes this)
Thank you,
Amira
Le mercredi 16 décembre 2015 14:21:49 UTC+1, Markus Alexander Kuppe a écrit :
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