Now suppose that we would like to verify the correct transmission of a very large array of bytes, or even an array of unknown size. SMV provides a way to do this by reducing a type with a large or unknown number of values to an abstract type, with a small fixed number of values. This type has one additional abstract value to represent all the remaining values in the original type.
For example, when verifying the correct transmission of byte i, we might reduce the index type to just two values - i and a value representing all numbers not equal to i, (which SMV denotes NaN). This is an abstraction, since NaN, when compared for equality against itself, produces an undetermined value. In fact, here is a truth table of the equality operator for the reduced type:
The program with the reduced index data type is an abstraction of the original program, such that any property that is true of the abstract program is true of the original (though the converse is not true).