array set ns {nop,nop nop nop,inc 1 1,inc 2 1,nop 1 2,inc inf 2,nop inf inf,inc inf inf,nop inf} set state nopWe see that we have two inputs to the next_state function, one is a number, or no_operation (sort of like an unactive state) or inf_inite, which is much sooner than need be, for obvious reason. The other is like a basic command: nop (no operation), or inc_crement, which works always except in infinity.The domains of the two variables are chosen independently, which makes it easier to make in principle any combination of command and previous state legal.The next state is of course obtained by:

set state $ns($state,$input)Where input can be set as 'nop' 'inc', as example:

set state nop set state $ns($state,nop) nop set state $ns($state,inc) 1 set state $ns($state,nop) 1 set state $ns($state,inc) 2 set state $ns($state,nop) 2 set state $ns($state,inc) inf set state $ns($state,nop) inf set state $ns($state,inc) infBecause we enumerate all possible state,input combinations a larger set of state transitions become easily unmanageable, though of course it would be easy to define them for a larger set of natural numbers in this way, even automatically.As from common enough mathematical notation, we'd have

#states x #inputstotal state transition possibilities, unless we limit the domains of the two variables in combinations somehow, for instance we could limit the domain for the 'nop' input to the initial state nop and the final state inf, and easily extend the domain of the state variable to {nop,1,2,inf} to {nop,1,2,...,n,inf}, where n is an element of the set of natural numbers.Lets add another operation to the state machine, and see what happens to these kind of considerations, and what we could do to make the machine tick perfectly, while keeping the number of states we need to explicitly mention limited preferably while maintaining mathematical correct definitions, and preferably inductive proof methods possible.When we want to, we can take the sets of all possible states and all possible inputs, and generate a list of all possible combinations:

foreach state {nop 1 2 inf} {foreach input {nop inc} {puts "$state,$input "}} nop,nop nop,inc 1,nop 1,inc 2,nop 2,inc inf,nop inf,incAdding a 'dec' to the domain of the input and a few more numerical elements to the state domain, we can have:

foreach state {nop 1 2 3 4 inf} {foreach input {nop inc dec} {puts " $state,$input "}} nop,nop nop,inc nop,dec 1,nop 1,inc 1,dec 2,nop 2,inc 2,dec 3,nop 3,inc 3,dec 4,nop 4,inc 4,dec inf,nop inf,inc inf,decOf course other transition possibilities could make certain combinations of elements from the domain of states and inputs unpermitted, so we can limit the number of state transitions we need to list:

foreach state {nop 1 2 inf} {foreach input {nop inc reset tilt} {puts " $state,$input --> "}} nop,nop --> nop nop,inc --> 1 nop,reset --> nop nop,tilt --> inf 1,nop --> 1 1,inc --> 2 1,reset --> nop 1,tilt --> inf 2,nop --> 2 2,inc --> inf 2,reset --> nop 2,tilt --> inf inf,nop --> inf inf,inc --> inf inf,reset --> nop inf,tilt --> infI added the desired new states in the table which was generated above, clearly, tilt always leaves us with and infinity state, while reset always puts us back at nop, which is sort of idle and zero and empty all at the same time.Of course we could define the extension pretty easily by stating or sort of overriding for the reset and tilt input cases that they always generate a next state of nop and tilt, respectively:

for all states: nextstate(state,reset) = nop nextstate(state,tilt) = infWhich reduces the tablesize we need to deal with back to what we started with.The idea of incrementing and decrementing is natural of course, and we could say of course:

state transition for input=inc: state/{inf} |-> state/{nop} where nextstate(state) = [expr $state +1] state transition for input=dec: state/{nop,inf} |-> state/{nop} where nextstate(state) = [expr $state -1]Of course things are easy, and would take a simple formula +1 or -1 mostly, but the operators aren't symmetrical, and we need to take into acount we cannot increment infinity by formula, and cannot define dec inf at all and dec 1 into the domain (woud be nop) easily or into the bottom of a natural number domain at all (there would always be a lower one).

As a bit of a fun unpractical example I do state of dutch politics machine page.