| Hello, TLA+ does not have primitives for random or probabilistic choice, but I believe that you refer to non-deterministically removing some element. Let me simplify matters by assuming that s is a variable that holds a sequence and that you want to describe an action that removes some element from s. You can do so by writing \E i \in 1 .. Len(s) : s' = SubSeq(s, 1, i-1) \o SubSeq(s, i+1, Len(s)) The generalization to your case of a matrix of sequences should now be obvious. Stephan
|