alloy - Alloy にマルチセットはありますか?

Question

Alloyでバッグ(マルチセット)を使用してシステムをモデル化する方法はありますか? また、バッグの明確な概念がない場合、回避策はありますか?

ありがとう。

Answer 1

E のマルチセット [別名バッグ] は、関数 E ->one Natural、または E ->lone (Natural-Zero) (不在の処理方法に関する好みに応じて) によって表現できます。

open util/natural
sig E {}
sig A { m : E -> one Natural }
sig B { n : E -> lone (Natural-Zero) }

fun bagunion[m, n : univ -> lone Natural]: univ -> lone Natural
{ e : (m+n).univ, x : Natural |      e in m.univ-n.univ implies x=e.m
                                else e in n.univ-m.univ implies x=e.n
                                else x=add[e.m, e.n]                  }

バッグ ユニオンを行うには、おそらくもっと適切な方法があります。