Confused about the implication operator in assertions

Question

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.

wmeyer wmeyer · Accepted Answer · 2017-09-01T21:47:58

I think your assertion should be:

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

In your original assertion, you assert three independent things. For example, every t' with a b would already be a counterexample.

Confused about the implication operator in assertions

1 Answers