/* Use Alloy to formalize the 'river crossing' problem. Define a predicate (operation) 'pred crossRiver [from, from', to, to': set Object]' that describes a *single* move of the farmer. For more details, see - Sections 9.3.4 of courseware - http://alloytools.org/tutorials/online */ // farmer and his possessions are objects abstract sig Object { eats: set Object } one sig Farmer, Fox, Chicken, Grain extends Object {} // defines who eats who fact { eats = Fox->Chicken + Chicken->Grain } // if farmer on 'from', move at most one other object to 'to'. // otherwise, no change pred crossRiver [from, to, from', to' : set Object] { Farmer in from && one x: from | { from' = from - x - Farmer - from'.eats to' = to + x + Farmer } } // every object exists exactly once on one of the two shores pred isLegal [near, far : set Object] { far = Object-near } // the farmer crosses to the far side of the river, but illegal states can occur crossScenario1: run { some fromShore, toShore, fromShore', toShore' : set Object | crossRiver[fromShore, toShore, fromShore', toShore'] } for 3 // the farmer crosses to the far side of the river, no illegal states crossScenario2: run { some fromShore, toShore, fromShore', toShore' : set Object | isLegal[fromShore, toShore] && crossRiver[fromShore, toShore, fromShore', toShore'] && isLegal[fromShore', toShore'] } for 3