what next?
basic optimizations
propagating equality: reduce by factor of #rel?
new version of Alcoa (5/00)
symmetry & other optimizations
new Alloy: signatures, sequence, closure
extend to APIs
use abstract relations instead
eg, Swing objects
non termination
see whether (state = state’) in some loop iteration
global properties
check object model invariants
eg, every active aircraft is tracked