Alloy code for a talk, "Wolf, Goat, & Cabbages In Two Styles!!", at !!Con West 2020

cabbages.als

open util/ordering[Snapshot]

abstract sig Object {
  eats: set Object
}

one sig Wolf extends Object {}
one sig Goat extends Object {}
one sig Cabbages extends Object {}
one sig Boat extends Object {}

fact foodWeb {
	eats = (Wolf -> Goat) + (Goat -> Cabbages)
}

sig Riverbank {}

fact twoSidesToEveryRiver {
	#Riverbank = 2
}

sig Snapshot {
	location: Object -> one Riverbank
}

fact goals {
	one first.location[Object]  // all together at first
	one last.location[Object]  // and at the end
	first.location[Boat] != last.location[Boat]  // we got across
}

fact safety {
	no t: Snapshot |
		some a: Object, b: a.eats |
			t.location[a] = t.location[b] and
			t.location[Boat] != t.location[b]
}

fact movement {
	all t: Snapshot - last |
		some here, there: Riverbank, cargo: Object | {
			t.location[Boat] = here
			here != there
			t.next.location = t.location - (Boat -> here) - (cargo -> here)
				+ (Boat -> there) + (cargo -> there)
		}
}

run {} for 8

Since I gave this talk 2.5 years ago, a new version of Alloy has been released. Time is now a core concept in the language. Here is what the code looks like in Alloy 6, using the new ✨ temporal keywords ⏳ ✨ historically, eventually, always, and until.