Coming back to this thread after doing what turned out to be a massive project in Alloy 6, I think I need to share some thoughts.
The project I worked on was specifically a series of work flows that enable a factory, and customer service technicians to get credentials for a new or serviced machine, by using a unique hardware identifier.
Alloy 6 had some very charming features, but also some very nasty drawbacks that make it jarring to work with.
Let’s open up with the nice features.
The big one is being able to effectively roll the dice and see many different structural combinations that are allowed in a given model. This highlighted about 60% of the problems we were going to run into.
Second, being able to use set theory to describe the various states of the machines, the sub component which stores the unique hardware identifier, and the types of mappings of connections to our backend found the next 30% of problems.
It can kinda model time with actions. This found the last 10% of problems that needed to be addressed.
There are some other nice features that are a little weird, like being able to describe “all the other machines” as machine - m where m is the machine the current function is applied to.
The pain points:
Specificity. Unlike TLA+, Alloy can’t tell you when you’re a variable or a mapping is being implicitly left to changed. In a massive system that spans across multiple machines, sub component, production facilities, and end users locations (gyms), you need to pathologically specify each step. With large numbers of variables and mappings that means lots unchanged or stuttering sets, in frankly a poorly scalable method. I also have the expectation that stuttering a machine would stutter it’s fields as well, but that’s not the case at all.
Lists. Without a language level list, this only exacerbates the previous issue, in so far, 40% of my specifications are just stutter and unchanged lines, of various flavors to lock down what’s modified.
Sub-sets. Things get real funky when describing what happens with sub-sets. I would expect that a subset of machine (e.g. powered_on machines) would also be stuttered if I stuttered it’s superset.
Now, would I be able to implement the same specification in TLA+? I don’t know, this project was more interested in the implicit structures that could be formed across machines and services, and that would’ve been very difficult in TLA+. However, modeling actions was frankly pulling teeth, and I would really hate to extend my model further.
In summary: I still think Alloy is good for structural studies, but I think it’s inappropriate for adoption of industry as a whole, especially with temporal studies or with verification.