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.
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.
Description: S/MIME cryptographic signature