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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/RingBuffer.tla
---
------------------------------ MODULE RingBuffer -------------------------------
(***************************************************************************)
(* Models a RingBuffer where each slot can contain an element from         *)
(* Values. Initially all slots contains NULL.                              *)
(*                                                                         *)
(* Read and write accesses to each slot are tracked to detect data races.  *)
(* This entails that each write and read of a slot has multiple steps.     *)
(*                                                                         *)
(* All models using the RingBuffer should assert the NoDataRaces invariant *)
(* that checks against data races between multiple producer threads and    *)
(* consumer threads.                                                       *)
(***************************************************************************)

LOCAL INSTANCE Naturals
LOCAL INSTANCE FiniteSets

CONSTANTS
    Size,    (* The number of slots in the RingBuffer.                *)
    Readers, (* The set of readers to the RingBuffer.                 *)
    Writers, (* The set of writers to the RingBuffer.                 *)
    Values,  (* The set of values storable in the RingBuffer's slots. *)
    NULL

ASSUME Size \in Nat \ {0}
ASSUME Writers /= {}
ASSUME Readers /= {}
ASSUME NULL \notin Values

VARIABLE ringbuffer

(* Last index in the RingBuffer. *)
LastIndex == Size - 1

(***************************************************************************)
(* Clients using the RingBuffer must ensure there are no data races.       *)
(* I.e. NoDataRaces must be an invariant in the spec using the Ringbuffer. *)
(***************************************************************************)
NoDataRaces ==
    \A i \in 0..LastIndex:
        /\ ringbuffer.readers[i] = {} \/ ringbuffer.writers[i] = {}
        /\ Cardinality(ringbuffer.writers[i]) <= 1
    
(* Initial state of RingBuffer. *)
Init ==
    ringbuffer = [
        slots |-> [i \in 0..LastIndex |-> NULL],
        readers |-> [i \in 0..LastIndex |-> {}],
        writers |-> [i \in 0..LastIndex |-> {}]
    ]

(* The index into the Ring Buffer for a sequence number.*)
IndexOf(sequence) ==
    sequence % Size

(***************************************************************************)
(* Write operations.                                                       *)
(***************************************************************************)

Write(index, writer, value) ==
    ringbuffer' = [
        ringbuffer EXCEPT
        !.writers[index] = @ \union {writer},
        !.slots[index] = value
    ]

EndWrite(index, writer) ==
    ringbuffer' = [ringbuffer EXCEPT !.writers[index] = @ \ {writer}]

(***************************************************************************)
(*  Read operations.                                                       *)
(***************************************************************************)

BeginRead(index, reader) ==
    ringbuffer' = [ringbuffer EXCEPT !.readers[index] = @ \union {reader}]

Read(index) ==
ringbuffer.slots[index]

EndRead(index, reader) ==
    ringbuffer' = [ringbuffer EXCEPT !.readers[index] = @ \ {reader}]

(***************************************************************************)
(* Invariants.                                                             *)
(***************************************************************************)

TypeOk ==
    ringbuffer \in [
        slots: UNION {[0..LastIndex -> Values \union {NULL}]},
        readers: UNION {[0..LastIndex -> SUBSET (Readers)]},
        writers: UNION {[0..LastIndex -> SUBSET (Writers)]}
    ]

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