---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/RegisterInterface.tla
---
--------------------------- MODULE RegisterInterface ---------------------------
CONSTANT Adr, Val, Proc, Reg
VARIABLE regFile
--------------------------------------------------------------------------------
RdRequest == [adr: Adr, val: Val, op: {"Rd"}]
WrRequest == [adr: Adr, val: Val, op: {"Wr"}]
FreeRegValue == [adr: Adr, val: Val, op: {"Free"}]
Request == RdRequest \union WrRequest
RegValue == Request \union FreeRegValue
RegFileTypeInvariant == regFile \in [Proc -> [Reg -> RegValue]]
================================================================================