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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/RTMemory.tla
---
------------------------------- 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
================================================================================