diff --git a/Sudoku/AnimationDefs.def b/Sudoku/AnimationDefs.def new file mode 100644 index 0000000000000000000000000000000000000000..d9c33b68407d11f380bb08a450c3ab09cc37d8ad --- /dev/null +++ b/Sudoku/AnimationDefs.def @@ -0,0 +1,20 @@ +DEFINITIONS + SET_PREF_MAXINT == 3; SET_PREF_TIME_OUT == 15000; + VISB_JSON_FILE == "visb_sudoku.json"; + + 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"; + ANIMATION_IMG1 == "images/sm_1.gif"; + ANIMATION_IMG2 == "images/sm_2.gif"; + ANIMATION_IMG3 == "images/sm_3.gif"; + ANIMATION_IMG4 == "images/sm_4.gif"; + ANIMATION_IMG5 == "images/sm_5.gif"; + ANIMATION_IMG6 == "images/sm_6.gif"; + ANIMATION_IMG7 == "images/sm_7.gif"; + ANIMATION_IMG8 == "images/sm_8.gif"; + ANIMATION_IMG9 == "images/sm_9.gif"; + ANIMATION_IMG16 == "images/sm_empty_box.gif"; + SET_PREF_MAX_OPERATIONS == 1; + MAX_OPERATIONS_SetCurPos == 82; + MAX_OPERATIONS_SetBoard == 10; \ No newline at end of file diff --git a/Sudoku/SudokuEvent.mch b/Sudoku/SudokuEvent.mch index 000d53d1d11ebd0c0a94179093d1dc07ba396448..e1d58cc6390e3f826481070a417e55b93c595272 100644 --- a/Sudoku/SudokuEvent.mch +++ b/Sudoku/SudokuEvent.mch @@ -1,32 +1,15 @@ MACHINE SudokuEvent /* A version of Sudoku where the solving happens inside an event - (c) 2021 Michael Leuschel + (c) 2021-2022 Michael Leuschel VisB Visualisation by Matteo Röhle and Michael Leuschel */ DEFINITIONS Sze == 3; Mx==(Sze*Sze); DOM == 1..Mx; D1 == 1..(Mx-1); D2 == 2..Mx ; RAN == (1..Mx); - SET_PREF_MAXINT == 3; SET_PREF_TIME_OUT == 15000; - VISB_JSON_FILE == "visb_sudoku.json"; 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"; - ANIMATION_IMG1 == "images/sm_1.gif"; - ANIMATION_IMG2 == "images/sm_2.gif"; - ANIMATION_IMG3 == "images/sm_3.gif"; - ANIMATION_IMG4 == "images/sm_4.gif"; - ANIMATION_IMG5 == "images/sm_5.gif"; - ANIMATION_IMG6 == "images/sm_6.gif"; - ANIMATION_IMG7 == "images/sm_7.gif"; - ANIMATION_IMG8 == "images/sm_8.gif"; - ANIMATION_IMG9 == "images/sm_9.gif"; - ANIMATION_IMG16 == "images/sm_empty_box.gif"; - SET_PREF_MAX_OPERATIONS == 1; - MAX_OPERATIONS_SetCurPos == 82; - MAX_OPERATIONS_SetBoard == 10; + "AnimationDefs.def"; /* PUZZLE CONSTRAINTS : */ PUZZLE1 == @@ -84,7 +67,7 @@ PROPERTIES 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 // current position on the board for making changes + curx, cury // current (cursor) position on the board for making changes INVARIANT Board : DOM --> (DOM +-> RAN) & curx : DOM & @@ -122,9 +105,9 @@ OPERATIONS !(x,y).(x:DOM & y:DOM => !(x2,y2).(x2|->y2: conflict_pos_sym(x,y) => SBoard(x)(y) /= SBoard(x2)(y2) - ) + ) /*@desc "The value must be different from that of all conflict positions" */ ) THEN - Board := SBoard + Board := SBoard // set the board to the found solution END END \ No newline at end of file diff --git a/Sudoku/SudokuEventUnicode.mch b/Sudoku/SudokuEventUnicode.mch new file mode 100644 index 0000000000000000000000000000000000000000..8e2cef0095971e198d7aedb70945c6f85846b042 --- /dev/null +++ b/Sudoku/SudokuEventUnicode.mch @@ -0,0 +1,126 @@ +MACHINE SudokuEventUnicode +/* A version of Sudoku where the solving happens inside an event + (c) 2021-2022 Michael Leuschel + VisB Visualisation by Matteo Röhle and Michael Leuschel +*/ +DEFINITIONS + Sze == 3; Mx==(Sze*Sze); + DOM == 1..Mx; D1 == 1..(Mx-1); D2 == 2..Mx ; + RAN == (1..Mx); + SUBSQS == λi.(i∈1..Sze | ((i-1)*Sze+1)..i*Sze); + SUBSQ == ran(SUBSQS); + "AnimationDefs.def"; + + /* PUZZLE CONSTRAINTS : */ + PUZZLE1 == + {(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(6↦2),(7↦9),(9↦5)}), + (2↦{(1↦9),(3↦2),(4↦7),(5↦1)}), + (3↦{(3↦6),(4↦8),(8↦1),(9↦2)}), + (4↦{(1↦2),(4↦3),(7↦8),(8↦5),(9↦1)}), + (5↦{(2↦7),(3↦3),(4↦5),(9↦4)}),(6↦{(3↦8),(6↦9),(7↦3),(8↦6)}), + (7↦{(1↦1),(2↦9),(6↦7),(8↦8)}), + (8↦{(1↦8),(2↦6),(3↦7),(6↦3),(7↦4),(9↦9)}), + (9↦{(3↦5),(7↦1)})} + ; + PUZZLE2 == + {(1↦{(1↦1),(2↦3),(4↦8),(5↦6),(6↦5),(9↦9)}), + (2↦{(3↦8),(6↦4),(7↦1),(9↦2)}), + (3↦{(4↦1),(5↦2)}), + (4↦{(3↦7),(4↦6),(7↦9),(9↦3)}), + (5↦{(1↦9),(2↦1),(3↦5),(4↦4),(8↦8),(9↦7)}), + (6↦{(1↦6),(3↦3),(5↦1),(6↦7),(8↦5)}), + (7↦{(7↦3),(8↦4),(9↦5)}), + (8↦{(3↦6),(4↦7),(6↦3),(7↦8),(8↦9)}), + (9↦{(3↦9),(5↦8),(9↦6)})}; + + PUZZLE3 == + {(1↦{(2↦4),(3↦3),(6↦5),(8↦8),(9↦7)}), + (2↦{(2↦9),(6↦3)}),(3↦{(5↦2),(8↦1)}),(4↦{(3↦9),(4↦8),(9↦5)}), + (5↦{(2↦5),(3↦8),(8↦2),(9↦6)}), + (6↦{(2↦7),(4↦2)}), + (7↦{(1↦5),(2↦8),(4↦1),(6↦2),(7↦4),(8↦7)}), + (8↦{(9↦3)}),(9↦{(1↦9),(2↦1),(4↦7),(5↦6),(7↦5)})} + ; + + PossibleVals(cx,cy) == // locally possible values by examining all direct neighbouring conflict positions + DOM \ ran({x,y,r| x↦y ∈ conflict_pos(cx,cy) ∧ y∈dom(Board(x)) ∧ r=Board(x)(y)}) +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" */, + PuzzleBoard /*@desc "Stored Puzzle" */ +PROPERTIES + PuzzleBoard ∈ DOM → (DOM ⇸ RAN) ∧ + PuzzleBoard ∈ {PUZZLE1,PUZZLE2,PUZZLE3} /*@desc "Provide three possible starting boards" */ ∧ + get_square = λx.(x∈DOM | 1 + (x-1)/3) /*@desc "Get square number (1..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 + ∨ + y=y2 // same row + or // same square + (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 ∨ (x=x2 ∧ y<y2))}) + /*@desc "only keep conflict positions which are lexicographically geq" */ +ASSERTIONS + get_square ∈ DOM → 1..Sze; + get_square(1) = 1; get_square(3)=1; get_square(4)=2; get_square(9)=3; + {1}× D2 ⊆ conflict_pos(1,1); + D2×{1} ⊆ conflict_pos(1,1); + (1..Sze)×(1..Sze) ⊆ {(1,1)} ∪ conflict_pos(1,1) +VARIABLES + Board, + curx, cury // current (cursor) position on the board for making changes +INVARIANT + Board ∈ DOM → (DOM ⇸ RAN) ∧ + curx ∈ DOM ∧ + cury ∈ DOM +INITIALISATION + Board := PuzzleBoard || + curx, cury := 1,1 +OPERATIONS + SetEmpty = BEGIN Board := λi.(i∈DOM|∅) END; + SetPuzzle = BEGIN Board := PuzzleBoard END; + SetCurPos(x,y) = // Change the current (cursor) position + SELECT x∈DOM ∧ y∈DOM THEN + curx, cury := x,y + END; + SetCurPosToDetPosition(dx,dy) = // Hint action∈ set the cursor to deterministic position + SELECT dx∈DOM ∧ dy∈DOM ∧ + ¬(dy∈dom(Board(dx))) ∧ + card(PossibleVals(dx,dy))=1 /*@desc "exactly one value possible" */ + THEN + curx, cury := dx,dy // Change current position + END; + SetBoard(val) = // Set the value of the board at the current position + SELECT val∈RAN ∧ cury ∉ dom(PuzzleBoard(curx)) THEN + Board(curx)(cury) := val + END; + ClearCurPos = // Clear the value at the current position + SELECT cury ∉ dom(PuzzleBoard(curx)) THEN + Board(curx) := {cury} ⩤ Board(curx) + END; + res <-- GetPossibleVals = // get possible values for the current position + BEGIN + res := PossibleVals(curx,cury) + END; + Solve(SBoard) = // Solve the board + SELECT + SBoard ∈ DOM → (DOM → RAN) /*@desc "The solution SBoard must be complete" */ ∧ + ∀(x,y).(y∈dom(Board(x)) + ⇒ SBoard(x)(y) = Board(x)(y)) /*@desc "Copy partial solution (Board variable)" */ ∧ + ∀(x,y).(x∈DOM ∧ y∈DOM ⇒ + ∀(x2,y2).(x2↦y2∈ conflict_pos_sym(x,y) + ⇒ SBoard(x)(y) ≠ SBoard(x2)(y2) + ) /*@desc "The value must be different from that of all conflict positions" */ + ) + THEN + Board := SBoard // set the board to the found solution + END +END \ No newline at end of file