Имам модел Alloy, който съдържа следното:
abstract sig person{}
one sig john,Steve extends person {Gender: man}
sig man{}
fact {
all name: person, Gender: man |
name.Gender = name.Gender => person =person}
Как мога да направя равенство между два подписа?
От въпроса ви не става ясно какво искате да направите и от вашия примерен код на Alloy изглежда, че може да страдате от някои обърквания.
Първо, моделът, който показвате, използва името Gender по два различни начина, което само по себе си не е незаконно, но изглежда предполага известно объркване. (Това със сигурност обърква любителите на този читател.)
В декларацията за двата единични подписа john и Steve, Gender обозначава две двоични релации, едната между подписа john и подписа man, другата между Steve и man. За да кажем същото в символична форма, Gender обозначава (a) някакво подмножество на john -> man и (b) някакво подмножество на Steve -> man.
В анонимния факт обаче Gender обозначава променлива от типа 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. Но нека се занимаваме с един проблем наведнъж; премахването на двойното използване на името Gender е първата стъпка.)
Втори проблем е, че каквато и формулировка на факта да сте имали предвид, тя почти сигурно не означава това, което сте искали да означава. Пренебрегвайки за момент спецификата на модела, вашият факт приема формата
fact { all V1 : sig1, V2 : sig2 |
Expression = Expression => sig1 = sig1
}
където Expression е V1.V2 или V1.Relation, за някаква Relation, дефинирана в модела. Тук има няколко грешни неща:
V1.V2 е безсмислено, когато V1 и V2 са имена на сигнатури или променливи, вариращи върху дадени сигнатури: операторът за точка има смисъл само ако един от неговите аргументи е името на релация.
Ако някой израз E изобщо има смисъл, тогава булев израз във формата E = E (например person.Gender = person.Gender) е верен, независимо какво означава E. Всичко, означено с E, естествено ще бъде равно на себе си. Така че условното може също да бъде написано
1 = 1 => person = person
По същата причина човек = лице винаги ще бъде вярно, независимо от модела: за всеки екземпляр на модел наборът от лица в екземпляра ще бъде идентичен с набора от лица в екземпляра. Така че условието винаги ще бъде вярно и фактът всъщност няма да наложи никакви ограничения върху екземплярите на модела.
Не е ясно как най-добре да ви помогнем да продължите напред. Може би един от начините да започнете е да се запитате кое от следните твърдения се опитвате да обхванете във вашия модел.
Имайте предвид, че тези твърдения не могат да бъдат верни едновременно. (Ако това не е очевидно, може да направите по-лошо, отколкото да се опитате да разберете защо. Alloy може да бъде полезна в това усилие.)
Късмет.
