alloy - 谓词的多重性

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

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

Answer 2

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

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