Home Articles

Alloy中关系运算的域和范围

Asked
Viewed 850 times
0

是否有任何操作返回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 Answers

  • 5

    您将在库模块relation.als中分别找到名称为 random 的二进制关系的范围和域函数 . 丹尼尔 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
    }
    
  • 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变为 univuniv 是包含模型中所有元素的一元集常量),则a1.univ包括参与关系a1的A的元素(即a1的域) . 原因是中间元素(即,univ中与a1的范围匹配的元素)都被移除 . 请注意,在a1.univ中,所有a1范围都匹配并被删除,因为univ包含模型中的所有元素,包括a1范围 .

    希望这可以帮助 .

Related