I bought Daniel Jackson's book Software Abstractions: Logic, Language and Analysis. It thoroughly discusses all aspects of Alloy software and methodology. I hav

I bought Daniel Jackson's book Software Abstractions: Logic, Language and Analysis. It thoroughly discusses all aspects of Alloy software and methodology. I have to say it is one of the best software book I've ever read. It covers relational modelling thoroughly and is very readable from cover to cover. Model checking is so much more pleasant to use than theorem proving. The Alloy software download jar file also includes both source and examples.