# How to initialize a hard-coded sequence?

**URL:** https://alloytools.discourse.group/t/how-to-initialize-a-hard-coded-sequence/553
**Category:** Questions
**Created:** [April 22, 2026, 3:22am UTC](https://alloytools.discourse.group/t/how-to-initialize-a-hard-coded-sequence/553 "2026-04-22T03:22:24Z")
**Posts on this page:** 7
**Page:** 1

<div class="post-metadata">

### Author: ![cam](https://avatars.discourse-cdn.com/v4/letter/c/bbe5ce/32.png) [@cam](https://alloytools.discourse.group/u/cam)
#### Post date: [April 22, 2026, 3:22am UTC](https://alloytools.discourse.group/t/how-to-initialize-a-hard-coded-sequence/553/1 "2026-04-22T03:22:24Z")

</div>

I have a set of ~20 singletons. What’s the best way to create a sequence of those singletons in the order I specify?

`````  
`sig A {} // #A = 20 things that need to be in a particular order`  
`sig B {`  
` myOrder: seq A // I want this to be all 20 things and specifically my order`  
`}`  
`````

The only two ways I can think to do it are:

1. specify `myOrder` as empty and then do something like

```auto
pred postInit {

    myOrder' = myOrder.add[firstA].add[secondA].etc

}

```

1. 

```auto
sig B {myOrder: seq A}{

    myOrder.idxOf[firstA] = 0

    myOrder.idxOf[secondA] = 1

    etc

}

```

Both of these seem ugly and possibly (? I don’t know enough to say) inefficient to analyze. So is there a better way?

---

<div class="post-metadata">

### Author: ![alcino](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/alcino/32/25_2.png) [@alcino](https://alloytools.discourse.group/u/alcino)
#### Post date: [April 22, 2026, 5:49pm UTC](https://alloytools.discourse.group/t/how-to-initialize-a-hard-coded-sequence/553/2 "2026-04-22T17:49:12Z")

</div>

Hi,  
If `A` is declared with `enum` we automatically get an ordering on them (using `util/ordering`). I’m not sure if there is a better way to do what you want, but the following should work:

```alloy
enum A {A1, A2, A3}
one sig B {
	myOrder: seq A
} {
	#myOrder = #A
	all a : A | idxOf[myOrder,a] = #a.prevs
}

```

Best,  
Alcino

---

<div class="post-metadata">

### Author: ![cam](https://avatars.discourse-cdn.com/v4/letter/c/bbe5ce/32.png) [@cam](https://alloytools.discourse.group/u/cam)
#### Post date: [April 22, 2026, 6:49pm UTC](https://alloytools.discourse.group/t/how-to-initialize-a-hard-coded-sequence/553/3 "2026-04-22T18:49:49Z")

</div>

Thanks for the reply, but I don’t think that will work in my case since my As are in a hierarchy of sigs

---

<div class="post-metadata">

### Author: ![cam](https://avatars.discourse-cdn.com/v4/letter/c/bbe5ce/32.png) [@cam](https://alloytools.discourse.group/u/cam)
#### Post date: [April 22, 2026, 7:03pm UTC](https://alloytools.discourse.group/t/how-to-initialize-a-hard-coded-sequence/553/4 "2026-04-22T19:03:03Z")

</div>

Related question since I’m still looking for a good solution here:  
Let’s say I set up this order with `ordering.lt` instead of `seq`, and that 19 of the 20 items are static in the order, but 1 of the 20 can move around in the order in a way constrained by the current state, so that for any given state there is only one valid order.

Will this be a combinatorial nightmare, or will the analyzer “know” to construct the valid order without rejecting every invalid order first?

---

<div class="post-metadata">

### Author: ![alcino](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/alcino/32/25_2.png) [@alcino](https://alloytools.discourse.group/u/alcino)
#### Post date: [April 23, 2026, 11:56am UTC](https://alloytools.discourse.group/t/how-to-initialize-a-hard-coded-sequence/553/5 "2026-04-23T11:56:29Z")

</div>

Hi,

I’m not sure exactly what are you trying to do, but if you want to have a mutable total order between all atoms of `A`, where only one specific atom `A1` is allowed to move around in the order, you could model the order explicitly and just add a fact to specify all atoms except `A1` keep their relative order.

```alloy
open util/relation

sig A {
	var succ : set A
}
one sig A1 extends A {}
sig B extends A {}
one sig B1,B2 extends B {}
sig C extends A {}
one sig C1,C2,C3 extends C {}

fact {
	always totalOrder[succ,A]
	all x,y : A - A1 | always {
		x in y.succ iff after x in y.succ
	}
}

run {}

```

If you run the command and then use the new fork button you can see the different ways `A1` can move around in the next state.

Maybe if you share a small complete model illustrating your specific problem we can be more helpful.

Best,  
Alcino

---

<div class="post-metadata">

### Author: ![cam](https://avatars.discourse-cdn.com/v4/letter/c/bbe5ce/32.png) [@cam](https://alloytools.discourse.group/u/cam)
#### Post date: [April 23, 2026, 6:14pm UTC](https://alloytools.discourse.group/t/how-to-initialize-a-hard-coded-sequence/553/6 "2026-04-23T18:14:22Z")

</div>

My second question was more generally about the analyzer since I don’t have a good intuition about how efficiently it can prune the possibility space.  
If I tell it that there is a variable ordering on 20 elements but then tightly constrain that ordering, which of these two heuristics is the more-correct way to think about it?

1. I have shot myself in the foot since there are a huge number of possible orderings on 20 elements, and it will have to search that whole space to find the ones that are valid.

or 2. Alloy will be able to construct the small number of valid orderings according to my constraints, so the large space of all orderings isn’t relevant.

---

<div class="post-metadata">

### Author: ![alcino](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/alcino/32/25_2.png) [@alcino](https://alloytools.discourse.group/u/alcino)
#### Post date: [April 24, 2026, 11:27am UTC](https://alloytools.discourse.group/t/how-to-initialize-a-hard-coded-sequence/553/7 "2026-04-24T11:27:04Z")

</div>

From my experience what influences more the efficiency is the size of the universe, not so much the quantity or complexity of the constraints. 20 atoms does seem a lot, but just give it a try.
