The hard part of learning to write TLA+ specs is learning to think abstractly about the system.

int i;
void main() {
	i = someNumber();
	i = i + 1;
}

We must describe:

• Possible initial values of variables.
• The relation between their values in the current state and their possible values in the next state.

Possible initial values of variables.

(i = 0) /\\ (pc = "start")

The relation between their values in the current state and their possible values in the next state. We’re not writing instructions for computing something. We’re writing a formula relating i, pc, i’, and pc’. It means: if pc = “start” the formula equals the then formula, otherwise it equals the else formula.

**if** current value of pc equals "start"
	**then** next value of i in {0, 1, ..., 1000}
			 next value of pc equals "middle"
**else if** current value of pc equals "middle"
				**then** next value of i equals current value of i + 1
						 next value of pc equals "done"
				**else** no next values

Initial-state formula: (i = 0) /\\ (pc = "start")

Next-state formula:
IF pc = "start"
	THEN (i' ∈ 0..1000) /\\
			 (pc' = "middle")
	ELSE IF pc = "middle"
				  THEN (i' = i + 1) /\\
							 (pc' = "done")
					ELSE FALSE

It’s important to remember that is a formula, not a sequence of commands.

\\/ /\\ pc = "start"
	 /\\ i' ∈ 0..1000
   /\\ pc' = "middle"
\\/ /\\ pc = "middle"
	 /\\ i' = i + 1
   /\\ pc' = "done"