Demonstration of bug in distributed lock

distlock.cfg

CONSTANTS
    Threads = {t1, t2, t3}
    NULL = NULL

SPECIFICATION Spec
PROPERTY NoRaces

distlock.tla

---- MODULE distlock ----
EXTENDS TLC, Integers, Sequences
CONSTANT Threads, NULL

Range(f) == {f[x] : x \in DOMAIN f}

(*--algorithm distlock
variable 
    data = 0;
    lock = NULL;

process writeData \in Threads
variable tmp = -1;
begin
    GetLock:
        await lock = NULL;
        lock := self;
    readData:
        tmp := data;
    calcData:
        tmp := tmp + 1;
    writeData:
        data := tmp;
    ReleaseLock:
        lock := NULL;
end process;

process clock = "clock"
begin
    ExpireLock:
        lock := NULL;
end process;
end algorithm; *)
====