我想表达这种约束：在一个以上的乐队中有一个歌手 .
以下是Band和Singer的声明 . 关系“乐队”将歌手映射到乐队 .
sig Band {}
sig Singer {
band: Band
}
这似乎表达了期望的约束：
some s: Singer | some s.band
反思后，我认为这不正确 . 它说（我相信）有一个歌手在_1841566频段 . （我对么？）
我希望约束说 more than one 乐队中有一个歌手 .
我认为这应该表达所需的约束：
some s: Singer | #s.band > 1
但Alloy工具表示不能生成任何实例 . 为什么？为什么不正确？表达所需约束的正确方法是什么？
1 回答
Alloy Analyzer表示，由于声明了场频带的方式，因此无法生成任何实例 .
默认情况下，字段声明中没有multiplicity关键字意味着多重性为 exactly one . 在你给出的Alloy模型中，乐队领域因此将给定歌手与一个乐队相关联，因此排除了歌手在多个乐队中演唱的任何情况 .
因此，将多重性关键字 some 添加到字段声明中应该可以解决问题 .
你最后提出的约束确实强制要求至少一个签名者应该严格地在一个以上的乐队中唱歌 .