TrainSwitchingPuzzle: Difference between revisions

No edit summary
No edit summary
 
(One intermediate revision by the same user not shown)
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 leading to a state satisfying the <tt>GOAL</tt> predicate. The trace consists of 22 steps.
Using breadth-first, ProB takes about 5 seconds to find the shortest solution leading to a state satisfying the <tt>GOAL</tt> predicate. The trace consists of 22 steps. A visualisation of this trace can be found on [http://www.youtube.com/watch?v=e5bjOMDBoQs YouTube].


<pre>
<pre>
Line 6: Line 6:
/* v2 without a special PassThroughTunnel operation */
/* v2 without a special PassThroughTunnel operation */
/* Puzzle Nr 40 from My best mathematical and logical puzzles, Martin Gardner */
/* Puzzle Nr 40 from My best mathematical and logical puzzles, Martin Gardner */
/* written by Michael Leuschel, 2010 */
/*
/*
We have ENGINE + two wagons A, B
We have ENGINE + two wagons A, B

Latest revision as of 14:50, 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 leading to a state satisfying the GOAL predicate. The trace consists of 22 steps. A visualisation of this trace can be found on YouTube.

MACHINE GardnerSwitchingPuzzle_v2
/* v2 without a special PassThroughTunnel operation */
/* Puzzle Nr 40 from My best mathematical and logical puzzles, Martin Gardner */
/* written by Michael Leuschel, 2010 */
/*
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