diff --git a/Sudoku/SudokuEvent.mch b/Sudoku/SudokuEvent.mch
index 0303435bb3343a0d1cfd8637d196b36f750afd6d..1ee706d19de1e571f0fa6a703e0f004d87b32b25 100644
--- a/Sudoku/SudokuEvent.mch
+++ b/Sudoku/SudokuEvent.mch
@@ -7,7 +7,8 @@ DEFINITIONS
DOM == 1..Mx; D1 == 1..(Mx-1); D2 == 2..Mx ;
RAN == (1..Mx);
SET_PREF_MAXINT == 3; SET_PREF_TIME_OUT == 45000;
- SUBSQ == ran(%i.(i:1..Sze | ((i-1)*Sze+1)..i*Sze));
+ SUBSQS == %i.(i:1..Sze | ((i-1)*Sze+1)..i*Sze);
+ SUBSQ == ran(SUBSQS);
ANIMATION_FUNCTION_DEFAULT == {r,c,i|r:1..Mx & c:1..Mx & i=16};
ANIMATION_FUNCTION == ( {r,c,i|r:DOM & c:DOM & i:RAN & i = Board(r)(c)} );
ANIMATION_IMG0 == "images/sm_0.gif";
@@ -40,10 +41,29 @@ PUZZLE == (
Board(9)(3)=5 & Board(9)(7)=1
);
- UnassignedPosition(x,y) == x:DOM & y:DOM & not(y:dom(Board(x)))
+ UnassignedPosition(x,y) == x:DOM & y:DOM & not(y:dom(Board(x)));
+
+CONSTANTS
+ get_square /*@desc "Subsquare (1,2,3) for a coordinate 1..9" */,
+ conflict_pos /*@desc "set of positions that are in conflict with a given position" */,
+ conflict_pos_sym /*@desc "symmetry-reduced version of conflict_pos" */
+PROPERTIES
+ get_square = %x.(x:DOM | 1 + (x-1)/3) /*@desc "Get square (1,2,3) for a coordinate 1..9" */
+ &
+ conflict_pos = %(x,y).(x:DOM & y:DOM | {x2,y2 | x2:DOM & y2:DOM & (x,y) /= (x2,y2) &
+ (x=x2 // same line
+ or
+ y=y2 // same row
+ or
+ (get_square(x) = get_square(x2) &
+ get_square(y) = get_square(y2) )
+ )
+ })
+ &
+ conflict_pos_sym = %(x,y).(x:DOM & y:DOM | {x2,y2| x2|->y2 : conflict_pos(x,y) & (x<x2 or (x=x2 & y<y2))})
VARIABLES
Board,
- curx, cury
+ curx, cury // current position on the board for making changes
INVARIANT
Board : DOM --> (DOM +-> RAN) &
curx : DOM &
@@ -53,39 +73,28 @@ INITIALISATION
curx, cury := 1,1
OPERATIONS
SetEmpty = BEGIN Board := %i.(i:DOM|{}) END;
-
SetPuzzle = BEGIN Board : (Board : DOM --> (DOM +-> RAN) & PUZZLE) END;
- //val <-- GetBoard(x,y) = PRE x:DOM & y:dom(Board(x)) THEN val := Board(x)(y) END;
SetCurPos(x,y) = PRE x:DOM & y:DOM THEN
- curx, cury := x,y
+ curx, cury := x,y // change current position
END;
SetBoard(val) = PRE val:RAN THEN
- Board(curx)(cury) := val // Set the Value at a given board position
+ Board(curx)(cury) := val // Set the Value at the current position
+ END;
+ ClearCurPos = BEGIN
+ Board(curx) := {cury} <<| Board(curx) // clear the value at the current position
END;
- solve(SBoard) = PRE
+ Solve(SBoard) = PRE
SBoard : DOM --> (DOM --> RAN) /*@desc "The solution must be complete" */ &
!(x,y).(y:dom(Board(x))
=> SBoard(x)(y) = Board(x)(y)) /*@desc "Copy partial solution (Board variable)" */ &
- !y.(y:DOM =>
- LET By BE By = SBoard(y) IN
- !(x1).(x1:D1
- => !x2.(x1<x2 & x2:D2
- => (SBoard(x1)(y) /= SBoard(x2)(y) &
- By(x1) /= By(x2)))
- )
- END
- ) /*@desc "Values are distinct on all columns and rows" */
- &
- !(s1,s2).(s1:SUBSQ & s2:SUBSQ => !x1.(x1:s1 =>
- !(y1,x2,y2).( (x1:s1 & x2:s1 & x1>=x2 & y1:s2 & y2:s2 & (x1=x2 => y1>y2)
- & (x1,y1) /= (x2,y2) )
- =>
- SBoard(x1)(y1) /= SBoard(x2)(y2)
- )
- ) ) /*@desc "Values are all distinct within each Sub-Square" */
+ !(x,y).(x:DOM & y:DOM =>
+ !(x2,y2).(x2|->y2: conflict_pos_sym(x,y)
+ => SBoard(x)(y) /= SBoard(x2)(y2)
+ )
+ )
THEN
Board := SBoard
END
diff --git a/Sudoku/SudokuFeld.svg b/Sudoku/SudokuFeld.svg
index efd7b12b32a46da1a22fdea8dc5601c671bb2252..cbefc9c1fab6e168449106d35a105e5bea8a8bea 100644
--- a/Sudoku/SudokuFeld.svg
+++ b/Sudoku/SudokuFeld.svg
@@ -16,7 +16,7 @@
.selected {
stroke : black;
stroke-width : 0.1;
- fill : lightgray
+ fill : thistle
}
.wrong {
stroke : red;
@@ -26,7 +26,7 @@
.hover {
stroke : black;
stroke-width : 0.1;
- fill : yellow
+ fill : whitesmoke
}
.normalKeypad {
fill : lightgray
diff --git a/Sudoku/visb_sudoku.json b/Sudoku/visb_sudoku.json
index f62a358eae0904f8c025003f9c94094691a052b7..3e09fb970c879b38aa1c135ee1c8270160873b7e 100644
--- a/Sudoku/visb_sudoku.json
+++ b/Sudoku/visb_sudoku.json
@@ -19,7 +19,7 @@
"repeat": [1,2,3,4,5,6,7,8,9],
"id": "board_%0_%1",
"attr": "class",
- "value" : "IF curx=%0 & cury=%1 THEN \"selected\" ELSIF %1:dom(Board(%0)) & (curx=%0 or cury=%1) & BOARD(%0)(%1)=BOARD(curx)(cury) THEN \"wrong\" ELSE \"normal\" END"
+ "value" : "IF curx=%0 & cury=%1 THEN \"selected\" ELSIF %0|->%1:conflict_pos(curx,cury) THEN IF %1:dom(Board(%0)) & BOARD(%0)(%1)=BOARD(curx)(cury) THEN \"wrong\" ELSE \"hover\" END ELSE \"normal\" END"
},
{
"for": {"from":1, "to":9},
@@ -46,6 +46,18 @@
"predicates" : ["val=%0"],
"hovers": [{ "attr":"class", "enter":"hoverKeypad", "leave":"normalKeypad"}
]
+ },
+ {
+ "id": "Solve",
+ "event": "Solve",
+ "hovers": [{ "attr":"class", "enter":"hoverKeyboard", "leave":"normalKeyboard"}
+ ]
+ },
+ {
+ "id": "Remove",
+ "event": "ClearCurPos",
+ "hovers": [{ "attr":"class", "enter":"hoverKeyboard", "leave":"normalKeyboard"}
+ ]
}
]
}