How to initialize a hard-coded sequence?

Questions
1

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
pred postInit {

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

}

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?

2

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:

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

Best,
Alcino

3

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

4

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?

5

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.

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

6

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.

7

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.