Warning message for always-empty joins
Closed this issue · 1 comments
tnelson commented
It's super easy to accidentally write a Forge constraint involving join that's always empty. Maybe you forget which side of a relation has a certain type.
sig A {r: B->C}
sig B {}
sig C {}
pred test {
-- always empty
all x : r.r | ...
}
Alloy had the ability to give a warning when this could be detected statically. I have made SO MANY ERRORS this way, and I students have as well. Let's bring back this warning message (and any others that seem appropriate?)
tnelson commented
This check, along with check for variable capture, is implemented in the last-checker.rkt module on dev branch.