Module Alias Namespace In Alloy 4

Question

Lets say I do the following:

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

What value does ordering/first have? Is it undefined? Do you need to use module aliases to disambiguate?

Answer 1

Yes, you should use aliases, e.g., like I did below

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}