Gilbreath Card Trick - Revision history

David Geleßus: Update some links

2021-02-03T13:40:03Z

Update some links

← Older revision		Revision as of 13:40, 3 February 2021
Line 18:		Line 18:
	in LNCS 6200, pp. 195-201, 2010.		in LNCS 6200, pp. 195-201, 2010.
	DOI: 10.1007/978-3-642-13754-9_10		DOI: 10.1007/978-3-642-13754-9_10
	~~http~~://~~www~~.~~springerlink~~.com/~~content/gn18673357154448~~/		https://link.springer.com/chapter/10.1007%2F978-3-642-13754-9_10
	*/		*/
	SETS		SETS
Line 53:		Line 53:
	* in the above model I perform symmetry reduction by hand, by forcing a particular order of the cards initially		* in the above model I perform symmetry reduction by hand, by forcing a particular order of the cards initially
	* a version of the model which does not do this can be found below; it requires symmetry reduction to be enabled for efficient model checking		* a version of the model which does not do this can be found below; it requires symmetry reduction to be enabled for efficient model checking
	* I have tried to translate this example to TLA+ and use [http://~~research~~.~~microsoft~~.~~com/en-us/um/people/lamport~~/tla/~~tlc~~.html TLC] (using our new B-TLC translator), but TLC cannot deal with the initialisation <tt> x,y : (x^y = initial) </tt>. Later Domink Hansen produced an adapted (more low-level) version of my B machine which can be run by TLC; see below.		* I have tried to translate this example to TLA+ and use [http://lamport.azurewebsites.net/tla/tools.html?unhideBut=hide-tlc&unhideDiv=tlc TLC] (using our new B-TLC translator), but TLC cannot deal with the initialisation <tt> x,y : (x^y = initial) </tt>. Later Domink Hansen produced an adapted (more low-level) version of my B machine which can be run by TLC; see below.
	* A (longer) Why3 encoding can be found here [http://proval.lri.fr/gallery/unraveling_a_card_trick.en.html http://proval.lri.fr/gallery/unraveling_a_card_trick.en.html].		* A (longer) Why3 encoding can be found here [http://proval.lri.fr/gallery/unraveling_a_card_trick.en.html http://proval.lri.fr/gallery/unraveling_a_card_trick.en.html].
	* Arguably model checking gives less insight into why the trick works than proof. However, by adding a graphical visualization, a different kind of insight can be gained. This is shown below.		* Arguably model checking gives less insight into why the trick works than proof. However, by adding a graphical visualization, a different kind of insight can be gained. This is shown below.
Line 81:		Line 81:
	/* Translation by Michael Leuschel of Example in "Unraveling a Card Trick" by Tony Hoare and Natarajan Shankar in LNCS 6200, pp. 195-201, 2010.		/* Translation by Michael Leuschel of Example in "Unraveling a Card Trick" by Tony Hoare and Natarajan Shankar in LNCS 6200, pp. 195-201, 2010.
	DOI: 10.1007/978-3-642-13754-9_10		DOI: 10.1007/978-3-642-13754-9_10
	~~http~~://~~www~~.~~springerlink~~.com/~~content/gn18673357154448~~/		https://link.springer.com/chapter/10.1007%2F978-3-642-13754-9_10
	*/		*/
	/* Model checking with hash symmetry taking 161.9 seconds to traverse		/* Model checking with hash symmetry taking 161.9 seconds to traverse
Line 110:		Line 110:
	== A more low-level version for use with TLC ==		== A more low-level version for use with TLC ==

	We later adapted the above model (without symmetry) to make it somewhat more low-level and to enable the translation to TLA+ for use with [http://~~research~~.~~microsoft~~.~~com/en-us/um/people/lamport~~/tla/~~tlc~~.html TLC] (this is a new feature inside ProB Tcl/Tk).		We later adapted the above model (without symmetry) to make it somewhat more low-level and to enable the translation to TLA+ for use with [http://lamport.azurewebsites.net/tla/tools.html?unhideBut=hide-tlc&unhideDiv=tlc TLC] (this is a new feature inside ProB Tcl/Tk).
	The machine is shown below.		The machine is shown below.
	The model checking time with ProB is now reduced to 75 seconds.		The model checking time with ProB is now reduced to 75 seconds.
	With the command "Verify -> External Tools -> Model Check with TLC..." you can use [http://~~research~~.~~microsoft~~.~~com/en-us/um/people/lamport~~/tla/~~tlc~~.html TLC] as a backend. The model checking time is then approximately 15 seconds (including the translation time from B to TLA+).		With the command "Verify -> External Tools -> Model Check with TLC..." you can use [http://lamport.azurewebsites.net/tla/tools.html?unhideBut=hide-tlc&unhideDiv=tlc TLC] as a backend. The model checking time is then approximately 15 seconds (including the translation time from B to TLA+).

	<pre>		<pre>
Line 121:		Line 121:
	/* Translation by Michael Leuschel of Example in "Unraveling a Card Trick" by Tony Hoare and Natarajan Shankar in LNCS 6200, pp. 195-201, 2010.		/* Translation by Michael Leuschel of Example in "Unraveling a Card Trick" by Tony Hoare and Natarajan Shankar in LNCS 6200, pp. 195-201, 2010.
	DOI: 10.1007/978-3-642-13754-9_10		DOI: 10.1007/978-3-642-13754-9_10
	~~http~~://~~www~~.~~springerlink~~.com/~~content/gn18673357154448~~/		https://link.springer.com/chapter/10.1007%2F978-3-642-13754-9_10
	*/		*/
	SETS		SETS

Michael Leuschel: /* A more low-level version for use with TLC */

2013-05-24T06:13:36Z

A more low-level version for use with TLC

← Older revision		Revision as of 06:13, 24 May 2013
Line 113:		Line 113:
	The machine is shown below.		The machine is shown below.
	The model checking time with ProB is now reduced to 75 seconds.		The model checking time with ProB is now reduced to 75 seconds.
	With the command "Verify -> External Tools -> Model Check with TLC..." you can use [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as a backend. The model checking time is then approximately 15 seconds.		With the command "Verify -> External Tools -> Model Check with TLC..." you can use [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as a backend. The model checking time is then approximately 15 seconds (including the translation time from B to TLA+).

	<pre>		<pre>

Michael Leuschel: /* A more low-level version for use with TLC */

2013-05-24T06:13:00Z

A more low-level version for use with TLC

← Older revision		Revision as of 06:13, 24 May 2013
Line 113:		Line 113:
	The machine is shown below.		The machine is shown below.
	The model checking time with ProB is now reduced to 75 seconds.		The model checking time with ProB is now reduced to 75 seconds.
	With the command "Verify -> External Tools -> Model Check with TLC..." you can use [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as a backend. The model checking time is then ~~below 20~~ seconds.		With the command "Verify -> External Tools -> Model Check with TLC..." you can use [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as a backend. The model checking time is then approximately 15 seconds.

	<pre>		<pre>

Michael Leuschel: /* A more low-level version for use with TLC */

2013-05-24T05:44:52Z

A more low-level version for use with TLC

@@ Line 150: / Line 150: @@
    Shuffle2 = PRE y/=<> & reversed=TRUE THEN dest := dest<-last(y) || y:= front(y) END
 END
 </pre>

Michael Leuschel at 05:42, 23 May 2013

2013-05-23T05:42:23Z

← Older revision		Revision as of 05:42, 23 May 2013
Line 8:		Line 8:

	I attempted to model this problem in B and wanted to use model checking to validate the property on the final sequence. As I wanted to measure the time spent modeling I used a stopwatch. It took 13 minutes (starting from an empty B specification) to produce a first model that could be model checked by ProB. Full validation was finished after 19 minutes from the start. The model checking itself generated 150,183 states and 179,158 transitions and took 2 minutes and 17 seconds on a Mac Book Air (1.8 GHz i7).		I attempted to model this problem in B and wanted to use model checking to validate the property on the final sequence. As I wanted to measure the time spent modeling I used a stopwatch. It took 13 minutes (starting from an empty B specification) to produce a first model that could be model checked by ProB. Full validation was finished after 19 minutes from the start. The model checking itself generated 150,183 states and 179,158 transitions and took 2 minutes and 17 seconds on a Mac Book Air (1.8 GHz i7).
	I am interested in seeing how much time is required to solve this in other formalisms and with other model checking tools (e.g., Promela with Spin, CSP with FDR, TLA+ with TLC).		(Further below on this page I also describe ways to reduce the model checking time.)
			I am very interested in seeing how much combined modelling and verification time is required to solve this task in other formalisms and with other model checking tools (e.g., Promela with Spin, CSP with FDR, TLA+ with TLC).

	Here is the specification		Here is the specification

Michael Leuschel at 05:40, 23 May 2013

2013-05-23T05:40:22Z

← Older revision		Revision as of 05:40, 23 May 2013
Line 52:		Line 52:
	* in the above model I perform symmetry reduction by hand, by forcing a particular order of the cards initially		* in the above model I perform symmetry reduction by hand, by forcing a particular order of the cards initially
	* a version of the model which does not do this can be found below; it requires symmetry reduction to be enabled for efficient model checking		* a version of the model which does not do this can be found below; it requires symmetry reduction to be enabled for efficient model checking
	* I have tried to translate this example to TLA+ and use TLC (using our new B-TLC translator), but TLC cannot deal with the initialisation <tt> x,y : (x^y = initial) </tt>.		* I have tried to translate this example to TLA+ and use [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] (using our new B-TLC translator), but TLC cannot deal with the initialisation <tt> x,y : (x^y = initial) </tt>. Later Domink Hansen produced an adapted (more low-level) version of my B machine which can be run by TLC; see below.
	* A (longer) Why3 encoding can be found here [http://proval.lri.fr/gallery/unraveling_a_card_trick.en.html http://proval.lri.fr/gallery/unraveling_a_card_trick.en.html].		* A (longer) Why3 encoding can be found here [http://proval.lri.fr/gallery/unraveling_a_card_trick.en.html http://proval.lri.fr/gallery/unraveling_a_card_trick.en.html].
	* Arguably model checking gives less insight into why the trick works than proof. However, by adding a graphical visualization, a different kind of insight can be gained. This is shown below.		* Arguably model checking gives less insight into why the trick works than proof. However, by adding a graphical visualization, a different kind of insight can be gained. This is shown below.
Line 109:		Line 109:
	== A more low-level version for use with TLC ==		== A more low-level version for use with TLC ==

	We later adapted the above model (without symmetry) to make it somewhat more low-level and to enable the translation to TLA+ for use with TLC (this is a new feature inside ProB Tcl/Tk).		We later adapted the above model (without symmetry) to make it somewhat more low-level and to enable the translation to TLA+ for use with [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] (this is a new feature inside ProB Tcl/Tk).
	The machine is shown below.		The machine is shown below.
	The model checking time with ProB is now reduced to 75 seconds.		The model checking time with ProB is now reduced to 75 seconds.
	With the command "Verify -> External Tools -> Model Check with TLC..." you can use TLC as a backend. The model checking time is then below 20 seconds.		With the command "Verify -> External Tools -> Model Check with TLC..." you can use [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as a backend. The model checking time is then below 20 seconds.

	<pre>		<pre>

Michael Leuschel at 05:38, 23 May 2013

2013-05-23T05:38:32Z

@@ Line 13: / Line 13: @@
 <pre>
 MACHINE CardTrick
-/* Translation of Example in
+/* Translation by Michael Leuschel of Example in
   "Unraveling a Card Trick" by Tony Hoare and Natarajan Shankar
    in LNCS 6200, pp. 195-201, 2010.
@@ Line 78: / Line 78: @@
 MACHINE CardTrickSym /* a version to be used with ProB's symmetry reduction */
 /* see comments in machine CardTrick for more details about the modeling effort */
-/* Translation of Example in "Unraveling a Card Trick" by Tony Hoare and Natarajan Shankar in LNCS 6200, pp. 195-201, 2010.
+/* Translation by Michael Leuschel of Example in "Unraveling a Card Trick" by Tony Hoare and Natarajan Shankar in LNCS 6200, pp. 195-201, 2010.
    DOI: 10.1007/978-3-642-13754-9_10
    http://www.springerlink.com/content/gn18673357154448/
@@ Line 100: / Line 100: @@
   ((x=<> & y=<>) => ok(dest))
 INITIALISATION x,y : (x^y = all^all^all^all ) || dest := <> || reversed := FALSE
 OPERATIONS
    Reverse = PRE reversed=FALSE THEN CHOICE x := rev(x) OR y := rev(y) END || reversed := TRUE END;

Michael Leuschel: /* Adding graphical visualization */

2013-05-22T16:38:36Z

Adding graphical visualization

← Older revision		Revision as of 16:38, 22 May 2013
Line 71:		Line 71:
	With the above, ProB will display the variables x, y and dist in a graphical way, and by animation one can gain insights into why it is impossible not to generate four quartets.		With the above, ProB will display the variables x, y and dist in a graphical way, and by animation one can gain insights into why it is impossible not to generate four quartets.

	[[File:ProB_Card_Screenshot.png]]		[[File:ProB_Card_Screenshot.png\|600px\|center]]

	== A version requiring symmetry reduction ==		== A version requiring symmetry reduction ==

Michael Leuschel at 16:36, 22 May 2013

2013-05-22T16:36:30Z

@@ Line 54: / Line 54: @@
 * I have tried to translate this example to TLA+ and use TLC (using our new B-TLC translator), but TLC cannot deal with the initialisation <tt> x,y : (x^y = initial)  </tt>.
 * A (longer) Why3 encoding can be found here [http://proval.lri.fr/gallery/unraveling_a_card_trick.en.html http://proval.lri.fr/gallery/unraveling_a_card_trick.en.html].
 == A version requiring symmetry reduction ==

Michael Leuschel at 11:47, 22 May 2013

2013-05-22T11:47:07Z

← Older revision		Revision as of 11:47, 22 May 2013
Line 5:		Line 5:
	* you reverse one of the sequences		* you reverse one of the sequences
	* you perform a (not necessarily perfect) riffle shuffle of the two sequences		* you perform a (not necessarily perfect) riffle shuffle of the two sequences
	* the resulting sequence ~~will itself~~ consist of a sequence of four quartets with one card from each suite.		* the resulting final sequence is guaranteed to consist of a sequence of four quartets with one card from each suite.

	I attempted to model this problem in B and wanted to use model checking to validate the property. As I wanted to measure the time spent modeling I used a stopwatch. It took 13 minutes (starting from an empty B specification) to produce a first model that could be model checked by ProB. Full validation was finished after 19 minutes from the start. The model checking itself generated 150,183 states and 179,158 transitions and took 2 minutes and 17 seconds on a Mac Book Air (1.8 GHz i7).		I attempted to model this problem in B and wanted to use model checking to validate the property on the final sequence. As I wanted to measure the time spent modeling I used a stopwatch. It took 13 minutes (starting from an empty B specification) to produce a first model that could be model checked by ProB. Full validation was finished after 19 minutes from the start. The model checking itself generated 150,183 states and 179,158 transitions and took 2 minutes and 17 seconds on a Mac Book Air (1.8 GHz i7).
	I am interested in seeing how much time is required to solve this in other formalisms and with other model checking tools (e.g., Promela with Spin, CSP with FDR, TLA+ with TLC).		I am interested in seeing how much time is required to solve this in other formalisms and with other model checking tools (e.g., Promela with Spin, CSP with FDR, TLA+ with TLC).