Re: [tlaplus] INSTANCE into a collection

["'Martin' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>]

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.



On 6/17/19 4:26 PM, Silnar 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 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/32184d90-bb77-b5a9-faeb-503b3c5ab3a7%40gmail.com.
For more options, visit https://groups.google.com/d/optout.