:- ['11_flux'].
:- chr('11_mailCnstr').


init(Z0) :- Z0 = [at(1),empty(1),empty(2),empty(3),
                  request(1,3),request(2,4) | Z],
            not_holds_all(request(_,_), Z),
            consistent(Z0).


  consistent(Z) :-
     holds(at(R),Z,Z1) -> R::[1..6], not_holds_all(at(_),Z1),
     empty_carries(Z),
     request_consistent(Z),
     duplicate_free(Z).

  state_update(Z1,pickup(B,R),Z2,[NotEmpty]) :-
     NotEmpty=false, holds(empty(B),Z1),
     holds(at(R1),Z1), 
     update(Z1,[carries(B,R)],[empty(B),request(R1,R)],Z2).

  state_update(Z1,deliver(B),Z2,[Empty,WrongAddress]) :-
     Empty=false, WrongAddress=false, holds(carries(B,R),Z1),
     holds(at(R),Z1),
     update(Z1,[empty(B)],[carries(B,R)],Z2).

  state_update(Z1,go(D),Z2,[]) :-
     holds(at(R),Z1), ( D = up -> R1 #= R+1 ; R1 #= R-1 ),
     update(Z1,[at(R1)],[at(R)],Z2).

  ab_state_update(Z1,pickup(B,R),Z2,[NotEmpty]) :-
     NotEmpty=false,
     holds(at(R1),Z1), 
     ( holds(empty(BP),Z1), BP #\= B, holds(request(R1,R),Z1),
          update(Z1,[carries(BP,R)],[empty(BP),request(R1,R)],Z2) ;
       holds(empty(B),Z1), holds(request(R1,RP),Z1), RP #\= R,
          update(Z1,[carries(B,RP)],[empty(B),request(R1,RP)],Z2) ;
       holds(empty(BP),Z1), holds(request(R1,RP),Z1), BP #\= B, RP #\= R,
          update(Z1,[carries(BP,RP)],[empty(BP),request(R1,RP)],Z2) ) ;
     NotEmpty=true, not_holds(empty(B),Z1), Z2 = Z1.

  ab_state_update(Z1,deliver(B),Z2,[Empty,WrongAddress]) :-
     Empty=false, WrongAddress=false,
     holds(at(R),Z1),
     ( holds(carries(BP,R),Z1), BP #\= B,
          update(Z1,[empty(BP)],[carries(BP,R)],Z2) ;
       holds(carries(BP,RP),Z1), RP #\= R,
          update(Z1,[empty(BP),request(R,RP)],[carries(BP,RP)],Z2) ) ;
     Empty=true, holds(empty(B),Z1), Z2 = Z1 ;
     WrongAddress=true, holds(at(R),Z1), holds(carries(B,RP),Z1),
     RP #\= R, Z2 = Z1.