alloy - Alloy 4 のモジュール エイリアス名前空間

Question

私が次のことをするとしましょう：

open util/ordering[A]
open util/ordering[B]

順序付け/最初にはどのような値がありますか? 未定義ですか？曖昧さをなくすためにモジュール エイリアスを使用する必要がありますか?

Answer 1

はい、エイリアスを使用する必要があります。たとえば、以下で行ったように

open util/ordering[A] as orda
open util/ordering[B] as ordb

sig A{}
sig B{}

sig C {
   firstA: A,
   firstB: B
} {
   firstA = orda/first
   firstB = ordb/first
}

run {one C}