Alloy is a tool for analyzing systems and seeing if they are designed correctly. You can read more here and download it here.
This is my tentative proposed documentation for the Alloy language.
This is not the official Alloy documentation. It's a staging ground for material that's intended to become official documentation, but for now I'm writing this independently, not as part of the alloy board.
This is a work in progress. This documentation is incomplete and changes may be made. There are also a lot of things that still need to be added.
This is meant as a reference, not a tutorial.
This is not comprehensive. Certain things are intentionally excluded, like bitshift operators, specific internal modules, anonymous predicates, and Alloy 3 legacy syntax. Generally these are things that I personally believe are only useful in very specific niche cases, and otherwise serve to confuse things.
I’ve added commentary in the markup of the pages that is invisible in the final output. If you see something
.. like this
Then it will not be rendered. If I used a special run predicate to
generate a particular visualization, I put it in a comment.
Anything with a [⋇] is an advanced topic and unnecessary to learn if you're just a beginner.
Issues with the documentation can be raised here.
I'm Hillel. I also wrote a guide to TLA+ and have a blog.