Множественность с предикатами

Итак, у меня есть следующее:

some sig Person {
    friends : set Person
}

fact TransitiveForThree {
    one p1, p2, p3 : Person {
        p1 in p2.friends && p2 in p3.friends => p1 in p3.friends
    }
}

Идея в том, что я хочу, чтобы существовал набор из 3 человек, где все они дружат друг с другом. Однако я бы хотел, чтобы существовал набор, в котором по крайней мере 3 или более людей, которые все являются друзьями. Может кто-нибудь объяснить, как это сделать с Alloy?


person SirGoose    schedule 17.03.2017    source источник


Ответы (1)


fact three_friends {some disj p, q, r : Person | p+q+r -> p+q+r in friends}

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

person user1513683    schedule 18.03.2017