[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. 

Thanks.

--
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.