Comparison between the TLA tool-set and Alloy

[Christian Schuhegger <christian....@xxxxxxxxx>]

Hello group,

I am a software engineer and a non-expert in "lightweight formal methods" (as Alloy calls it) tools like model-checking. I want to add such lightweight formal methods to my tool-box of engineering techniques.

I have now read the Alloy book "Software Abstractions" from Daniel Jackson and the TLA+ book "Specifying Systems" from Leslie Lamport. I was trying to find a source that compares the two approaches, because both of them look similar to me.

The two main questions that I have are:
1) What is the difference in expressive power of the two? Can one do more than the other? I understand that both of them have their roots in first-order logic.
I would be mostly interested in verifying the safety properties of a specification and only to a lesser degree in verifying the liveness properties, but of course more is better.

2) What are the runtime comparisons of checking larger instances? I understand that Alloy is based on boolean SAT solvers, which should make it quite fast to even look at moderate instance sizes and Alloy should profit from advances in the SAT solvers performance. I did not find the details on how the TLA+ model checker is implemented. I believe that runtime is an important factor to determine the usefulness of the tool in the daily work.

2.1) I have seen the graphical exploration possibilities of Alloy that make it easier to understand counter examples. The TLA+ model-checker seems to be text based. Is there a graphical exploration tool for TLA+, too?

One more question I have is how PlusCal would fit into the picture. PlusCal was not existing when the TLA+ book was written. It seems that PlusCal would narrow the gap between a specification and a final implementation considerably, which might be a huge advantage in itself.

Any way forward from here will mean a considerable investment of time into one of the two tools and I would like to understand what might be the best bet for me.

Many thanks and best regards,
Christian