使用 "always" 时未找到实例

Question

我正在尝试可视化支付对象的规范，它从"queued";processing"complete"帮助"。我想到了以下几点:

enum State {Queued, Processing, Complete}
sig Payment {
var state: State
}
pred processPayment[p: Payment] {
p.state = Queued // guard
p.state' = Processing // action
}
pred completePayment[p: Payment] {
p.state = Processing // guard
p.state' = Complete // action
}
fact init {
Payment.state = Queued
}
fact next {
always (some p : Payment | processPayment[p] or completePayment[p])
}
run {} for 1 Payment

不幸的是，我没有找到这个规范的实例。根据我的理解，一个状态为"Queued"初始状态和下一个处于"处理"状态的状态;根据https://haslab.github.io/formal-software-design/overview/index.html上的教程，应该允许使用always (some p : Payment | processPayment[p] or completePayment[p])"公式。我错过什么了吗?

Answer 1

问题原来是缺少终止谓词，添加下面的(或口吃)修复它。

pred afterComplete[p: Payment] {
p.state = Complete // guard
p.state' = Complete // action
}

Answer 2

我不是专家，但我相信这是不可能的任何一个谓词是真的在0。我认为你需要一个这样的holdPayment谓词:

pred holdPayment[p:Payment] {
p.state = p.state'
}
fact next {
always (some p : Payment | processPayment[p] or completePayment[p] or holdPayment[p])
}
run {} for 1 Payment