Configuring state space creation

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.

Configuring state space creation

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.