digraph.als: a directed graph (no additional constraints)
dirtreecorrect: correct implementation of directed trees
dtreebug: buggy implementation of directed trees; injectivity uses ~edges.edges (wrongly) instead of edges.~edges
coloredtrees: spec from section 2
coloredtreesbug: spec from section 2 with areflexivity commented out
gwh: non-homeomorphically irreducible trees
abc: a logic puzzle from our intro FM class
addr: address book (related but not identical to Alloy book spec)
bempl: toy lab security policy spec
other: another toy lab security policy spec
CD2Alloy1: UML diagram 1 (via CDDiff compiler)
CD2Alloy2: UML diagram 2 (via CDDiff compiler)
diff1: UML diagram difference (1 vs 2)
diff2: UML diagram difference (2 vs 1)
flow: 2013 Flowlog NIB spec translation, with transitive-closure bug
gene: Alloy book geneology
grade: Gradebook
grand: Alloy book grandpa
resfm: Emina Torlak's resolution model for FM08