Как можно ограничить сплаймом множество внутри своего подмножества?

Question

Следующий код Сплав говорит, что каждый номер имеет набор ключей:

sig Key {} 

sig Room { 
    keys: set Key 
} 

keys отношение должно быть ограничено. Как бы то ни было, он допускает такие случаи, как: ключ K1 используется в кучке комнат. Ой! Мы этого не хотим. Мы хотим, чтобы каждый ключ использовался только с одной комнатой. Вот график, иллюстрирующий вселенную действительных случаев (и подмножество экземпляров, что мы на самом деле хотим, чтобы):

Множество случаев, что мы на самом деле хотим красиво выражается этот сплав код:

Room lone -> Key 

Экземпляры для этого кода сплава изображены на приведенном выше рисунке небольшим кружком.

Итак, как мы ограничиваем keys? Один из ответов таков: создать факт сплава, который говорит следующее:

keys in Room lone -> Key 

Подумайте, что это графически говорит. Он говорит, что большой круг должен находиться внутри маленького круга (см. Ниже). Разве это не странно? Как круг может быть внутри своего круга? Может ли кто-нибудь дать мне интуицию об этом, пожалуйста? Кажется странным.

Answer 1

• , если у вас есть только sig Room {keys: set Key} без каких-либо дополнительных фактов/ограничений, домен для keys связи является большим кругом;

• Вы можете решить добавить некоторые ограничения (например, keys in Room lone -> Key) именно с целью сокращения домена для отношения keys (так, чтобы он стал маленьким кругом).

Таким образом, правильный способ подумать не о том, что большой круг должен находиться внутри маленького круга (?!); скорее, подумайте об этом, используя маленький круг вместо большого круга в качестве домена (набор всех допустимых значений) для keys.