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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/ZSequences.tla
---
------------------------------ MODULE ZSequences -------------------------------
(***************************************************************************)
(* Defines operators on finite zero-indexed sequences, where a sequence of *)
(* length n is represented as a function whose domain is the set 0..(n-1)  *)
(* (the set {0, 1, ... , n-1}).                                            *)
(***************************************************************************)

LOCAL INSTANCE FiniteSets
LOCAL INSTANCE Naturals
LOCAL INSTANCE Sequences

\* The empty zero-indexed sequence
EmptyZSeq == <<>>

\* The set of valid indices for zero-indexed sequence s
ZIndices(s) ==
    IF s = EmptyZSeq
    THEN {}
    ELSE DOMAIN s

\* The set of all zero-indexed sequences of elements in S with length n
LOCAL ZSeqOfLength(S, n) ==
    IF n = 0
    THEN {EmptyZSeq}
    ELSE [0..(n - 1) -> S]

\* The set of all zero-indexed sequences of elements in S
ZSeq(S) == UNION {ZSeqOfLength(S, n): n \in Nat}

\* The length of zero-indexed sequence s
ZLen(s) ==
    IF s = EmptyZSeq
    THEN 0
    ELSE Cardinality(DOMAIN s)

\* Converts from a one-indexed sequence to a zero-indexed sequence
ZSeqFromSeq(seq) ==
    IF seq = <<>>
    THEN EmptyZSeq
    ELSE [i \in 0..(Len(seq) - 1) |-> seq[i + 1]]

\* Converts from a zero-indexed sequence to a one-indexed sequence
SeqFromZSeq(zseq) ==
    IF zseq = EmptyZSeq
    THEN <<>>
    ELSE [i \in 1..ZLen(zseq) |-> zseq[i - 1]]

\* Lexicographic order on zero-indexed sequences a and b
a \preceq b ==
    LET
        s1len == ZLen(a)
        s2len == ZLen(b)
    RECURSIVE IsLexLeq(_, _, _)
        IsLexLeq(s1, s2, i) ==
            CASE i = s1len \/ i = s2len -> s1len <= s2len
                [] s1[i] < s2[i] -> TRUE
                [] s1[i] > s2[i] -> FALSE
                [] OTHER -> IsLexLeq(s1, s2, i + 1)
    IN IsLexLeq(a, b, 0)

\* Rotate the string s to the left by r indices
Rotation(s, r) ==
    IF s = EmptyZSeq
    THEN EmptyZSeq
    ELSE [i \in ZIndices(s) |-> s[(i + r) % ZLen(s)]]

\* The set of all rotations of zero-indexed sequence s
Rotations(s) ==
    IF s = EmptyZSeq
    THEN {}
    ELSE {[
                shift |-> r,
                seq |-> Rotation(s, r)
            ]: r \in ZIndices(s)
        }

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