Sudoku - Revision history

Assaf: /* Playing b-threads */

2014-04-29T09:48:39Z

‎Playing b-threads

BpAdmin at 08:35, 29 April 2014

2014-04-29T08:35:50Z

Assaf: /* Design Notes */

2014-04-15T11:41:30Z

‎Design Notes

Assaf: /* Events */

2014-04-15T11:40:36Z

‎Events

Assaf: /* Events */

2014-04-15T11:18:33Z

‎Events

Assaf at 11:18, 15 April 2014

2014-04-15T11:18:07Z

Assaf: Created page with "= Sudoku = In this example one can see two properties of behavioral programming * How different heuristics and pieces of knowledge about the problem domain can be used separ..."

2014-04-15T11:17:37Z

Created page with "= Sudoku = In this example one can see two properties of behavioral programming * How different heuristics and pieces of knowledge about the problem domain can be used separ..."

New page

= Sudoku =
In this example one can see two properties of behavioral programming
* How different heuristics and pieces of knowledge about the problem domain can be used separately to program an application
* How model-checking can be used to help find a desired scenario.

= Requirements =
In the cells of a 9X9 grid which is also divided into 9 3X3 boxes, place the digits 1-9 such that in each row, column and box, each digit appears exactly once.

= Events =

* Move: A single event class with 9X9X9 = 721 instances. The class has 5 data fields:
** number: the number written in the cell (1-9)
** row: The row of the cell (1-9)
** col: the column of the cell (1-9)
** boxrow: The row of the 3X3 box in which this cell resides (1-3)
** boxcol: the column of the 3X3 box in which this cell resides (1-3)

The triggering of the event symbolizes the writing of the digit in the associated cell.

== b-threads ==
* DefaultMove: Each of the 81 instances of this b-thread class, is associated with a cell, and requests all possible 9 digits

@@ Line 27: / Line 27: @@
 * PlaceANumberInARow: With an instance for each digit and each row, this b-thread tries to place a particular digit in the row. It waits till there is only one place to put it, and then requests the corresponding event.
 * PlaceANumberInAColumn: With an instance for each digit and each row, this b-thread tries to place a particular digit in the Column. It waits till there is only one place to put it,  and then requests the corresponding event.
 * EliminateEight: For each cell, an instance of this b-thread checks the possibilities for the cell, and eliminates possibilities as conflicting events occur elsewhere. When the number of remaining possibilities is one, the b-thread requests the remaining digit.
 == b-threads that support model-checking ==

@@ Line 9: / Line 9: @@
 = Events =
 * Move: A single event class with 9X9X9 = 721 instances, indicating the writing of a given digit in a given cell. The class has the following data fields:
 ** number: the digit written in the cell  (1-9)
@@ Line 17: / Line 17: @@
 ** boxcol: the column of the 3X3 box in which this cell resides (1-3)
 When enough data is provided, the strategies below are sufficient for solving the game.
 When not enough data is provided, model checking explores the different possibilities until a solution is found.
 == Playing b-threads ==
 * MakeGivenMoves: This b-thread provides the opening input to the riddle - filling in the known cells.
 * DefaultMove: Each of the 81 instances of this b-thread class, is associated with a cell, and requests all possible 9 digits. Once an event occurs, all other events for the cell are blocked.
 * DetectWin: This b-thread simply counts until 81 events have been triggered. The correctness of the solution is guaranteed
 * EliminateTwoInABox: This b-thread tries to write a number in a cell after  the same number was written in two other columns of this box. It does not check if the cell is occopied or if the digit was already written in the present column - this is provided by event-blocking in other b-threads.
 * PlaceANumberInARow: With an instance for each digit and each row, this b-thread tries to place a particular digit in the row. It waits till there is only one place to put it, and then requests the corresponding event.
 * PlaceANumberInAColumn: With an instance for each digit and each row, this b-thread tries to place a particular digit in the Column. It waits till there is only one place to put it,  and then requests the corresponding event.
 * EliminateEight: For each cell, an instance of this b-thread checks the possibilities for the cell, and eliminates possibilities as conflicting events occur elsewhere. When the number of remaining possibilities is one, the b-thread requests the remaining digit.
 == b-threads that support model-checking ==
 PruneWhenNoSolution: This b-thread requests an event at a low priority. If it is triggered, it means that all move events are blocked, hence the game has failed. It then calls the model-checking API to prune the search.
-−
 == Design Notes ==
 * The b-thread DefaultMove could have been split into two. One that requests the default moves and terminates, and one that waits for any event in a cell and blocks all alternative digits in the cell. The present design works because a pending request of DefaultMove is unified with any granted request due to the stratgies/heuristics b-threads, as well as the GivenMoves b-thread.

← Older revision		Revision as of 11:41, 15 April 2014
Line 34:		Line 34:


−	== Design Notes ==	+	== Design Notes ==
−	* The b-thread DefaultMove could have been split into two. One that requests the default moves and terminates, and one that waits for any event in a cell and blocks all alternative digits in the cell. The present design works because a pending request of DefaultMove is unified with any granted request due to the stratgies/heuristics b-threads.	+	* The b-thread DefaultMove could have been split into two. One that requests the default moves and terminates, and one that waits for any event in a cell and blocks all alternative digits in the cell. The present design works because a pending request of DefaultMove is unified with any granted request due to the stratgies/heuristics b-threads, as well as the GivenMoves b-thread.

@@ Line 9: / Line 9: @@
 = Events =
-* Move: A single event class with 9X9X9 = 721 instances. The class has 5 data fields:
+* Move: A single event class with 9X9X9 = 721 instances, indicating the writing of a given digit in a given cell. The class has the following data fields:
-** number: the number written in the cell  (1-9)
 ** row: The row  of the cell (1-9)
 ** col: the column of the cell  (1-9)
 ** boxrow: The row of the 3X3 box in which this cell resides (1-3)
 ** boxcol: the column of the 3X3 box in which this cell resides (1-3)
-== b-threads ==
+== Design Notes ==
-* DefaultMove: Each of the 81 instances of this b-thread class, is associated with a cell, and requests all possible 9 digits
+* The b-thread DefaultMove could have been split into two. One that requests the default moves and terminates, and one that waits for any event  in a cell and blocks all alternative digits in the cell. The present design works because a pending request of DefaultMove is unified with any granted request due to the stratgies/heuristics b-threads.