language Essence 1.3

$You are given an 8 pint bucket of water, and$ two empty buckets which can contain 5 and 3 pints respectively.
$You are required to divide the water into two by pouring water between buckets$ (that is, to end up with 4 pints in the 8 pint bucket, and
$4 pints in the 5 pint bucket). given buckets : int letting Buckets be domain int(1..buckets) given initialState : function int --> int given finalState : function int --> int given capacity : function int --> int letting maxCapacity be max([capacity(i) | i : Buckets]) given HORIZON : int find actions : sequence (maxSize HORIZON) of (Buckets, Buckets, int(1..maxCapacity)) find states : sequence (maxSize HORIZON) of function (total) Buckets --> int(0..buckets)$ action i transforms state i to state i+1
such that |actions| = |states| - 1

$cannot pour from the a bucket to itself such that forAll (i, (bFrom, bTo, amount)) in actions . bFrom != bTo$ can only pour if there is enough water
such that forAll (i, (bFrom, bTo, amount)) in actions . amount <= states(i)(bFrom)

$bucket capacity such that forAll (i, f) in states . forAll b : Buckets . f(b) <= capacity(b)$ preservation of water
such that forAll (i, (bFrom, bTo, amount)) in actions . states(i)(bFrom) - amount = states(i+1)(bFrom)
such that forAll (i, (bFrom, bTo, amount)) in actions . states(i)(bTo) + amount = states(i+1)(bTo)
such that forAll (i, (bFrom, bTo, amount)) in actions .
forAll b : Buckets . !(b in {bFrom, bTo}) -> states(i)(b) = states(i+1)(b)

$after an action, either the source bucket is empty$                      or the target bucket is full
such that forAll (i, (bFrom, bTo, amount)) in actions . states(i+1)(bFrom) = 0 \/
states(i+1)(bTo) = capacity(bTo)

$initial and final state such that states(1) = initialState such that states(|states|) = finalState$ minimise the number of actions
find nbActions : int(0..HORIZON)
such that nbActions = |actions|
minimising nbActions