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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sat, 27 May 2023 16:25:22 +0200*References*: <4aebde62-6086-4b90-b7d0-04e2b8903326n@googlegroups.com>

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

**Follow-Ups**:**Re: [tlaplus] Question about SYMMETRY optimization***From:*Dmitry Kulagin

**References**:**[tlaplus] Question about SYMMETRY optimization***From:*Dmitry Kulagin

- Prev by Date:
**Re: [tlaplus] Design Validation using TLA+/TLC Model checker** - Next by Date:
**[tlaplus] Defining the set of all bags** - Previous by thread:
**[tlaplus] Question about SYMMETRY optimization** - Next by thread:
**Re: [tlaplus] Question about SYMMETRY optimization** - Index(es):