Re: [tlaplus] Comparison between the TLA tool-set and Alloy

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....@xxxxxxxxx> 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