定义多个约束有什么问题?

问题描述 投票:0回答:1

我正在尝试用 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``定义的约束上,这对我来说实际上看起来很合理。

有什么想法吗?谢谢

constraints alloy
1个回答
0
投票

“调试”不一致规范的通常解决方案是注释掉事实并查看规范是否变得一致,这会提示可能存在的问题。

这里,

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 事实应该几乎只用于一般真理。

© www.soinside.com 2019 - 2024. All rights reserved.