Overconstraint - the bane of declarative modeling

Overconstraint means that you have accidentally constrained your system to eliminate possibilities which you intended to allow.

In the extreme, it eliminate all examples. This is particularly dangerous, since it means that there are no counterexamples to your other assertions because there are no examples at all, not because they are actually true. You can use the run command to help spot overconstraint.

In more subtle cases, it may mask examples which would revealed faults or safety concerns. Currently, there isn't tool support for this, and most modelers find it to be the main time-cost when debugging a model.

Alloy Analyzer can be configured to use unsat core extraction technology to provide a tool which not only helps identify overconstraints, but also narrows down where you need to look for the source of overconstraints you are aware of.

The flip side of overconstraint is underconstraint, in which you allow possibilities which you had meant to disallow. It is a much less serious problem, and much easier to identify.