Once a TNCES has been successfully loaded you can select either 'Maximal', 'Interleaving Max' or 'Interleaving' step semantics to be used in state space computations in the Configure submenu of the State space menu. Maximal step semantics is the default.
In maximal step semantics the maximal number or spontaneous transitions is selected in each step and the transitions forced by them.
In interleaving step semantics only one spontaneous transition is selected in each step and the transitions that are forced by it.
In interleaving max step semantics all possible sets of spontaneous enabled transitions are considered. Also all possible forced transitions are fired with them.