---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/MC.tla
---
---------------------------------- MODULE MC -----------------------------------
EXTENDS Hanoi, TLC
\* CONSTANT definitions @modelParameterConstants:0D
const_146427254081039000 ==
5
--------------------------------------------------------------------------------
\* CONSTANT definitions @modelParameterConstants:1N
const_146427254082040000 ==
3
--------------------------------------------------------------------------------
\* SPECIFICATION definition @modelBehaviorSpec:0
spec_146427254083041000 ==
Spec
--------------------------------------------------------------------------------
================================================================================
\* Modification History
\* Created Thu May 26 16:22:20 CEST 2016 by markus