new version which uses external SVG and B definitions

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

N-Queens/QueensWithEventsVisBDef.mch

+MACHINE QueensWithEventsVisBDef
+  // a version which uses no external VisB JSON file; just B DEFINITIONS
+CONSTANTS n
+PROPERTIES
+ n : NATURAL &
+ n <= MXQ
+DEFINITIONS
+      VISB_JSON_FILE == "";
+      WID == 45; WID1 == WID+2; MXQ == 20;
+      Light == "#ffce9e";
+      Dark == "#d18b47";
+      VISB_SVG_OBJECTS1 == {i,j•i:1..MXQ & j:1..MXQ | 
+                           rec(svg_class:"rect", x:i*WID1, y:j*WID1, width:WID, height:WID, stroke:"gray",
+                               visibility:bool(i<=n & j<=n),
+                               fill:IF i|->j:queens THEN "red" 
+                                    ELSIF (i+j) mod 2 = 0 THEN Light
+                                    ELSE Dark END,
+                               title: ```Col ${i}, Row ${j}```,
+                               hovers: rec(stroke:"black")
+                              )};
+      VISB_SVG_OBJECTS2 == {i•i:1..MXQ | rec(svg_class:"image", 
+          //href:IF (i+queens(i)) mod 2 = 0 THEN "./Chess_qll45.svg" ELSE "./Chess_qld45.svg" END,
+          href:IF (i+queens(i)) mod 2 = 0 THEN "https://upload.wikimedia.org/wikipedia/commons/9/9a/Chess_qll45.svg" ELSE "https://upload.wikimedia.org/wikipedia/commons/7/7d/Chess_qld45.svg" END,
+                                            x:i*WID1, fill:"blue",
+                                            visibility:bool(i:dom(queens)),
+                                            y:queens(i)*WID1)
+                           };
+      SET_PREF_TIME_OUT == 6000;
+      SET_PREF_CLPFD == TRUE;
+      SET_PREF_MAX_INITIALISATIONS == 121;
+      SET_PREF_MAX_OPERATIONS == 10;
+      MAX_OPERATIONS_SetQueen == 1000;
+      MAX_OPERATIONS_ChangeQueen == 1000;
+      MAX_OPERATIONS_Solve == 4;
+
+      is_attacked(q1) == q1:dom(queens) &
+                         #q2.(q2:dom(queens) & q2 /= q1 &
+                              (no_attack(q1,q2,queens) => queens(q1) = queens(q2)));
+      pos_is_attacked(q1,q1row) ==
+                         #q2.(q2:dom(queens) & q2 /= q1 &
+                              (no_attack_pos(q1,q1row,q2,queens(q2)) => q1row = queens(q2)));
+      no_attack(q1,q2,board) == no_attack_pos(q1,board(q1),q2,board(q2));
+      no_attack_pos(q1,q1row,q2,q2row) == (q1row+q2-q1 /= q2row & q1row-q2+q1 /= q2row);
+      Solution(board) == (
+         board :  perm(1..n) /* for each column the row in which the queen is in */
+         &
+         !(q1,q2).(q1:1..n & q2:2..n & q2>q1 => no_attack(q1,q2,board) )
+        )
+VARIABLES queens
+INVARIANT
+  queens : (1..n) +-> (1..n)
+INITIALISATION
+  queens := {}
+OPERATIONS
+  Solve = ANY solution WHERE
+      Solution(solution) &
+      !x.(x:dom(queens) => solution(x)=queens(x))
+  THEN
+     queens := solution
+  END;
+  SolveFuzzy = ANY solution WHERE
+      Solution(solution) &
+      !x.(x:dom(queens) => solution(x):{queens(x)-1,queens(x),queens(x)+1})
+  THEN
+     queens := solution
+  END;
+  SetQueen(i,j) = SELECT i:1..n & j:1..n & i /: dom(queens) THEN
+     queens(i) := j
+  END;
+  ChangeQueen(i,j) = SELECT i:1..n & j:1..n & i : dom(queens) & j /= queens(i) THEN
+     queens(i) := j
+  END;
+  TryQueen(i,j) = PRE i:1..n & j:1..n THEN
+      IF i /: dom(queens) THEN
+          SELECT i:1..n & j:1..n & i /: dom(queens) THEN
+              queens(i) := j
+          END ELSE
+          SELECT i:1..n & j:1..n & i : dom(queens) & j /= queens(i) THEN
+              queens(i) := j
+          END 
+       END
+    END;
+  r<--Get(yy) = PRE yy:dom(queens) THEN r:= queens(yy) END
+END
\ No newline at end of file