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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/RealTimeHourClock.tla
---
--------------------------- MODULE RealTimeHourClock ---------------------------
EXTENDS Reals, HourClock
VARIABLE now
CONSTANT Rho
ASSUME (Rho \in Real) /\  (Rho > 0)
--------------------------------------------------------------------------------

--------------------------------- MODULE Inner ---------------------------------
VARIABLE t
TNext == t' = IF HCnxt THEN 0 ELSE t + (now' - now)
Timer == (t = 0) /\ [][TNext]_<< t, hr, now >>
MaxTime == [](t <= 3600 + Rho)
MinTime == [][HCnxt => t \geq 3600 - Rho]_hr
HCTime == Timer /\ MaxTime /\ MinTime
================================================================================

I(t) == INSTANCE Inner

NowNext ==
    /\ now' \in {r \in Real: r > now}
    /\ UNCHANGED hr

RTnow ==
    /\ now \in Real
    /\ [][NowNext]_now
    /\ \A r \in Real: WF_now(NowNext /\ (now' > r))

RTHC == HC /\ RTnow /\ ( \EE t : I(t)!HCTime )
================================================================================