a few quick comments on your spec:
- all actions should determine the values of all state variables at the successor state, so you should add "/\ ack' = ack" to the definition of Send,
- seq is used as a sequence, but then you write "x \in seq": TLA+ doesn't allow you to use set-theoretic operators for sequences,
- your protocol will only ever send and receive the constant value N, wouldn't it be more interesting to send different values?
Also, as written, your channels only grow, so the state space of your protocol is infinite. Given that sender and receiver strictly alternate their actions, why use a channel at all?
Have you looked at some introductory material about TLA+ and PlusCal [1,2]?
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/BC112024-2D43-42DD-B321-17BF324AD3C0%40gmail.com.