Модуль util/ordering содержит комментарий в верхней части файла о том факте, что граница параметра модуля должна иметь точно границу, разрешенную областью действия для указанной подписи.
Я несколько раз читал (например, здесь), что это оптимизация, которая позволяет генерировать хороший предикат, нарушающий симметрию, который я могу понять. (Кстати, в отношении указанного сообщения, я прав на сделать вывод, что ключевое слово exactly в спецификации параметра модуля здесь для явного применения этой точной границы (в то время как это было неявно в версиях Alloy до 4.x)?)
Однако комментарий также содержит часть, которая, похоже, не относится к оптимизации, а на самом деле относится к проблеме, имеющей семантический оттенок:
* 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.
Итак, я не понимаю этого, в частности, последнее предложение о Ord.last и Ord.next... Допустим, я моделирую полностью упорядоченную подпись S классическим способом (т.е. задавая тотальную, рефлексивную, антисимметричную, транзитивное отношение в S -> S, все это возможно с использованием простой логики первого порядка) и что я позабочусь о том, чтобы указать точную границу для S: будет ли это эквивалентно указанию open util/ordering[S] (игнорирование эффективности и запутанных проблем с именами атомов)?
