set - Alloy負のカーディナリティが可能な理由

Question

一部のモデルを Alloy 言語で説明しています。有限ステート マシンを記述するために、次の数行のコードを用意しました。

sig FSA_state {
    transitions: some FSA_state,
    initial: lone InitialState
}

sig InitialState {}

fact i {
    all f: FSA_state | #(f.transitions) <= 0
}

pred show {
}

run show for 5 but 1 InitialState

現在、単一の状態でゼロ以上の遷移を行う理由を理解しようとしています。「エバリュエーター」ツールを使用して、一部の世界ではセット遷移で負のカーディナリティがあることがわかりました。どのように可能ですか (セットはゼロ未満の要素を持つことはできません)? Evaluatorで使用した命令は#(FSA_state.transitions)