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

--------------------------- MODULE AlternatingBit ---------------------------
EXTENDS Naturals, Sequences
CONSTANTS Data
VARIABLES msgQ, 
          ackQ, 
          sBit, 
          sAck, 
          rBit, 
          sent, 
          rcvd  
-----------------------------------------------------------------------------
ABInit == /\ msgQ = << >>
          /\ ackQ = << >>
          /\ sBit \in {0, 1}
          /\ sAck = sBit
          /\ rBit = sBit
          /\ sent \in Data
          /\ rcvd \in Data

ABTypeInv == /\ msgQ \in Seq({0,1} \X Data)
             /\ ackQ \in Seq({0,1})
             /\ sBit \in {0, 1}
             /\ sAck \in {0, 1}
             /\ rBit \in {0, 1}
             /\ sent \in Data
             /\ rcvd \in Data
-----------------------------------------------------------------------------
SndNewValue(d) == 
  /\ sAck = sBit
  /\ sent' = d
  /\ sBit' = 1 - sBit
  /\ msgQ' = Append(msgQ, <<sBit', d>>) 
  /\ UNCHANGED <<ackQ, sAck, rBit, rcvd>>

ReSndMsg == 
  /\ sAck # sBit
  /\ msgQ' = Append(msgQ, <<sBit, sent>>)
  /\ UNCHANGED <<ackQ, sBit, sAck, rBit, sent, rcvd>>

RcvMsg == 
  /\ msgQ # <<>>
  /\ msgQ' = Tail(msgQ)
  /\ rBit' = Head(msgQ)[1] 
  /\ rcvd' = Head(msgQ)[2] 
  /\ UNCHANGED <<ackQ, sBit, sAck, sent>>

SndAck == /\ ackQ' = Append(ackQ, rBit)
          /\ UNCHANGED <<msgQ, sBit, sAck, rBit, sent, rcvd>>

RcvAck == /\ ackQ # << >>
          /\ ackQ' = Tail(ackQ)
          /\ sAck' = Head(ackQ)
          /\ UNCHANGED <<msgQ, sBit, rBit, sent, rcvd>>

Lose(q) == 
   /\ q # << >>
   /\ \E i \in 1..Len(q) : 
          q' = [j \in 1..(Len(q)-1) |-> IF j < i THEN q[j] 
                                                 ELSE q[j+1] ]
   /\ UNCHANGED <<sBit, sAck, rBit, sent, rcvd>>

LoseMsg == Lose(msgQ) /\ UNCHANGED ackQ

LoseAck == Lose(ackQ) /\ UNCHANGED msgQ

ABNext == \/  \E d \in Data : SndNewValue(d) 
          \/  ReSndMsg \/ RcvMsg \/ SndAck \/ RcvAck 
          \/  LoseMsg \/ LoseAck 
-----------------------------------------------------------------------------
abvars == << msgQ, ackQ, sBit, sAck, rBit, sent, rcvd>>

ABFairness == /\ WF_abvars(ReSndMsg) /\ WF_abvars(SndAck)   
              /\ SF_abvars(RcvMsg) /\ SF_abvars(RcvAck) 
-----------------------------------------------------------------------------
ABSpec == ABInit /\ [][ABNext]_abvars /\ ABFairness
-----------------------------------------------------------------------------
THEOREM ABSpec => []ABTypeInv
=============================================================================