0

是否有任何操作可以返回 Alloy 中关系的范围和域。

假设我在 Alloy 中定义了一个 sig，如下所示：

sig A {r : B }

sig B {}

我正在寻找要在 r 上应用的操作并给我 B（可能类似于返回 B 的 r[B]）

上面的情况可能看起来很愚蠢，因为 r[B] 会返回 B，所以为什么我一开始不使用 B！实际上，我发现范围和域操作（如果它们存在的话）对于编写事实（约束）非常有用。例如：

sig O {sup:O}

sig M{mid: O, sup:O} {mid.sup=sup}

sig F{fid:O, sup:O}{fid.sup=sup}


fact K{
   all o:O | lone so:M | so.mid=o 
   all o:O | lone so:F | so.fid=o
   all o:O | one i:(fid+mid) | o in i[O]   //I want to say fid+mid is injective, so expecting i[O] return range of i
 }

任何想法？:)

4

2 回答 2

5

ran您将分别在名称和下的库模块relation.als 中找到二进制关系的范围和域函数dom。Daniel Jackson 关于软件抽象的书的 3.2.5 和 3.4.3.6 部分有简短的讨论。

另一方面，您也可以不使用库函数。对于任何二元关系r ， r的域和范围也可以很容易地分别表示为r.univ和univ.r。使用框运算符代替点，范围也可以表示为r[univ]。（请注意，您的示例r[B]将不返回任何内容，因为它等效于Br并且 B 中的任何内容都不匹配 R 中任何对的第一项（因为第一项都在 A 中，而不是 B 中，并且在示例中 A 和B 是不相交的). 如果你想要 B 的子集出现在 r 的对中，你想写Ar，或者等价的 r[A]. 在这种情况下，由于r中的第一项始终是A的元素，因此Ar等价于univ.r。

请注意，域和范围这两个词有多种用法。术语域有时用于表示作为关系对中的第一项出现的事物的集合（并且对于作为任何对中的第二项出现的事物的集合的范围类似），有时用于表示可能作为一对中的第一个（第二个）项目出现的东西。库函数和表达式r.univ和univ.r在第一种意义上计算域和范围，而不是第二种。就您的第一个示例而言，在合金中，关系r的域不一定等于集合B; 它也可以是B的真子集。

[附录]为了检查关系fid + mid是单射的，一种简单的方法是写

fact {
  all o : O | lone x : M + F | x.mid = o or x.fid = o
}

如果您想断言也完全超过，请使用one而不是；我不明白“内射”意味着这一点。lonefid + midM + F

更简洁的表述可能采用更“相关”的风格：

lone (mid + fid).o

用这个成语重铸，你的事实将是

fact mid_fid_injective {
  all o : O | lone mid.o
  all o : O | lone fid.o
  all o : O | lone (mid + fid).o
}

但是当然这里的第一和第二个陈述是由第三个暗示的，所以你可以通过

fact mid_fid_injective {
  all o : O | lone (mid + fid).o
}
于 2014-08-21T01:50:26.737 回答
1

我想添加一些关于点运算符的评论，这将有助于理解为什么 r.univ 和 unive.r 分别是关系 r 的返回域和范围。

Alloy 中的点操作类似于合成操作。为了描述它，假设以下设置：

a1 is an arrow /relation from A to B
a2 is and arrow/ relation from B to C

那么 a1.a2 是从 A 到 C 的箭头/关系。在 a1.a2 中，属于 B 并且在 a1 的范围和 a2 的域中的中间元素被省略。

在合金中，点操作也可以用于集合。在上面的例子中，如果 a2 变成一个univ（univ是一个一元集合常数，它包括模型中的所有元素），a1.univ 包括参与关系 a1（即 a1 的域）的 A 的元素。原因是中间元素（即univ中匹配a1范围的元素）都被移除了。请注意，在 a1.univ 中，所有 a1 范围都被匹配和删除，因为 univ 包含模型中的所有元素，包括 a1 范围。

希望这可以帮助。

于 2014-12-02T18:06:51.933 回答