CODEWITHSUNDEEP
alloy
user2664856
user2664856

Reputation: 630

Access object numbers in examples

If I have just one sig A and want to chain multiple instances of it (for example by a successor relation), Alloy will number them (A1, A2, A3 ,...) randomly.

Is there a way to tell it, that I want these in ascending order ?

Or that A3 has to come after A1, but A2 before A4 or similar constraints.

Upvotes: 1

Views: 97

Answers (2)

ivcha
ivcha

Reputation: 463

There is no way of connecting names of sig instances to whatever relation you defined in your model (be it with your "chaining relation" or util/ordering library), in the general case. (Essentially, this is up to Alloy's solver which might instantiate fresh names unpredictably.)

One alternative, that could perhaps work in your case, might be to declare multiple sigs, for example:

one sig A1, A2, A3, ... extends A {}

with a "chaining relation":

succ = A1 -> A2 + A2 -> A3 + ...

Now, since the ordering is fixed explicitly on signatures with names, that are ordered, the models found by Alloy will indeed satisfy your desired property.

Upvotes: 1

Alcino Cunha
Alcino Cunha

Reputation: 186

If your goal is to impose a total order on A then I would suggest using the util/ordering library:

open util/ordering[A]

If you use this library then the Analyzer will do its best to keep the A atoms in ascending order (according to the next relation that is declared in the library, meaning that A$1.next will be A$2 and so on). Also, analysis will be more efficient due to improved symmetry breaking. However, you need to be aware that signature A will become fully saturated, in the sense that a scope of 5 A will be the same as exactly 5 A.

Upvotes: 2

Related Questions