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.