英文:
Nested maps in Alloy
问题
我试图在Alloy中建模嵌套映射（例如`{a: {b: 3}}`），其中像`{a: {a: 3}}`这样具有相同键重复的映射是无效的。我尝试使用下面列出的最终事实来实现这一点，但显然我没有正确地建模，因为Alloy报告找不到任何实例。
打开工具/自然数
签名 键 {}
签名 嵌套映射 { 映射: 键 -> 键 -> 一个 自然数 }
// 强制存在非空映射
事实 { #嵌套映射 > 0 }
事实 { 所有 m: 嵌套映射 | #m.映射 > 0 }
// 添加此事实使Alloy无法找到任何实例
事实 { 所有 d: 嵌套映射 |
所有 k1: 键 |
所有 k2: 键 |
所有 计数: 自然数 |
((k1 -> k2 -> 计数) 在 d.映射) => k1 != k2
}
英文:
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
}
答案1
得分: 1
"A -> B -> one C" 意味着每个单独的 "A -> B" 必须映射到恰好一个 C。这包括 "key1 -> key1"，这与您的 "fact" 不兼容。您可能希望说的是每个单独的 "A -> B" 必须映射到最多一个 C，这可以使用 "A -> B -> lone C" 来实现。
英文:
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.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论