我正在尝试用 Alloy 编写一个简单的(我认为)模型,但显然我没有明白这一点......
问题很简单... 模拟道路网络的图表。
显然,汽车可以在道路上或在十字路口上,但不能同时在两者上。这是我的代码:
//SIGNATURES
sig Cross {
var cars: set Car,
roads: some Road
}
sig Road {
var cars: set Car
}
sig Car {}
//FACTS
fact CrossConstraints {
(all r : Road |
#({cr : Cross | r in cr.roads}) = 2)
}
fact CarConstraints {
(all c : Car |
no cr1, cr2 : Cross |
c in cr1.cars and c in cr2.cars)
(all c : Car |
no r1, r2 : Road |
c in r1.cars and c in r2.cars)
(all c : Car |
(one r : Road | c in r.cars ) or
(one cr : Cross | c in cr.cars))
}
fact {
#Car > 1
}
这对我来说似乎很好,但分析器找不到我的模型的实例...... 看来问题出在为``Car``定义的约束上,这对我来说实际上看起来很合理。
有什么想法吗?谢谢
“调试”不一致规范的通常解决方案是注释掉事实并查看规范是否变得一致,这会提示可能存在的问题。
这里,
CarConstraints
事实确实太有力了。你是说:
在这里,您的意思是汽车不能有两个十字架除非它们碰巧是同一个十字架。换句话说,您希望
cars
(因为 Cross
和 Road
都是 内射)。为了说明这一点(对于十字架),您有多种选择:
(all c : Car |
no disj cr1, cr2 : Cross |
c in cr1.cars and c in cr2.cars)
或
// I prefer this because it doesn't feature negation, which is error-prone
(all c : Car, cr1, cr2 : Cross |
c in cr1.cars and c in cr2.cars implies cr1 = cr2)
最后,由于这是与物理现实相对应的结构事实,因此您可以直接在领域模型中陈述这一点(并立即删除相应的事实陈述):
sig Cross {
var cars: disj set Car,
roads: some Road
}
(从技术上讲,最后一个更强,因为它前面有一个隐含的
always
;无论如何,你的事实可能应该带有一个 always
前缀)。
此外,与您想要见证的实例(
CrossConstraints
和#Car > 1
)相关的基数约束在IMO中应该输入run
命令而不是作为事实陈述。 IMO 事实应该几乎只用于一般真理。