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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/Util.tla
---
--------------------------------- MODULE Util ----------------------------------
EXTENDS Sequences, Functions, Naturals, TLC
\* Simple utility functions
intersects(a, b) == a \intersect b /= {}
max(s) == CHOOSE i \in s: (~\E j \in s: j > i)
min(s) == CHOOSE i \in s: (~\E j \in s: j < i)

ReduceSet( op(_, _) , set, base) ==
    LET iter[s \in SUBSET set] ==
        IF s = {} THEN base
        ELSE LET x == CHOOSE x \in s: TRUE
            IN op(x, iter[s \ {x}])
    IN iter[set]

ReduceSeq( op(_, _) , seq, acc) == FoldFunction(op, acc, seq)

Index(seq, e) == CHOOSE i \in 1..Len(seq): seq[i] = e

SeqToSet(s) == {s[i]: i \in DOMAIN s}
Last(seq) == seq[Len(seq)]
IsEmpty(seq) == Len(seq) = 0
\* Remove all occurrences of `elem` from `seq`
Remove(seq, elem) == SelectSeq(seq, LAMBDA e: e /= elem )

\* Dual to UNION on intersect
INTERSECTION(setOfSets) == ReduceSet(\intersect, setOfSets, UNION setOfSets)

\* Borrowed from Stephan Merz. TLA+ Case Study: A Resource Allocator. [Intern report] A04-R-101 || merz04a, 2004, 20 p. ffinria-00107809f
(* The set of permutations of a finite set, represented as sequences.  *)
PermSeqs(S) ==
    LET perms[ss \in SUBSET S] ==
        IF ss = {} THEN {<<>>}
        ELSE LET ps == [x \in ss |->
                {Append(sq, x): sq \in perms[ss \ {x}]}]
            IN UNION {ps[x]: x \in ss}
    IN perms[S]

\* Helper to write "unit test" ASSUMES which print when false
test(lhs, rhs) == lhs /= rhs => Print(<< lhs, " IS NOT ", rhs >>, FALSE)

================================================================================
\* Modification History
\* Last modified Sun Aug 05 16:44:44 ET 2023 by murat
\* Created Tue Apr 28 16:43:24 CEST 2020 by tim