The commands to search for valid initial state or valid state satisfying the invariant both present the same dialog with the same text. For the invariant related command this should not be called an initial state, but "State satisfying the invariant...".
The commands to search for valid initial state or valid state satisfying the invariant both present the same dialog with the same text. For the invariant related command this should not be called an initial state, but "State satisfying the invariant...".