simplify model

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)))
+   !(x,y).(x:DOM & y:DOM =>
+            !(x2,y2).(x2|->y2: conflict_pos_sym(x,y)
+               => SBoard(x)(y) /= SBoard(x2)(y2)
              )
-      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" */
     THEN
         Board := SBoard
     END

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

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"}
+                ]
     }
   ]
 }