minor change

Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>

Sudoku/SudokuEventUnicode.mch

@@ -5,7 +5,7 @@ MACHINE SudokuEventUnicode
 */
 DEFINITIONS
  Sze == 3; Mx==(Sze*Sze);
- DOM == 1..Mx; D1 == 1..(Mx-1); D2 == 2..Mx ;
+ DOM == 1..Mx;
  RAN == (1..Mx);
  SUBSQS == λi.(i∈1..Sze | ((i-1)*Sze+1)..i*Sze);
  SUBSQ == ran(SUBSQS);
@@ -45,7 +45,7 @@ DEFINITIONS
   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" */,
+  get_square /*@desc "Subsquare 1..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" */
@@ -71,8 +71,8 @@ PROPERTIES
 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}× (2..Mx) ⊆ conflict_pos(1,1);
+   (2..Mx)×{1} ⊆ conflict_pos(1,1);
   (1..Sze)×(1..Sze) ⊆ {(1,1)} ∪ conflict_pos(1,1)
 VARIABLES
   Board,
@@ -86,11 +86,14 @@ INITIALISATION
   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))) ∧ 
@@ -98,18 +101,22 @@ OPERATIONS
     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" */ ∧