alloy - Alloy 4 中的模块别名命名空间

Question

假设我执行以下操作：

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

ordering/first 有什么价值？它是未定义的吗？您是否需要使用模块别名来消除歧义？

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}