Die Hard Problem from TLA+

[Tim Weaver]

I just recently discovered PiCat. Thanks for making such an interesting tool! I've tried and failed multiple times to utilize both TLA+ and Alloy as tools to model software systems, and I'm hoping PiCat will be a success. The fact that it runs in my terminal and doesn't require an entire Java backend is fantastic.

I'm a software engineer and not a mathematician, but I think these modeling tools could really help make software design and development a much better place than it currently is at many companies. As a first attempt to do something interesting I wanted to see if I could write a solver for the Die Hard problem that is famously described by Leslie Lamport for TLA+. Here's a Medium article about it (although their solution is not the optimal solution that Leslie gets).

% In the movie Die Hard 3, the heroes must obtain exactly 4 gallons of
% water using a 5 gallon jug, a 3 gallon jug, and a water faucet.

import planner.

% States are number of gallons in Small and Big jugs
% [Small, Big]
% Starting state: both empty
% [0,0]
% Final State: 4-gallons in the big jug, small jug don't care
% [_, 4]


main =>
  init,
  best_plan_unbounded([0,0], Plan),
  foreach (Step in Plan)
    println(Step)
  end.

init =>
  % 5-gallon jug
  member(Big, 0..5),

  % 4-gallon jug
  member(Small, 0..3).

final(Goal) =>
  Goal = [_,4].


%
% Small to Big
%
action([Small, Big], NextS,Action,Cost) ?=>
  Action = $small_to_big(Small,Big),
  if Big + Small <= 5 then
    B = Big + Small,
    S = 0,
  else
    B = 5,
    S = Small - (5 - Big),
  end,
  NextS = [S,B],
  Cost = 1.

%
% Big to Small
%
action([Small, Big],NextS,Action,Cost) ?=>
  Action = $big_to_small(Small,Big),
  if Big + Small <= 3 then
    B = 0,
    S = Big + Small,
  else
    B = Big - (3 - Small),
    S = 3,
  end,
  NextS = [S,B],
  Cost = 1.

%
% Fill Small
%
action([Small, Big], NextS,Action,Cost) ?=>
  Action = $fill_small(Small,Big),
  NextS = [3,Big],
  Cost = 1.

%
% Empty Small
%
action([Small, Big], NextS,Action,Cost) ?=>
  Action = $empty_small(Small,Big),
  NextS = [0,Big],
  Cost = 1.

%
% Fill Big
%
action([Small, Big], NextS,Action,Cost) ?=>
  Action = $fill_big(Small,Big),
  NextS = [Small,5],
  Cost = 1.

%
% Empty Big
%
action([Small, Big], NextS,Action,Cost) =>
  Action = $empty_big(Small,Big),
  NextS = [Small,0],
  Cost = 1.

My program appears to be successful at solving the problem:

𝝨 picat diehard.pi
fill_big(0,0)
big_to_small(0,5)
empty_small(3,2)
big_to_small(0,2)
fill_big(2,0)
big_to_small(2,5)

I have a couple questions, however:

1. It doesn't print out the final state of the jugs just, which after doing `big_to_small(2,5)` should be `[3,4]`. I'm not sure how to get that. Something like `big_to_small(2,5) -> [3,4]` maybe.
2. Did I use `init` correctly? Again I was trying to mimic what I know from TLA+, and it appears to do the right thing, but maybe not the PiCat way of doing it?
3. I couldn't find any other PiCat solutions to this particular program to compare with. Maybe someone knows of some?

Thanks

[Hakan Kjellerstrand]

Hi Time.

Welcome to Picat!

Here are some answers on your questions.

* It doesn't print out the final state of the jugs just, which after doing `big_to_small(2,5)` should be `[3,4]`. I'm not sure how to get that. Something like `big_to_small(2,5) -> [3,4]` maybe.

The reason that your program does not show the last step is because the action in action/4 does not show the full action, it only shows the From state, not the To state.

For example the action small_to_big is:

"""

action([Small, Big], NextS,Action,Cost) ?=>
  Action = $small_to_big(Small,Big),
  if Big + Small <= 5 then
    B = Big + Small,
    S = 0,
  else
    B = 5,
    S = Small - (5 - Big),
  end,
  NextS = [S,B],
  Cost = 1.
"""

  And this only shows the from part, not the to part.

Here's a better way of stating it, were the Action is placed after the NextS step.

action([Small, Big], NextS,Action,Cost) ?=>

  % Action = $small_to_big(Small,Big),  % <- original place

  if Big + Small <= 5 then
    B = Big + Small,
    S = 0,
  else
    B = 5,
    S = Small - (5 - Big),
  end,
  NextS = [S,B],

  Action = $small_to_big([[Small,Big],to,NextS]),  % <--
  Cost = 1.

With these changes in all action/4 clauses the program shows this solution, i.e. with both from state and the to state:

fill_big([[0,0],to,[0,5]])
big_to_small([[0,5],to,[3,2]])
empty_small([[3,2],to,[0,2]])
big_to_small([[0,2],to,[2,0]])
fill_big([[2,0],to,[2,5]])
big_to_small([[2,5],to,[3,4]])

(Which is the unique and optimal solution.)

* Did I use `init` correctly? Again I was trying to mimic what I know from TLA+, and it appears to do the right thing, but maybe not the PiCat way of doing it?

  init/0 in your program does not have any effect on the program since the enumeration of member/2 is done only in the init/0 predicate (Picat does not support global variables like in traditional imperative programming languages).  For this specific planner problem, there's no need for any enumeration using member/2 since it's all "pure math", but for certain problems member/2 is very useful, and then they must be inside the action/4 clauses.

* I couldn't find any other PiCat solutions to this particular program to compare with. Maybe someone knows of some?

The Picat distribution contains a version of this problem:  exs/planner/water.pi though the plan does not state the details as much as in your program.

Also, I wrote a general program using planner for solving these kind of puzzles: https://hakank.org/picat/n_water_jugs.pi

* It supports not just 3 jugs, but n jugs

* It also supports puzzles when there's only a certain amount of water to distribute.

  And this is a drawback of this approach since the initialization must include some finite amount of water.

The (slight variant of) Die Hard 3 problem is in go3/0.

Hope this helps.

Best

Hakan

[Tim Weaver]

Thank you for the response and the extremely helpful information! I've been studying the examples you have on your site, thanks for putting in the effort to make and publish those. I missed the n_water_jugs file. I will continue to study and learn.

Thanks again

Tim