alloy - 在状态之间添加删除关系

Question

我有这个合金模型

module Test
sig B {}

sig A {
c: some B,
delta: c lone -> lone c
}


pred operationA[disj x, x': A,  
c1, c2: B]{
x'.delta = x.delta + (c1->c2)
x'.delta = x'.delta - (c1->c2)
x'.c = x.c
} 

run operationA for 10 but 2 A

这不会为我生成任何实例。我在 x' 状态下添加关系 c1->c2 并再次删除它，出于某种原因它不允许我这样做。

Answer 1

Alloy 语言是声明性的，这意味着您编写的规范说明最终必须发生什么，而不是如何实现（这是命令式方法）。因此，operationA谓词的主体被解释为您在那里编写的三行的合取，而不是要执行的操作序列。

更具体地说，该行x'.delta = x'.delta - (c1->c2)表示x'.delta关系的内容同时等于x'.delta - c1->c2。就其本身而言，当且仅当x'.delta不包含元组时，该行是可满足c1->c2的（因为-运算符是一个集合差异，并且如果您尝试从集合中删除不存在的东西，则结果是相同的集合）。但是，上一行x'.delta = x.delta + (c1->c2)表示x'.deltamust include的内容c1->c2(加上 中的任何内容x.delta，因此这两行加在一起是不能满足的。

如果要对命令式算法的三个步骤进行建模，则必须使用三个变量，例如x、x'和x''。