如何反转 Alloy 中的序列关系

Question

sig Customer {
    orders: seq RecordedOrder,
}

sig RecordedOrder {}

fact "example fact" {
    all o:RecordedOrder |
        #o.~orders > 0;
}

如何反转订单关系，正常的 ~ 运算符不起作用，我收到此错误

~ can be used only with a binary relation.Instead, its possible type(s) are:{this/Customer->seq/Int->this/RecordedOrder}

有办法实现这个吗？

我希望扭转这种关系

Answer 1

您可以像这样“反转序列”：

open util/ternary

sig Customer {
    orders: seq RecordedOrder,
}

sig RecordedOrder {}

fact "example fact" {
    all o:RecordedOrder |
        some o.(flip13[orders])
}

但这不会为您提供每个

RecordedOrder

的序列。如果

c.orders

是

(1 -> ro1) + (0 -> ro2)

，那么

ro2.flip13[orders]

将是

1 -> c

，这不是一个有效的序列！

如果您只想获取客户到订单的映射，可以使用

select13

代替：

open util/ternary

sig Customer {
    orders: seq RecordedOrder,
}

sig RecordedOrder {}

fact "example fact" {
    all o:RecordedOrder |
        some o.~(select13[orders])
}

这为您提供了一个可以正常反转的二元关系。