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

------------------------ 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 \cup {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
=============================================================================