[tlaplus] Question about SYMMETRY optimization

[Dmitry Kulagin <dmitry.kulagin@xxxxxxxxx>]

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.