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関係で、2 番目の列の名前の多重度はどのくらいなのか、興味がありました。また、以下は可能ですか

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

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 つ以上の要素が含まれており、そのうちの 2 つが同じName原子を持っていることがわかります。