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

--------------------------- MODULE BinaryHourClock --------------------------
EXTENDS Naturals

VARIABLE bits 

H(hr) == INSTANCE HourClock 

BitArrayVal(b) == 
    LET n  ==  CHOOSE i \in Nat : DOMAIN b = 0..i

        val[i \in 0..n]  == 
            IF  i=0  THEN  b[0] * 2^0  ELSE  (b[i] * 2^i) + val[i-1]
    IN val[n] 

HourVal(b) == IF b \in[(0.. 3) -> {0,1}] THEN BitArrayVal(b) 
                                         ELSE 99 
 
IR(b, h) == [](h = HourVal(b))

BHC  ==  \EE hr : IR(bits, hr) /\ H(hr)!HC
=============================================================================