Alloy is an open source language and analyzer for software modeling

A couple use cases for this:

1. You're writing an access control policy feature. There are many different moving parts to it: you can assign policies to individuals or user roles, some resources can inherit policies from parent resources, some policies can have multiple conditions, etc. Is there some weird feature interaction that lets somebody see a resource they shouldn't?

2. You're modeling an invoice. Every invoice has a number of items, each item has a supplier. Some items may correspond to their own invoice the supplier is paying, with its own line items. Its possible for you to pay for an item by supplier S that corresponds to an invoice where they pay you. Also two suppliers may be able to supply the same item and have different invoices for that item. Does your model of this have any insane edge cases you should be worried about?

It's more about data structures and testing every variation up to a fixed maximum size.

One consequence of this is that Alloy is a much smaller language: you can fit the entire syntax on a single sheet. It's also much easier in TLA+ to write a spec that you can't model-check, while with Alloy you have to be actively trying. It’s also impossible to write an unbound model in Alloy, so you’re guaranteed that every spec is over a finite state space. Which gets rid of the common TLA+ runtime problem of “is this taking a long time because it’s a big state space or because it’s an infinite state space".

Re tooling: Alloy converts to SAT, which makes model checking much, much faster. Specs that would take minutes to check in TLA+ take less than a second in Alloy. Being able to model-find as well as model-check is really nice, as is the ability to generate multiple counter/examples. The visualizer is really useful, too, especially for showing counterexamples to nontech folk. But the thing I honestly miss most when working in TLA+ is the REPL. It’s not the best REPL, but it’s a hell of a lot better than no REPL.

Okay, so drawbacks: Alloy doesn’t have an inbuilt notion of time. You have to add it in as a sequence sig. This means you can’t study liveness properties or deadlocks or anything like that. It also makes simulating concurrency awkward. This isn’t a huge problem if you have simple interactions or only one structure that’s changing, but the more “timelike” the problem gets, the worse Alloy becomes at handling it.

Less fundamental but still a big problem I keep having: no good iteration or recursion. Transitive closure is pretty nice but it’s not powerful enough. For example:

    sig node {edge: set Node}

The biggest problem with Alloy adoption, though, is social: there’s no comprehensive online documentation. If you want to learn it you have to buy _Software Abstractions_. Fantastic book but not something that’s especially convenient, and it doesn't cover newer features. We're working on changing this, but it will be a while before we have comprehensive online documentation available.

Which one is more appropriate to use really depends on your problem. As a very, very, VERY rough rule of thumb: TLA+ is best you're most interested in the dynamics of a system: the algorithms, the concurrency, etc. Alloy is best when you're most interested in the statics of a system: the requirements, the data relationships, the ontology, etc. My standard demos for showcasing TLA+ are concurrent transfers and trading platforms, while my standard demos for Alloy are access policies and itemized billing. You can use each in the other's niche, too (see Zave's work on Chord), so it's not a stark division.

I barely know anything about TLA+ though.

Likewise I searched in vain for one of these diagrams. It sounds interesting but the 'GUI' is just two text windows and a toolbar that look straight out of 1996 which doesn't bode well.

http://alloytools.org/documentation.html

Including tutorials

http://alloytools.org/tutorials/online/

http://alloytools.org/tutorials/day-course/