You might find SPIN more approachable, the syntax is similar to a cross between C and bash :)
Here's an example from the book "The SPIN model checker", by Holzmann, the creator of SPIN:
mtype = { P, C, N };
mtype turn = P;
pid who;
inline request(x, y, z) {
atomic { x == y -> x = z; who = _pid }
}
inline release(x, y) {
atomic { x = y; who = 0 }
}
active [2] proctype producer()
{
do
:: request(turn, P, N) ->
printf("P%d\n", _pid);
assert(who == _pid);
release(turn, C)
od
}
active [2] proctype consumer()
{
do
:: request(turn, C, N) ->
printf("C%d\n", _pid);
assert(who == _pid);
release(turn, P)
od
}
And this is Dekker's mutual exclusion algorithm from the same book:
bit turn;
bool flag[2];
byte cnt;
active [2] proctype mutex()
{ pid i, j;
i = _pid;
j = 1 - _pid;
again:
flag[i] = true;
do
:: flag[j] ->
if
:: turn == j ->
flag[i] = false;
(turn != j) -> /* wait until true */
flag[i] = true
:: else ->
skip /* do nothing */
fi
:: else ->
break /* break from loop */
od;
cnt++;
assert(cnt == 1); /* critical section */
cnt--;
turn = j;
flag[i] = false;
goto again
}
I don't like the TLA syntax, which is quite different from a typical programming language. In this blog's deadlock example it looked much nicer than usual for some reason.
TLA+ is intentionally made to look different from a typical programming language because it is very different. Even a simple programming language is far more complex than the simple mathematics underlying TLA+. If all you want to do is to verify some simple assertion about a relatively simple program, then SPIN might indeed suit you better (assuming you can express what you want in SPIN). But TLA+'s main contribution is to allow you to design and deeply understand a complex system, and how and why it works, by reducing it to its bare essentials, and describing it at whatever level of detail you're interested in (often in multiple levels of detail, which are then formally related to one another).
Here's an example from the book "The SPIN model checker", by Holzmann, the creator of SPIN:
And this is Dekker's mutual exclusion algorithm from the same book: I don't like the TLA syntax, which is quite different from a typical programming language. In this blog's deadlock example it looked much nicer than usual for some reason.