Software Abstractions: Models Repository
All models are in Alloy Version 3.0

Chapter 2: Whirlwind Tour
addressBook1.als
addressBook2a.als
addressBook2b.als
addressBook3.als

Chapter 3: Logic
joins.als
splits.als

Chapter 4: Language
uniqueInts.als
filesystem.als
grandpa1.als
grandpa2.als
lights.als
lights2.als
ring.als
theorems.als

Chapter 5: Analysis
addressBook.als
addressBook-simpler.als
addressBook.als
lists.als
ring.als
sets.als
unionClosure.als
webcache1.als

Chapter 6: Examples
book.als
hotel.als
hotelEvents.als
assets.als
abstractMemory.als
cacheMemory.als
checkCache.als
checkFixedSize.als
checkFixedSizeInlined.als
fixedSizeMemory.als
fixedSizeMemory_H.als
ringElection.als

Appendix E: Alternative Approaches
addressBook.als
hotel-event-based.als
hotel-new-frame.als
hotel-refined.als
hotel.als
hotelNoCheckout.als