Does Alloy have the ability to model a sequence? I could do it manually (i.e create a succeeds relation, and list all the one X where it applies), but imagine there is a more elegant approach.
0
votes
1 Answers
1
votes
Does Alloy have the ability to model a sequence?
Yes.
I could do it manually (i.e create a succeeds relation, and list all the one X where it applies),
Yes, and in some cases that is the way you want to go.
but imagine there is a more elegant approach.
As Colonel Thirty Two has already pointed out, util/ordering can be helpful, as can util/seqrel and util/sequence.
But in Alloy 4, the simplest route to sequences is the seq keyword documented on the Alloy website. I believe it was introduced after the second edition of Software abstractions went to press; at least, there's no index entry there for seq.
