Re: [tlaplus] Question about SYMMETRY optimization

[Dmitry Kulagin <dmitry.kulagin@xxxxxxxxx>]

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

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