Равенство в сплаве

Из вашего вопроса неясно, что вы хотите сделать, и из вашего примера кода Alloy похоже, что вы можете страдать от некоторой путаницы.

Во-первых, модель, которую вы показываете, использует название "Пол" двумя разными способами, что само по себе не является незаконным, но, похоже, вызывает некоторую путаницу. (Конечно, это сбивает с толку читателя.)

В объявлении для двух одноэлементных подписей john и Steve пол обозначает два бинарных отношения, одно между подписью john и подписью man, а другое — между Steve и man. Чтобы выразить то же самое в символической форме, Пол обозначает (а) некоторое подмножество john -> man и (b) некоторое подмножество Steve -> man.

Однако в анонимном факте Пол обозначает переменную типа man.

Вашу модель будет легче понять, если вы найдете способ переименовать один или другой из них. Поскольку имена переменных в количественном выражении произвольны, ваш факт будет означать то же самое, если вы переформулируете его как

fact { all P : person, M : man | P.M = P.M => person = person }

Если это не то, что вы хотели сказать, то, возможно, вы хотели сказать что-то вроде

fact { all P : person, M : man | 
    P.Gender = P.Gender => person = person 
}

Переименование переменной заставляет вас выбрать то или иное значение. Это хорошая вещь. (К сожалению, ни одна из формулировок в Alloy на самом деле неудовлетворительна. Но давайте разберемся с одной проблемой за раз; избавление от двойного использования имени «гендер» — это первый шаг.)

Вторая проблема заключается в том, что какую бы формулировку факта вы ни имели в виду, она почти наверняка означает не то, что вы хотели. Игнорируя на мгновение специфику модели, ваш факт принимает форму

fact { all V1 : sig1, V2 : sig2 | 
  Expression = Expression => sig1 = sig1
}

где Expression — это либо V1.V2, либо V1.Relation для некоторого отношения, определенного в модели. Здесь несколько неправильных вещей:

• V1.V2 не имеет смысла, где V1 и V2 являются именами сигнатур или переменных, находящихся в диапазоне заданных сигнатур: оператор точки имеет смысл, только если один из его аргументов является именем отношения.

• Если какое-либо выражение E вообще имеет смысл, то логическое выражение формы E = E (например, person.Gender = person.Gender) истинно независимо от того, что означает E. Все, что обозначается E, естественно, будет равно самому себе. Таким образом, условное выражение также может быть написано

  1 = 1 => person = person
  

• По той же причине человек = человек всегда будет истинным, независимо от модели: для любого экземпляра модели набор лиц в экземпляре будет идентичен набору лиц в экземпляре. Таким образом, условное выражение всегда будет истинным, и этот факт фактически не будет накладывать никаких ограничений на экземпляры модели.

Непонятно, как лучше всего помочь вам двигаться вперед. Возможно, одним из способов начать было бы спросить себя, какое из следующих утверждений вы пытаетесь зафиксировать в своей модели.

• Есть набор лиц.
• Некоторые люди — мужчины (имеют пол = «мужчина»). Другие не мужчины.
• Джон — личность мужского пола.
• Стив — мужчина.
• Джон и Стив — разные личности.
• Если x и y — люди одного пола, то x и y — один и тот же человек. т.е. нет двух людей одного пола.

Обратите внимание, что эти утверждения не могут быть истинными одновременно. (Если это не очевидно, вы можете поступить хуже, чем попытаться выяснить, почему. Alloy может помочь в этом.)

Удачи.