Реляционное соединение и операторы в сплаве

Question

Я изучал Alloy в общем и нашел некоторые концепции, которые мне нужно прояснить.

Прежде всего. (Dot Join). Я понял, как это работает для тривиальных примеров, но в таком случае:

sig B {}
sig A {
rel: B -> C
}
sig C {
rel1: B -> A
}
rel = {(a1,b1,c1), (a2,b2,c2)}
rel1 = {(c1,b1,a1),(c2,b2,a2)}
rel.rel1 = {(a1,b1,b1,a1),(a2,b2,b2,a2)}
rel1.rel = {(c1,b1,b1,c1),(c2,b2,b2,c2)

Я не получаю результат rel.rel1 или rel1.rel. Может кто-нибудь объяснить, как это работает, пожалуйста?

У меня также есть проблемы с операторами <: и>:.

Заранее спасибо.

Answer 1

Это подробно объясняется множеством примеров в моей книге (Software Abstractions, MIT Press, 2012).

Кроме того, вы можете найти эти слайды из старой беседы полезными:

На слайде 80 приведен расширенный пример различных точечных объединений.