how to make sure action in tla is expressed as it would be?

[Yongqiang Yang]

For example, we have an action A which is enabled on both s7->s8 and s10->s11 as I expects.  Imagine that I made a mistake in writing action A, so that s10 can not transfer to s11.  Because s7->s8 is expressed right, so coverage of action A is not zero. I can not find a violate to find error in action A, because s10 is expected and the transfering from s10 to s11 does not work.

How to find errors like above? Any ideas?

I published the problem in my last post about cpu usage of liveness checking in tlc. I think the problem is a different one, and others can find the problem easily by discussion in a posts with itself description. 

Thanks.

[Yongqiang Yang]

BTW： liveness checking in TLC is too slowly due to using only one cpu.

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