Most people that use these tools told me TLA+ and Alloy do different things with their automated tooling. They usually say TLA+ looks at ordering of things with Alloy looking at structuring. I only found a few people comparing them directly, though. Do you have a resource showing TLA+ does same thing as Alloy or as easily?
Re SPIN
Im saying they were used similarly. You wrote in one artocle like set theory, model-checking for temporal errors, and so on are new. That was the default in high-assurance decades ago using things like Z specs with SPIN for concurrency. Then, they tried to go for verifying high-level code, then rough code, code then assembly, and so on with refinement proofs. However, it started with algorithmic verification with specs in set theory, first-order logic, and ASM's. Writeups like yours tell me Lamport's concept was to similarly use those easier formalisms leaving off anything but the algorithm. Then add more automation to get more bang for buck for more developers. A good idea since the subset of that which Z and SPIN offered had already prevented serious, sometimes deep, errors in prior systems.
Now, far as SPIN, it was used to chech the properties of concurrency models, hardware specs, caching, protocols, standards, and distributed systems. Industry found bugs in all these things using it with relatively little training vs other methods that required rare specialists. Sound familiar? TLA+ now shows up as tool of choice for quite a few of those areas with SPIN still used a lot due to maturity & being well-known. That's why I said they're similar: people are specifying and model checking similar things with them similarly with much less effort than provers.
The easier proving on TLA+ and high-level nature are real benefits ovee SPIN. It's why I recommend TLA+. ;)
> Do you have a resource showing TLA+ does same thing as Alloy or as easily?
See, Why Amazon Chose TLA+[1]. They found Alloy pleasant enough but a bit weirder than TLA+, and TLA+ is richer in terms of expressivity and features. I learned Alloy and played with it after knowing TLA+ well, and while I think it is an extremely nice and useful tool (although its syntax is indeed weird), it is absolutely trivial to express anything you can in Alloy in TLA+, and that's without even TLA (i.e., just the +). Their tooling is a bit different, so I guess there may be cases where Alloy would be more convenient even if you already know TLA+.
> Im saying they were used similarly. ...
Yeah. Deep formal methods are, in general, much more similar to one another than they are different.
The only in-depth study I know about is "Alloy meets TLA+".[1] Their conclusion was that Alloy is much more flexible and easier to use _unless_ your system is dynamic, because you have to manually model time in Alloy.
Most people that use these tools told me TLA+ and Alloy do different things with their automated tooling. They usually say TLA+ looks at ordering of things with Alloy looking at structuring. I only found a few people comparing them directly, though. Do you have a resource showing TLA+ does same thing as Alloy or as easily?
Re SPIN
Im saying they were used similarly. You wrote in one artocle like set theory, model-checking for temporal errors, and so on are new. That was the default in high-assurance decades ago using things like Z specs with SPIN for concurrency. Then, they tried to go for verifying high-level code, then rough code, code then assembly, and so on with refinement proofs. However, it started with algorithmic verification with specs in set theory, first-order logic, and ASM's. Writeups like yours tell me Lamport's concept was to similarly use those easier formalisms leaving off anything but the algorithm. Then add more automation to get more bang for buck for more developers. A good idea since the subset of that which Z and SPIN offered had already prevented serious, sometimes deep, errors in prior systems.
Now, far as SPIN, it was used to chech the properties of concurrency models, hardware specs, caching, protocols, standards, and distributed systems. Industry found bugs in all these things using it with relatively little training vs other methods that required rare specialists. Sound familiar? TLA+ now shows up as tool of choice for quite a few of those areas with SPIN still used a lot due to maturity & being well-known. That's why I said they're similar: people are specifying and model checking similar things with them similarly with much less effort than provers.
The easier proving on TLA+ and high-level nature are real benefits ovee SPIN. It's why I recommend TLA+. ;)