5

In the river crossing Alloy model, this predicate:

pred crossRiver [from, from', to, to': set Object] {
  one x: from | {
    from' = from - x - Farmer - from'.eats
    to' = to + x + Farmer
  }
}

models the river crossing: One of the objects x from the from side moves to the to side, along with the Farmer.

To test my understanding, I changed: one x: from to lone x: from - Farmer --- the former moving "exactly one thing" across the river, and the latter moving "at most one non-Farmer thing".

I thought the latter better models the problem: The Farmer is hardcoded in the equality constraints and always crosses the river, and lone should better convey that the farmer can take zero or one things with them across the river.

However, when running the model after this change, the results are nonsense:

Alloy visualization projected on State

Here the second state instance shows the chicken and grain on both sides of the river and the farmer not having crossed at all.

What am I missing? (This was run on Alloy 4.2_2015-02-22)

Matheus Cuba
  • 2,068
  • 1
  • 20
  • 31
lynaghk
  • 63
  • 3

1 Answers1

1

When you change the one to lone you allow Alloy to trivially return true from the crossRiver predicate, regardless of what the near and far look like. Therefore, the model state is not constrained in any way for that step. Ergo, every possible set of values for near and far in State is perfectly ok for Alloy.

This does not mean Alloy will somehow optimize it and never constrain. It will try for one (constrains properly near and far) and it will just true not constraining the solution. However, both solutions must be in the solution space. Clearly there are lots more unconstrained solutions so you likely see rubbish.

If you use one, then Alloy must satisfy the predicate, which means that the body with the the far and near relations are constrained in such a way that only a valid crossing is modeled in State.

Just think of Alloy as a stone carving tool. You start with a huge block of states: every thinkable combinations of atoms in near and far and State are in there. However, if you skip a constraint in the trace then you get just a random combination of atoms.

A common problem where something similar is happening is:

  some f : Foo | no f

This looks like it is always false. Alas, when there are no Foo atoms this is true since the body is never looked at.

Peter Kriens
  • 15,196
  • 1
  • 37
  • 55