Eliminate random element from seq

[p.to...@studenti.unipi.it]

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)

[Stephan Merz]

Hello,

a trivial error in your definition, and probably the one that TLC tells you about, is that you pass the set containing the only element 1..Len(seq) – which itself is a set of integers – to the Random operator, which will therefore return that set, and the evaluation of the expression `j<i' in the definition of Remove fails because < expects two integers. You clearly meant to write

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

without the set brackets around the argument to Random.

However, the more fundamental issue is that you cannot define a function whose outcome is random: a function is deterministic and always returns the same result for the same input. In particular, the CHOOSE operator yields an arbitrary but fixed element: no matter how often you repeat the experiment, TLC will always compute the same sequence. If this were not so, TLA+ would violate the elementary reflexivity law

  \A x : x = x

of first-order logic.

Also, I'm assuming that you do not really mean "random" in the sense of probability theory, but that you intend to write a specification that allows any execution in which an arbitrary element of your original sequence is removed. We just saw that this cannot be done using just functions and TLA+ operators, but you can instead use a relational expression and for example write something like

Next == 

  \/ ...

  \/ \E i \in 1 .. Len(seq) : seq' = Remove(i, seq)

where your specification has a variable seq that represents the current system state.

Hope this helps,

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