I have two Alloy facts:
fact A5 {
all a, b : Filler, s, t : Slot |
(b in s.slot_of and s in a.fills and a in t.slot_of) implies b in t.slot_of
}
fact A6 {
all a, b : Filler, s, t : Slot | ((b in s.slot_of and s in a.fills) and
(a in t.slot_of and t in b.fills)) implies a = b
}
As I noticed that relation calculus style seems more efficient than predicate calculus style (less variables and clauses generated), I wanted to rewrite them using relation calculus style.
For A5, I have this:
fact A5 { slot_of.fills.slot_of in slot_of }
which works well and is, if I correctly understand the styles, in relation calculus style.
But for A6, I didn’t achieve to rewrite it. For now, I got this:
fact A6 {
all a, b : Filler | (a->b in fills.slot_of and b->a in fills.slot_of) implies a = b
}
which is more efficient, but I think it is still in predicate calculus style. So I have some questions: is my current A6 in predicate calculus style? is it possible to rewrite it in relation calculus style? if so, how?
It's still in predicate calculus style because you're using the all
quantifier. To be relational, it can't use any quantifiers.
I think your intended fact is "the only symmetric relations are reflexive ones". The set of all reflexive relations is iden
and the set of all symmetric relations in r
is r & ~r
. So if you want to make A6
fully relational, you'd write fills.slot_of & ~(fills.slot_of) in iden
.