Re: [tlaplus] TCP Protocl model satisfies

Hello,

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]?

Regards,

Stephan

[1] https://lamport.azurewebsites.net/tla/learning.html

[2] https://learntla.com

On 23 Dec 2022, at 08:51, Sharon Kas <camel2469@xxxxxxxxx> wrote:

Hey, I start to learn the TLA+ and the PlusCal, so I search on the Internet some cool question about it and i found something like that:
Build a model of TCP Protocol
The model satisfies requirements R1, R2:
R1: Any sent packet finally has to be received.

R2: There is infinitely many packets sent through the system

So i start to try to write down the algorithem but i can undersatnd how to apporch it, i know that this two are easy but, still something missing:
this is what i already write:

---- MODULE TCP ----

EXTENDS Naturals, Sequences
CONSTANTS N
VARIABLES seq, ack, state

Init == /\ seq = <<>>
/\ ack = <<>>
/\ state = 0

Send(x) == /\ state = 0
/\ seq' = Append(seq, x)
/\ state' = 1

Recv(x) == /\ state = 1
/\ x \in seq
/\ ack' = Append(ack, x)
/\ state' = 0
Spec == Init /\ [][Send(N) \/ Recv(N)]_<<seq, ack, state>>

So now i want to try to satisify the system with the two properties, can some one help me please with that. 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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/704dee58-6f70-4398-adc3-86c58949fdf6n%40googlegroups.com.

--
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.