* You define initial states and all possible state transitions.

* It will brute force all states.

* You can add a variety of assertions.