Single rafting versus one quantifier at the river crossing

Question

Into a river crossing an 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 } } 

simulates a river crossing: one of the x objects from the from side moves to the to side with the farmer.

To test my understanding, I changed: one x: from to lone x: from - Farmer --- the previous movement "exactly one thing" across the river, and the second - "no more than one non-farmer thing."

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

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

Here a second example of the state shows chicken and grain on both sides of the river, and the farmer has not crossed at all.

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

Answer 1

When you change one to lone , you allow Alloy to return true true from the crossRiver predicate, regardless of how near and far look. Therefore, the state of the model is not limited in any way for this step. Ergo, all possible values ​​for near and far in State great for rafting.

This does not mean that the alloy somehow optimizes it and never restrains it. It will try to execute one (correctly hide near and far ), and it just true will not limit the solution. However, both solutions must be in the decision space. Clearly there are many more unlimited solutions, so you are likely to see garbage.

If you use one , then Alloy must satisfy the predicate, which means that a body with far and near relationships is bounded so that only a valid intersection is modeled in the state.

Just think of the alloy as a stone carving tool. You start with a huge block of states: all conceivable combinations of atoms in near and far and State are there. However, if you skip the trace restriction, you will only get a random combination of atoms.

A common problem when something like this happens:

  some f : Foo | no f 

It seems like it's always a lie. Alas, when there are no Fu atoms, this is true, since the body never looks.