是否可以在签名事实中使用无点表达式？答案

【问题标题】：Is it possible to use pointfree expressions in signature facts?是否可以在签名事实中使用无点表达式？
【发布时间】：2019-09-23 09:08:51
【问题描述】：

假设我们有以下合金模型：

sig A {}

sig B  {
  R : A
  } 

fact {
  R.~R in iden
  }

run {}

在执行运行时，alloy 会找到一个实例。我想我会尝试将模型的事实更改为 签名事实，如下所示：

sig A {}

sig B  {
  R : A
    } {
    R.~R in iden
    }

run {}

但当我这样做时，合金会告诉我：

A type error has occurred:
~ can be used only with a binary relation.
Instead, its possible type(s) are:
{this/A}

【问题讨论】：

标签： alloy

【解决方案1】：

为了补充已经给出的答案，是的，这是可能的。

您可以使用@运算符。

sig A {}

sig B  {
  R : A
    } {
    @R.~@R in iden
    }

run {}

【讨论】：

【解决方案2】：

在签名内部，R 被视为 A 类型，而不是 B->A。

但是这个事实属于签名之外，因为它是关于 R 的全局结构，而不是 R 的局部部分，b.R，对于每个 b:B。

如果您在 B 中有第二个关系，例如 S:A，则对于每个 b:B，您可以拥有诸如 R != S 之类的签名事实，转换为 b.R != b.S。

【讨论】：