| 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2D0BBC4E-F342-4AE0-AC2D-BDD13471DD87%40gmail.com. |