Model version: {{META.model_version}}
Generator version: {{META.version}}
Generation timestemp: {{META.timestamp}}


------------------------------ MODULE model ------------------------------

EXTENDS TLC, FiniteSets, Sequences, Naturals