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

*From*: Dmitry Kulagin <dmitry.kulagin@xxxxxxxxx>*Date*: Mon, 29 May 2023 09:38:37 +0400*References*: <4aebde62-6086-4b90-b7d0-04e2b8903326n@googlegroups.com> <187D1C98-9092-49F4-9E27-36A8737F3A2B@gmail.com>

Thanks, Stephan!

Unfortunately, TLC doesn't support such a construct, this is known limitation: TLC cannot handle definitions that come from a parameterized instantiation.

Also, I don't believe that "\A x,y \in Endpoints : x # y => FIFO(x,y)!Spec" would qualify as a "nice" temporal formula.

Therefore, I had to resort to explicit (non-parameterized) instantiations, which seem to break symmetry even if the problem at hand is fully symmetric.

Thank you,

Dmitry

On Sat, May 27, 2023 at 6:25 PM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:

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 <- yFifoCompliance == \A x,y \in Endpoints : x # y => FIFO(x,y)!SpecIn 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.StephanOn 26 May 2023, at 09:14, Dmitry Kulagin <dmitry.kulagin@xxxxxxxxx> wrote:Good day,

I want to apply SYMMETRY optimization, but I am not sure it is safe thing to do.

I have a model for FIFO (FifoSpec). And I have a more complicated model of a channel (ChannelSpec). Channel comprises two FIFOs in reverse directions.

I have a set of endpoints (Endpoints), which contains only two endpoints, because it is p2p communication.

ChannelSpec refines FifoSpec to ensure that it implements both FIFOs correctly.

EndpointX == CHOOSE endpoint \in Endpoints : TRUE

EndpointY == CHOOSE endpoint \in Endpoints : endpoint /= EndpointX

Fifo_XY == INSTANCE FifoSpec WITH

Src <- EndpointX

Dst <- EndpointY

Fifo_YX == INSTANCE FifoSpec WITH

Src <- EndpointY

Dst <- EndpointX

FifoCompliance == Fifo_XY!Spec /\ Fifo_YX!Spec

ChannelSpec is fully symmetric wrt Endpoints, but I am not sure that refinement relations can be considered symmetric, because there is CHOOSE operator involved. On the other hand, FifoCompliance does look symmetric to me.

Is it safe to use SYMMETRY optimization for Endpoints to modelcheck FifoCompliance?Thank you,Dmitry--

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/4aebde62-6086-4b90-b7d0-04e2b8903326n%40googlegroups.com.

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.

To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/VIPs6zkKV44/unsubscribe.

To unsubscribe from this group and all its topics, 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.

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/CAN0wswkOmbhiPw4Jdu1PiYbobvSymq%3DG_8LRn0nEnXCPAEEHew%40mail.gmail.com.

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

**Re: [tlaplus] Question about SYMMETRY optimization***From:*Stephan Merz

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