Question about evaluation of Sequences

[Tim Soethout]

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

[Stephan Merz]

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

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABZ6pRfSwipHCO1kQ0T2JpiA8U3mA7mgza0Y9KR1_%3D2tA-y8JQ%40mail.gmail.com.

[timso...@gmail.com]

Thanks!

I see. So `Append(seq, elem)` adds `elem` to the end of `seq`, but `Head(seq)` denotes the first. 

I was somehow expecting that `Append` and `Head` where each other's duals, but this is not the case.

Thanks again for the quick response.

On Wednesday, March 25, 2020 at 2:19:38 PM UTC+1, Stephan Merz wrote:

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 <t...@timsoethout.nl> 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 tla...@googlegroups.com.