[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Sequences in TLA plus


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.


On 4 Oct 2018, at 22:07, yashmeh...@xxxxxxxxx wrote:

I want to to have sequence returned by randomly removing an element from it. As of now I am removing the head. How can I randomly remove any one element from it? 
A' = [A EXCEPT ![p][q] = Tail(@)]

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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.