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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/RealTime_SS.tla
---
------------------------------ MODULE RealTime_SS ------------------------------
EXTENDS Reals
VARIABLE now

RTBound(A, v, D, E) ==
    LET TNext(t) == t' = IF <<A>>_v \/ ~(ENABLED <<A>>_v) '
    THEN 0
    ELSE t + (now' - now)

        Timer(t) == (t = 0) /\ [][TNext(t)]_<< t, v, now >>

        MaxTime(t) == [](t <= E)

        MinTime(t) == [][A => t \geq D]_v
    IN \EE t : Timer(t) /\ MaxTime(t) /\ MinTime(t)
--------------------------------------------------------------------------------
RTnow(v) == LET NowNext ==
        /\ now' \in {r \in Real: r > now}
        /\ UNCHANGED v
    IN
    /\ now \in Real
    /\ [][NowNext]_now
    /\ \A r \in Real: WF_now(NowNext /\ (now' > r))
================================================================================