Sudoku Solved in the ProB REPL - Revision history

Jan Gruteser: fix typo

2024-03-05T14:39:59Z

fix typo

← Older revision		Revision as of 14:39, 5 March 2024
Line 46:		Line 46:
	</pre>		</pre>

	Now, we will try and complete the constraints and put pairs of ~~co-ordinates~~ within each sub-square into the variable <tt>Diff3</tt>, and computing the union of <tt>Diff1</tt>, <tt>Diff2</tt> and <tt>Diff3</tt>:		Now, we will try and complete the constraints and put pairs of coordinates within each sub-square into the variable <tt>Diff3</tt>, and computing the union of <tt>Diff1</tt>, <tt>Diff2</tt> and <tt>Diff3</tt>:

	<pre>		<pre>

Michael Leuschel at 08:33, 24 November 2014

2014-11-24T08:33:42Z

← Older revision		Revision as of 08:33, 24 November 2014
Line 3:		Line 3:
	We will use the new feature of the REPL (available in ProB 1.4) to introduce local variables with the <tt>let</tt> construct.		We will use the new feature of the REPL (available in ProB 1.4) to introduce local variables with the <tt>let</tt> construct.
	Below we have started the REPL using <tt>probcli -repl</tt> and also using the preference <tt>-p REPL_UNICODE TRUE</tt> to display the formula again using Unicode operators (warning: this can slow down certain terminal applications). We also recommend you use the <tt>rlwrap</tt> tool available under Unix and Linux to start probcli, so that you have a command history.		Below we have started the REPL using <tt>probcli -repl</tt> and also using the preference <tt>-p REPL_UNICODE TRUE</tt> to display the formula again using Unicode operators (warning: this can slow down certain terminal applications). We also recommend you use the <tt>rlwrap</tt> tool available under Unix and Linux to start probcli, so that you have a command history.
	Every character following the <tt>>>></tt> until the end of the line is typed by the user. The next line, starting with ⇝, shows the Unicode rendering of the ASCII expression or predicate typed by the user. The lines below then show the output computed by ProB.		Every character following the <tt>>>></tt> until the end of the line is typed by the user. The next line, starting with ⇝, shows the Unicode rendering of the ASCII expression or predicate typed by the user. The lines below then show the output computed by ProB; the responses are immediate (80 ms or less for all queries below on a Mac Book Air).

Michael Leuschel at 08:31, 24 November 2014

2014-11-24T08:31:33Z

