How to revers a seq relation in Alloy

Question

sig Customer {
    orders: seq RecordedOrder,
}

sig RecordedOrder {}

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

How can I revers the orders relation, the normal ~ operator doesn't work and I get this error

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

Is there a way to achieve this ?

I expect to reverse the relation

Answer 1

You can "reverse a seq" like this:

open util/ternary

sig Customer {
    orders: seq RecordedOrder,
}

sig RecordedOrder {}

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

But this isn't going to give you a sequence for each RecordedOrder. If c.orders is (1 -> ro1) + (0 -> ro2), then ro2.flip13[orders] will be 1 -> c, which isn't a valid sequence!

If you just want to get the mapping of customers to orders, you can use select13 instead:

open util/ternary

sig Customer {
    orders: seq RecordedOrder,
}

sig RecordedOrder {}

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

This gives you a binary relation you can reverse as normal.