[tlaplus] INSTANCE into a collection

[Silnar <m.zdankiewicz@xxxxxxxxx>]

Hi,

Assuming that I have a Channel defined like below:

-------------------------- MODULE Channel -----------------------------

EXTENDS Naturals, Sequences

CONSTANT Msg
VARIABLE chan

TypeInvariant == chan \in Seq(Msg)

Init == chan = New

Ready == Len(chan) > 0

Send(msg) == chan' = Append(chan, msg)

Receive == chan' = Tail(chan)

=======================================================================


Is it possible to INSTANCE it into a collection of channels,
perhaps like this:

Channels(p) == INSTANCE Channel WITH chan <- channels[p]

??


I am experimenting with the code below...
I see no way to initialize channels variable using Channels(p)!Init and Channels(p)!Send(...) probably won't work because it only sets channels[p]' not the whole channels' variable.

I feel that it is impossible, but I don't exactly understand why.
Can you explain me what in TLA disallows that ?


My experiments:

-------------------------------- MODULE TlaSandbox --------------------------------

EXTENDS Naturals, Sequences

VARIABLE channels

Player == {"p1", "p2"}
Msg == {"a", "b"}

Channels(p) == INSTANCE Channel WITH chan <- channels[p]  

Init ==
    /\  channels = [p \in Player |-> <<>>]  \* TODO: Can't use Channels(p)!Init


PlayerSend(self) ==
    /\  ~Channels(self)!Ready
    /\  Channels(self)!Send("a")

PlayerReceive(self) ==
    /\  Channels(self)!Ready
    /\  Channels(self)!Receive

Next ==
    \E p \in Player:
        \/  PlayerSend(p)
        \/  PlayerReceive(p)

=============================================================================

Thanks.

-- 
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b6ea130d-b96d-45d2-bf22-a83e8eeb2108%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.