Nested maps in Alloy

Question

I'm trying to model nested maps in Alloy (e.g. {a: {b: 3}}) where mapping such as {a: {a: 3}} with the same key repeated are invalid. I tried to do this with the final fact listed below, but I'm obviously not modeling something correctly since Alloy reports no instances are found.

open util/natural

sig Key {}

sig NestedMap { map: Key -> Key -> one Natural }

// Force a non-empty map to exist
fact { #NestedMap > 0 }
fact { all m: NestedMap | #m.map > 0 }

// Adding this fact makes Alloy unable to find any instances
fact { all d: NestedMap |
        all k1: Key |
        all k2: Key |
        all count: Natural |
        ((k1 -> k2 -> count) in d.map) => k1 != k2
}

Answer 1

A -> B -> one C means that every single A -> B must be mapped to exactly one C. This includes key1 -> key1, which is incompatible with your fact. You probably instead wanted to say that every single A -> B must be mapped to at most one C, which can be done with A -> B -> lone C.