---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/MCConsensus.tla
---
------------------------------ MODULE MCConsensus ------------------------------
EXTENDS Consensus, TLC
\* MV CONSTANT declarations@modelParameterConstants
CONSTANTS
a, b, c
--------------------------------------------------------------------------------
\* MV CONSTANT definitions Value
const_156017750645611000 ==
{a, b, c}
--------------------------------------------------------------------------------
================================================================================
\* Modification History
\* Created Mon Jun 10 07:38:26 PDT 2019 by lamport