Re: [tlaplus] INSTANCE into a collection

On 17 Jun 2019, at 23:30, Silnar <m.zdankiewicz@xxxxxxxxx> wrote:

Hi Stephan,

Thanks for the link to Leslie's recent note on (not) reusing TLA+ modules.
I must say that reasoning on simple abstractions in TLA+ is great - it enforces you to focus on the solutions instead of the details.

On the other hand, I still find choosing the simplest possible abstractions pretty challenging and when they don't end up being simple I resort to 'reusing'.
It's a strong habit from programming :)

Out of curiosity I tried to implement your "horribly inefficient" version, but I get:
In computing initial states, the right side of \IN is not enumerable.
in:
channels \in [p \in Player |-> Seq(Msg)]
after overriding Nat as:
Nat = 1..2
Here you can find the full source code: [1]

After overriding Nat with 1..2 the following types should look like this:
Msg == Nat
    => Msg == 1..2
Seq(S) == UNION {[1..n -> S] : n \in Nat}
    => Seq(S) == UNION {[1..n -> S] : n \in 1..2}
and TLC should see channels like below:
channels \in [p \in Player |-> UNION {[1..n -> 1..2] : n \in 1..2}]
How is that still not enumerable ?

I also found another way of reusing, by extracting the whole 'channels' variable to separate module.
It might be useful.
Here is the source: [2]

In case you would like to run it in Toolbox, here are all examples with configured models: [3]

Cheers.

[1]: https://github.com/Silnar/TlaPlayground/blob/master/TlaInstanceIntoCollection/TlaInstanceIntoCollection2.tla
[2]: https://github.com/Silnar/TlaPlayground/blob/master/TlaInstanceIntoCollection/Channels.tla
[3]: https://github.com/Silnar/TlaPlayground

W dniu poniedziałek, 17 czerwca 2019 17:41:10 UTC+2 użytkownik Stephan Merz napisał:
Hello,

the two formulas

channels = [p \in Player |-> << >>]   and   \A p \in Player : channels[p] = << >>

are not equivalent. In particular, the latter doesn't tell you what the domain of `channels' is, or in fact if it is a function at all. You could rewrite your initial condition as follows

ChanType == channels \in [Player -> Seq(Msg)]
Init == ChanType /\ \A p \in Player : Channels(p)!Init

The problem is that TLC will not be able to enumerate the infinite set of type-correct channel values (unbounded queues), and even if you override the `Seq' operator so that it returns the set of sequences up to some length bound, it is very inefficient to first enumerate all possible sequences and then reduce the set to just the empty sequence for each player.

Essentially the same applies to the definition of actions: using your definitions, you could write

Next ==
  /\ ChanType'
  /\ \E p \in Player :
/\ PlayerSend(p) \/ PlayerReceive(p)
/\ \A q \in Player \ {p} : UNCHANGED channels[q]

but again, these definitions are not suitable for TLC (or horribly inefficient if you restrict to bounded sequences).

–––

If you want to use a separate module for the basic operations on a channel (which is probably overkill for such a simple example [1]), I recommend that you define operators in a "functional" style:

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

EXTENDS Naturals, Sequences

New == << >>

Ready(chan) == Len(chan) > 0

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

Receive(chan) == Tail(chan)

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

and then use them as follows

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

EXTENDS Channel

CONSTANT Player, Msg \* these are best instantiated from the Toolbox
VARIABLE channels

Init ==
/\ channels = [p \in Player |-> New]

PlayerSend(self) ==
/\ ~ Ready(channels[self])
/\ \E msg \in Msg : channels' = [channels EXCEPT ![self] = Send(@,msg)]

PlayerReceive(self) ==
/\ Ready(channels[self])
/\ channels' = [channels EXCEPT ![self] = Receive(@)]

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

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

Regards,
Stephan

[1] I recommend reading Leslie's recent note on (not) reusing TLA+ modules: https://groups.google.com/forum/#!topic/tlaplus/BHBNTkJ2QFE

On 17 Jun 2019, at 16:26, Silnar <m.zdan...@gmail.com> wrote:

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 tla...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
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.

--
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/df1ae47e-298e-4113-942d-bd948f9fc07a%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.