SE-410-Models

A collection of models made during SE 410: Software Modeling

Created in Alloy 6

Random resources I used

Main Website: https://alloy.readthedocs.io/en/latest/index.html

Tutorial (By Hwayne, creator of the documentation):

  1. https://www.hillelwayne.com/post/alloy6/
  2. https://hillelwayne.com/projects/
  3. https://www.hillelwayne.com/post/formally-modeling-migrations/

Tutorial (By University of Iowa):

  1. https://homepage.cs.uiowa.edu/~tinelli/classes/181/Fall22/Notes/03.1-intro-to-alloy.pdf
  2. https://homepage.cs.uiowa.edu/~tinelli/classes/181/Fall22/Notes/03.2-intro-to-alloy.pdf
  3. https://homepage.cs.uiowa.edu/~tinelli/classes/181/Fall22/Notes/03.3-intro-to-alloy.pdf

Other Tutorials and Papers:

  1. https://msitko.pl/blog/2020/05/24/guide-to-alloy.html
  2. https://dl.acm.org/doi/abs/10.1145/505145.505149?casa_token=Y0RgqSyBBuUAAAAA:Z3R6jov19MJMQpNJQGj70AEuJoZlLc-vuunxttK8rQCOB_pXc_mXvYtRlKL1DVhaIr_9HKxE1F8axQ
  3. https://www.doc.ic.ac.uk/project/examples/2007/271j/suprema_on_alloy/Final%20Report/LaTeX/report.pdf
  4. https://haslab.github.io/formal-software-design/index.html (This is the tutorial I'm using the most)

Q&A about syntax changes from Alloy 4 -> Alloy 6:

  1. https://stackoverflow.com/questions/76167330/alloy-book-example-is-wrong
  2. https://stackoverflow.com/questions/77589881/should-the-book-example-be-refined-to-avoid-inconsistent-results

Interesting discussion on Alloy vs TLA+: https://alloytools.discourse.group/t/alloy-6-vs-tla/329