libtlafmt 0.4.1

A formatter library for TLA+ specs, core of tlafmt
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/DistributedReplicatedLog.tla
---
This spec was inspired by https://github.com/microsoft/CCF/blob/main/tla/consensus/abs.tla.

This spec has a machine-closed fairness constraint, which differs from the the CRDT and
ReplicatedLog examples.  However, this spec assumes that a server can consistently read the
state of all other servers, which is clearly not a realistic assumption for a real
distributed system.  A real system would rely on some messaging protocol to determine the
lag between servers (compare Raft).

----------------------- MODULE DistributedReplicatedLog ------------------------
EXTENDS Sequences, SequencesExt, Integers, FiniteSets, FiniteSetsExt

CONSTANT Lag, Servers, Values
ASSUME Lag \in Nat /\ IsFiniteSet(Servers)

VARIABLE cLogs
vars == << cLogs >>

TypeOK ==
    /\ cLogs \in [Servers -> Seq(Values)]

Init ==
    /\ cLogs \in [Servers -> {<<>>}]

Copy(i) ==
    \E j \in Servers:
        /\ Len(cLogs[j]) > Len(cLogs[i])
        /\ \* Sync some prefix up to prefix = suffix of the unsynced suffix.
            LET L == (Len(cLogs[j]) - Len(cLogs[i]))
            \* Force to proportionally to the lag L copy more.
            \* Lag: 1 -> 0..L, 2 -> 1..L, 3 -> 2..L 
            IN \E l \in L - 1..L:
                cLogs' = [cLogs EXCEPT ![i] = @ \o SubSeq(cLogs[j], Len(@) + 1, Len(@) + l)]

Extend(i) ==
    /\ \A j \in Servers:
            Len(cLogs[j]) <= Len(cLogs[i])
    /\ \E s \in BoundedSeq(Values, Lag - Max({Len(cLogs[i]) - Len(cLogs[j]): j \in Servers})):
            cLogs' = [cLogs EXCEPT ![i] = @ \o s]

Next ==
    \E i \in Servers:
        \/ Copy(i)
        \/ Extend(i)

Spec ==
    /\ Init
    /\ [][Next]_vars
    /\ \A s \in Servers: WF_vars(Extend(s)) /\ WF_vars(Copy(s))

--------------------------------------------------------------------------------
\* Invariants

Abs(n) ==
    IF n < 0 THEN - n ELSE n

BoundedLag ==
    \A i, j \in Servers: Abs(Len(cLogs[i]) - Len(cLogs[j])) <= Lag

THEOREM Spec => []BoundedLag

--------------------------------------------------------------------------------
\* Liveness

AllExtending ==
    \A s \in Servers: []<> <<IsStrictPrefix(cLogs[s], cLogs'[s])>>_cLogs

THEOREM Spec => AllExtending

InSync ==
    \* TLC correctly verifies that InSync is not a property of the system because
    \* followers are permitted to copy only a prefix of the missing suffix.
    \A i, j \in Servers: []<>(cLogs[i] = cLogs[j])

================================================================================