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

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