diff --git a/Sudoku/SudokuEvent.mch b/Sudoku/SudokuEvent.mch index f4d2c65595200562e6cd652b007b58d729fba933..74dad17e30a3335cfe684995fbbce9b14a2b7e65 100644 --- a/Sudoku/SudokuEvent.mch +++ b/Sudoku/SudokuEvent.mch @@ -28,20 +28,20 @@ DEFINITIONS MAX_OPERATIONS_SetBoard == 10; /* PUZZLE CONSTRAINTS : */ -PUZZLE == ( + PUZZLE(BOARD) == ( - Board(1)(1)=7 & Board(1)(2)=8 & Board(1)(3)=1 & Board(1)(4)=6 & Board(1)(6)=2 - & Board(1)(7)=9 & Board(1)(9) = 5 & - Board(2)(1)=9 & Board(2)(3)=2 & Board(2)(4)=7 & Board(2)(5)=1 & - Board(3)(3)=6 & Board(3)(4)=8 & Board(3)(8)=1 & Board(3)(9)=2 & + BOARD(1)(1)=7 & BOARD(1)(2)=8 & BOARD(1)(3)=1 & BOARD(1)(4)=6 & BOARD(1)(6)=2 + & BOARD(1)(7)=9 & BOARD(1)(9)=5 & + BOARD(2)(1)=9 & BOARD(2)(3)=2 & BOARD(2)(4)=7 & BOARD(2)(5)=1 & + BOARD(3)(3)=6 & BOARD(3)(4)=8 & BOARD(3)(8)=1 & BOARD(3)(9)=2 & - Board(4)(1)=2 & Board(4)(4)=3 & Board(4)(7)=8 & Board(4)(8)=5 & Board(4)(9)=1 & - Board(5)(2)=7 & Board(5)(3)=3 & Board(5)(4)=5 & Board(5)(9)=4 & - Board(6)(3)=8 & Board(6)(6)=9 & Board(6)(7)=3 & Board(6)(8)=6 & + BOARD(4)(1)=2 & BOARD(4)(4)=3 & BOARD(4)(7)=8 & BOARD(4)(8)=5 & BOARD(4)(9)=1 & + BOARD(5)(2)=7 & BOARD(5)(3)=3 & BOARD(5)(4)=5 & BOARD(5)(9)=4 & + BOARD(6)(3)=8 & BOARD(6)(6)=9 & BOARD(6)(7)=3 & BOARD(6)(8)=6 & - Board(7)(1)=1 & Board(7)(2)=9 & Board(7)(6)=7 & Board(7)(8)=8 & - Board(8)(1)=8 & Board(8)(2)=6 & Board(8)(3)=7 & Board(8)(6)=3 & Board(8)(7)=4 & Board(8)(9)=9 & - Board(9)(3)=5 & Board(9)(7)=1 + BOARD(7)(1)=1 & BOARD(7)(2)=9 & BOARD(7)(6)=7 & BOARD(7)(8)=8 & + BOARD(8)(1)=8 & BOARD(8)(2)=6 & BOARD(8)(3)=7 & BOARD(8)(6)=3 & BOARD(8)(7)=4 & BOARD(8)(9)=9 & + BOARD(9)(3)=5 & BOARD(9)(7)=1 ); UnassignedPosition(x,y) == x:DOM & y:DOM & not(y:dom(Board(x))); @@ -49,8 +49,10 @@ PUZZLE == ( 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" */ + conflict_pos_sym /*@desc "symmetry-reduced version of conflict_pos" */, + PuzzleBoard /*@desc "Stored Puzzle" */ PROPERTIES + PuzzleBoard : DOM --> (DOM +-> RAN) & PUZZLE(PuzzleBoard) & 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) & @@ -72,11 +74,11 @@ INVARIANT curx : DOM & cury : DOM INITIALISATION - Board : (Board : DOM --> (DOM +-> RAN) & PUZZLE) || + Board := PuzzleBoard || curx, cury := 1,1 OPERATIONS SetEmpty = BEGIN Board := %i.(i:DOM|{}) END; - SetPuzzle = BEGIN Board : (Board : DOM --> (DOM +-> RAN) & PUZZLE) END; + SetPuzzle = BEGIN Board := PuzzleBoard END; SetCurPos(x,y) = PRE x:DOM & y:DOM THEN diff --git a/Sudoku/SudokuFeld.svg b/Sudoku/SudokuFeld.svg index eb1279c8920106f6c4e2517c2d34d8cb8305e628..1e63b66b23edfb747c17bf5011d441be620362a3 100644 --- a/Sudoku/SudokuFeld.svg +++ b/Sudoku/SudokuFeld.svg @@ -13,6 +13,11 @@ stroke-width : 0.1; fill : white } + .fixed { + stroke : lightgray; + stroke-width : 0.1; + fill : white + } .selected { stroke : gray; stroke-width : 0.1; diff --git a/Sudoku/visb_sudoku.json b/Sudoku/visb_sudoku.json index 9a792e53dfbf141f46fc9d9c3cfd4aec00b73e11..278f8485b0b68ce46b6a497d03b1ea57522d1611 100644 --- a/Sudoku/visb_sudoku.json +++ b/Sudoku/visb_sudoku.json @@ -19,7 +19,6 @@ "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 %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},