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
}
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
.