---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/SerialMemory.tla
---
----------------------------- MODULE SerialMemory ------------------------------
EXTENDS RegisterInterface
Inner(InitMem, opQ, opOrder) == INSTANCE InnerSerial
Spec == \E InitMem \in [Adr -> Val]:
\EE opQ, opOrder : Inner(InitMem, opQ, opOrder)!Spec
================================================================================