Why is the invariant of the following state machine (2 mod 5) OR (3 mod 5)? Consider a state machine with tuple of numbers describing its state, i.e. $(i,j)$ such that $i \geq 0$ and $j \geq 0$.
The initial state is $q_0 =(i,j) = (15, 12)$
There are only two transitions allowed:
$(i,j) \to (i-3, j+2)$
and 
$(i,j) \to (j,i)$
I was told that the invariant of this state machine is the following predicate:
$P(k)$ = " for state step k, the difference between i and j is $i -j = 5k+2$ or $i-j = 5k+3$".
I was able to verify that this is indeed true by induction, however, without knowing the answer beforehand (i.e. $i -j = 5k+2$ or $i-j = 5k+3$) I would have not been able to realize this on my own. How do you realize that this invariant holds without just knowing the answer? What are some ways people found this out? Is there a trick for realizing that the reminder of the difference mod 5 is always 2 or 3? If the starting state would have been different, would it have been a different invariant? Is there a way of finding out the invariant without making it feel it came out of thin air? How did people figure out the pattern?
 A: I came across this same problem — aka "The Temple of Forever" — in the MIT 6.042j OCW course in the recitations. Following the notes really gave me no explanation on how they arrived the $5k + 2$ and $5k + 3$ invariants, so after a little searching, I found some help.
First, in ch. 4.1, pg. 85 of the Lehman, Leighton, Meyer book, there is a useful method for visualizing each state in a state machine.



After writing out each state in this way, for the "exchange" transition e.g.


*

*$(r,g) \to (r-3, g+2)$, $k=1$

*$\to (r-6, g+4)$, $k=2$

*$\to (r-9, g+6)$, $k=3$


Aha! There's a clear pattern emerging, where the difference of $r-g$ was some multiple of 5 times the step number, i.e. $5k$. That at least got me going, but because I'm still trying to grasp all these concepts, it still wasn't totally clear to me.
A little more searching revealed some earlier course notes by Lehman with a more thorough explanation for how they arrived at the $5k + 2$ and $5k + 3$ invariants.



It would be great if there was more explanation available for these kinds of problems, but I guess that's what you get for a free MIT course. Hope that's helpful for getting you on the right track for finding those tricky invariants.
A: Well, that is a good question. I am afraid there is no easy answer. 
In this particular case, the transitions are extremely simple. For example, there are no squares or cubes. You might notice for example that $i+j$ goes down by 1 each time that the first transition happens and remains the same if the second transition happens. 
Given simple transitions, any invariant has to be simple. The simplest of all is that something like $i+j$ is always the same. We have just seen that is unlikely to work here, because $i+j$ sometimes goes down and sometimes doesn't. At that point looking for something simple that remains fixed modulo something is a good bet. Why? Well, there are not many other simple things left to try.
From that point on, things are simpler. We are obviously looking for a linear relationship. So something like $ai+bj=c\mod k$ for fixed $a,b,c,k$. The first thing to try is obviously $a=b=1$, but that won't work because there would be no change for the second type and -1 for the first. There is no way of making that work. 
After trying a few more things that fail to work. You pause for thought. If you repeatedly get transition 2, then the best you can hope for with a linear thing like $ai+bj$ is for it to toggle backwards and forwards. So you want $a=-b$, and you need to accept two values of $k$.
After that breakthrough, you are on the home straight.
All that sounds totally messy. It is. But that is problem solving. The old adage is that no preparation is "necessary or sufficient". You constantly think to yourself can I think of any similar or simpler case that I already know, or might be able to handle? Equally important, you have to be energetic and try lots of things.
You also have to be energetic about constantly learning new things. Most results are proved by adaptations of existing proofs, not by totally new insights.
