首页 文章

为什么我为两个关系的连接和三个关系的连接得到相同的图形?

提问于
浏览
0

下面我创建三组:名称,地址和主机 . addr字段将Name映射到Address . 主机字段将地址映射到主机 .

sig Name {
    addr: Address
}

sig Address {
    host: Host
}

sig Host {}

在这里,我要求Alloy Analyzer为两个关系的连接创建一个实例:addr和host .

run {one addr.host} for 1

这是生成的图形:

enter image description here

接下来,我要求Alloy Analyzer为三个关系的连接创建一个实例:addr,每个元组中相同原子的三元关系,以及主机 .

run {one addr.{a, b, c: univ | a = b and b = c}.host} for 1

令人惊讶的是,生成的图形与上面显示的图形相同 . 为什么是这样?

1 回答

  • 1

    可视化工具通过为每个命名关系和集合赋值来显示实例 . 你的第二个例子中只有两个命名关系 . 如果要查看作为表达式给出的关系的值,则需要对其进行命名,例如:

    run {some r: univ -> univ -> univ | 
      r = {a, b, c: univ | a = b and b = c} and 
      one addr.r.host} for 1
    

相关问题