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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/MCDistributedReplicatedLog.tla
---
---------------------- MODULE MCDistributedReplicatedLog -----------------------
EXTENDS DistributedReplicatedLog, FiniteSetsExt

ASSUME
    \* LongestCommonPrefix in View for a single server would always shorten the
    \* log to <<>>, reducing the state-space to a single state.
    Cardinality(Servers) > 1

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

\* Combining the following conditions makes the state space finite:
\* 1) The divergence of any two logs is bounded (See Extend action)
\*
\* 2) Terms is a *finite* set.
ASSUME IsFiniteSet(Values)
\*
\* 3) The longest common prefix of all logs is discarded.
DropCommonPrefix ==
    LET commonPrefixBound == Len(LongestCommonPrefix(Range(cLogs)))
        Drop(seq, idx) == SubSeq(seq, idx + 1, Len(seq))
    IN [s \in Servers |-> Drop(cLogs[s], commonPrefixBound)]

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