A Gentle Introduction to Modeling, using Alloy

First, special thanks to Daniel Jackson for his incredible patience in answering my endless questions. And, thanks to Daniel and his team for creating such a wonderful and powerful modeling language and tool, Alloy .

Thanks to Charles Wallace for creating this wonderful Alloy Cheat Sheet (Word doc).

Here is a zip file containing all the materials in this Alloy tutorial -- all the Powerpoint slides, examples, and lab exercises.

Table of Contents

  1. [Slides] 10 people coming over for dinner, how will they be seated, can all the seating constraints be satisfied?
  2. [Slides] Alloy is a (fantastic) modeling language and modeling tool ... 3 secrets to understanding Alloy.
  3. [Slides] Farmer needs to ferry a goat, wolf, and cabbage across a river, but his boat can only carry one item at a time.
  4. [Slides] The Einstein puzzle. Einstein said that only 2% of the world could solve it. We will solve it!
  5. [Slides] A step-by-step instruction guide for navigating though Alloy models.
  6. [Slides] I like Alloy because ...
  7. [Slides] Software testing versus Alloy instance generation.
  8. [Slides] Model the cut and paste operations of icons on a desktop.
  9. [Slides] Alloy can tell you whether two models are equivalent - this is really awesome!
  10. [Slides] Creating easy-to-read models.
  11. [Slides] How to implement multiple inheritance in Alloy.
  12. [Slides] What is the universe for your model?
  13. [Slides] Creating high confidence, highly dependable, critical software.
  14. [Slides] Eve steals Alice's password ... how to prevent it.
  15. [Slides] Socrates is mortal ... modeling inferences.
  16. [HTML] The Rule of Maximum Practical Formality.
  17. [Slides] When, What, and Why of creating system and software models.
  18. [Slides] Want to truly understand sets? Learn Alloy! Want to learn Alloy? Learn sets!
  19. [Slides] The root cause of all security failures.
  20. [MS Word] What does it mean to order a set? (Since, by definition, sets are unordered)
  21. [Slides] Object model versus event model
  22. [MS Word] When writing software you must provide a step-by-step set of instructions to the computer. A model of the software, however, doesn’t do that.
  23. [MS Word] Model a green wave - create a model of traffic lights such that drivers encounter a series of green lights.
  24. [Slides] How to implement an encapsulation design in Alloy.
  25. [HTML] SysML versus Alloy.
  26. [HTML] The dirty little lies of the software industry.
  27. [MS Word] Model the binary search algorithm. Dealing with arithmetic overflow.
  28. [Slides] How to ensure each hotel guest has a unique set of keys. Show equivalence of two constraint approaches.
  29. [MS Word] Alloy model of playing tic-tac-toe.
  30. [MS Word] Lessons Learned in Model Building using Alloy.

Roger L. Costello
May 6, 2018