Alloy

Classroom material

• Basic genealogy model (with some bugs). Basic model with corrections. Extended genealogy model using predicates (but with a bug). Corrected, Extended genealogy model using predicates.
• Slides, part 1.
• Slides, part 2.

Alloy software

• Alloy 6 software. Download the jar, and run it as "java -jar org.alloytools.alloy.dist.jar". (You may need to install Java version 11.)
• Alloy 4 software. Download the jar, and run it as "java -jar alloy4.2_2015-02-22.jar". (You may need to install Java version 11.)

References

• Alloy language reference.
• Paper on how Alloy translates quantifier-free relational formulas to propositional formulas.
• Alloy Web site.
• Alloy online tutorial.
• Book on Alloy, by Daniel Jackson.