scheduler: TLA+ spec of the system scheduler

[pkazmierczak]

This PR is an experiment in using TLA+ to model a high-level specification of the system scheduler. For now, we focus on modeling transitions in the state machine and provide a very basic temporal formula:

$$\text{SystemCoverage} \;\triangleq\; \Diamond\left( \forall j \in \text{currentJobs}:\; \forall c \in \text{eligibleNodes}:\; Eligible(j,c) \;\Rightarrow\; allocs[j][c] = 1 \right)$$

which means that for every job, every node will eventually have exactly one alloc. We provide some other basic safety properties like making sure nodes don't exceed capacity.