Apalache type annotations for DiningPhilosophers.tla, applied via INSTANCE so the original spec remains free of tool-specific idiosyncrasies.