In Alloy name resolution for fields is not based on namespaces.

module debug

sig Singer          {band: Band}
sig RadioStation    {band: Frequency}
sig Band, Frequency {}

pred show () {
  all b:Band | some b.~band
  all b:Band | some band.b
  all b:Band | some s:Singer | s->b in band
}
run show for 3

Declares 4 basic types: Singer, RadioStation, Band and Frequency and 2 fields band of types Singer -> Band and RadioStation -> Frequency.

The predicate show contains 3 equivalent constraints. The field band is in all cases resolved to the field in Singer.

band : Singer -> Band or RadioStation -> Frequency

~band : Band -> Singer or Frequency -> RadioStation

b : Band

s : Singer

s->b : Singer -> Band

thus

b.~band reads as b:Band . ~band:Band->Singer (since reading ~band:Frequency->RadioStation would fail to join ‘.’ with b)

band.b reads as band:Singer->Band . b:Band (same reason)

s->b in band reads as s->b:Singer->Band in band:Singer->Band (same reason)

So basically disambiguation is done further up the AST.

If disambiguation fails all b:Object | some b.~band (Object is supertype of all basic types, so band can now refer to both fields), then an error is shown

If no field survives after disambiguation, then it is an unresolved reference.

This means that a lookup now basically gets multiple stages: (1) do a lookup without constraints and find all possible values, (2) propagate all possible values up through the AST until you reach a point where one or more alternatives can be discarded (3) discard the alternatives also back down the tree s.t. the name is only resolved to the correct declaration.

Submitted by Daco Harkes on 9 February 2015 at 15:31