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


------------------------- 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 \leq  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)
=============================================================================