Signature `Test`

has two fields, `a`

and `b`

:

```
sig Test {
a: lone Value,
b: lone Value
}
sig Value {}
```

Note that `a`

and `b`

may or may not have a value.

A `Test`

is valid only if it satisfies this codependency: If `a`

has a value, then `b`

must also have a value:

```
pred valid (t: Test) {
one t.a => one t.b
}
```

I want to create an assertion and I expect the Alloy Analyzer to find counterexamples. The assertion is this: If `t: Test`

is valid, then `t': Test`

is also valid, where `t'`

is identical to `t`

, except `t'`

does not have a value for `b`

:

```
assert Valid_After_Removing_b_Value {
all t, t': Test {
t'.a = t.a
no t'.b
valid[t] => valid[t']
}
}
```

I expect the Alloy Analyzer to generate counterexamples like this: `t`

has a value for `a`

and `b`

. `t'`

has a value for `a`

but not for `b`

. So, `t`

is valid, but `t'`

is not. But the Analyzer gives counterexamples like this: `t`

has a value for `a`

and `b`

and `t'`

has a value for `a`

and `b`

. I don't understand that. If `t`

has a value for `a`

and `b`

, then `t`

is valid. Likewise, if `t'`

has a value for `a`

and `b`

, then `t'`

is valid. How could that be a counterexample?

What is the right way to express the assertion? Again, my goal is to express this: I assert that if `t`

is valid, then a slightly lesser version of `t`

(e.g., `b`

has no value) is also valid. That should generate counterexamples, due to the codependency.