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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/JointActionMemory.tla
---
--------------------------- MODULE JointActionMemory ---------------------------
EXTENDS MemoryInterface

----------------------- MODULE InnerEnvironmentComponent -----------------------
VARIABLE rdy
IE == rdy = [p \in Proc |-> TRUE]

Erqst(p) ==
    /\ rdy[p]
    /\ \E req \in MReq: Send(p, req, memInt, memInt')
    /\ rdy' = [rdy EXCEPT ![p] = FALSE]

ERsp(p) ==
    /\ \E rsp \in Val \union {NoVal}:
        Reply(p, rsp, memInt, memInt')
    /\ rdy' = [rdy EXCEPT ![p] = TRUE]

NE == \E p \in Proc: Erqst(p) \/ ERsp(p)

IESpec == IE /\ [][NE]_<< memInt, rdy >>
================================================================================

------------------------- MODULE InnerMemoryComponent --------------------------
EXTENDS InternalMemory
MRqst(p) ==
    /\ \E req \in MReq:
        /\ Send(p, req, memInt, memInt')
        /\ buf' = [buf EXCEPT ![p] = req]
        /\ ctl' = [ctl EXCEPT ![p] = "busy"]
    /\ UNCHANGED mem

NM == \E p \in Proc: MRqst(p) \/ Do(p) \/ Rsp(p)

IMSpec == IInit /\ [][NM]_<< memInt, mem, ctl, buf >>
================================================================================

IEnv(rdy) == INSTANCE InnerEnvironmentComponent

IMem(mem, ctl, buf) == INSTANCE InnerMemoryComponent

Spec ==
    /\ \EE rdy : IEnv(rdy)!IESpec
    /\ \EE mem, ctl, buf : IMem(mem,ctl,buf)!IMSpec
================================================================================