** Next:** Using case analysis over
** Up:** Case analysis
** Previous:** Case analysis
** Contents**

###

A very simple example

Now, let's look at a trivial example of this. Let's return to our
very simple example of transmitting a sequence of bytes. Here is the
specification again:

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.
Note that our specification (layer `spec`) says that at
all times the output value must be equal to the element
of array `bytes` indicated by the index value `out.idx`.
We would like to break this specification into cases and consider
only one index value at a time. To do this, we add the following
declaration:

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

In this case, the property we are splitting into cases is `out.data//spec`, the assignment to `out.data` in layer `spec`. The resulting cases are `out.data//spec_case[i]`.
Note, however, that in the subcase declaration, we only give a
layer name for the new cases, since the signal name is redundant.
This declaration is exactly as if we had written

forall (i in INDEX)
layer spec_case[i]:
if (out.idx = i)
out.data := bytes[out.idx];

except that SMV recognizes that if we prove `out.data//spec_case[i]`
for all `i`, we don't have to prove `out.data//spec`.
Run this example, and
look in the properties pane. You'll see that `out.data//spec` does
not appear, but instead we have `out.data//spec_case[0]`. Note
that only the case `i = 0` appears, since INDEX is a scalarset
type, and SMV knows that all the other cases are symmetric to this
one. Now look in the cone pane. You'll notice that all of the elements
of the array `bytes` are in the cone. This is because the
definition of `inp.data` in layer `spec` references all of
them. However, all of them except element 0 are in the `undefined`
layer. This is a heuristic used by SMV: if a property references some
specific value or values of a given scalarset type, then only the
corresponding elements of arrays over that type are used. The rest are
given the undefined value. You might try clicking on element `bytes[1]` and choosing `Abstraction|Explain Layer` to get an
explanation of why this signal was left undefined. You can, of course,
override this heuristic by explicitly specifying a layer for the other
elements. In this case, however, the heuristic works, since property
`out.data//spec_case[0]` verifies correctly.

** Next:** Using case analysis over
** Up:** Case analysis
** Previous:** Case analysis
** Contents**
2003-01-07