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

--------------------- MODULE RTMemory ----------------------
EXTENDS MemoryInterface, RealTime_SS
CONSTANT Rho
ASSUME (Rho \in Real) /\ (Rho > 0)
 
   ---------------- MODULE Inner ----------------------------------
   EXTENDS InternalMemory
   Respond(p) == (ctl[p] # "rdy") /\ (ctl'[p] = "rdy")
   RTISpec == /\ ISpec
              /\ \A p \in Proc : RTBound(Respond(p), ctl, 0, Rho)
              /\ RTnow(<<memInt, mem, ctl, buf>>)
   ==========================================================

Inner1(mem, ctl, buf) == INSTANCE Inner
RTSpec == \EE mem, ctl, buf : Inner1(mem, ctl, buf)!RTISpec
=============================================================