| Hello, you are right when you worry about the validity of symmetry reduction in the presence of CHOOSE. But if I understand correctly, in your specific situation we can get rid of them without changing the semantics. In fact, essentially your choices of the two endpoints are non-deterministic (they could be reversed without changing the meaning), and I'd consider that using CHOOSE in such a situation is a bit of a kludge. Here's what I'd try to get around it (I'm assuming that FifoCompliance is the property that you use to check refinement): FIFO(x,y) == INSTANCE FifoSpec WITH Src <- x, Dst <- y FifoCompliance == \A x,y \in Endpoints : x # y => FIFO(x,y)!Spec In this formulation, symmetry of endpoints is quite obviously not broken. But I haven't actually tried, and I am not entirely sure if TLC accepts this. Stephan
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/187D1C98-9092-49F4-9E27-36A8737F3A2B%40gmail.com. |