Solution to farmer puzzle using Alloy 6 temporal primitives

models
1

Hello!

The current sample model examples/tutorial/farmer.als (link) distributed with Alloy 6 doesn’t use the new temporal primitives (always, eventually, ' etc.). It might be nice to add another version that uses the new functionality, so that users see they don’t need to deal with util/ordering etc.

Although there are already nice sample models showing off the temporal primitives, like trash.als, I think the puzzle is well known enough to be more approachable on its own.

As such, I have a model here - I’m sure it could be much improved :upside_down_face:

Farmer puzzle - Alloy 6 model 
abstract sig Place {
  other: one Place
}
one sig Near, Far extends Place {}
fact other {
  other = Near->Far + Far->Near
}

abstract sig Entity {
  eats: set Entity,
  var place: one Place,
}
one sig Farmer, Fox, Chicken, Grain extends Entity {}

fact eating {
  eats = Fox->Chicken + Chicken->Grain
}

fact init {
  Entity.place = Near
}

pred move [who: Entity] { who.place' = who.place.other }
pred stay [who: Entity] { who.place' = who.place }

pred step {
  -- everybody either moves or does nothing (possible actions)
  all e: Entity | move[e] or stay[e]

  -- entities on the other side from Farmer always stay
  all e: place.(Farmer.place.other) | stay[e]

  -- Farmer always moves
  move[Farmer]

  -- at most 1 non-Farmer entity moves each step (given it's with him)
  lone e: place.(Farmer.place) - Farmer | move[e]
  
  -- nobody can eat anybody when Farmer's gone
  no disj e1,e2: place.(Farmer.place.other) | e1 in e2.eats
}

goal: run {
  always step
  eventually Entity.place = Far
}
2 Likes
2

Your model seems OK to me. My main remark would be that the usual way to model transition systems is to define “self-contained” events (i.e. containing a guard, an effect and frame conditions stating what’s left unchanged by the event), but more global constraints as you did here are also possible (it’s perhaps harder to grasp when the model is larger).

3

I cannot but see these posts as a challenge, and I love them! :slight_smile:

This is my model:

enum Object { farmer, chicken, grain, fox }

one sig W {
	var far, near, boat : set Object
} {
	always {

		# boat <= 3

		all obj : Object | obj in near iff obj not in far

			move[near,far,boat] 
		or 	move[far,near,boat] 
		or 	(near=near' and far=far' and no boat)
	} 
}

pred move[ from, to, boat: set Object ] {

	boat in from
	farmer in boat

	from' = from-boat
	fox + chicken not in from'
	chicken + grain not in from'
}

run {
	W.near = Object
	eventually W.far = Object	
}
2 Likes
4

Thanks for the note about best practices for the events! Indeed I didn’t yet try anything larger-scale than these examples, so that issue didn’t bite me yet.

5

FYI, in Alloy 6, signature facts are automatically prepended an always operator, so no need for always here. The idea is that a signature fact can naturally represent a class invariant (which is not the case in your model due to the presence of near').

6

Ok, good to know. But I guess it can’t harm? Primary reason I used this was the nice name scoping :slight_smile:

I now understand why my initial condition near=Object failed in the fact signature :slight_smile:

7

The Constraint Logic Programming (CLP / Prolog etc.) paradigm can be observed through this elegant expression of the puzzle.

8

What does “one sig W” mean here, and why did you pick the name “W”?

9

What does “one sig W” mean here, and why did you pick the name “W”?

As a programmer I am allergic to globals. So W = World. It keeps the state I am reasoning about. By putting it in a sig, I can easily add other things in the same module without the globals interfering. Same reason I do not use facts but instead use predicates that are then invoked in the command. Makes the spec easier to debug, extend, and test.