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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/Sequences.tla
---
------------------------------- MODULE Sequences -------------------------------
(***************************************************************************)
(* Defines operators on finite sequences, where a sequence of length n is  *)
(* represented as a function whose domain is the set 1..n (the set         *)
(* {1, 2, ... , n}).  This is also how TLA+ defines an n-tuple, so         *)
(* tuples are sequences.                                                   *)
(***************************************************************************)

LOCAL INSTANCE Naturals
(*************************************************************************)
  (* Imports the definitions from Naturals, but don't export them.         *)
  (*************************************************************************)

Seq(S) == UNION {[1..n -> S]: n \in Nat}
(*************************************************************************)
  (* The set of all sequences of elements in S.                            *)
  (*************************************************************************)

Len(s) == CHOOSE n \in Nat: DOMAIN s = 1..n
(*************************************************************************)
  (* The length of sequence s.                                             *)
  (*************************************************************************)

s \o t == [i \in 1..(Len(s) + Len(t)) |-> IF i <= Len(s) THEN s[i]
    ELSE t[i - Len(s)]]
(*************************************************************************)
  (* The sequence obtained by concatenating sequences s and t.             *)
  (*************************************************************************)

Append(s, e) == s \o << e >>
(**************************************************************************)
  (* The sequence obtained by appending element e to the end of sequence s. *)
  (**************************************************************************)

Head(s) == s[1]
Tail(s) == [i \in 1..(Len(s) - 1) |-> s[i + 1]]
(*************************************************************************)
  (* The usual head (first) and tail (rest) operators.                     *)
  (*************************************************************************)

SubSeq(s, m, n) == [i \in 1..(1 + n - m) |-> s[i + m - 1]]
(*************************************************************************)
  (* The sequence <<s[m], s[m+1], ... , s[n]>>.                            *)
  (*************************************************************************)

SelectSeq(s, Test(_) ) ==
    (*************************************************************************)
  (* The subsequence of s consisting of all elements s[i] such that        *)
  (* Test(s[i]) is true.                                                   *)
  (*************************************************************************)
    LET F[i \in 0..Len(s)] ==
    (*******************************************************************)
        (* F[i] equals SelectSeq(SubSeq(s, 1, i), Test]                    *)
        (*******************************************************************)
        IF i = 0 THEN <<>>
        ELSE IF Test(s[i]) THEN Append(F[i - 1], s[i])
            ELSE F[i - 1]
    IN F[Len(s)]
================================================================================