formal-methods - 对 TLA+ 中变量的当前状态值和下一个状态值进行算术运算

Question

我想写一个这样的（a）公式：

y' = x' - x

但每次我尝试运行模型时，我都会收到错误消息，«在评估中，标识符 x 要么未定义，要么不是运算符。»

到底是怎么回事？这样的公式真的不能写吗？为什么？我该如何解决这个问题？

谢谢。