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

--------------------------- MODULE ChannelRefinement ------------------------
EXTENDS Naturals, Sequences
VARIABLES h, l

ErrorVal ==  CHOOSE v : v \notin [val : 1..12, rdy : {0, 1}, ack : {0, 1}]

BitSeqToNat[s \in Seq({0,1})] ==
   IF  s = << >>  THEN  0  ELSE  Head(s) + 2 * BitSeqToNat[Tail(s)]

H == INSTANCE Channel WITH chan <- h, Data <- 1..12
L == INSTANCE Channel WITH chan <- l, Data <- {0,1}
  ---------------------------- MODULE Inner ---------------------------------
  VARIABLE bitsSent

  Init == /\ bitsSent = << >>
          /\ IF L!Init THEN H!Init
                       ELSE h = ErrorVal 

  SendBit == \E b \in {0, 1}: 
                /\ L!Send(b) 
                /\ IF Len(bitsSent) < 3
                     THEN /\ bitsSent' = <<b>> \o bitsSent
                          /\ UNCHANGED h 
                     ELSE /\ bitsSent'= <<>>
                          /\ H!Send(BitSeqToNat[<<b>> \o bitsSent])

  RcvBit == /\ L!Rcv 
            /\ IF bitsSent = << >> THEN H!Rcv  
                                   ELSE UNCHANGED h 
            /\ UNCHANGED bitsSent

  Error == /\ l' # l
           /\ ~((\E b \in {0,1} : L!Send(b)) \/ L!Rcv) 
           /\ h' = ErrorVal

  Next == SendBit \/ RcvBit \/ Error 

  InnerIR == Init /\ [][Next]_<<l,h,bitsSent>>
  ===========================================================================
I(bitsSent) == INSTANCE Inner 
IR == \EE bitsSent : I(bitsSent)!InnerIR
=============================================================================