首页 文章

没有找到3元素的反例

提问于
浏览
2

我正在学习Alloy并试图让它找到两个二元关系 rs ,这样 s 等于 r 的传递闭包,并且 s 不等于 r . 我想我可以通过执行以下操作让Alloy执行此操作:

sig V
{
  r : V,
  s : V
}
assert F { not ( some (s-r) and s=^r ) }
check F

现在合金4.2找不到一个反例,尽管一个简单的3元素结构显然是 r = {(V0,V1), (V1,V2)}s = r + {(V0,V2)} .

有人可以解释发生了什么吗?

1 回答

  • 2

    直接翻译您的要求:

    // find two binary relations r and s such that 
    // s equals the transitive closure of r ands is not equal to r
    
    run {some r, s: univ -> univ | s != r and s = ^r}
    

    这给出了一个预期的实例 . 您的规范中的错误是您的声明将关系限制为函数;应该有

    sig V {
      r: set V,
      s: set V
      }
    

    要么

    sig V {r, s: set V}
    

相关问题