scalarset BIT 0..7; scalarset INDEX 0..31; typedef BYTE array BIT of boolean; module main(){ /* the abstract model */ bytes : array INDEX of BYTE; next(bytes) := bytes; /* the input and output signals */ inp, out : struct{ valid : boolean; idx : INDEX; data : BYTE; } /* the refinement maps */ layer spec: { if(inp.valid) inp.data := bytes[inp.idx]; if(out.valid) out.data := bytes[out.idx]; }

And let's use our original very trivial implementation:

init(out.valid) := 0; next(out) := inp; }That is, the output is just the input delayed by one time unit.

As before, let's break the specification up into cases, one for each index value:

forall (i in INDEX) subcase spec_case[i] of out.data//spec for out.idx = i;

If you run this example,
and look in the cone pane, you'll
see that there are five state variables in the cone for both `inp.idx`
and `out.idx`. This is expected, since five bits are needed to encode
32 values. However, notice that for case `i`, if the index value at the
output is not equal to `i`, we don't care what the output is. Our property
`spec_case[i]` only specifies the output at those times when `out.idx = i`.
We can therefore group all of the index values not equal to `i` into a class,
represented by a single abstract value (`NaN`), and expect that the specification
might still be true. To do this, add the following declaration:

forall (i in INDEX) using INDEX->{i} prove out.data//spec_case[i];

This tells SMV to reduce the data type `INDEX` to an abstract type
consisting of just the value `i` and `NaN` (note, we don't
specify `NaN` explicitly). Now,
open the new version, and
observe the cone. You'll notice the state variables `inp.idx` and `out.idx`
now require only one boolean variable each to encode them, since their type has been reduced
to two values. Now try verifying the property `out.data//spec_case[0]`. The result
is true, since the values we reduced to the abstract value don't actually matter for
the particular case of the specification we are verifying.

Now, let's suppose that we don't know in advance what the size of the array of bytes will be. Using data type reductions, we can prove the correctness of our implementation for any size array (including an infinite array). To do this, change the declaration

scalarset INDEX 0..31;

to the following:

scalarset INDEX undefined;

This tells SMV that `INDEX` is a symmetric type, but doesn't say exactly
what the values in the type are. In such a case, SMV *must* have a data
type reduction for `INDEX` to prove any properties, because it can only
verify properties of finite state systems. Now run the new version. You'll notice that the result is exactly the same as in the previous
case. One boolean variable is used to encode values of type `INDEX`, and
the specification is found to be true. In fact, in the previous case, SMV didn't
in any way use the fact that type `INDEX` was declared to have the specific
range `0..31`. Thus it's not surprising that when we remove this information
the result is the same. By using finite state verification techniques, we have
proved a property of a system with an infinite number of states (and an infinite number
of systems with finite state spaces).

One might ask what would happen if, using a scalarset of undefined range, we omitted the data type reduction. Wouldn't that give us an infinite state verification problem? Try removing the declaration

forall (i in INDEX) using INDEX->{i} prove out.data//spec_case[i];

from the problem and run the resulting file.
You'll observe that nothing has changed from the previous case. Since SMV can't
handle undefined scalarsets without a data type reduction, it guesses a reduction.
It simply includes in the reduced type all the specific values of the given type
that appear in the property. In this case, there is only one, the index `i`.