//// 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, _) }