Sieve/Sieve_VisB.mch

+MACHINE Sieve_VisB
+// A version of the Sieve model with a simple VisB visualisation
+DEFINITIONS
+  SET_PREF_MAXINT == 99;
+  SET_PREF_MININT == -1;
+  MINLIM == MAXINT-1;
+  GOAL == (cur=1 & numbers /= {});
+  VISB_SVG_FILE == "";
+  VISB_SVG_BOX == rec(height:220, width:220, viewBox:"0 0 220 220");
+  vsz == 20;
+  VISB_SVG_OBJECTS2 == {x,y•x:0..9 & y:0..9 | rec(`id`:("nr",x,y), svg_class:"text",
+                                                 x:vsz+x*vsz, y:vsz+y*vsz, `font-size`:10,
+                                                 text:x+y*10)};
+  VISB_SVG_OBJECTS1 == {x,y•x:0..9 & y:0..9 | rec(`id`:("rec",x,y), svg_class:"rect",
+                                                 x:15+x*vsz, y:5+y*vsz,
+                                                 stroke:"green", `stroke-width`:1.5,fill:"white",
+                                                 width:vsz-1, height:vsz-1)};
+  VISB_SVG_UPDATES2 == {x,y•x:0..9 & y:0..9 | rec(`id`:("rec",x,y),
+                                                   stroke:IF x+y*10=cur THEN "red"
+                                                          ELSIF x+y*10:numbers THEN "green" ELSE "gray" END,
+                                                   fill: IF x+y*10:numbers THEN "white" ELSE "gray" END)};
+VARIABLES numbers,cur, limit
+INVARIANT
+ numbers <: INTEGER & cur:NATURAL1 & limit:NATURAL1
+INITIALISATION numbers := {} || cur := 1 || limit := 1
+OPERATIONS
+  StartSieve(lim) = PRE cur=1 & lim>MINLIM & lim <= MAXINT THEN
+    numbers := 2..lim ||
+    cur := 2 ||
+    limit := lim
+  END;
+  prime <-- TreatNumber(cc) = PRE cc=cur & cur>1 & cur*cur<= limit THEN
+    IF cc:numbers THEN
+       numbers := numbers - ran(%n.(n:cur..limit/cur|cur*n))
+/*        numbers := numbers - ran(%n.(n:2..limit/cur|cur*n)) */
+      || prime := TRUE
+    ELSE
+       prime := FALSE
+    END ||
+    cur := cur+1
+  END;
+  r <-- Finish = PRE cur*cur>limit THEN
+    cur := 1 || r := card(numbers)
+  END
+END
+

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" */ ∧