//// This is the problem:
//// (1) There is a chicken, a fox, a bag of grain, a farmer, and a boat.
//// (2) Initially all these things are on the left side of a river bank.
//// (3) The farmer wants to take everything to right side of a river bank,
//// (4) But the farmer can only fit one additional object in the boat at a time,
//// (5) And if the chicken is left alone with grain it eats all the grain,
//// (6) And if the fox is left along with the chicken it eats the chicken.
//// How does the farmer move everything with anything being eaten?
//// Ideally we would like to specify this problem as a transition system where the transitions
//// are of the form Move_X, and then we would like to model-check this system (reachibility).
//// This view can be easily specified using model transformations to encode transitions and then applying
//// bounded symbolic model checking. However, this example shows how to encode the model checking
//// problem explicitly so the usual domain model finding accomplishes the same task. Shortly we will provide
//// examples that directly utilize the FORMULA model checker.
//// We need to do two things: First, introduce time into the system so
//// we can keep track of where things were and where they are now. In this simple encoding we will make this
//// an infinite state system, because time will be part of the state and it continues to progress even if the farmer
//// stands still. Second, because we define an infinite state system, we need to put an upper bound on how far into
//// the future we are willing to look for solutions. The larger the upper bound the more work the solver has to do.
//// The states of the system are encoded by location terms of the form location(t, o, s), which means, at time t
//// the object o is on side s. Objects can also be in the middle when they are in transiting in the boat. As the program
//// runs it records the states of the system using location terms.
//// The Move_X transitions are encoded as Move(t, o) terms, which mean at time t object o should be taken from one side
//// and put in the boat to be sent to the other side. There program must account for the time it takes to Move objects
//// and that the farmer must must be on the same side as the object and must not be in the middle. There are a number
//// of cases to properly encode the consquences of Move(t, o).
domain RiverCrossing
{
Object ::= { chicken, fox, grain, farmer }.
Side ::= { left, right, middle }.
location ::= (t: Natural, o: Object, s: Side).
[Unique(t -> o)]
primitive Move ::= (t: Natural, o: Object).
primitive Bound ::= (t: Natural).
//// This is the initial state of the system.
location(0, chicken, left).
location(0, fox, left).
location(0, grain, left).
location(0, farmer, left).
//// These describe if anything has been eaten, and if the problem is solved.
eaten := location(t, chicken, s), location(t, fox, s), location(t, farmer, sp), sp != s.
eaten := location(t, chicken, s), location(t, grain, s), location(t, farmer, sp), sp != s.
done := location(t, farmer, right), count(location(t,_,right)) = 4.
//// CASE 1: If Move(t, o) is requested and o is on the same side as the farmer (which is not the middle) then
//// then o and the farmer are in the river (middle) at time t + 1.
location(tnext, o, middle),
location(tnext, farmer, middle) :-
location(t, o, s),
location(t, farmer, s),
Move(t, o),
s != middle,
tnext = t + 1,
Bound(end), t < end.
//// STATIONARY CASES 2 - 3 describe when we try to Move an object that cannot be moved.
//// CASE 2: If Move(t, o) is requested but o is not on the same side as the farmer
//// then o is on the same side in the next time step.
location(tnext, o, s) :-
location(t, o, s),
location(t, farmer, sp),
Move(t, o),
s != sp,
tnext = t + 1,
Bound(end), t < end.
//// CASE 3: If Move(t, o) is requested but o is not on the same side as the farmer
//// and the farmer is not in the middle, then the farmer stays on the same side.
location(tnext, farmer, sp) :-
location(t, o, s),
location(t, farmer, sp),
Move(t, o),
s != sp,
sp != middle,
tnext = t + 1,
Bound(end), t < end.
//// STATIONARY CASES 4 - 5 describe what happens when we don't move an object.
//// CASE 4: If there was no request to move anything and o is not in the middle
//// then it stats on the same side.
location(tnext, o, s) :-
location(t, o, s),
fail Move(t, _),
s != middle,
tnext = t + 1,
Bound(end), t < end.
//// CASE 5: If where are Moving something other than o, then o stays in the same place.
//// except for the farmer, who implicitly moves with everything, and except for things
//// in the middle which are moving on the boat.
location(tnext, o, s) :-
location(t, o, s),
Move(t, op),
o != op,
o != farmer,
s != middle,
tnext = t + 1,
Bound(end), t < end.
//// RIVER CROSSING CASES 6 - 7 describe what happens to things in the boat
//// CASE 6: If some thing is in the middle and it was on the right in the previous
//// time step, then it is on the left in the next time step.
location(tnext, o, left) :-
location(t, o, middle),
location(tp, o, right),
tp = t - 1, tnext = t + 1,
Bound(end), t < end.
//// CASE 7: If some thing is in the middle and it was on the left in the previous
//// time step, then it is on the right in the next time step.
location(tnext, o, right) :-
location(t, o, middle),
location(tp, o, left),
tp = t - 1, tnext = t + 1,
Bound(end), t < end.
conforms := !eaten & done.
}
//// Give the time bound and the number of Move operations we are willing to consider.
//// The pre-populated times are to avoid unecessary work that is an artifact of the
//// encoding.
partial model Solve of RiverCrossing
{
Bound(14)
Move(0, _)
Move(2, _)
Move(4, _)
Move(6, _)
Move(8, _)
Move(10, _)
Move(12, _)
}