Re: [tlaplus] INSTANCE into a collection

[Silnar <m.zdankiewicz@xxxxxxxxx>]

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

W dniu wtorek, 18 czerwca 2019 10:07:52 UTC+2 użytkownik Stephan Merz napisał:

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

-- 
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/150b641c-4eb4-450a-aac8-b27a3c389d63%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.