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

*From*: Michael Leuschel <leus...@xxxxxxxxxxxxxxxxxxxxx>*Date*: Tue, 22 Apr 2014 11:09:55 +0200*References*: <a6ad15de-04f4-44a8-aa44-b1cc6e18966a@googlegroups.com>

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

**Attachment:
smime.p7s**

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

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

- Prev by Date:
**Re: 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: Comparison between the TLA tool-set and Alloy** - Next by thread:
**Re: [tlaplus] Comparison between the TLA tool-set and Alloy** - Index(es):