Model version: {{META.model_version}} Generator version: {{META.version}} Generation timestemp: {{META.timestamp}} ------------------------------ MODULE model ------------------------------ EXTENDS TLC, FiniteSets, Sequences, Naturals