合金规格答案

【问题标题】：Alloy specifications合金规格
【发布时间】：2021-07-16 11:17:06
【问题描述】：

我是一个学习Alloy的初学者，我想知道这个n.^地址是什么意思（也许有一个例子）？因为从逻辑上讲，如果我们将地址视为一组像（A0，A1）这样的对，那么我们如何将 n （例如 N0）与这个集合连接起来？由于地址中最左边的对元素与n的性质不同，我认为这是不可能的。如果有人能指导我，我将不胜感激

【问题讨论】：

标签： software-design alloy

【解决方案1】：

我已经有一段时间没有使用合金了，但是 ^ 运算符表示其操作数关系的传递闭包。所以如果address 是{(a,b), (b,c)} 那么^address 是{(a,b), (b,c), (a,c)}。

n.^address 是n 上新关系的投影。

所以如果n 是a，那么n.^address 是{b,c}

例子：

abstract sig atom{
    address: lone atom
}
one sig a,b,c extends atom{}

fact {
    address = a->b + b->c
}

check {
    a.^address = b+c
}

【讨论】：

【解决方案2】：

你问“这个n.^地址是什么意思？”

表达式 n.^address 是由 n 表示的元组集合和由 ^address 表示的元组集合之间的连接.

表达式 ^address 反过来表示关系 address 的传递闭包，即包含传递的 address 的最小关系.

是否存在，或者原则上，n 中的任何元组，其最右边的值与 ^address 中某个元组的最左边的值相同 - - 或者，换一种说法，表达式 n.^address 是否保证表示空集 - 部分取决于变量 n 和关系 address 被定义，部分是关于宇宙是如何被填充的。 address 的传递闭包是否与 address 相同或更大的关系也是如此。

如果N0、A0 和A1 都是原子，并且关系address 只包含(A0, A1) 对和表达式n 表示（包含）原子N0 的（单例集），那么实际上表达式 n.^address 将表示空集。另一方面，如果 address 包含元组 (N0, A0) 以及元组 (A0, A1)，则

表达式address表示包含元组(A0, A1)的单例集，
表达式^address也表示包含元组(A0, A1)的单例集，并且
表达式n.^address表示包含元组(N0, A1)的单例集，因为集合{(N0, A0)}与集合{(A0, A1)}的连接是集合{(N0, A1)}。

由于您没有提供有关您心目中的合金模型的更多信息，因此无法提供更多信息。

【讨论】：