% 3 sheep an three wolves shall cross a river in a boat % which carries at most 2 animals at once. % On either side, the wolves may never outnumber the sheep % or the sheep will be eaten. actions: cross(S,W) requires #int(S), #int(W), P = S+W, 1 <= P, P <= 2. fluents: here(A,N) requires animal(A), range(N). boat_here. always: executable cross(S,W) if boat_here, here(sheep,HS), here(wolf,HW), HS >= S, HW >= W. executable cross(S,W) if not boat_here, here(sheep,HS), here(wolf,HW), AS = S + HS, AS <= 3, AW = W + HW, AW <= 3. caused -boat_here after cross(S,W), boat_here. caused boat_here after cross(S,W), not boat_here. caused here(sheep,S_new) if S_old = S_new+S after cross(S,W), boat_here, here(sheep,S_old). caused here(wolf,W_new) if W_old = W_new+W after cross(S,W), boat_here, here(wolf,W_old). caused here(sheep,S_new) if S_new = S_old+S after cross(S,W), not boat_here, here(sheep,S_old). caused here(wolf,W_new) if W_new = W_old+W after cross(S,W), not boat_here, here(wolf,W_old). caused -here(sheep,N) after here(sheep,N), cross(S,W), S > 0. caused -here(wolf,N) after here(wolf,N), cross(S,W), W > 0. forbidden here(wolf,N1), here(sheep,N2), 0 < N2, N2 < N1. forbidden here(wolf,N1), here(sheep,N2), N2 < 3, N1 < N2. inertial here(A,N). inertial boat_here. noConcurrency. initially: here(wolf,3). here(sheep,3). boat_here. goal: here(sheep,0), here(wolf,0) ? (11)