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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/MCInnerSequential.tla
---
--------------------------- MODULE MCInnerSequential ---------------------------
EXTENDS InnerSequential

CONSTANT MaxQLen
Constraint == \A p \in Proc: Len(opQ[p]) <= MaxQLen

AlwaysResponds ==
    (*************************************************************************)
  (* A simple liveness property, implied by the fact that every request    *)
  (* eventually generates a response.                                      *)
  (*************************************************************************)
    \A p \in Proc, r \in Reg:
        (regFile[p][r].op /= "Free") ~> (regFile[p][r].op = "Free")
================================================================================