Solution to farmer puzzle using Alloy 6 temporal primitives


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 { = Near

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

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.( | stay[e]

  -- Farmer always moves

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

goal: run {
  always step
  eventually = Far
1 Like

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).

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

		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	
1 Like

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.

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').

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: