| Hello,
you'll find this easier to do with a sequence. Suppose your sequence is held in variable q, then you can write an action like
/\ q # << >> /\ q' = Append(Tail(q), Head(q))
Moreover, an array (i.e., a function) with domain 1 .. N for some N \in Nat is just a sequence, so the same will work. If your array has a different domain, you'll have to write an explicit function definition, for which you may take inspiration from the definitions of Append, Tail, and Head in the standard Sequences module.
Stephan
I'm very new to TLA+ and I've been trying to figure out if I can use arrays like a queue. Basically I want to move the first element of the array to the back then move everything forward one step. Like a queue were the first person in line went to the back. Is this possible? -- 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.
|