Is a relation total?

1

In the Alloy fragment below, a check like isTotal is problematic because of the “unbounded universal quantifier” problem described by Jackson in Software Abstractions (sec. 5.3).

pred op [a, b: X] {
  ...
}

check isTotal {
  all a: X | some b: X | op[a, b]
}

But what about a construction like the following to see if a relation is total?

sig P {
  pre: X,
  post: lone X
}

check isTotal2 {
  all p: P | op[p.pre, p.post] => some p.post
}

I suppose there must be some cases in which it fails, because I haven’t seen it suggested before. Can anyone help shed light on a check like this? It seems to be useful in some cases, if not (I suppose?) completely general in some sense.

Am I missing something?

2

Hi, in my view the situation is quite similar.

The issue in the first case is the universal quantification on b (universal because checking model implies assertion is reduced in Alloy to verifying that model and not assertion is UNSAT): are all possible values for b indeed considered by the analysis (is it even possible: X may admit only infinite instances while Alloy is a finite-model finder)?

But such a universal quantification will also be present in the second case:

all p: P | op[p.pre, p.post] => some p.post
==
all p: P | some b: X | op[p.pre, p.post] => p.post = b      (b not free in op[...])
3

Thank you for your response, David.

If I understand correctly, you’re saying the isTotal and isTotal2 checks should have the same difficulty, in that they both produce spurious counterexamples.

It turns out, though, that they don’t, at least in the cases I’ve tried. Consider the concrete example below:

abstract sig Y {}
one sig y0, y1, y2 extends Y {}

sig X { r: Y }

pred op [a, b: X] {
  b.r = (y0->y1 + y1->y2 + y2->y0)[a.r]
}
  
run { some a, b: X | op[a, b] }

So, using op, if you start with a.r = y1 you’ll get b.r = y2, etc. For this example, isTotal produces counterexamples, but isTotal2 does not.

We can try this on an operation that’s not total (at least as I understand things, but please correct me if I am wrong) and see that a counterexample is found (as it should be):

// like op but undefined when a.r = y0
pred op3 [a, b: X] {
  not a.r = y0 => op[a, b]
}

// produces counterexamples with X.r = y0
check isTotal3 {
  all p: P | op3[p.pre, p.post] => some p.post
}

This leads me to believe that the encodings of isTotal and isTotal2/3 are different. In fact, a check like isTotal2/3 has worked (as a check for total relations) on everything I’ve tried, including the linked list example in Kuncak and Jackson’s “Relational Analysis of Algebraic Datatypes” paper.

Regards,
John

4

This kind of reasoning is always a bit confusing so bear with me if I’m stating stupid things. My reasoning is that there are two issues at stake.

First, there is a theoretical issue of size, which may lead to spurious counterexamples.

Second, for op, isTotal2 doesn’t state the same thing as isTotal. I rewrote your example by turning checks into runs and then applying Skolemization and substituting the Skolem constants where it’s possible. This gives:

abstract sig Y {}
one sig y0, y1, y2 extends Y {}
sig X { r: Y }
sig P {
  pre: X,
  post: lone X
}

// Skolem constant for P
one sig _p in P {}

// Skolem constant for X
one sig _a in X {} 

fact { _a = pre[_p] }

pred op [b: X] {
  b.r = (y0->y1 + y1->y2 + y2->y0)[_a.r] }

pred isTotal { all b: X | not op[b] }

pred isTotal2 { all b: X | op[_p.post] and _p.post != b }

Now, due to dualizing, isTotal is consistent and isTotal2 is not, as they should.

Now, I looked at the remaining topics hastily but if I’m not mistaken:

If you add a generator axiom for X, (isTotal and generator) is inconsistent as it should:

pred generator { 
	#X = #Y
	all disj x1, x2: X | x1.r != x2.r }

Then you can also check that isTotal2 => isTotal is valid, isTotal => isTotal2 is not and, funnily enough: generator and isTotal => isTotal2 is.
Hope I got the last parts right.

5

This is so helpful, David. Thank you very much for doing this.

I see that the following check is also valid, and it’s what we’re after, so it goes both ways:

check { isTotal2 <=> (isTotal and generator) }

Wouldn’t this mean that a check like isTotal2 is useful when generator axioms are too difficult or too costly to come by? Has it not been proposed by others?

Regards,
John