谓词的多重性

Question

所以我有以下内容：

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 个或更多 人都是朋友。有人能解释一下如何用合金做到这一点吗？

Answer 1

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

没试过！它确实迫使集团中的三个人与自己成为朋友。您需要将范围设置为至少包含 3 个人。

Answer 2

sig Person {friends: set Person}
run {some s: set Person | #s >= 3 and s->s in friends}