Is using util/ordering exactly the same as axiomat

Question

The util/ordering module contains a comment at the top of the file about the fact that the bound of the module parameter is constrained to have exactly the bound permitted by the scope for the said signature.

I have read a few times (here for instance) that it is an optimization that allows to generate a nice symmetry-breaking predicate, which I can grasp. (BTW, with respect to the said post, am I right to infer that the exactly keyword in the module parameter specification is here to enforce explictly this exact bound (while it was implicit in pre-4.x Alloy versions)?)

However, the comment also contains a part that does not seem to refer to optimization but really to an issue that has a semantic flavour:

 * Technical comment:
 * An important constraint: elem must contain all atoms permitted by the scope.
 * This is to let the analyzer optimize the analysis by setting all fields of each
 * instantiation of Ord to predefined values: e.g. by setting 'last' to the highest
 * atom of elem and by setting 'next' to {<T0,T1>,<T1,T2>,...<Tn-1,Tn>}, where n is
 * the scope of elem. Without this constraint, it might not be true that Ord.last is
 * a subset of elem, and that the domain and range of Ord.next lie inside elem.  

So, I do not understand this, in particular the last sentence about Ord.last and Ord.next... Suppose I model a totally-ordered signature S in the classical way (i.e. specifying a total, reflexive, antisymmetric, transitive relation in S -> S, all this being possible using plain first-order logic) and that I take care to specify an exact bound for S: will it be equivalent to stating open util/ordering[S] (ignoring efficiency and confusing atom-naming issues)?

Answer 1

Sorry for the slow response to this. This isn't very clear, is it? All it means is that because of the symmetry breaking, the values of last, prev and next are hardwired. If that were done, and independently elem were to be bound to a set that is smaller than the set of all possible atoms for elem, then you'd have strange violations of the declarations such as Ord.last not being in the set elem. So there's nothing to understand beyond: (1) that the exactly keyword forces elem to contain all the atoms in the given scope, and (2) the ordering relation is hardwired so that the atoms appear in the "natural" order.