[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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. 


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/334f1325-d661-4911-91a6-f92f877c161a%40googlegroups.com.