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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100

--------------------------- MODULE ReplicatedLog ----------------------------
EXTENDS Naturals, Sequences

CONSTANTS Node, Transaction

VARIABLES log, executed

vars == <<log, executed>>

TypeOK ==
  /\ log \in Seq(Transaction)
  /\ executed \in [Node -> Nat]

Convergence == []<>(\A n \in Node : executed[n] = Len(log))

Safety ==
    \A n \in Node : executed[n] <= Len(log)

Init ==
  /\ log = <<>>
  /\ executed = [n \in Node |-> 0]

WriteTx(n, tx) ==
  /\ executed[n] = Len(log)
  /\ log' = Append(log, tx)
  /\ executed' = [executed EXCEPT ![n] = @ + 1]

ExecuteTx(n) ==
  /\ executed[n] < Len(log)
  /\ executed' = [executed EXCEPT ![n] = @ + 1]
  /\ UNCHANGED log

\* Why does WriteTx also increment executed?
\* It increments executed[n] for one of the nodes n.
\* ExecuteTx catches up the other nodes.
\* With a single node, ExecuteTx is a no-op because
\* t is never enabled.

Next ==
  \/ \E n \in Node : \E tx \in Transaction: WriteTx(n, tx)
  \/ \E n \in Node : ExecuteTx(n)

Spec ==
  /\ Init
  /\ [][Next]_vars

THEOREM Spec => []Safety
THEOREM Spec => []TypeOK

ExecFairSpec ==
  /\ Spec
  /\ \A n \in Node : WF_vars(ExecuteTx(n))
  \* The following conjunct causes the spec to not be machine
  \* closed. This is orthogonal to the Finite Monotonic
  \* approach.
  /\ \A n \in Node : <>[][ExecuteTx(n)]_vars

WriteFairSpec ==
  /\ Spec
  /\ \A n \in Node : \A tx \in Transaction: WF_vars(WriteTx(n, tx))
  \* The following conjunct causes the spec to not be machine
  \* closed. This is orthogonal to the Finite Monotonic
  \* approach.
  /\ \A n \in Node : \A tx \in Transaction: <>[][WriteTx(n, tx)]_vars

\* ExecFairSpec and WriteFairSpec both work because every suffix with
\* infinitely many WriteTx implies Convergence to WriteTx's enablement
\* condition.  Likewise, every suffix with infinitely many ExecuteTx
\* implies Convergence.
THEOREM ExecFairSpec => Convergence
THEOREM WriteFairSpec => Convergence

-----------------------------------------------------------------------------

InsufficientlyFairSpecA ==
    /\ Spec
    /\ WF_vars(Next)

InsufficientlyFairSpecB ==
    /\ Spec
    /\ \A n \in Node : \A tx \in Transaction: WF_vars(WriteTx(n, tx))

InsufficientlyFairSpecC ==
    /\ Spec
    /\ \A n \in Node : \A tx \in Transaction : WF_vars(ExecuteTx(n))

-----------------------------------------------------------------------------

EffectivelyFalseSpecA ==
    /\ Spec
    /\ \A n \in Node : \A tx \in Transaction : WF_vars(ExecuteTx(n))
    /\ \A n \in Node : \A tx \in Transaction: <>[][WriteTx(n, tx)]_vars

EffectivelyFalseSpecB ==
    /\ Spec
    /\ \A n \in Node : \A tx \in Transaction: WF_vars(WriteTx(n, tx))
    /\ \A n \in Node : <>[][ExecuteTx(n)]_vars

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