Search code examples
alloyformal-methods

Ordering predicate is unsatisfiable

There seems to be something I don't understand about the first branch of the ordering predicate in ff_next of this alloy model.

open util/ordering[Exposure]
open util/ordering[Tile]
open util/ordering[Point]

sig Exposure {}

sig Tile {}

sig Point {
    ex: one Exposure,
    tl: one Tile
} fact {
    // Uncommenting the line below makes the model unsatisfiable
    // Point.ex = Exposure  
    Point.tl = Tile
}

pred ff_next[p, p': Point] {
    (p.tl = last) => (p'.ex = next[p.ex] and p'.tl = first)
    else (p'.ex = p.ex and p'.tl = next[p.tl])
}

fact ff_ordering {
    first.ex = first
    first.tl = first
    all p: Point - last | ff_next[p, next[p]]
}

run {}

The intuition here is that I have a number of exposures, each of which I want to perform at a number of tile positions. Think doing panorama images and then stitching them together, but doing this multiple times with different camera settings.

With the noted line commented out the first instance I get is this:

One pass over the panorama

This is equivalent to one pass over the panorama with exposure one, and then dropping the other exposures on the floor.

The issue seems to be the first branch after the => in ff_next but I don't understand what's wrong. That branch is never satisfied, which would move to the next exposure and the start of the panorama. If I uncomment the line Point.ex = Exposure the model becomes unsatisfiable, because it requires that branch.

Any help on why that branch is not satisfiable?

Solution

  • It looks like you're trying to express "every tile must correspond to point with the current exposure before we move to the next exposure." The problem is a major pitfall with ordering: It forces the signature to be exact. If you write

    run {} for 6 but 3 Tile, 2 Exposure

    Then that works as expected. There are only models when #Point = #Exposure * #Tile. You can write your own reduced version of ordering if this is an issue for you.