I've been going over Alloy in general and found some concepts that I need some clearance on.
First of all, the . (Dot Join). I got how it works for trivial examples but in a case like this:
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)
I don't get the result of rel.rel1 or rel1.rel. Can somebody explain how it works please?
I am also having problems with <: and >: operators.
Thanks in advance.
This is explained in detail with lots of examples in my book (Software Abstractions, MIT Press, 2012).
Also, you might find these slides from an old talk helpful:
From slide 80 on, there's an extended example of various dot joins.