[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Chris Newcombe <chris.n...@xxxxxxxxx>*Date*: Wed, 23 Apr 2014 08:46:06 -0700*References*: <a6ad15de-04f4-44a8-aa44-b1cc6e18966a@googlegroups.com> <9928CB46-6A86-4C01-A875-D4DC2AE00987@cs.uni-duesseldorf.de>

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

On Tue, Apr 22, 2014 at 2:09 AM, Michael Leuschel <leus...@xxxxxxxxxxxxxxxxxxxxx> wrote:

Dear Christian,I will quickly try and answer some of your questions (but I am myself more of a B expert).Alloy is restricted to first-order relations and sets.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.

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+.TLC is an explicit state model checker, i.e., it will explicitly compute all reachable states of the specification and will detect loops.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 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

**Follow-Ups**:**Re: [tlaplus] Comparison between the TLA tool-set and Alloy***From:*Christian Schuhegger

**References**:**Comparison between the TLA tool-set and Alloy***From:*Christian Schuhegger

**Re: [tlaplus] Comparison between the TLA tool-set and Alloy***From:*Michael Leuschel

- Prev by Date:
**Re: [tlaplus] Comparison between the TLA tool-set and Alloy** - Next by Date:
**Re: [tlaplus] Comparison between the TLA tool-set and Alloy** - Previous by thread:
**Re: [tlaplus] Comparison between the TLA tool-set and Alloy** - Next by thread:
**Re: [tlaplus] Comparison between the TLA tool-set and Alloy** - Index(es):