alloy - 集合的多重性

Question

鉴于以下定义：

sig Name,Addr{}
sig Book{ addr : Name -> some Addr}

Let Name = { (J),(t), (b)}
Addr = {(1), (2)}
Book = {(bb0)}

我很好奇在关系addr : Name -> some Addr中，第二列中名称的多重性是什么。此外，以下是否可能

addr = {(bbo, j , 1), (bb0, j, 2)}

我试图了解 j 是否可以在第二列中多次出现

Answer 1

简短的回答是肯定的，但我只是通过尝试才弄清楚，你必须正确定义你的模型：

abstract sig Name,Addr{}
abstract sig Book{ addr : Name -> some Addr}

one sig J,t,b extends Name {}
one sig a1,a2 extends Addr {}
one sig bb0 extends Book {}

run { #addr > 3 } for 4 int

执行它并使用求值器进行求值，addr你会看到它包含超过 3 个元素，其中两个具有相同的Name原子。