No 3-element counterexample found

Question

I am learning Alloy and was trying to make it find two binary relations r and s, such that s equals the transitive closure of r, and such that s is not equal to r. I suppose I can ask Alloy to do this by executing the following:

sig V
{
  r : V,
  s : V
}
assert F { not ( some (s-r) and s=^r ) }
check F

Now Alloy 4.2 cannot find a counterexample, although an easy 3-element structure would be the one where r = {(V0,V1), (V1,V2)} and s = r + {(V0,V2)} obviously.

Can someone explain what is going on?

Answer 1

Translating your requirement directly:

// find two binary relations r and s such that 
// s equals the transitive closure of r ands is not equal to r

run {some r, s: univ -> univ | s != r and s = ^r}

This gives an instance as expected. The mistake in your spec is that your declarations restrict the relations to be functions; should instead have

sig V {
  r: set V,
  s: set V
  }

or

sig V {r, s: set V}