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 d

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. [1] https://arxiv.org/pdf/1603.03599.pdf https://arxiv.org/pdf/1603.03599.pdf