1 2 3 4 5 6
SPECIFICATION Spec CONSTANT defaultInitValue = defaultInitValue \* Add statements after this line. PROPERTIES eventually_equal