Archive containing all models (zip)

Chapter 2: Whirlwind Tour
addressBook1a.als
addressBook1b.als
addressBook1c.als
addressBook1d.als
addressBook1e.als
addressBook1f.als
addressBook1g.als
addressBook1h.als
addressBook2a.als
addressBook2b.als
addressBook2c.als
addressBook2d.als
addressBook2e.als
addressBook3a.als
addressBook3b.als
addressBook3c.als
addressBook3d.als
theme.thm (Use this theme to get the customizations shown in the book)

Chapter 4: Language
filesystem.als
grandpa1.als
grandpa2.als
grandpa3.als
lights.als

Chapter 5: Analysis
addressBook.als
lists.als
sets1.als
sets2.als

Chapter 6: Examples
hotel.thm (Use this theme to get the customizations shown in the book)
hotel1.als
hotel2.als
hotel3.als
hotel4.als
mediaAssets.als
memory/abstractMemory.als
memory/cacheMemory.als
memory/checkCache.als
memory/checkFixedSize.als
memory/fixedSizeMemory.als
memory/fixedSizeMemory_H.als
ringElection.thm (Use this theme to get the customizations shown in the book)
ringElection1.als
ringElection2.als

Appendix A: Exercises
addressBook1.als
addressBook2.als
barbers.als
closure.als
distribution.als
phones.als
prison.als
properties.als
ring.als
spanning.als
tree.als
tube.als
undirected.als

Appendix E: Alternative Approaches
hotel.thm (Use this theme to get the customizations shown in the book)
p300-hotel.als
p303-hotel.als
p306-hotel.als