[tlaplus] Eliminate random element from seq

[p.tollot@xxxxxxxxxxxxxxxxx]

Hi, i want to write a function that given a sequence will return a sequence as the one passed but without one element at random, this is my solution but it is wrong, someone can tell me why? And what would be a correct solution? Thanks

EXTENDS Integers, Sequences

Remove(i, seq) == 

  [j \in 1..(Len(seq)-1) |-> IF j < i THEN seq[j] 

                                      ELSE seq[j+1]]

Random(S) ==  CHOOSE x \in S : TRUE

                                      

Err(seq) ==

    Remove(Random({1..Len(seq)}), seq)

-- 
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/2b6263b2-50cc-4591-b748-ea66d0b23bd8%40googlegroups.com.