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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/InnerSequential.tla
---
---------------------------- MODULE InnerSequential ----------------------------
EXTENDS RegisterInterface, Naturals, Sequences, FiniteSets
VARIABLE opQ, mem
--------------------------------------------------------------------------------
Done == CHOOSE v: v \notin Reg
--------------------------------------------------------------------------------
DataInvariant ==
    /\ RegFileTypeInvariant
    /\ opQ \in [Proc -> Seq([req: Request, reg: Reg \union {Done}])]
    /\ mem \in [Adr -> Val]
    /\ \A p \in Proc: \A r \in Reg:
        Cardinality({i \in DOMAIN opQ[p]: opQ[p][i].reg = r})
        = IF regFile[p][r].op = "Free" THEN 0 ELSE 1

Init ==
    /\ regFile \in [Proc -> [Reg -> FreeRegValue]]
    /\ opQ = [p \in Proc |-> <<>>]
    /\ mem \in [Adr -> Val]
--------------------------------------------------------------------------------
IssueRequest(proc, req, reg) ==
    /\ regFile[proc][reg].op = "Free"
    /\ regFile' = [regFile EXCEPT ![proc][reg] = req]
    /\ opQ' = [opQ EXCEPT ![proc] = Append(@, [req |-> req, reg |-> reg])]
    /\ UNCHANGED mem

RespondToRd(proc, reg) ==
    /\ regFile[proc][reg].op = "Rd"
    /\ \E val \in Val:
        /\ regFile' = [regFile EXCEPT ![proc][reg].val = val,
            ![proc][reg].op = "Free"]
        /\ opQ' = LET idx == CHOOSE i \in DOMAIN opQ[proc]:
                opQ[proc][i].reg = reg
            IN [opQ EXCEPT ![proc][idx].req.val = val,
            ![proc][idx].reg = Done]
    /\ UNCHANGED mem

RespondToWr(proc, reg) ==
    /\ regFile[proc][reg].op = "Wr"
    /\ regFile' = [regFile EXCEPT ![proc][reg].op = "Free"]
    /\ LET idx == CHOOSE i \in DOMAIN opQ[proc]: opQ[proc][i].reg = reg
        IN opQ' = [opQ EXCEPT ![proc][idx].reg = Done]
    /\ UNCHANGED mem

RemoveOp(proc) ==
    /\ opQ[proc] /= <<>>
    /\ Head(opQ[proc]).reg = Done
    /\ mem' = IF Head(opQ[proc]).req.op = "Rd"
        THEN mem
        ELSE [mem EXCEPT ![Head(opQ[proc]).req.adr] =
            Head(opQ[proc]).req.val]
    /\ opQ' = [opQ EXCEPT ![proc] = Tail(@)]
    /\ UNCHANGED regFile

Internal(proc) ==
    /\ RemoveOp(proc)
    /\ (Head(opQ[proc]).req.op = "Rd") =>
        (mem[Head(opQ[proc]).req.adr] = Head(opQ[proc]).req.val)

Next == \E proc \in Proc:
    \/ \E reg \in Reg:
        \/ \E req \in Request: IssueRequest(proc, req, reg)
        \/ RespondToRd(proc, reg)
        \/ RespondToWr(proc, reg)
    \/ Internal(proc)
--------------------------------------------------------------------------------
Spec ==
    /\ Init
    /\ [][Next]_<< regFile, opQ, mem >>
    /\ \A proc \in Proc, reg \in Reg:
        WF_<< regFile, opQ, mem >> (RespondToRd(proc, reg)
            \/ RespondToWr(proc, reg))
    /\ \A proc \in Proc: WF_<< regFile, opQ, mem >> (RemoveOp(proc))

--------------------------------------------------------------------------------
THEOREM Spec => []DataInvariant
================================================================================