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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/TokenRing.tla
---
------------------------------- MODULE TokenRing -------------------------------
(***********************************************************************************)
(* Dijkstra's classical stabilizing token ring algorithm: EWD426                   *)
(* https://muratbuffalo.blogspot.com/2015/01/dijkstras-stabilizing-token-ring.html *)
(***********************************************************************************)
EXTENDS Naturals, FiniteSets

CONSTANTS N, M
ASSUME NAssumption == N \in Nat \ {0} \* At least one node
ASSUME MAssumption == M \in Nat \ {0} \* Value domain of c 

ASSUME NMAssumption == N <= M + 1

Node == 0..N - 1

VARIABLES
    c \* counter at each node, token is defined as function of c's in nbring nodes

vars == << c >>

TypeOK ==
    /\ c \in [Node -> 0..M - 1]
--------------------------------------------------------------------------------

Init ==
    /\ c \in [Node -> 0..M - 1]

CreateToken ==
    (* Node 0 executes this action to inject new value into system *)
    /\ c[0] = c[N - 1]
    /\ c' = [c EXCEPT ![0] = (c[N - 1] + 1) % M]

PassToken(i) ==
    (* Other nodes just copy value of the predecessor *)
    /\ i /= 0
    /\ c[i] /= c[i - 1]
    /\ c' = [c EXCEPT ![i] = c[i - 1]]

--------------------------------------------------------------------------------
Next ==
    \/ CreateToken
    \/ \E i \in Node \ {0}: PassToken(i)

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

--------------------------------------------------------------------------------
UniqueToken ==
    \E i \in 0..N:                                  \* unique token at i (or i=N => token is at 0)
        /\ \A j \in 0..i - 1: c[j] = c[0]           \* before i all c equals c[0] 
        /\ \A j \in i..N - 1: c[j] = (c[0] - 1) % M \* after i all c following c[0]
    
(* Stabilization property *)
Stab == <>[]UniqueToken

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

Alias ==
    [
        counter |-> c,
        unique |-> UniqueToken
    ]

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