0

所以我有以下内容:

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

4

2 回答 2

0
sig Person {friends: set Person}
run {some s: set Person | #s >= 3 and s->s in friends}
于 2017-03-20T12:59:50.153 回答
0
fact three_friends {some disj p, q, r : Person | p+q+r -> p+q+r in friends}

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

于 2017-03-18T05:23:43.623 回答