diff --git a/N-Queens/QueensWithEventsVisBDef.mch b/N-Queens/QueensWithEventsVisBDef.mch new file mode 100644 index 0000000000000000000000000000000000000000..82ad65df16864720c2e9ef8e628b2a3e205bd84c --- /dev/null +++ b/N-Queens/QueensWithEventsVisBDef.mch @@ -0,0 +1,84 @@ +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