tnelson/Forge

Warning message for always-empty joins

Closed this issue · 1 comments

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?)

This check, along with check for variable capture, is implemented in the last-checker.rkt module on dev branch.