Comment by deboflo

You can also use the model checker to, via brute force, find a sequence of states that result in a desired outcome (which is expressed as a set of conditions called an “invariant”). For example, steps to solve the tower of honoi or the Die Hard 3 jug problems.