Re: [tlaplus] Question about evaluation of Sequences

[Stephan Merz <stephan.merz@xxxxxxxxx>]

Hello,

Head(seq) denotes the first element of a sequence, you want the last element. Try

Last(seq) == seq[Len(seq)]

(assuming that the sequence is non-empty).

Stephan

On 25 Mar 2020, at 14:16, Tim Soethout <tim@xxxxxxxxxxxxxx> wrote:

Hi,

I'm using TLA+ for some modeling and TLC finds a counter example, but I don't understand why?

This statement:

`Len(committed[r1]) = (Len(committed[r2])+1) => Append(committed[r2], Head(committed[r1])) = committed[r1]`

is FALSE, but I don't see how?

The value of committed is `(r1 :> <<t1, t2>> @@ r2 :> <<t1>>)`.

What I'm trying to do is: If committed[r1] is 1 shorter than committed[r2], check if the last element from committed[r1] appended to committed[r2] makes them equal.

In this example case this should hold, right? What am I missing?

Thanks for potentially helping me.

Best regards,

Tim

--
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/CABZ6pRfSwipHCO1kQ0T2JpiA8U3mA7mgza0Y9KR1_%3D2tA-y8JQ%40mail.gmail.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/D946CB70-82D9-4CD8-AC2D-55A21A217C7F%40gmail.com.