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

Re: [tlaplus] Question about SYMMETRY optimization



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