Finite vs. infinite state space

Okay, the first "real" post. So what is a finite state space model?
Any model that you can explore completely is by definition finite. That means you can try out every single combination in finite time (although in some cases this can be a very long time).

Opposite, an infinite model is one where the number of inputs grow infinite.

Theoretically we cannot have infinite models in a computer, because the state space will be determined by the variables in the model which all have finite ranges - but say you combine two 32bit integers, the state space explodes to 18446744073709551616 states - which is practically infinite.

In general model exploration is bound by number of states and steps, and as such we don't know if a model is infinite if it has more states than the state bound. A classic example of a (practically) infinite model would be a counter with internal state variable int x = 0, and the action Increment() { x++; }. This model will generate a state for every value x >= 0. Exploring the model gives the following result:

So basically what this means is that anytime you have numbers in your model that can take arbitraty values you have infinite state space. Bummer. Okay, but there are of course ways to work with this. Enter: Equivalence Class Partitioning - ECP is all about determining which values you consider to be different. A great example is the addition function of your calculator - say add(x,y), consider testing that: add(2,2) = 4 if this holds true, would you expect add(2,3) <> 5? Of course not, if addition works for 2 it should work for 3 as well. Thus we consider y > 0 equivalent. Likewise y < 0 should be equivalent and y = 0 is a boundary case. (really, for all practical purposes we would assume y completely equivalent).

We can apply ECP the same way to our model state variables. Instead of modeling the counter fully we could assume that x > 0 is equivalent, thus we adjust the model slightly to be Increment() { if(x < 1) x++; }. Notice that the increment action is valid from any state, but calling Increment with x = 1 does not change the internal state representation. The model is now limited to two states, x = 0 and x = 1. It is also finite under our equivalence assumption. Model exploration gives:

Closing exercise: Extend the counter model to support negative numbers using a Decrement() action and apply ECP to make the state space finite.

[1] Counter models