Comparison between the TLA tool-set and Alloy

[Christian Schuhegger]

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

[fl]

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.

PlusCal allows to write specifications in a procedural way and then translate them in TLA. Try it to see

why a specific tool is welcome.

-- 

FL 

[Michael Leuschel]

Dear Christian,

I will quickly try and answer some of your questions (but I am myself more of a B expert).

On 22 Apr 2014, at 08:05, Christian Schuhegger <christian....@gmail.com> wrote:

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.

Alloy is restricted to first-order relations and sets.

I.e., in Alloy you cannot model sets of sets or functions which take sets as arguments or return sets.

There is no such restriction in TLA+ (or B).

There are other differences, such as the untyped nature of TLA+.

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.

TLC is an explicit state model checker, i.e., it will explicitly compute all reachable states of the specification and will detect loops.

TLC does not use a SAT solver. TLC is comparable to Spin, but for a much higher-level language and with an efficient method to store states on disk.

Alloy is a model finder / constraint solver. In Alloy, you can “only” do bounded-model checking.

Typically, in Alloy you set up a single transition of your system and ask Alloy to find a value for your variables which satisfies some invariant before the transition but fails to satisfy the invariant afterwards.

For example, take a simple Lift model with 

 - a variable level

 - the proposed invariant  level>=0 and

 - the initialisation  level = 4  and

 - the transition to go down one level if we are not at level 1:  “level/=1 & level’ = level-1”.

Here, TLC would compute the statespace consisting of the states

  “level=4”  —>  “level=3”  —>  “level=2”  —> “level=1"

The last state would be considered a deadlock, but in all reachable states the invariant “level>=0” is true.

In Alloy you would typically ask if there a solution for the following constraint:

  level>=0  and  level /=1 & level’ = level-1 and  not(level’>0)’

Alloy would report: yes there is such a state: level=0 and level’=-1.

I.e., Alloy shows that the invariant “level>=0” is not inductive, but the generated counter example “level=0” cannot be reached from the initial state as TLC shows.

Both methods are quite complementary.

Best regards,

Michael Leuschel

[Chris Newcombe]

Hi Christian,

   >>I was trying to find a source that compares [Alloy and TLA+], because both of them look similar to me.

I have evaluated Alloy and TLA+ fairly thoroughly.  As it happens, I've just written a paper about that, called "Why Amazon Chose TLA+".  The paper been accepted for the ABZ'2014 conference in June [1], and will be published in the conference proceedings.  I therefore cannot distribute it broadly before the conference, but if you wish I can send you a private copy to review.  Have you considered coming to the conference?  Leslie is giving the keynote about TLA+, there is a workshop on TLA+, and there are many papers about Alloy, and B/Event-B.

Part of my evaluation is already available, in a talk that I gave at HPTS (bi-annual workshop on High Performance Transaction Systems) in 2011

         Slides including notes : http://hpts.ws/papers/2011/sessions_2011/Debugging.pdf

         Specifications for 2 'real world' algorithms for transaction isolation, in both Alloy and TLA+ : http://hpts.ws/papers/2011/sessions_2011/amazonbundle.tar.gz 

regards,

Chris

[1] http://www.irit.fr/ABZ2014/program.html

[Christian Schuhegger]

Thanks Chris, that is helpful!

I would be interested in having a copy before June. Could you please send it to me as a private copy in advance? I will have a look at the conference and decide if I will join.

I will also have a look at your other references.

Thanks a lot!