TrainSwitchingPuzzle - Revision history

Michael Leuschel at 14:50, 4 October 2010

2010-10-04T14:50:30Z

← Older revision		Revision as of 14:50, 4 October 2010
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>

Michael Leuschel at 05:47, 4 October 2010

2010-10-04T05:47:02Z

← Older revision		Revision as of 05:47, 4 October 2010
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

Michael Leuschel at 05:45, 4 October 2010

2010-10-04T05:45:41Z

← Older revision		Revision as of 05:45, 4 October 2010
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.		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.

	<pre>		<pre>

Michael Leuschel at 05:44, 4 October 2010

2010-10-04T05:44:38Z

← Older revision		Revision as of 05:44, 4 October 2010
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>

Michael Leuschel: Created page with 'This model was developed to solve Puzzle Nr 40 from the book "My best mathematical and logical puzzles" by Martin Gardner. `MACHINE GardnerSwitchingPuzzle_v2 /* v2 without …'`

2010-10-04T05:24:58Z 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 …' New page 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 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 </tt>

TrainSwitchingPuzzle - Revision history

Michael Leuschel at 14:50, 4 October 2010

Michael Leuschel at 05:47, 4 October 2010

Michael Leuschel at 05:45, 4 October 2010

Michael Leuschel at 05:44, 4 October 2010

Michael Leuschel: Created page with 'This model was developed to solve Puzzle Nr 40 from the book "My best mathematical and logical puzzles" by Martin Gardner. MACHINE GardnerSwitchingPuzzle_v2 /* v2 without …'

Michael Leuschel: Created page with 'This model was developed to solve Puzzle Nr 40 from the book "My best mathematical and logical puzzles" by Martin Gardner. `MACHINE GardnerSwitchingPuzzle_v2 /* v2 without …'`