thun/TLA.pl

   1 \r
   2 :- use_module(library(clpfd)).\r
   3 \r
   4 \r
   5 % relly(PC, I, PCnext, Inext).\r
   6 \r
   7 initial_state :- relly(start, 0, _, _).\r
   8 \r
   9 relly(start, _I, middle, Inext) :- Inext in 0..1000.\r
  10 relly(middle, I,   done, Inext) :- Inext #= I + 1.\r
  11 \r
  12 \r
  13 % next(PC, I) :- \r
  14 next(done, _).\r
  15 next(PC, I) :- PC \= done, relly(PC, I, PCnext, Inext), next(PCnext, Inext).\r
  16 \r
  17 \r
  18 % ?- relly(start, 17, middle, 534).\r
  19 % true.\r
  20 \r
  21 % ?- relly(middle, 534, 77, done).\r
  22 % false.\r
  23 \r
  24 % ?- initial_state.\r
  25 % true.\r
  26 \r
  27 % ?- relly(start, 0, PC, I).\r
  28 % PC = middle,\r
  29 % I in 0..1000.\r
  30 \r
  31 % ?- relly(start, 0, PC, I), relly(PC, I, PCnext, Inext).\r
  32 % PC = middle,\r
  33 % PCnext = done,\r
  34 % I in 0..1000,\r
  35 % I+1#=Inext,\r
  36 % Inext in 1..1001.\r
  37 \r
  38 \r
  39 \r
  40 type_ok(Small, Big) :- Small in 0..3, Big in 0..5.\r
  41 \r
  42 \r
  43 next_dh(Small, Big, S, B, Mi, Mo) :-\r
  44     B #\= 4, type_ok(Small, Big),\r
  45     die_hard(Move, Small, Big, Si, Bi),\r
  46     State = [Move, Si, Bi],\r
  47     (Bi = 4 -> Mo=[State|Mi] ; next_dh(Si, Bi, S, B, [State|Mi], Mo)).\r
  48 \r
  49 \r
  50 % die_hard(Small, Big, S, B).\r
  51 die_hard(fill_small, Small, Big, 3, Big) :- Small #\= 3.\r
  52 die_hard(  fill_big, Small, Big, Small, 5) :- Big #\= 5.\r
  53 \r
  54 die_hard(empty_small, Small, Big, 0, Big) :- Small #> 0.\r
  55 die_hard(  empty_big, Small, Big, Small, 0) :- Big #> 0.\r
  56 \r
  57 die_hard(small_to_big, Small, Big, S, B) :-\r
  58     Big #< 5, Small #> 0,\r
  59     small_to_big(Small, Big, S, B).\r
  60 \r
  61 die_hard(big_to_small, Small, Big, S, B) :-\r
  62     Small #< 3, Big #> 0,\r
  63     big_to_small(Small, Big, S, B).\r
  64 \r
  65 big_to_small(Small, Big, S, 0) :-\r
  66     Small + Big #=< 3,\r
  67     S is Small + Big.\r
  68 \r
  69 big_to_small(Small, Big, 3, B) :-  % \r
  70     Small + Big #> 3,\r
  71     B is Big - (3 - Small).\r
  72 \r
  73 small_to_big(Small, Big, 0, B) :-\r
  74     Small + Big #=< 5,\r
  75     B is Small + Big.\r
  76 \r
  77 small_to_big(Small, Big, S, 5) :-\r
  78     Small + Big #> 5,\r
  79     S is Small - (5 - Big).\r
  80 \r
  81 /*\r
  82 \r
  83 \r
  84 call_with_depth_limit(next_dh(0, 0, S, B, Mi, Mo), 12, REsult).\r
  85 \r
  86 \r
  87 \r
  88 \r
  89 \r
  90 \r
  91 \r
  92 \r
  93 \r
  94 \r
  95 \r
  96 \r
  97 \r
  98 \r
  99 \r
 100 \r
 101 \r
 102 \r
 103 \r
 104 \r
 105 \r
 106 \r
 107 \r
 108 \r
 109 \r
 110 \r
 111 \r
 112 \r
 113 \r
 114 \r
 115 \r
 116 call_with_depth_limit(next_dh(0, 0, S, B), 12, REsult).\r
 117 \r
 118 find...\r
 119 \r
 120 fill big\r
 121 0 0 -> 0 5\r
 122 big to small\r
 123 0 5 -> 3 2\r
 124 empty small\r
 125 3 2 -> 0 2\r
 126 big to small\r
 127 0 2 -> 2 0\r
 128 fill big\r
 129 2 0 -> 2 5\r
 130 big to small\r
 131 2 5 -> 3 4\r
 132 \r
 133 \r
 134 */