INSTANCE into a collection

[Silnar]

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.

[Martin]

Hi Silnar,

It seems you want to assign Channels(p)!Init in the map. This is probably not
helpful because it is a predicate (i.e. its "value" is only true, false or
undefined) and you expect this to always hold. It would make more sense to say
"for each Player p, the the Init predicate of its channel must hold", or in TLA:

Init == \A p \in Player: Channels(p)!Init

cheers,
Martin


P.S. I have not looked much if there is a simpler way to go about it but I
noticed you are using the constant New within Channel without having it declared.

[Stephan Merz]

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

--
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+u...@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.

[Silnar]

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

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.

[Stephan Merz]

Hi,

the problem is the conjunct

channels \in [p \in Player |-> Seq(Msg)]

The right-hand side denotes the function that assigns to each player the set of sequences of messages. You want the set of such functions, written as

channels \in [Player -> Seq(Msg)]

The corresponding TLA+ modules are attached to this message. Note that with respect to my previous message, I had to replace the conjunct ChanType' with

channels' \in [Player -> Seq(Msg)]

so that it corresponds to the syntactic form that TLC expects.

In the Toolbox, I used the definition override

Seq(S) <- UNION {[1..n -> S] : n \in 0 .. 2}

Regards,

Stephan

[Silnar]

Wow, thanks for all the clarifications.

I updated examples.

They are published here: [1].

They may help someone exploring the topic of instancing.

I noticed that defining operators in functional style also allows to compose them, for example:

  channels' = [channels EXCEPT ![self] = Channel!Send(Channel!Receive(@), msg)]

which may be very handy.

Thanks for help! :)

[1] https://github.com/Silnar/TlaPlayground/tree/master/TlaInstanceIntoCollection