← Older revision		Revision as of 08:31, 24 November 2014
Line 131:		Line 131:

	Also, many [[Using_the_Command-Line_Version_of_ProB\|commands available for probcli]] also work inside the REPL:		Also, many [[Using_the_Command-Line_Version_of_ProB\|commands available for probcli]] also work inside the REPL:
	* <tt>-p PREF VALUE</tt> to set preference values, e.g., <tt>-p ~~MAXINT~~ 999</tt>,		* <tt>-p PREF VALUE</tt> to set preference values, e.g., <tt>-p MAX_DISPLAY_SET 999</tt> if you want the pretty printer to display sets up until size 999 in full (above the sets <tt>Diff1</tt>,... were truncated as the default value is 100,
	* <tt>-init</tt> to intialise a previously loaded specification		* <tt>-init</tt> to intialise a previously loaded specification,
	* <tt>-animate Nr</tt> to animate a certain number of steps		* <tt>-animate Nr</tt> to animate a certain number of steps,
	* <tt>-mc Nr</tt> to model check the specification, exploring at most Nr states		* <tt>-mc Nr</tt> to model check the specification, exploring at most Nr states.

Michael Leuschel at 08:48, 22 November 2014

2014-11-22T08:48:45Z

← Older revision		Revision as of 08:48, 22 November 2014
Line 130:		Line 130:
	* <tt>:q</tt> to quit the REPL.		* <tt>:q</tt> to quit the REPL.

	Also, many [[~~http://www.stups.uni-duesseldorf.de/ProB/index.php5/~~Using_the_Command-Line_Version_of_ProB\|commands available for probcli] also work inside the REPL:		Also, many [[Using_the_Command-Line_Version_of_ProB\|commands available for probcli]] also work inside the REPL:
	* <tt>-p PREF VALUE</tt>, e.g., <tt>-p MAXINT 999</tt>,		* <tt>-p PREF VALUE</tt> to set preference values, e.g., <tt>-p MAXINT 999</tt>,
	* <tt>-init</tt> to intialise a previously loaded specification		* <tt>-init</tt> to intialise a previously loaded specification
	* <tt>-animate Nr</tt> to animate a certain number of steps		* <tt>-animate Nr</tt> to animate a certain number of steps
	* <tt>-mc Nr</tt> to model check the specification, exploring at most Nr states		* <tt>-mc Nr</tt> to model check the specification, exploring at most Nr states

Michael Leuschel at 08:47, 22 November 2014

2014-11-22T08:47:40Z

← Older revision		Revision as of 08:47, 22 November 2014
Line 129:		Line 129:
	* <tt>:r</tt> to reload a previously loaded B specification (above we did not load any specification), and		* <tt>:r</tt> to reload a previously loaded B specification (above we did not load any specification), and
	* <tt>:q</tt> to quit the REPL.		* <tt>:q</tt> to quit the REPL.

			Also, many [[http://www.stups.uni-duesseldorf.de/ProB/index.php5/Using_the_Command-Line_Version_of_ProB\|commands available for probcli] also work inside the REPL:
			* <tt>-p PREF VALUE</tt>, e.g., <tt>-p MAXINT 999</tt>,
			* <tt>-init</tt> to intialise a previously loaded specification
			* <tt>-animate Nr</tt> to animate a certain number of steps
			* <tt>-mc Nr</tt> to model check the specification, exploring at most Nr states

Michael Leuschel at 08:41, 22 November 2014

2014-11-22T08:41:29Z

← Older revision		Revision as of 08:41, 22 November 2014
Line 109:		Line 109:
	</pre>		</pre>

	Note, you can browse command ~~can be used~~ to show our ~~definitions~~:		Note, you can use the browse command <tt>:b</tt> to show the let definitions, and any other identifier available (in our case none, as we have not loaded any pre-existing B specification):
	<pre>		<pre>
	>>> :b		>>> :b
Line 125:		Line 125:
	</pre>		</pre>

	Other useful REPL commands are <tt>:t EXPR</tt> to display the type of an expression, <tt>:r</tt> to reload a previously loaded B specification (above we did not load any specification), and <tt>:q</tt> to quit the REPL.		Other useful REPL commands are:
			* <tt>:t EXPR</tt> to display the type of an expression,
			* <tt>:r</tt> to reload a previously loaded B specification (above we did not load any specification), and
			* <tt>:q</tt> to quit the REPL.

Michael Leuschel at 08:39, 22 November 2014

2014-11-22T08:39:29Z

← Older revision		Revision as of 08:39, 22 November 2014
Line 3:		Line 3:
	We will use the new feature of the REPL (available in ProB 1.4) to introduce local variables with the <tt>let</tt> construct.		We will use the new feature of the REPL (available in ProB 1.4) to introduce local variables with the <tt>let</tt> construct.
	Below we have started the REPL using <tt>probcli -repl</tt> and also using the preference <tt>-p REPL_UNICODE TRUE</tt> to display the formula again using Unicode operators (warning: this can slow down certain terminal applications). We also recommend you use the <tt>rlwrap</tt> tool available under Unix and Linux to start probcli, so that you have a command history.		Below we have started the REPL using <tt>probcli -repl</tt> and also using the preference <tt>-p REPL_UNICODE TRUE</tt> to display the formula again using Unicode operators (warning: this can slow down certain terminal applications). We also recommend you use the <tt>rlwrap</tt> tool available under Unix and Linux to start probcli, so that you have a command history.
			Every character following the <tt>>>></tt> until the end of the line is typed by the user. The next line, starting with ⇝, shows the Unicode rendering of the ASCII expression or predicate typed by the user. The lines below then show the output computed by ProB.


Line 45:		Line 46:
	</pre>		</pre>

	Now, we will try and complete the constraints and ~~add the~~ co-ordinates within each sub-square:		Now, we will try and complete the constraints and put pairs of co-ordinates within each sub-square into the variable <tt>Diff3</tt>, and computing the union of <tt>Diff1</tt>, <tt>Diff2</tt> and <tt>Diff3</tt>:

	<pre>		<pre>
Line 58:		Line 59:
	</pre>		</pre>

	A full Sudoku solution can now be found:		A full Sudoku solution, with distinct values in each row, column and sub-square, can now be found as follows:
	<pre>		<pre>
	>>> Board : DOM --> (DOM --> DOM) & !(x1,x2,y1,y2).((x1,x2,y1,y2):Diff => Board(x1)(y1) /= Board(x2)(y2))		>>> Board : DOM --> (DOM --> DOM) & !(x1,x2,y1,y2).((x1,x2,y1,y2):Diff => Board(x1)(y1) /= Board(x2)(y2))
Line 67:		Line 68:
	</pre>		</pre>

	Let us now try and add some additional constraints for certain positions on the board:		Let us now try and add some additional constraints for certain pre-established positions on the board, and put those into the variable <tt>P</tt> and require that the solution <tt>Board</tt> contains those values:
	<pre>		<pre>
	>>> let P = {(1,1,7), (1,2,8), (1,3,1), (2,1,9)}		>>> let P = {(1,1,7), (1,2,8), (1,3,1), (2,1,9)}
Line 80:		Line 81:
	</pre>		</pre>

	~~Let us now check that inconsistencies are detected:~~
	~~<pre>~~
	~~>>> let P = {(1,1,7), (1,2,8), (1,3,1), (2,1,9), (2,2,9)}~~
	~~⇝ {((1↦1)↦7),((1↦2)↦8),((1↦3)↦1),((2↦1)↦9),((2↦2)↦9)}~~
	~~Expression Value =~~
	~~{((1\|->1)\|->7),((1\|->2)\|->8),((1\|->3)\|->1),((2\|->1)\|->9),((2\|->2)\|->9)}~~
	~~>>> Board : DOM --> (DOM --> DOM) & !(x1,x2,y1,y2).((x1,x2,y1,y2):Diff => Board(x1)(y1) /= Board(x2)(y2)) & !(x,y,z).((x,y,z):P => Board(x)(y)=z)~~
	⇝ ∃(Board).((Board ∈ DOM → (DOM → DOM) ∧ ∀(x1,x2,y1,y2).((((x1 ∈ ℤ ∧ x2 ∈ ℤ) ∧ y1 ∈ ℤ) ∧ y2 ∈ ℤ) ∧ ((x1 ↦ x2) ↦ y1) ↦ y2 ∈ Diff ⇒ Board(x1)(y1) ≠ Board(x2)(y2))) ∧ ∀(x,y,z).(((x ∈ ℤ ∧ y ∈ ℤ) ∧ z ∈ ℤ) ∧ (x ↦ y) ↦ z ∈ P ⇒ Board(x)(y) = z))
	~~Existentially Quantified Predicate over Board is FALSE~~
	~~</pre>~~

	You can visualise the solution using the show command of the REPL:		You can visualise the solution using the show command of the REPL:
Line 106:		Line 97:
	</pre>		</pre>

	~~The~~ browse command can be used to show our definitions:
			Let us now check that inconsistencies are detected by our tool:
			<pre>
			>>> let P = {(1,1,7), (1,2,8), (1,3,1), (2,1,9), (2,2,9)}
			⇝ {((1↦1)↦7),((1↦2)↦8),((1↦3)↦1),((2↦1)↦9),((2↦2)↦9)}
			Expression Value =
			{((1\|->1)\|->7),((1\|->2)\|->8),((1\|->3)\|->1),((2\|->1)\|->9),((2\|->2)\|->9)}
			>>> Board : DOM --> (DOM --> DOM) & !(x1,x2,y1,y2).((x1,x2,y1,y2):Diff => Board(x1)(y1) /= Board(x2)(y2)) & !(x,y,z).((x,y,z):P => Board(x)(y)=z)
			⇝ ∃(Board).((Board ∈ DOM → (DOM → DOM) ∧ ∀(x1,x2,y1,y2).((((x1 ∈ ℤ ∧ x2 ∈ ℤ) ∧ y1 ∈ ℤ) ∧ y2 ∈ ℤ) ∧ ((x1 ↦ x2) ↦ y1) ↦ y2 ∈ Diff ⇒ Board(x1)(y1) ≠ Board(x2)(y2))) ∧ ∀(x,y,z).(((x ∈ ℤ ∧ y ∈ ℤ) ∧ z ∈ ℤ) ∧ (x ↦ y) ↦ z ∈ P ⇒ Board(x)(y) = z))
			Existentially Quantified Predicate over Board is FALSE
			</pre>

			Note, you can browse command can be used to show our definitions:
	<pre>		<pre>
	>>> :b		>>> :b
Line 121:		Line 124:
	P = {((1\|->1)\|->7),((1\|->2)\|->8),((1\|->3)\|->1),((2\|->1...		P = {((1\|->1)\|->7),((1\|->2)\|->8),((1\|->3)\|->1),((2\|->1...
	</pre>		</pre>

			Other useful REPL commands are <tt>:t EXPR</tt> to display the type of an expression, <tt>:r</tt> to reload a previously loaded B specification (above we did not load any specification), and <tt>:q</tt> to quit the REPL.

Michael Leuschel at 08:29, 22 November 2014

2014-11-22T08:29:23Z

← Older revision		Revision as of 08:29, 22 November 2014
Line 1:		Line 1:
	For this example we try and solve a Sudoku using the REPL (Read-Eval-Print-Loop) of ProB only, without constructing any B machine. The REPL can either be started using probcli's command <tt>-repl</tt> or by starting the [[Eval_Console\|Eval Console in ProB Tcl/Tk]].		For this example we try and solve a [http://en.wikipedia.org/wiki/Sudoku Sudoku] using the REPL (Read-Eval-Print-Loop) of ProB only, without constructing any B machine. The REPL can either be started using probcli's command <tt>-repl</tt> or by starting the [[Eval_Console\|Eval Console in ProB Tcl/Tk]].

	We will use the new feature of the REPL (available in ProB 1.4) to introduce local variables with the <tt>let</tt> construct.		We will use the new feature of the REPL (available in ProB 1.4) to introduce local variables with the <tt>let</tt> construct.
	Below we have started the REPL using <tt>probcli -repl</tt> and also using the preference <tt>-p REPL_UNICODE TRUE</tt> to display the formula again using Unicode operators (warning: this can slow down certain ~~terminals~~). We also recommend you use the <tt>rlwrap</tt> tool available under Unix and Linux to have a command history.		Below we have started the REPL using <tt>probcli -repl</tt> and also using the preference <tt>-p REPL_UNICODE TRUE</tt> to display the formula again using Unicode operators (warning: this can slow down certain terminal applications). We also recommend you use the <tt>rlwrap</tt> tool available under Unix and Linux to start probcli, so that you have a command history.


Line 9:		Line 9:
	Type ":help" for more information.		Type ":help" for more information.

	First let us define two useful values:		First let us define two useful values: the domain <tt>DOM</tt> for the numbers to be put inside the Sudoku and the group of indices <tt>SUBSQ</tt> which can be used to construct the 3x3 sub-squares:
	<pre>		<pre>
	>>> let DOM = 1..9		>>> let DOM = 1..9
Line 21:		Line 21:
	</pre>		</pre>

	Now let us encode in Diff1 and Diff2 coordinates at which the values on the Sudoku board have to be different:		Now let us encode in <tt>Diff1</tt> and <tt>Diff2</tt> sets of pairs of coordinates at which the values on the Sudoku board have to be different (because they lie on the same column or row respectively):

	<pre>		<pre>
Line 34:		Line 34:
	</pre>		</pre>

	We have not yet encoded that in each sub square the values must also all be distinct.		We have not yet encoded that in each sub-square the values must also all be distinct.
	Nonetheless, let us try and solve the puzzle as it stands:		Nonetheless, let us try and solve the puzzle as it stands, by looking for a full board (of type <tt>DOM --> (DOM --> DOM)</tt>) which has distinct values on each row and column:

	<pre>		<pre>

Michael Leuschel at 09:05, 11 July 2014

2014-07-11T09:05:28Z

@@ Line 89: / Line 89: @@
   ⇝  ∃(Board).((Board ∈ DOM → (DOM → DOM) ∧ ∀(x1,x2,y1,y2).((((x1 ∈ ℤ ∧ x2 ∈ ℤ) ∧ y1 ∈ ℤ) ∧ y2 ∈ ℤ) ∧ ((x1 ↦ x2) ↦ y1) ↦ y2 ∈ Diff ⇒ Board(x1)(y1) ≠ Board(x2)(y2))) ∧ ∀(x,y,z).(((x ∈ ℤ ∧ y ∈ ℤ) ∧ z ∈ ℤ) ∧ (x ↦ y) ↦ z ∈ P ⇒ Board(x)(y) = z))
 Existentially Quantified Predicate over Board is FALSE
 </pre>

Michael Leuschel at 16:12, 10 July 2014

2014-07-10T16:12:28Z

← Older revision		Revision as of 16:12, 10 July 2014
Line 58:		Line 58:
	</pre>		</pre>

	A solution can now be found:		A full Sudoku solution can now be found:
	<pre>		<pre>
	>>> Board : DOM --> (DOM --> DOM) & !(x1,x2,y1,y2).((x1,x2,y1,y2):Diff => Board(x1)(y1) /= Board(x2)(y2))		>>> Board : DOM --> (DOM --> DOM) & !(x1,x2,y1,y2).((x1,x2,y1,y2):Diff => Board(x1)(y1) /= Board(x2)(y2))