TrainSwitchingPuzzle: Difference between revisions

(Created page with 'This model was developed to solve Puzzle Nr 40 from the book "My best mathematical and logical puzzles" by Martin Gardner. <tt> MACHINE GardnerSwitchingPuzzle_v2 /* v2 without …')
 
No edit summary
Line 1: Line 1:
This model was developed to solve Puzzle Nr 40 from the book "My best mathematical and logical puzzles" by Martin Gardner.
This model was developed to solve Puzzle Nr 40 from the book "My best mathematical and logical puzzles" by Martin Gardner.
Using breadth-first, ProB takes about 5 seconds to find the shortest solution, consisting of 22 steps.


<tt>
<pre>
 
MACHINE GardnerSwitchingPuzzle_v2
MACHINE GardnerSwitchingPuzzle_v2
/* v2 without a special PassThroughTunnel operation */
/* v2 without a special PassThroughTunnel operation */
Line 61: Line 61:
   END
   END
END
END
</tt>
</pre>

Revision as of 05:44, 4 October 2010

This model was developed to solve Puzzle Nr 40 from the book "My best mathematical and logical puzzles" by Martin Gardner. Using breadth-first, ProB takes about 5 seconds to find the shortest solution, consisting of 22 steps.

MACHINE GardnerSwitchingPuzzle_v2
/* v2 without a special PassThroughTunnel operation */
/* Puzzle Nr 40 from My best mathematical and logical puzzles, Martin Gardner */
/*
We have ENGINE + two wagons A, B
Only ENGINE can go through tunnel
Layout:
 ==ENGINE ======+======A======\
               /              |
               |             TUN
               |             NEL
               |              |
                \             /
 ======================B======
Task: move A to B's position and vice versa and return ENGINE to original position
*/
SETS
 TRAINS={engine,A,B};
 TRACKS = {topleft,top_middle,bot_left,bot_middle,leftlink}
DEFINITIONS
 GOAL == occ(topleft) = [engine] & occ(top_middle)=[B] & occ(bot_middle)=[A]
CONSTANTS
  link, restrict
PROPERTIES
  link = {topleft |->top_middle, leftlink |->top_middle, 
                          top_middle |-> bot_middle, /* Tunnel */
          bot_middle|-> bot_left, bot_middle |-> leftlink} &
  restrict = (link*{{}}) <+
            { (top_middle|->bot_middle) |-> {A,B} } /* A,B are not allowed to take the tunnel */
VARIABLES occ
INVARIANT
 occ: TRACKS --> iseq(TRAINS) &
 !(t1,t2).(t1:TRACKS & t1/=t2 => ran(occ(t1)) /\ ran(occ(t2)) = {} ) &
 UNION(t).(t:TRACKS|ran(occ(t))) = TRAINS
/*
 Sequence Order on Track Sections:
 ====1=2=3======+====1=2=3====\
               /              |
               3             TUN
               2             NEL
               1              |
                \             /
 ====3=2=1===========3=2=1====
*/
INITIALISATION occ := {topleft |-> [engine], top_middle |-> [A], bot_middle |->[B],
                       leftlink |-> <>, bot_left |-> <> }
OPERATIONS
  Move(Seq,T1,T2,Rest) = PRE Seq : iseq1(TRAINS) & Rest : iseq(TRAINS) &
           occ(T1)= Rest^Seq & engine:ran(Seq) & T1|->T2 : link &
           restrict((T1,T2)) /\ ran(Seq) = {} THEN
    occ := occ <+ {T1 |-> Rest, T2 |-> (Seq^occ(T2))}
  END;
  MoveRev(Seq,T1,T2,Rest) = PRE Seq : iseq1(TRAINS) & Rest : iseq(TRAINS) &
           occ(T1)= Seq^Rest & engine:ran(Seq) & T2|->T1 : link &
           restrict((T2,T1)) /\ ran(Seq) = {}  THEN
    occ := occ <+ {T1 |-> Rest, T2 |-> (occ(T2)^Seq)}
  END
END