module Store -- potentially undetetermined values abstract sig PUValue {} abstract sig Value extends PUValue {} sig Number extends Value{} sig Record extends Value {} sig Location extends Value {} sig EquivalenceClass extends PUValue { locs: set Location } sig Store { domain: set Location, determined: set Location, lookup: Location -> PUValue, next: Location, alloc: Store }{ all loc: Location | loc in domain <=> some lookup[loc] all loc: Location | loc in determined <=> loc in domain and lookup[loc] in Value next not in domain } assert AlternativeDomainFormulation { all s: Store | s.domain = s.lookup.univ } pred undetermined [s:Store, x: Location] { x in s.domain and not (x in s.determined) } pred determined [s:Store, x: Location] { x in s.determined } assert AltUnDetermined { all loc: Location, s: Store | undetermined[s,loc] iff loc in s.domain and s.lookup[loc] not in Value } check AlternativeDomainFormulation check AltUnDetermined