-- Propositiones ad Acuendos Juvenes
-- XVIII. PROPOSITIO DE HOMINE ET CAPRA ET LVPO.
-- Alloy book: A.3.5: Goose, Beans, Fox
-- http://www.archimedes-lab.org/atelier.html?http://www.archimedes-lab.org/earlymathpuzzlers/alcuin_propositiones.html

abstract sig Being {
      Eats : set Being,             -- Eats is a relation
      where : one Bank,             -- where is a function
      CanEat, SameBank: set Being   -- both are relations
}

one sig Fox, Goose, Beans, Farmer extends Being {}

abstract sig Bank { cross: one Bank }  -- cross is a function

one sig Left, Right extends Bank {}

fact {
   Eats         = Fox -> Goose  + Goose -> Beans
   cross        = Left -> Right + Right -> Left   -- a bijection
   SameBank = where . ~where               -- an equivalence relation
   CanEat     = SameBank & Eats
}

-- Finding instances satisfying the invariant

run { CanEat . where in (Being->Farmer) . where }

-- Behaviour (TBC)