如何表达这种约束：不止一个乐队有一个歌手

Question

我想表达这样的约束：一个歌手不止一个乐队

下面声明乐队和歌手。关系 "band" 将歌手映射到乐队。

sig Band {}

sig Singer {
  band: Band
}

这似乎表达了所需的约束：

some s: Singer | some s.band

仔细一想，我觉得不对。它说（我相信）一个或多个乐队中有一位歌手。 （我说的对吗？）

我想约束说不止一个乐队有歌手。

我认为这应该表达所需的约束：

some s: Singer | #s.band > 1

但是Alloy工具说无法生成任何实例。为什么？为什么不正确？表达所需约束的正确方法是什么？

Answer 1

Alloy 分析器说由于声明字段带的方式，无法生成任何实例。

默认情况下，在字段声明中没有多重性关键字意味着多重性恰好是一个。 在您给出的 Alloy 模型中， band 字段因此将给定的歌手与一个乐队联系起来，因此排除了歌手在多个乐队中演唱的任何情况。

将多重性关键字 some 添加到您的字段声明中应该可以解决问题。

sig Band {}

sig Singer {
  band: some Band
}

您上次提出的限制 some s: Singer | #s.band > 1 确实强制要求至少一名签名者应该严格地在一个以上的乐队中演唱。