Formulating Effect axiom

Question

How to write correctly the effect axiom for empty(b,t)-action using the predicate contains(b,l,t) The predicate evaluates True , if the bucket b holds l liters of water at time t.

empty(b,t): completely empties bucket b at time t. The effect of the transfer is visible at time t+1

transfer(b,b',t): transfers as much water from bucket b to bucket b' as possible without spilling any starting at time t. The effect of the transfer is visible at time t+1.

Bucket 1 is filled with water and holds 7 liters. Bucket 2 is empty and holds 3 liters. The target state is that b2 contains 1 liter of water.

I would say that the correct solution is:

to any b,t,l( empty(b,t) -> contains(b,l,t))

would this be correct or should I set the amount of liters to l= 5 , for example ?

Answer 1

I'm leaving the old answer because it leaves some parts to think about (and the question is about implementing the empty action only). Just to provide a full implementation too:

:- use_module(library(clpfd)).

bucket_capacity(b1,7).
bucket_capacity(b2,3).
bucket_capacity(b3,5).

% projections to a single bucket
state_bucket_value(buckets(X, _, _),b1,X).
state_bucket_value(buckets(_, Y, _),b2,Y).
state_bucket_value(buckets(_, _, Z),b3,Z).

% state update relation by a single bucket
state_updated_bucket_value(buckets(_, Y, Z), buckets(X0, Y,  Z ), b1, X0).
state_updated_bucket_value(buckets(X, _, Z), buckets(X,  Y0, Z ), b2, Y0).
state_updated_bucket_value(buckets(X, Y, _), buckets(X,  Y,  Z0), b3, Z0).


% initial state
state_goesto_action(S0, S0, []) :-
    S0 = buckets(X,Y,Z),
    bucket_capacity(b1,X),
    bucket_capacity(b2,Y),
    bucket_capacity(b3,Z).
% state transition for emptying
state_goesto_action(S1, S2, [empty(Bucket) | History]) :-
    state_updated_bucket_value(S1, S2, Bucket, 0),
    state_goesto_action(_S0, S1, History).
% state transition for pouring
state_goesto_action(S1, S3, [pour(From,To) | History]) :-
    bucket_capacity(b1,Max),
    state_bucket_value(S1,From,X),
    state_bucket_value(S1,To,Y),
    From0 #= min(X+Y, Max),
    To0 #= max(X-Y, 0),
    state_updated_bucket_value(S1, S2, From, From0),
    state_updated_bucket_value(S2, S3, To, To0),
    state_goesto_action(_S0, S1, History).

To find out, if we can find a bucket with exactly one litre, we can fairly enumerate all histories:

?- length(L,_), state_bucket_value(S,_,1), state_goesto_action(_, S, L).
L = [pour(b1, b3), pour(b1, b2), empty(b1), pour(b1, b3)],
S = buckets(5, 0, 1) ;
L = [pour(b1, b3), pour(b1, b2), pour(b1, b1), pour(b1, b3)],
S = buckets(5, 0, 1) ;
L = [pour(b1, b3), pour(b1, b2), pour(b2, b1), empty(b1)],
S = buckets(7, 0, 1) ;
L = [pour(b1, b3), pour(b1, b2), pour(b2, b1), pour(b1, b1)],
[...].

And just to check if the predicate is reversible:

?- L = [pour(b1, b3), pour(b1, b2), empty(b1), pour(b1, b3)], state_goesto_action(_, S, L).
L = [pour(b1, b3), pour(b1, b2), empty(b1), pour(b1, b3)],
S = buckets(5, 0, 1) ;
false.

Edit: Removed domain constraints to speed up computation (we start with a fixed state, so constraints will always be ground and can be propagated without labeling).

Answer 2

I think the answer would be:

Empty(b,t) => Contains(b,0,t+1)