添加状态

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

的合金语言是声明，意思是你写的规范有什么到底发生而不是如何做到这一点（这是势在必行的做法）。因此，谓词的主体被解释为您在其中编写的三行的连接词，而不是作为要执行的一系列操作。

更具体地说，行x'.delta = x'.delta - (c1->c2)说，x'.delta关系的内容是同时等于x'.delta - c1->c2。在它自己的情况下，当且仅当x'.delta不包含元组c1->c2（因为-运算符是一组差异，并且如果您尝试从集合中删除一些尚未存在的东西，则结果是相同的集合）。然而，前行，x'.delta = x.delta + (c1->c2)说的x'.delta内容必须包括c1->c2（加上无论是在x.delta，所以这两条线一起是不可满足的。

如果您要建模三个步骤势在必行算法，你会必须使用三个变量，例如，x,x'和x''。