对断言中的蕴涵运算符感到困惑

Question

签名 Test 有两个字段，a 和 b:

sig Test {
    a: lone Value,
    b: lone Value
}

sig Value {}

请注意 a 和 b 可能有也可能没有值。

一个Test只有满足这个依赖关系才有效：如果a有一个值，那么b也必须有一个值：

pred valid (t: Test) {
    one t.a  => one t.b
}

我想创建一个断言，我希望 Alloy 分析器找到反例。断言是这样的：如果 t: Test 有效，则 t': Test 也有效，其中 t' 与 t 相同，除了 t' 没有值b:

assert Valid_After_Removing_b_Value {
    all t, t': Test {  
         t'.a = t.a
         no t'.b 
         valid[t] => valid[t']
    }
}

我希望 Alloy 分析器生成这样的反例：t 具有 a 和 b 的值。 t' 有 a 的值，但没有 b 的值。因此，t 有效，但 t' 无效。但是 Analyzer 给出了这样的反例：t 具有 a 和 b 的值，而 t' 具有 a 和 b 的值。我不明白。如果 t 具有 a 和 b 的值，则 t 有效。同样，如果 t' 具有 a 和 b 的值，则 t' 有效。怎么可能是反例呢？

表达断言的正确方式是什么？同样，我的目标是表达这一点：我断言如果 t 是有效的，那么 t 的稍微小一点的版本（例如，b 没有值）也是有效的。由于相互依赖性，这应该会产生反例。

Answer 1

我认为你的说法应该是：

assert Valid_After_Removing_b_Value {
    all t, t': Test {  
         (t'.a = t.a &&
          no t'.b &&
         valid[t]) => valid[t']
    }
}

在您最初的断言中，您断言了三个独立的事物。例如，每个带有 b 的 t' 都已经是一个反例。

对断言中的蕴涵运算符感到困惑

Confused about the implication operator in assertions

alloy