Alloy中关系运算的域和范围-Java 学习之路

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

假设我在Alloy中定义了一个sig：

sig A {r : B }

sig B {}

我正在寻找和操作应用于r并给我B（可能像r [B]返回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
 }

任何的想法？ :)

2 回答

5
您将在库模块relation.als中分别找到名称为 ran 和 dom 的二进制关系的范围和域函数 . 丹尼尔 Jackson 关于软件抽象的书中的第3.2.5和3.4.3.6节进行了简短的讨论 .

另一方面，您也可以不使用库函数 . 对于任何二元关系r，r的域和范围也可以分别容易地表示为r.univ和univ.r . 使用box运算符而不是dot，范围也可以表示为r [univ] . （注意你的例子r [B]什么都不返回，因为它等同于Br，B中没有任何东西匹配R中任何一对的第一项（因为第一项都在A中，而不是B，在示例A和B是不相交的 . 如果你想要出现在r对中的B的子集，你想要写Ar，或者等价r [A] . 在这种情况下，因为r中的第一项始终是A的元素， Ar相当于univ.r.

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

[附录]要检查关系 fid + mid 是否是单射的，一种简单的方法就是写
```
fact {
  all o : O | lone x : M + F | x.mid = o or x.fid = o
}
```
如果要断言 fid + mid 也总是超过 M + F ，请使用 one 而不是 lone ;我不会因为这个原因而无法接受 .

terser公式可能采取更“关系”的风格：
```
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
}
```
回复于 2024-04-20T19:52:56+08:00
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的域中的中间元素 .

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

希望这可以帮助 .
回复于 2024-04-20T19:52:56+08:00

Alloy中关系运算的域和范围

2 回答

相关问题