diff --git a/Sudoku/SudokuFeld.svg b/Sudoku/SudokuFeld.svg
index 1e63b66b23edfb747c17bf5011d441be620362a3..7e7c78428ceaad6d01bf0e001d4a8cfd436f2239 100644
--- a/Sudoku/SudokuFeld.svg
+++ b/Sudoku/SudokuFeld.svg
@@ -29,10 +29,20 @@
 		fill : rosybrown
 	}
 	.hover {
-		stroke : black;
+		stroke : lightgray;
 		stroke-width : 0.1;
 		fill : whitesmoke
 	}
+	.conflictpos {
+		stroke : lightgray;
+		stroke-width : 0.1;
+		fill : whitesmoke
+	}
+	.samevalue {
+		stroke : lightgray;
+		stroke-width : 0.1;
+		fill : lavender
+	}
 	.normalKeypad {
 		fill : lightgray
 	}
@@ -96,7 +106,16 @@
 	.SmallBoxes{
 		stroke: lightgray;
 	}
-	
+	.OnTipFrames{
+		stroke: purple;
+		fill: none;
+		stroke-width : 1.0;
+	}
+	.OffTipFrames{
+		stroke: none;
+		fill: none;
+		stroke-width : 0.1;
+	}
 		
 </style>
 
@@ -992,6 +1011,7 @@
 	</text>
 	</g>
 
+
  <g id="Buttons" transform="translate(110,40)">
   <title>Set cell to</title>
 
@@ -1015,34 +1035,47 @@
   <text x="48.90335" y="52.000538" id="bt_9" xml:space="preserve" class="normalTextkeyboard">9</text>
  </g>
 
+<g id="TipFrame" transform="translate(110,40)" visibility="hidden">
+	<rect rx="0.6" class="OffTipFrames" x="0.9" y="0.9" width="18.2" height="18.2" id="TipFrame_1"/>
+  	<rect rx="0.6" class="OffTipFrames" x="0.9" y="20.9" width="18.2" height="18.2" id="TipFrame_4"/>
+  	<rect rx="0.6" class="OffTipFrames" x="20.9" y="0.9" width="18.2" height="18.2" id="TipFrame_2"/>
+  	<rect rx="0.6" class="OffTipFrames" x="20.9" y="20.9" width="18.2" height="18.2" id="TipFrame_5"/>
+  	<rect rx="0.6" class="OffTipFrames" x="40.9" y="0.9" width="18.2" height="18.2" id="TipFrame_3"/>
+  	<rect rx="0.6" class="OffTipFrames" x="40.9" y="20.9" width="18.2" height="18.2" id="TipFrame_6"/>
+  	<rect rx="0.6" class="OffTipFrames" x="40.9" y="40.9" width="18.2" height="18.2" id="TipFrame_9"/>
+  	<rect rx="0.6" class="OffTipFrames" x="20.9" y="40.9" width="18.2" height="18.2" id="TipFrame_8"/>
+  	<rect rx="0.6" class="OffTipFrames" x="0.9" y="40.9" width="18.2" height="18.2" id="TipFrame_7"/>
+</g>
+
+
 <g id="NewGameButton" transform="translate(110,10)">
   <title>NewGame</title>
   <rect rx="1.2" id="newGameRect" height="9.3" width="59.4" y="0.4" x="0.3" stroke="#6200cc" fill="#7b00ff"/>
-  <text transform="matrix(1 0 0 1 0 0)" font-style="normal"  font-weight="bold" xml:space="preserve" text-anchor="start" font-family="sans-serif" font-size="3.9" id="NewGameText" y="6.25" x="20.039063" stroke-width="0" stroke="#6000c6" fill="#ffffff" >New Game</text>
+  <text transform="matrix(1 0 0 1 0 0)" font-style="normal"  font-weight="bold" xml:space="preserve" text-anchor="start" font-family="sans-serif" font-size="3.9" id="NewGameText" y="6.25" x="20.039063" stroke-width="0" stroke="#6000c6" fill="#ffffff" >New Puzzle</text>
  </g>
 
 
  <g id="Tip"  transform="translate(110,22.5)">
-  <title>Tip</title>
+  <title>Show feasible values</title>
   <ellipse ry="7" rx="7" id="TippCircle" cy="7.5" cx="7.5" class="normalKeyboard"/>
   <text transform="matrix(1 0 0 1 0 0)" class="normalActionbuttons" font-style="normal" font-weight="normal" xml:space="preserve" text-anchor="start" font-family="sans-serif" font-size="10" id="TippText" y="10.96203" x="4.71516" stroke-width="0" stroke="null" fill="#7f00ff">?</text>
  </g>
 
 <g id="Add" transform="translate(125,22.5)">
-  <title>Add</title>
+  <title>(not available)</title>
   <ellipse ry="7" rx="7" id="AddCircle" cy="7.5" cx="7.5" class="normalKeyboard"/>
   <text style="cursor: move;" font-style="normal" class="normalActionbuttons" font-weight="normal" xml:space="preserve" text-anchor="start" font-family="sans-serif" font-size="10" id="AddText" y="10.96203" x="4.71516" stroke-width="0" stroke="null" fill="#7f00ff">+</text>
  </g>
  
  <g id="Remove" transform="translate(140,22.5)">
-  <title>Remove</title>
+  <title>Erase cell value</title>
   <ellipse ry="7" rx="7" id="RemoveCircle" cy="7.5" cx="7.5" class="normalKeyboard"/>
   <text style="cursor: move;" font-style="normal" class="normalActionbuttons" font-weight="normal" xml:space="preserve" text-anchor="start" font-family="sans-serif" font-size="10" id="RemoveText" y="10" x="6" stroke-width="0" stroke="null" fill="#7f00ff">-</text>
  </g>
 
 
 <g id="Solve" transform="translate(155,22.5)">
-  <title>Solve</title>
+  <title>Solve the puzzle automatically</title>
   <ellipse ry="7" rx="7" id="SolveCircle" cy="7.5" cx="7.5" class="normalKeyboard"/>
   <text style="cursor: move;" transform= "scale(-1,1) rotate(-40 -9 9)" font-style="normal" class="normalActionbuttons" font-weight="normal" xml:space="preserve" text-anchor="start" font-family="sans-serif" font-size="10" id="SolveText" y="11" x="-9" stroke-width="0" stroke="null" fill="#7f00ff">L</text>
  </g>
diff --git a/Sudoku/visb_sudoku.json b/Sudoku/visb_sudoku.json
index 97b3842173aaa0cb9fb58931663ab39deaa7c4a4..d5d538ea547a51656f67f17141d2d7dd66eb6826 100644
--- a/Sudoku/visb_sudoku.json
+++ b/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  %0|->%1:conflict_pos(curx,cury) THEN IF %1:dom(Board(%0)) & BOARD(%0)(%1)=BOARD(curx)(cury) THEN \"wrong\" ELSE \"hover\" END ELSIF %1:dom(Board(%0)) & BOARD(%0)(%1)=BOARD(curx)(cury) THEN \"hover\" ELSIF %1:dom(PuzzleBoard(%0)) THEN \"fixed\" 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 \"conflictpos\" END ELSIF %1:dom(Board(%0)) & BOARD(%0)(%1)=BOARD(curx)(cury) THEN \"samevalue\" ELSIF %1:dom(PuzzleBoard(%0)) THEN \"fixed\" ELSE \"normal\" END"
     },
 	{
 	  "for": {"from":1, "to":9},
@@ -27,6 +27,12 @@
       "id": "txt_%0_%1",
       "attr": "visibility",
       "value" : "IF %1 : dom(Board(%0)) THEN \"visible\" ELSE \"hidden\" END"
+    },
+	{
+	  "for": {"from":1, "to":9},
+      "id": "TipFrame_%0",
+      "attr": "class",
+      "value" : "IF %0:PossibleVals(curx,cury) THEN \"OnTipFrames\" ELSE \"OffTipFrames\" END"
     }
 ],
   "events": [
@@ -59,6 +65,11 @@
       "hovers": [{ "attr":"class", "enter":"hoverKeyboard", "leave":"normalKeyboard"}
                 ]
     },
+    {
+	  "id": "Tip",
+      "hovers": [{ "id":"TipFrame", "attr":"visibility", "enter":"visible", "leave":"hidden"}
+                ]
+    },
     {
 	  "id": "NewGameButton",
       "event": "SetPuzzle",
diff --git a/traces/SudokuEvent.prob2trace b/traces/SudokuEvent.prob2trace
new file mode 100644
index 0000000000000000000000000000000000000000..2c35538ffb38dca73d35e4bc9a43e165bdd46e7f
--- /dev/null
+++ b/traces/SudokuEvent.prob2trace
@@ -0,0 +1,584 @@
+{
+  "description": "",
+  "transitionList": [
+    {
+      "name": "$setup_constants",
+      "params": {},
+      "results": {},
+      "destState": {
+        "conflict_pos": "{(1↦1↦{(1↦2),(1↦3),(1↦4),(1↦5),(1↦6),(1↦7),(1↦8),(1↦9),(2↦1),(2↦2),(2↦3),(3↦1),(3↦2),(3↦3),(4↦1),(5↦1),(6↦1),(7↦1),(8↦1),(9↦1)}),(1↦2↦{(1↦1),(1↦3),(1↦4),(1↦5),(1↦6),(1↦7),(1↦8),(1↦9),(2↦1),(2↦2),(2↦3),(3↦1),(3↦2),(3↦3),(4↦2),(5↦2),(6↦2),(7↦2),(8↦2),(9↦2)}),(1↦3↦{(1↦1),(1↦2),(1↦4),(1↦5),(1↦6),(1↦7),(1↦8),(1↦9),(2↦1),(2↦2),(2↦3),(3↦1),(3↦2),(3↦3),(4↦3),(5↦3),(6↦3),(7↦3),(8↦3),(9↦3)}),(1↦4↦{(1↦1),(1↦2),(1↦3),(1↦5),(1↦6),(1↦7),(1↦8),(1↦9),(2↦4),(2↦5),(2↦6),(3↦4),(3↦5),(3↦6),(4↦4),(5↦4),(6↦4),(7↦4),(8↦4),(9↦4)}),(1↦5↦{(1↦1),(1↦2),(1↦3),(1↦4),(1↦6),(1↦7),(1↦8),(1↦9),(2↦4),(2↦5),(2↦6),(3↦4),(3↦5),(3↦6),(4↦5),(5↦5),(6↦5),(7↦5),(8↦5),(9↦5)}),(1↦6↦{(1↦1),(1↦2),(1↦3),(1↦4),(1↦5),(1↦7),(1↦8),(1↦9),(2↦4),(2↦5),(2↦6),(3↦4),(3↦5),(3↦6),(4↦6),(5↦6),(6↦6),(7↦6),(8↦6),(9↦6)}),(1↦7↦{(1↦1),(1↦2),(1↦3),(1↦4),(1↦5),(1↦6),(1↦8),(1↦9),(2↦7),(2↦8),(2↦9),(3↦7),(3↦8),(3↦9),(4↦7),(5↦7),(6↦7),(7↦7),(8↦7),(9↦7)}),(1↦8↦{(1↦1),(1↦2),(1↦3),(1↦4),(1↦5),(1↦6),(1↦7),(1↦9),(2↦7),(2↦8),(2↦9),(3↦7),(3↦8),(3↦9),(4↦8),(5↦8),(6↦8),(7↦8),(8↦8),(9↦8)}),(1↦9↦{(1↦1),(1↦2),(1↦3),(1↦4),(1↦5),(1↦6),(1↦7),(1↦8),(2↦7),(2↦8),(2↦9),(3↦7),(3↦8),(3↦9),(4↦9),(5↦9),(6↦9),(7↦9),(8↦9),(9↦9)}),(2↦1↦{(1↦1),(1↦2),(1↦3),(2↦2),(2↦3),(2↦4),(2↦5),(2↦6),(2↦7),(2↦8),(2↦9),(3↦1),(3↦2),(3↦3),(4↦1),(5↦1),(6↦1),(7↦1),(8↦1),(9↦1)}),(2↦2↦{(1↦1),(1↦2),(1↦3),(2↦1),(2↦3),(2↦4),(2↦5),(2↦6),(2↦7),(2↦8),(2↦9),(3↦1),(3↦2),(3↦3),(4↦2),(5↦2),(6↦2),(7↦2),(8↦2),(9↦2)}),(2↦3↦{(1↦1),(1↦2),(1↦3),(2↦1),(2↦2),(2↦4),(2↦5),(2↦6),(2↦7),(2↦8),(2↦9),(3↦1),(3↦2),(3↦3),(4↦3),(5↦3),(6↦3),(7↦3),(8↦3),(9↦3)}),(2↦4↦{(1↦4),(1↦5),(1↦6),(2↦1),(2↦2),(2↦3),(2↦5),(2↦6),(2↦7),(2↦8),(2↦9),(3↦4),(3↦5),(3↦6),(4↦4),(5↦4),(6↦4),(7↦4),(8↦4),(9↦4)}),(2↦5↦{(1↦4),(1↦5),(1↦6),(2↦1),(2↦2),(2↦3),(2↦4),(2↦6),(2↦7),(2↦8),(2↦9),(3↦4),(3↦5),(3↦6),(4↦5),(5↦5),(6↦5),(7↦5),(8↦5),(9↦5)}),(2↦6↦{(1↦4),(1↦5),(1↦6),(2↦1),(2↦2),(2↦3),(2↦4),(2↦5),(2↦7),(2↦8),(2↦9),(3↦4),(3↦5),(3↦6),(4↦6),(5↦6),(6↦6),(7↦6),(8↦6),(9↦6)}),(2↦7↦{(1↦7),(1↦8),(1↦9),(2↦1),(2↦2),(2↦3),(2↦4),(2↦5),(2↦6),(2↦8),(2↦9),(3↦7),(3↦8),(3↦9),(4↦7),(5↦7),(6↦7),(7↦7),(8↦7),(9↦7)}),(2↦8↦{(1↦7),(1↦8),(1↦9),(2↦1),(2↦2),(2↦3),(2↦4),(2↦5),(2↦6),(2↦7),(2↦9),(3↦7),(3↦8),(3↦9),(4↦8),(5↦8),(6↦8),(7↦8),(8↦8),(9↦8)}),(2↦9↦{(1↦7),(1↦8),(1↦9),(2↦1),(2↦2),(2↦3),(2↦4),(2↦5),(2↦6),(2↦7),(2↦8),(3↦7),(3↦8),(3↦9),(4↦9),(5↦9),(6↦9),(7↦9),(8↦9),(9↦9)}),(3↦1↦{(1↦1),(1↦2),(1↦3),(2↦1),(2↦2),(2↦3),(3↦2),(3↦3),(3↦4),(3↦5),(3↦6),(3↦7),(3↦8),(3↦9),(4↦1),(5↦1),(6↦1),(7↦1),(8↦1),(9↦1)}),(3↦2↦{(1↦1),(1↦2),(1↦3),(2↦1),(2↦2),(2↦3),(3↦1),(3↦3),(3↦4),(3↦5),(3↦6),(3↦7),(3↦8),(3↦9),(4↦2),(5↦2),(6↦2),(7↦2),(8↦2),(9↦2)}),(3↦3↦{(1↦1),(1↦2),(1↦3),(2↦1),(2↦2),(2↦3),(3↦1),(3↦2),(3↦4),(3↦5),(3↦6),(3↦7),(3↦8),(3↦9),(4↦3),(5↦3),(6↦3),(7↦3),(8↦3),(9↦3)}),(3↦4↦{(1↦4),(1↦5),(1↦6),(2↦4),(2↦5),(2↦6),(3↦1),(3↦2),(3↦3),(3↦5),(3↦6),(3↦7),(3↦8),(3↦9),(4↦4),(5↦4),(6↦4),(7↦4),(8↦4),(9↦4)}),(3↦5↦{(1↦4),(1↦5),(1↦6),(2↦4),(2↦5),(2↦6),(3↦1),(3↦2),(3↦3),(3↦4),(3↦6),(3↦7),(3↦8),(3↦9),(4↦5),(5↦5),(6↦5),(7↦5),(8↦5),(9↦5)}),(3↦6↦{(1↦4),(1↦5),(1↦6),(2↦4),(2↦5),(2↦6),(3↦1),(3↦2),(3↦3),(3↦4),(3↦5),(3↦7),(3↦8),(3↦9),(4↦6),(5↦6),(6↦6),(7↦6),(8↦6),(9↦6)}),(3↦7↦{(1↦7),(1↦8),(1↦9),(2↦7),(2↦8),(2↦9),(3↦1),(3↦2),(3↦3),(3↦4),(3↦5),(3↦6),(3↦8),(3↦9),(4↦7),(5↦7),(6↦7),(7↦7),(8↦7),(9↦7)}),(3↦8↦{(1↦7),(1↦8),(1↦9),(2↦7),(2↦8),(2↦9),(3↦1),(3↦2),(3↦3),(3↦4),(3↦5),(3↦6),(3↦7),(3↦9),(4↦8),(5↦8),(6↦8),(7↦8),(8↦8),(9↦8)}),(3↦9↦{(1↦7),(1↦8),(1↦9),(2↦7),(2↦8),(2↦9),(3↦1),(3↦2),(3↦3),(3↦4),(3↦5),(3↦6),(3↦7),(3↦8),(4↦9),(5↦9),(6↦9),(7↦9),(8↦9),(9↦9)}),(4↦1↦{(1↦1),(2↦1),(3↦1),(4↦2),(4↦3),(4↦4),(4↦5),(4↦6),(4↦7),(4↦8),(4↦9),(5↦1),(5↦2),(5↦3),(6↦1),(6↦2),(6↦3),(7↦1),(8↦1),(9↦1)}),(4↦2↦{(1↦2),(2↦2),(3↦2),(4↦1),(4↦3),(4↦4),(4↦5),(4↦6),(4↦7),(4↦8),(4↦9),(5↦1),(5↦2),(5↦3),(6↦1),(6↦2),(6↦3),(7↦2),(8↦2),(9↦2)}),(4↦3↦{(1↦3),(2↦3),(3↦3),(4↦1),(4↦2),(4↦4),(4↦5),(4↦6),(4↦7),(4↦8),(4↦9),(5↦1),(5↦2),(5↦3),(6↦1),(6↦2),(6↦3),(7↦3),(8↦3),(9↦3)}),(4↦4↦{(1↦4),(2↦4),(3↦4),(4↦1),(4↦2),(4↦3),(4↦5),(4↦6),(4↦7),(4↦8),(4↦9),(5↦4),(5↦5),(5↦6),(6↦4),(6↦5),(6↦6),(7↦4),(8↦4),(9↦4)}),(4↦5↦{(1↦5),(2↦5),(3↦5),(4↦1),(4↦2),(4↦3),(4↦4),(4↦6),(4↦7),(4↦8),(4↦9),(5↦4),(5↦5),(5↦6),(6↦4),(6↦5),(6↦6),(7↦5),(8↦5),(9↦5)}),(4↦6↦{(1↦6),(2↦6),(3↦6),(4↦1),(4↦2),(4↦3),(4↦4),(4↦5),(4↦7),(4↦8),(4↦9),(5↦4),(5↦5),(5↦6),(6↦4),(6↦5),(6↦6),(7↦6),(8↦6),(9↦6)}),(4↦7↦{(1↦7),(2↦7),(3↦7),(4↦1),(4↦2),(4↦3),(4↦4),(4↦5),(4↦6),(4↦8),(4↦9),(5↦7),(5↦8),(5↦9),(6↦7),(6↦8),(6↦9),(7↦7),(8↦7),(9↦7)}),(4↦8↦{(1↦8),(2↦8),(3↦8),(4↦1),(4↦2),(4↦3),(4↦4),(4↦5),(4↦6),(4↦7),(4↦9),(5↦7),(5↦8),(5↦9),(6↦7),(6↦8),(6↦9),(7↦8),(8↦8),(9↦8)}),(4↦9↦{(1↦9),(2↦9),(3↦9),(4↦1),(4↦2),(4↦3),(4↦4),(4↦5),(4↦6),(4↦7),(4↦8),(5↦7),(5↦8),(5↦9),(6↦7),(6↦8),(6↦9),(7↦9),(8↦9),(9↦9)}),(5↦1↦{(1↦1),(2↦1),(3↦1),(4↦1),(4↦2),(4↦3),(5↦2),(5↦3),(5↦4),(5↦5),(5↦6),(5↦7),(5↦8),(5↦9),(6↦1),(6↦2),(6↦3),(7↦1),(8↦1),(9↦1)}),(5↦2↦{(1↦2),(2↦2),(3↦2),(4↦1),(4↦2),(4↦3),(5↦1),(5↦3),(5↦4),(5↦5),(5↦6),(5↦7),(5↦8),(5↦9),(6↦1),(6↦2),(6↦3),(7↦2),(8↦2),(9↦2)}),(5↦3↦{(1↦3),(2↦3),(3↦3),(4↦1),(4↦2),(4↦3),(5↦1),(5↦2),(5↦4),(5↦5),(5↦6),(5↦7),(5↦8),(5↦9),(6↦1),(6↦2),(6↦3),(7↦3),(8↦3),(9↦3)}),(5↦4↦{(1↦4),(2↦4),(3↦4),(4↦4),(4↦5),(4↦6),(5↦1),(5↦2),(5↦3),(5↦5),(5↦6),(5↦7),(5↦8),(5↦9),(6↦4),(6↦5),(6↦6),(7↦4),(8↦4),(9↦4)}),(5↦5↦{(1↦5),(2↦5),(3↦5),(4↦4),(4↦5),(4↦6),(5↦1),(5↦2),(5↦3),(5↦4),(5↦6),(5↦7),(5↦8),(5↦9),(6↦4),(6↦5),(6↦6),(7↦5),(8↦5),(9↦5)}),(5↦6↦{(1↦6),(2↦6),(3↦6),(4↦4),(4↦5),(4↦6),(5↦1),(5↦2),(5↦3),(5↦4),(5↦5),(5↦7),(5↦8),(5↦9),(6↦4),(6↦5),(6↦6),(7↦6),(8↦6),(9↦6)}),(5↦7↦{(1↦7),(2↦7),(3↦7),(4↦7),(4↦8),(4↦9),(5↦1),(5↦2),(5↦3),(5↦4),(5↦5),(5↦6),(5↦8),(5↦9),(6↦7),(6↦8),(6↦9),(7↦7),(8↦7),(9↦7)}),(5↦8↦{(1↦8),(2↦8),(3↦8),(4↦7),(4↦8),(4↦9),(5↦1),(5↦2),(5↦3),(5↦4),(5↦5),(5↦6),(5↦7),(5↦9),(6↦7),(6↦8),(6↦9),(7↦8),(8↦8),(9↦8)}),(5↦9↦{(1↦9),(2↦9),(3↦9),(4↦7),(4↦8),(4↦9),(5↦1),(5↦2),(5↦3),(5↦4),(5↦5),(5↦6),(5↦7),(5↦8),(6↦7),(6↦8),(6↦9),(7↦9),(8↦9),(9↦9)}),(6↦1↦{(1↦1),(2↦1),(3↦1),(4↦1),(4↦2),(4↦3),(5↦1),(5↦2),(5↦3),(6↦2),(6↦3),(6↦4),(6↦5),(6↦6),(6↦7),(6↦8),(6↦9),(7↦1),(8↦1),(9↦1)}),(6↦2↦{(1↦2),(2↦2),(3↦2),(4↦1),(4↦2),(4↦3),(5↦1),(5↦2),(5↦3),(6↦1),(6↦3),(6↦4),(6↦5),(6↦6),(6↦7),(6↦8),(6↦9),(7↦2),(8↦2),(9↦2)}),(6↦3↦{(1↦3),(2↦3),(3↦3),(4↦1),(4↦2),(4↦3),(5↦1),(5↦2),(5↦3),(6↦1),(6↦2),(6↦4),(6↦5),(6↦6),(6↦7),(6↦8),(6↦9),(7↦3),(8↦3),(9↦3)}),(6↦4↦{(1↦4),(2↦4),(3↦4),(4↦4),(4↦5),(4↦6),(5↦4),(5↦5),(5↦6),(6↦1),(6↦2),(6↦3),(6↦5),(6↦6),(6↦7),(6↦8),(6↦9),(7↦4),(8↦4),(9↦4)}),(6↦5↦{(1↦5),(2↦5),(3↦5),(4↦4),(4↦5),(4↦6),(5↦4),(5↦5),(5↦6),(6↦1),(6↦2),(6↦3),(6↦4),(6↦6),(6↦7),(6↦8),(6↦9),(7↦5),(8↦5),(9↦5)}),(6↦6↦{(1↦6),(2↦6),(3↦6),(4↦4),(4↦5),(4↦6),(5↦4),(5↦5),(5↦6),(6↦1),(6↦2),(6↦3),(6↦4),(6↦5),(6↦7),(6↦8),(6↦9),(7↦6),(8↦6),(9↦6)}),(6↦7↦{(1↦7),(2↦7),(3↦7),(4↦7),(4↦8),(4↦9),(5↦7),(5↦8),(5↦9),(6↦1),(6↦2),(6↦3),(6↦4),(6↦5),(6↦6),(6↦8),(6↦9),(7↦7),(8↦7),(9↦7)}),(6↦8↦{(1↦8),(2↦8),(3↦8),(4↦7),(4↦8),(4↦9),(5↦7),(5↦8),(5↦9),(6↦1),(6↦2),(6↦3),(6↦4),(6↦5),(6↦6),(6↦7),(6↦9),(7↦8),(8↦8),(9↦8)}),(6↦9↦{(1↦9),(2↦9),(3↦9),(4↦7),(4↦8),(4↦9),(5↦7),(5↦8),(5↦9),(6↦1),(6↦2),(6↦3),(6↦4),(6↦5),(6↦6),(6↦7),(6↦8),(7↦9),(8↦9),(9↦9)}),(7↦1↦{(1↦1),(2↦1),(3↦1),(4↦1),(5↦1),(6↦1),(7↦2),(7↦3),(7↦4),(7↦5),(7↦6),(7↦7),(7↦8),(7↦9),(8↦1),(8↦2),(8↦3),(9↦1),(9↦2),(9↦3)}),(7↦2↦{(1↦2),(2↦2),(3↦2),(4↦2),(5↦2),(6↦2),(7↦1),(7↦3),(7↦4),(7↦5),(7↦6),(7↦7),(7↦8),(7↦9),(8↦1),(8↦2),(8↦3),(9↦1),(9↦2),(9↦3)}),(7↦3↦{(1↦3),(2↦3),(3↦3),(4↦3),(5↦3),(6↦3),(7↦1),(7↦2),(7↦4),(7↦5),(7↦6),(7↦7),(7↦8),(7↦9),(8↦1),(8↦2),(8↦3),(9↦1),(9↦2),(9↦3)}),(7↦4↦{(1↦4),(2↦4),(3↦4),(4↦4),(5↦4),(6↦4),(7↦1),(7↦2),(7↦3),(7↦5),(7↦6),(7↦7),(7↦8),(7↦9),(8↦4),(8↦5),(8↦6),(9↦4),(9↦5),(9↦6)}),(7↦5↦{(1↦5),(2↦5),(3↦5),(4↦5),(5↦5),(6↦5),(7↦1),(7↦2),(7↦3),(7↦4),(7↦6),(7↦7),(7↦8),(7↦9),(8↦4),(8↦5),(8↦6),(9↦4),(9↦5),(9↦6)}),(7↦6↦{(1↦6),(2↦6),(3↦6),(4↦6),(5↦6),(6↦6),(7↦1),(7↦2),(7↦3),(7↦4),(7↦5),(7↦7),(7↦8),(7↦9),(8↦4),(8↦5),(8↦6),(9↦4),(9↦5),(9↦6)}),(7↦7↦{(1↦7),(2↦7),(3↦7),(4↦7),(5↦7),(6↦7),(7↦1),(7↦2),(7↦3),(7↦4),(7↦5),(7↦6),(7↦8),(7↦9),(8↦7),(8↦8),(8↦9),(9↦7),(9↦8),(9↦9)}),(7↦8↦{(1↦8),(2↦8),(3↦8),(4↦8),(5↦8),(6↦8),(7↦1),(7↦2),(7↦3),(7↦4),(7↦5),(7↦6),(7↦7),(7↦9),(8↦7),(8↦8),(8↦9),(9↦7),(9↦8),(9↦9)}),(7↦9↦{(1↦9),(2↦9),(3↦9),(4↦9),(5↦9),(6↦9),(7↦1),(7↦2),(7↦3),(7↦4),(7↦5),(7↦6),(7↦7),(7↦8),(8↦7),(8↦8),(8↦9),(9↦7),(9↦8),(9↦9)}),(8↦1↦{(1↦1),(2↦1),(3↦1),(4↦1),(5↦1),(6↦1),(7↦1),(7↦2),(7↦3),(8↦2),(8↦3),(8↦4),(8↦5),(8↦6),(8↦7),(8↦8),(8↦9),(9↦1),(9↦2),(9↦3)}),(8↦2↦{(1↦2),(2↦2),(3↦2),(4↦2),(5↦2),(6↦2),(7↦1),(7↦2),(7↦3),(8↦1),(8↦3),(8↦4),(8↦5),(8↦6),(8↦7),(8↦8),(8↦9),(9↦1),(9↦2),(9↦3)}),(8↦3↦{(1↦3),(2↦3),(3↦3),(4↦3),(5↦3),(6↦3),(7↦1),(7↦2),(7↦3),(8↦1),(8↦2),(8↦4),(8↦5),(8↦6),(8↦7),(8↦8),(8↦9),(9↦1),(9↦2),(9↦3)}),(8↦4↦{(1↦4),(2↦4),(3↦4),(4↦4),(5↦4),(6↦4),(7↦4),(7↦5),(7↦6),(8↦1),(8↦2),(8↦3),(8↦5),(8↦6),(8↦7),(8↦8),(8↦9),(9↦4),(9↦5),(9↦6)}),(8↦5↦{(1↦5),(2↦5),(3↦5),(4↦5),(5↦5),(6↦5),(7↦4),(7↦5),(7↦6),(8↦1),(8↦2),(8↦3),(8↦4),(8↦6),(8↦7),(8↦8),(8↦9),(9↦4),(9↦5),(9↦6)}),(8↦6↦{(1↦6),(2↦6),(3↦6),(4↦6),(5↦6),(6↦6),(7↦4),(7↦5),(7↦6),(8↦1),(8↦2),(8↦3),(8↦4),(8↦5),(8↦7),(8↦8),(8↦9),(9↦4),(9↦5),(9↦6)}),(8↦7↦{(1↦7),(2↦7),(3↦7),(4↦7),(5↦7),(6↦7),(7↦7),(7↦8),(7↦9),(8↦1),(8↦2),(8↦3),(8↦4),(8↦5),(8↦6),(8↦8),(8↦9),(9↦7),(9↦8),(9↦9)}),(8↦8↦{(1↦8),(2↦8),(3↦8),(4↦8),(5↦8),(6↦8),(7↦7),(7↦8),(7↦9),(8↦1),(8↦2),(8↦3),(8↦4),(8↦5),(8↦6),(8↦7),(8↦9),(9↦7),(9↦8),(9↦9)}),(8↦9↦{(1↦9),(2↦9),(3↦9),(4↦9),(5↦9),(6↦9),(7↦7),(7↦8),(7↦9),(8↦1),(8↦2),(8↦3),(8↦4),(8↦5),(8↦6),(8↦7),(8↦8),(9↦7),(9↦8),(9↦9)}),(9↦1↦{(1↦1),(2↦1),(3↦1),(4↦1),(5↦1),(6↦1),(7↦1),(7↦2),(7↦3),(8↦1),(8↦2),(8↦3),(9↦2),(9↦3),(9↦4),(9↦5),(9↦6),(9↦7),(9↦8),(9↦9)}),(9↦2↦{(1↦2),(2↦2),(3↦2),(4↦2),(5↦2),(6↦2),(7↦1),(7↦2),(7↦3),(8↦1),(8↦2),(8↦3),(9↦1),(9↦3),(9↦4),(9↦5),(9↦6),(9↦7),(9↦8),(9↦9)}),(9↦3↦{(1↦3),(2↦3),(3↦3),(4↦3),(5↦3),(6↦3),(7↦1),(7↦2),(7↦3),(8↦1),(8↦2),(8↦3),(9↦1),(9↦2),(9↦4),(9↦5),(9↦6),(9↦7),(9↦8),(9↦9)}),(9↦4↦{(1↦4),(2↦4),(3↦4),(4↦4),(5↦4),(6↦4),(7↦4),(7↦5),(7↦6),(8↦4),(8↦5),(8↦6),(9↦1),(9↦2),(9↦3),(9↦5),(9↦6),(9↦7),(9↦8),(9↦9)}),(9↦5↦{(1↦5),(2↦5),(3↦5),(4↦5),(5↦5),(6↦5),(7↦4),(7↦5),(7↦6),(8↦4),(8↦5),(8↦6),(9↦1),(9↦2),(9↦3),(9↦4),(9↦6),(9↦7),(9↦8),(9↦9)}),(9↦6↦{(1↦6),(2↦6),(3↦6),(4↦6),(5↦6),(6↦6),(7↦4),(7↦5),(7↦6),(8↦4),(8↦5),(8↦6),(9↦1),(9↦2),(9↦3),(9↦4),(9↦5),(9↦7),(9↦8),(9↦9)}),(9↦7↦{(1↦7),(2↦7),(3↦7),(4↦7),(5↦7),(6↦7),(7↦7),(7↦8),(7↦9),(8↦7),(8↦8),(8↦9),(9↦1),(9↦2),(9↦3),(9↦4),(9↦5),(9↦6),(9↦8),(9↦9)}),(9↦8↦{(1↦8),(2↦8),(3↦8),(4↦8),(5↦8),(6↦8),(7↦7),(7↦8),(7↦9),(8↦7),(8↦8),(8↦9),(9↦1),(9↦2),(9↦3),(9↦4),(9↦5),(9↦6),(9↦7),(9↦9)}),(9↦9↦{(1↦9),(2↦9),(3↦9),(4↦9),(5↦9),(6↦9),(7↦7),(7↦8),(7↦9),(8↦7),(8↦8),(8↦9),(9↦1),(9↦2),(9↦3),(9↦4),(9↦5),(9↦6),(9↦7),(9↦8)})}",
+        "conflict_pos_sym": "{(1↦1↦{(1↦2),(1↦3),(1↦4),(1↦5),(1↦6),(1↦7),(1↦8),(1↦9),(2↦1),(2↦2),(2↦3),(3↦1),(3↦2),(3↦3),(4↦1),(5↦1),(6↦1),(7↦1),(8↦1),(9↦1)}),(1↦2↦{(1↦3),(1↦4),(1↦5),(1↦6),(1↦7),(1↦8),(1↦9),(2↦1),(2↦2),(2↦3),(3↦1),(3↦2),(3↦3),(4↦2),(5↦2),(6↦2),(7↦2),(8↦2),(9↦2)}),(1↦3↦{(1↦4),(1↦5),(1↦6),(1↦7),(1↦8),(1↦9),(2↦1),(2↦2),(2↦3),(3↦1),(3↦2),(3↦3),(4↦3),(5↦3),(6↦3),(7↦3),(8↦3),(9↦3)}),(1↦4↦{(1↦5),(1↦6),(1↦7),(1↦8),(1↦9),(2↦4),(2↦5),(2↦6),(3↦4),(3↦5),(3↦6),(4↦4),(5↦4),(6↦4),(7↦4),(8↦4),(9↦4)}),(1↦5↦{(1↦6),(1↦7),(1↦8),(1↦9),(2↦4),(2↦5),(2↦6),(3↦4),(3↦5),(3↦6),(4↦5),(5↦5),(6↦5),(7↦5),(8↦5),(9↦5)}),(1↦6↦{(1↦7),(1↦8),(1↦9),(2↦4),(2↦5),(2↦6),(3↦4),(3↦5),(3↦6),(4↦6),(5↦6),(6↦6),(7↦6),(8↦6),(9↦6)}),(1↦7↦{(1↦8),(1↦9),(2↦7),(2↦8),(2↦9),(3↦7),(3↦8),(3↦9),(4↦7),(5↦7),(6↦7),(7↦7),(8↦7),(9↦7)}),(1↦8↦{(1↦9),(2↦7),(2↦8),(2↦9),(3↦7),(3↦8),(3↦9),(4↦8),(5↦8),(6↦8),(7↦8),(8↦8),(9↦8)}),(1↦9↦{(2↦7),(2↦8),(2↦9),(3↦7),(3↦8),(3↦9),(4↦9),(5↦9),(6↦9),(7↦9),(8↦9),(9↦9)}),(2↦1↦{(2↦2),(2↦3),(2↦4),(2↦5),(2↦6),(2↦7),(2↦8),(2↦9),(3↦1),(3↦2),(3↦3),(4↦1),(5↦1),(6↦1),(7↦1),(8↦1),(9↦1)}),(2↦2↦{(2↦3),(2↦4),(2↦5),(2↦6),(2↦7),(2↦8),(2↦9),(3↦1),(3↦2),(3↦3),(4↦2),(5↦2),(6↦2),(7↦2),(8↦2),(9↦2)}),(2↦3↦{(2↦4),(2↦5),(2↦6),(2↦7),(2↦8),(2↦9),(3↦1),(3↦2),(3↦3),(4↦3),(5↦3),(6↦3),(7↦3),(8↦3),(9↦3)}),(2↦4↦{(2↦5),(2↦6),(2↦7),(2↦8),(2↦9),(3↦4),(3↦5),(3↦6),(4↦4),(5↦4),(6↦4),(7↦4),(8↦4),(9↦4)}),(2↦5↦{(2↦6),(2↦7),(2↦8),(2↦9),(3↦4),(3↦5),(3↦6),(4↦5),(5↦5),(6↦5),(7↦5),(8↦5),(9↦5)}),(2↦6↦{(2↦7),(2↦8),(2↦9),(3↦4),(3↦5),(3↦6),(4↦6),(5↦6),(6↦6),(7↦6),(8↦6),(9↦6)}),(2↦7↦{(2↦8),(2↦9),(3↦7),(3↦8),(3↦9),(4↦7),(5↦7),(6↦7),(7↦7),(8↦7),(9↦7)}),(2↦8↦{(2↦9),(3↦7),(3↦8),(3↦9),(4↦8),(5↦8),(6↦8),(7↦8),(8↦8),(9↦8)}),(2↦9↦{(3↦7),(3↦8),(3↦9),(4↦9),(5↦9),(6↦9),(7↦9),(8↦9),(9↦9)}),(3↦1↦{(3↦2),(3↦3),(3↦4),(3↦5),(3↦6),(3↦7),(3↦8),(3↦9),(4↦1),(5↦1),(6↦1),(7↦1),(8↦1),(9↦1)}),(3↦2↦{(3↦3),(3↦4),(3↦5),(3↦6),(3↦7),(3↦8),(3↦9),(4↦2),(5↦2),(6↦2),(7↦2),(8↦2),(9↦2)}),(3↦3↦{(3↦4),(3↦5),(3↦6),(3↦7),(3↦8),(3↦9),(4↦3),(5↦3),(6↦3),(7↦3),(8↦3),(9↦3)}),(3↦4↦{(3↦5),(3↦6),(3↦7),(3↦8),(3↦9),(4↦4),(5↦4),(6↦4),(7↦4),(8↦4),(9↦4)}),(3↦5↦{(3↦6),(3↦7),(3↦8),(3↦9),(4↦5),(5↦5),(6↦5),(7↦5),(8↦5),(9↦5)}),(3↦6↦{(3↦7),(3↦8),(3↦9),(4↦6),(5↦6),(6↦6),(7↦6),(8↦6),(9↦6)}),(3↦7↦{(3↦8),(3↦9),(4↦7),(5↦7),(6↦7),(7↦7),(8↦7),(9↦7)}),(3↦8↦{(3↦9),(4↦8),(5↦8),(6↦8),(7↦8),(8↦8),(9↦8)}),(3↦9↦{(4↦9),(5↦9),(6↦9),(7↦9),(8↦9),(9↦9)}),(4↦1↦{(4↦2),(4↦3),(4↦4),(4↦5),(4↦6),(4↦7),(4↦8),(4↦9),(5↦1),(5↦2),(5↦3),(6↦1),(6↦2),(6↦3),(7↦1),(8↦1),(9↦1)}),(4↦2↦{(4↦3),(4↦4),(4↦5),(4↦6),(4↦7),(4↦8),(4↦9),(5↦1),(5↦2),(5↦3),(6↦1),(6↦2),(6↦3),(7↦2),(8↦2),(9↦2)}),(4↦3↦{(4↦4),(4↦5),(4↦6),(4↦7),(4↦8),(4↦9),(5↦1),(5↦2),(5↦3),(6↦1),(6↦2),(6↦3),(7↦3),(8↦3),(9↦3)}),(4↦4↦{(4↦5),(4↦6),(4↦7),(4↦8),(4↦9),(5↦4),(5↦5),(5↦6),(6↦4),(6↦5),(6↦6),(7↦4),(8↦4),(9↦4)}),(4↦5↦{(4↦6),(4↦7),(4↦8),(4↦9),(5↦4),(5↦5),(5↦6),(6↦4),(6↦5),(6↦6),(7↦5),(8↦5),(9↦5)}),(4↦6↦{(4↦7),(4↦8),(4↦9),(5↦4),(5↦5),(5↦6),(6↦4),(6↦5),(6↦6),(7↦6),(8↦6),(9↦6)}),(4↦7↦{(4↦8),(4↦9),(5↦7),(5↦8),(5↦9),(6↦7),(6↦8),(6↦9),(7↦7),(8↦7),(9↦7)}),(4↦8↦{(4↦9),(5↦7),(5↦8),(5↦9),(6↦7),(6↦8),(6↦9),(7↦8),(8↦8),(9↦8)}),(4↦9↦{(5↦7),(5↦8),(5↦9),(6↦7),(6↦8),(6↦9),(7↦9),(8↦9),(9↦9)}),(5↦1↦{(5↦2),(5↦3),(5↦4),(5↦5),(5↦6),(5↦7),(5↦8),(5↦9),(6↦1),(6↦2),(6↦3),(7↦1),(8↦1),(9↦1)}),(5↦2↦{(5↦3),(5↦4),(5↦5),(5↦6),(5↦7),(5↦8),(5↦9),(6↦1),(6↦2),(6↦3),(7↦2),(8↦2),(9↦2)}),(5↦3↦{(5↦4),(5↦5),(5↦6),(5↦7),(5↦8),(5↦9),(6↦1),(6↦2),(6↦3),(7↦3),(8↦3),(9↦3)}),(5↦4↦{(5↦5),(5↦6),(5↦7),(5↦8),(5↦9),(6↦4),(6↦5),(6↦6),(7↦4),(8↦4),(9↦4)}),(5↦5↦{(5↦6),(5↦7),(5↦8),(5↦9),(6↦4),(6↦5),(6↦6),(7↦5),(8↦5),(9↦5)}),(5↦6↦{(5↦7),(5↦8),(5↦9),(6↦4),(6↦5),(6↦6),(7↦6),(8↦6),(9↦6)}),(5↦7↦{(5↦8),(5↦9),(6↦7),(6↦8),(6↦9),(7↦7),(8↦7),(9↦7)}),(5↦8↦{(5↦9),(6↦7),(6↦8),(6↦9),(7↦8),(8↦8),(9↦8)}),(5↦9↦{(6↦7),(6↦8),(6↦9),(7↦9),(8↦9),(9↦9)}),(6↦1↦{(6↦2),(6↦3),(6↦4),(6↦5),(6↦6),(6↦7),(6↦8),(6↦9),(7↦1),(8↦1),(9↦1)}),(6↦2↦{(6↦3),(6↦4),(6↦5),(6↦6),(6↦7),(6↦8),(6↦9),(7↦2),(8↦2),(9↦2)}),(6↦3↦{(6↦4),(6↦5),(6↦6),(6↦7),(6↦8),(6↦9),(7↦3),(8↦3),(9↦3)}),(6↦4↦{(6↦5),(6↦6),(6↦7),(6↦8),(6↦9),(7↦4),(8↦4),(9↦4)}),(6↦5↦{(6↦6),(6↦7),(6↦8),(6↦9),(7↦5),(8↦5),(9↦5)}),(6↦6↦{(6↦7),(6↦8),(6↦9),(7↦6),(8↦6),(9↦6)}),(6↦7↦{(6↦8),(6↦9),(7↦7),(8↦7),(9↦7)}),(6↦8↦{(6↦9),(7↦8),(8↦8),(9↦8)}),(6↦9↦{(7↦9),(8↦9),(9↦9)}),(7↦1↦{(7↦2),(7↦3),(7↦4),(7↦5),(7↦6),(7↦7),(7↦8),(7↦9),(8↦1),(8↦2),(8↦3),(9↦1),(9↦2),(9↦3)}),(7↦2↦{(7↦3),(7↦4),(7↦5),(7↦6),(7↦7),(7↦8),(7↦9),(8↦1),(8↦2),(8↦3),(9↦1),(9↦2),(9↦3)}),(7↦3↦{(7↦4),(7↦5),(7↦6),(7↦7),(7↦8),(7↦9),(8↦1),(8↦2),(8↦3),(9↦1),(9↦2),(9↦3)}),(7↦4↦{(7↦5),(7↦6),(7↦7),(7↦8),(7↦9),(8↦4),(8↦5),(8↦6),(9↦4),(9↦5),(9↦6)}),(7↦5↦{(7↦6),(7↦7),(7↦8),(7↦9),(8↦4),(8↦5),(8↦6),(9↦4),(9↦5),(9↦6)}),(7↦6↦{(7↦7),(7↦8),(7↦9),(8↦4),(8↦5),(8↦6),(9↦4),(9↦5),(9↦6)}),(7↦7↦{(7↦8),(7↦9),(8↦7),(8↦8),(8↦9),(9↦7),(9↦8),(9↦9)}),(7↦8↦{(7↦9),(8↦7),(8↦8),(8↦9),(9↦7),(9↦8),(9↦9)}),(7↦9↦{(8↦7),(8↦8),(8↦9),(9↦7),(9↦8),(9↦9)}),(8↦1↦{(8↦2),(8↦3),(8↦4),(8↦5),(8↦6),(8↦7),(8↦8),(8↦9),(9↦1),(9↦2),(9↦3)}),(8↦2↦{(8↦3),(8↦4),(8↦5),(8↦6),(8↦7),(8↦8),(8↦9),(9↦1),(9↦2),(9↦3)}),(8↦3↦{(8↦4),(8↦5),(8↦6),(8↦7),(8↦8),(8↦9),(9↦1),(9↦2),(9↦3)}),(8↦4↦{(8↦5),(8↦6),(8↦7),(8↦8),(8↦9),(9↦4),(9↦5),(9↦6)}),(8↦5↦{(8↦6),(8↦7),(8↦8),(8↦9),(9↦4),(9↦5),(9↦6)}),(8↦6↦{(8↦7),(8↦8),(8↦9),(9↦4),(9↦5),(9↦6)}),(8↦7↦{(8↦8),(8↦9),(9↦7),(9↦8),(9↦9)}),(8↦8↦{(8↦9),(9↦7),(9↦8),(9↦9)}),(8↦9↦{(9↦7),(9↦8),(9↦9)}),(9↦1↦{(9↦2),(9↦3),(9↦4),(9↦5),(9↦6),(9↦7),(9↦8),(9↦9)}),(9↦2↦{(9↦3),(9↦4),(9↦5),(9↦6),(9↦7),(9↦8),(9↦9)}),(9↦3↦{(9↦4),(9↦5),(9↦6),(9↦7),(9↦8),(9↦9)}),(9↦4↦{(9↦5),(9↦6),(9↦7),(9↦8),(9↦9)}),(9↦5↦{(9↦6),(9↦7),(9↦8),(9↦9)}),(9↦6↦{(9↦7),(9↦8),(9↦9)}),(9↦7↦{(9↦8),(9↦9)}),(9↦8↦{(9↦9)}),(9↦9↦∅)}",
+        "PuzzleBoard": "{(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(6↦2),(7↦9),(9↦5)}),(2↦{(1↦9),(3↦2),(4↦7),(5↦1)}),(3↦{(3↦6),(4↦8),(8↦1),(9↦2)}),(4↦{(1↦2),(4↦3),(7↦8),(8↦5),(9↦1)}),(5↦{(2↦7),(3↦3),(4↦5),(9↦4)}),(6↦{(3↦8),(6↦9),(7↦3),(8↦6)}),(7↦{(1↦1),(2↦9),(6↦7),(8↦8)}),(8↦{(1↦8),(2↦6),(3↦7),(6↦3),(7↦4),(9↦9)}),(9↦{(3↦5),(7↦1)})}",
+        "get_square": "{(1↦1),(2↦1),(3↦1),(4↦2),(5↦2),(6↦2),(7↦3),(8↦3),(9↦3)}"
+      },
+      "destStateNotChanged": [],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "$initialise_machine",
+      "params": {},
+      "results": {},
+      "destState": {
+        "Board": "{(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(6↦2),(7↦9),(9↦5)}),(2↦{(1↦9),(3↦2),(4↦7),(5↦1)}),(3↦{(3↦6),(4↦8),(8↦1),(9↦2)}),(4↦{(1↦2),(4↦3),(7↦8),(8↦5),(9↦1)}),(5↦{(2↦7),(3↦3),(4↦5),(9↦4)}),(6↦{(3↦8),(6↦9),(7↦3),(8↦6)}),(7↦{(1↦1),(2↦9),(6↦7),(8↦8)}),(8↦{(1↦8),(2↦6),(3↦7),(6↦3),(7↦4),(9↦9)}),(9↦{(3↦5),(7↦1)})}",
+        "curx": "1",
+        "cury": "1"
+      },
+      "destStateNotChanged": [],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetCurPos",
+      "params": {
+        "x": "4",
+        "y": "2"
+      },
+      "results": {},
+      "destState": {
+        "curx": "4",
+        "cury": "2"
+      },
+      "destStateNotChanged": [
+        "Board"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetBoard",
+      "params": {
+        "val": "4"
+      },
+      "results": {},
+      "destState": {
+        "Board": "{(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(6↦2),(7↦9),(9↦5)}),(2↦{(1↦9),(3↦2),(4↦7),(5↦1)}),(3↦{(3↦6),(4↦8),(8↦1),(9↦2)}),(4↦{(1↦2),(2↦4),(4↦3),(7↦8),(8↦5),(9↦1)}),(5↦{(2↦7),(3↦3),(4↦5),(9↦4)}),(6↦{(3↦8),(6↦9),(7↦3),(8↦6)}),(7↦{(1↦1),(2↦9),(6↦7),(8↦8)}),(8↦{(1↦8),(2↦6),(3↦7),(6↦3),(7↦4),(9↦9)}),(9↦{(3↦5),(7↦1)})}"
+      },
+      "destStateNotChanged": [
+        "curx",
+        "cury"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetCurPos",
+      "params": {
+        "x": "6",
+        "y": "2"
+      },
+      "results": {},
+      "destState": {
+        "curx": "6"
+      },
+      "destStateNotChanged": [
+        "Board",
+        "cury"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetBoard",
+      "params": {
+        "val": "1"
+      },
+      "results": {},
+      "destState": {
+        "Board": "{(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(6↦2),(7↦9),(9↦5)}),(2↦{(1↦9),(3↦2),(4↦7),(5↦1)}),(3↦{(3↦6),(4↦8),(8↦1),(9↦2)}),(4↦{(1↦2),(2↦4),(4↦3),(7↦8),(8↦5),(9↦1)}),(5↦{(2↦7),(3↦3),(4↦5),(9↦4)}),(6↦{(2↦1),(3↦8),(6↦9),(7↦3),(8↦6)}),(7↦{(1↦1),(2↦9),(6↦7),(8↦8)}),(8↦{(1↦8),(2↦6),(3↦7),(6↦3),(7↦4),(9↦9)}),(9↦{(3↦5),(7↦1)})}"
+      },
+      "destStateNotChanged": [
+        "curx",
+        "cury"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetCurPos",
+      "params": {
+        "x": "9",
+        "y": "2"
+      },
+      "results": {},
+      "destState": {
+        "curx": "9"
+      },
+      "destStateNotChanged": [
+        "Board",
+        "cury"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetBoard",
+      "params": {
+        "val": "2"
+      },
+      "results": {},
+      "destState": {
+        "Board": "{(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(6↦2),(7↦9),(9↦5)}),(2↦{(1↦9),(3↦2),(4↦7),(5↦1)}),(3↦{(3↦6),(4↦8),(8↦1),(9↦2)}),(4↦{(1↦2),(2↦4),(4↦3),(7↦8),(8↦5),(9↦1)}),(5↦{(2↦7),(3↦3),(4↦5),(9↦4)}),(6↦{(2↦1),(3↦8),(6↦9),(7↦3),(8↦6)}),(7↦{(1↦1),(2↦9),(6↦7),(8↦8)}),(8↦{(1↦8),(2↦6),(3↦7),(6↦3),(7↦4),(9↦9)}),(9↦{(2↦2),(3↦5),(7↦1)})}"
+      },
+      "destStateNotChanged": [
+        "curx",
+        "cury"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetCurPos",
+      "params": {
+        "x": "4",
+        "y": "3"
+      },
+      "results": {},
+      "destState": {
+        "curx": "4",
+        "cury": "3"
+      },
+      "destStateNotChanged": [
+        "Board"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetBoard",
+      "params": {
+        "val": "9"
+      },
+      "results": {},
+      "destState": {
+        "Board": "{(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(6↦2),(7↦9),(9↦5)}),(2↦{(1↦9),(3↦2),(4↦7),(5↦1)}),(3↦{(3↦6),(4↦8),(8↦1),(9↦2)}),(4↦{(1↦2),(2↦4),(3↦9),(4↦3),(7↦8),(8↦5),(9↦1)}),(5↦{(2↦7),(3↦3),(4↦5),(9↦4)}),(6↦{(2↦1),(3↦8),(6↦9),(7↦3),(8↦6)}),(7↦{(1↦1),(2↦9),(6↦7),(8↦8)}),(8↦{(1↦8),(2↦6),(3↦7),(6↦3),(7↦4),(9↦9)}),(9↦{(2↦2),(3↦5),(7↦1)})}"
+      },
+      "destStateNotChanged": [
+        "curx",
+        "cury"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetCurPos",
+      "params": {
+        "x": "5",
+        "y": "1"
+      },
+      "results": {},
+      "destState": {
+        "curx": "5",
+        "cury": "1"
+      },
+      "destStateNotChanged": [
+        "Board"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetBoard",
+      "params": {
+        "val": "6"
+      },
+      "results": {},
+      "destState": {
+        "Board": "{(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(6↦2),(7↦9),(9↦5)}),(2↦{(1↦9),(3↦2),(4↦7),(5↦1)}),(3↦{(3↦6),(4↦8),(8↦1),(9↦2)}),(4↦{(1↦2),(2↦4),(3↦9),(4↦3),(7↦8),(8↦5),(9↦1)}),(5↦{(1↦6),(2↦7),(3↦3),(4↦5),(9↦4)}),(6↦{(2↦1),(3↦8),(6↦9),(7↦3),(8↦6)}),(7↦{(1↦1),(2↦9),(6↦7),(8↦8)}),(8↦{(1↦8),(2↦6),(3↦7),(6↦3),(7↦4),(9↦9)}),(9↦{(2↦2),(3↦5),(7↦1)})}"
+      },
+      "destStateNotChanged": [
+        "curx",
+        "cury"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetCurPos",
+      "params": {
+        "x": "9",
+        "y": "1"
+      },
+      "results": {},
+      "destState": {
+        "curx": "9"
+      },
+      "destStateNotChanged": [
+        "Board",
+        "cury"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetBoard",
+      "params": {
+        "val": "3"
+      },
+      "results": {},
+      "destState": {
+        "Board": "{(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(6↦2),(7↦9),(9↦5)}),(2↦{(1↦9),(3↦2),(4↦7),(5↦1)}),(3↦{(3↦6),(4↦8),(8↦1),(9↦2)}),(4↦{(1↦2),(2↦4),(3↦9),(4↦3),(7↦8),(8↦5),(9↦1)}),(5↦{(1↦6),(2↦7),(3↦3),(4↦5),(9↦4)}),(6↦{(2↦1),(3↦8),(6↦9),(7↦3),(8↦6)}),(7↦{(1↦1),(2↦9),(6↦7),(8↦8)}),(8↦{(1↦8),(2↦6),(3↦7),(6↦3),(7↦4),(9↦9)}),(9↦{(1↦3),(2↦2),(3↦5),(7↦1)})}"
+      },
+      "destStateNotChanged": [
+        "curx",
+        "cury"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetCurPos",
+      "params": {
+        "x": "7",
+        "y": "3"
+      },
+      "results": {},
+      "destState": {
+        "curx": "7",
+        "cury": "3"
+      },
+      "destStateNotChanged": [
+        "Board"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetBoard",
+      "params": {
+        "val": "4"
+      },
+      "results": {},
+      "destState": {
+        "Board": "{(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(6↦2),(7↦9),(9↦5)}),(2↦{(1↦9),(3↦2),(4↦7),(5↦1)}),(3↦{(3↦6),(4↦8),(8↦1),(9↦2)}),(4↦{(1↦2),(2↦4),(3↦9),(4↦3),(7↦8),(8↦5),(9↦1)}),(5↦{(1↦6),(2↦7),(3↦3),(4↦5),(9↦4)}),(6↦{(2↦1),(3↦8),(6↦9),(7↦3),(8↦6)}),(7↦{(1↦1),(2↦9),(3↦4),(6↦7),(8↦8)}),(8↦{(1↦8),(2↦6),(3↦7),(6↦3),(7↦4),(9↦9)}),(9↦{(1↦3),(2↦2),(3↦5),(7↦1)})}"
+      },
+      "destStateNotChanged": [
+        "curx",
+        "cury"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetCurPos",
+      "params": {
+        "x": "3",
+        "y": "1"
+      },
+      "results": {},
+      "destState": {
+        "curx": "3",
+        "cury": "1"
+      },
+      "destStateNotChanged": [
+        "Board"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetBoard",
+      "params": {
+        "val": "4"
+      },
+      "results": {},
+      "destState": {
+        "Board": "{(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(6↦2),(7↦9),(9↦5)}),(2↦{(1↦9),(3↦2),(4↦7),(5↦1)}),(3↦{(1↦4),(3↦6),(4↦8),(8↦1),(9↦2)}),(4↦{(1↦2),(2↦4),(3↦9),(4↦3),(7↦8),(8↦5),(9↦1)}),(5↦{(1↦6),(2↦7),(3↦3),(4↦5),(9↦4)}),(6↦{(2↦1),(3↦8),(6↦9),(7↦3),(8↦6)}),(7↦{(1↦1),(2↦9),(3↦4),(6↦7),(8↦8)}),(8↦{(1↦8),(2↦6),(3↦7),(6↦3),(7↦4),(9↦9)}),(9↦{(1↦3),(2↦2),(3↦5),(7↦1)})}"
+      },
+      "destStateNotChanged": [
+        "curx",
+        "cury"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetCurPos",
+      "params": {
+        "x": "6",
+        "y": "1"
+      },
+      "results": {},
+      "destState": {
+        "curx": "6"
+      },
+      "destStateNotChanged": [
+        "Board",
+        "cury"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetBoard",
+      "params": {
+        "val": "5"
+      },
+      "results": {},
+      "destState": {
+        "Board": "{(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(6↦2),(7↦9),(9↦5)}),(2↦{(1↦9),(3↦2),(4↦7),(5↦1)}),(3↦{(1↦4),(3↦6),(4↦8),(8↦1),(9↦2)}),(4↦{(1↦2),(2↦4),(3↦9),(4↦3),(7↦8),(8↦5),(9↦1)}),(5↦{(1↦6),(2↦7),(3↦3),(4↦5),(9↦4)}),(6↦{(1↦5),(2↦1),(3↦8),(6↦9),(7↦3),(8↦6)}),(7↦{(1↦1),(2↦9),(3↦4),(6↦7),(8↦8)}),(8↦{(1↦8),(2↦6),(3↦7),(6↦3),(7↦4),(9↦9)}),(9↦{(1↦3),(2↦2),(3↦5),(7↦1)})}"
+      },
+      "destStateNotChanged": [
+        "curx",
+        "cury"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetCurPos",
+      "params": {
+        "x": "9",
+        "y": "1"
+      },
+      "results": {},
+      "destState": {
+        "curx": "9"
+      },
+      "destStateNotChanged": [
+        "Board",
+        "cury"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetCurPos",
+      "params": {
+        "x": "7",
+        "y": "9"
+      },
+      "results": {},
+      "destState": {
+        "curx": "7",
+        "cury": "9"
+      },
+      "destStateNotChanged": [
+        "Board"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "SetBoard",
+      "params": {
+        "val": "3"
+      },
+      "results": {},
+      "destState": {
+        "Board": "{(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(6↦2),(7↦9),(9↦5)}),(2↦{(1↦9),(3↦2),(4↦7),(5↦1)}),(3↦{(1↦4),(3↦6),(4↦8),(8↦1),(9↦2)}),(4↦{(1↦2),(2↦4),(3↦9),(4↦3),(7↦8),(8↦5),(9↦1)}),(5↦{(1↦6),(2↦7),(3↦3),(4↦5),(9↦4)}),(6↦{(1↦5),(2↦1),(3↦8),(6↦9),(7↦3),(8↦6)}),(7↦{(1↦1),(2↦9),(3↦4),(6↦7),(8↦8),(9↦3)}),(8↦{(1↦8),(2↦6),(3↦7),(6↦3),(7↦4),(9↦9)}),(9↦{(1↦3),(2↦2),(3↦5),(7↦1)})}"
+      },
+      "destStateNotChanged": [
+        "curx",
+        "cury"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    },
+    {
+      "name": "Solve",
+      "params": {
+        "SBoard": "{(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(5↦3),(6↦2),(7↦9),(8↦4),(9↦5)}),(2↦{(1↦9),(2↦5),(3↦2),(4↦7),(5↦1),(6↦4),(7↦6),(8↦3),(9↦8)}),(3↦{(1↦4),(2↦3),(3↦6),(4↦8),(5↦9),(6↦5),(7↦7),(8↦1),(9↦2)}),(4↦{(1↦2),(2↦4),(3↦9),(4↦3),(5↦7),(6↦6),(7↦8),(8↦5),(9↦1)}),(5↦{(1↦6),(2↦7),(3↦3),(4↦5),(5↦8),(6↦1),(7↦2),(8↦9),(9↦4)}),(6↦{(1↦5),(2↦1),(3↦8),(4↦4),(5↦2),(6↦9),(7↦3),(8↦6),(9↦7)}),(7↦{(1↦1),(2↦9),(3↦4),(4↦2),(5↦6),(6↦7),(7↦5),(8↦8),(9↦3)}),(8↦{(1↦8),(2↦6),(3↦7),(4↦1),(5↦5),(6↦3),(7↦4),(8↦2),(9↦9)}),(9↦{(1↦3),(2↦2),(3↦5),(4↦9),(5↦4),(6↦8),(7↦1),(8↦7),(9↦6)})}"
+      },
+      "results": {},
+      "destState": {
+        "Board": "{(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(5↦3),(6↦2),(7↦9),(8↦4),(9↦5)}),(2↦{(1↦9),(2↦5),(3↦2),(4↦7),(5↦1),(6↦4),(7↦6),(8↦3),(9↦8)}),(3↦{(1↦4),(2↦3),(3↦6),(4↦8),(5↦9),(6↦5),(7↦7),(8↦1),(9↦2)}),(4↦{(1↦2),(2↦4),(3↦9),(4↦3),(5↦7),(6↦6),(7↦8),(8↦5),(9↦1)}),(5↦{(1↦6),(2↦7),(3↦3),(4↦5),(5↦8),(6↦1),(7↦2),(8↦9),(9↦4)}),(6↦{(1↦5),(2↦1),(3↦8),(4↦4),(5↦2),(6↦9),(7↦3),(8↦6),(9↦7)}),(7↦{(1↦1),(2↦9),(3↦4),(4↦2),(5↦6),(6↦7),(7↦5),(8↦8),(9↦3)}),(8↦{(1↦8),(2↦6),(3↦7),(4↦1),(5↦5),(6↦3),(7↦4),(8↦2),(9↦9)}),(9↦{(1↦3),(2↦2),(3↦5),(4↦9),(5↦4),(6↦8),(7↦1),(8↦7),(9↦6)})}"
+      },
+      "destStateNotChanged": [
+        "curx",
+        "cury"
+      ],
+      "preds": [],
+      "postconditions": [],
+      "description": ""
+    }
+  ],
+  "variableNames": [
+    "Board",
+    "curx",
+    "cury"
+  ],
+  "constantNames": [
+    "get_square",
+    "conflict_pos",
+    "conflict_pos_sym",
+    "PuzzleBoard"
+  ],
+  "setNames": [],
+  "machineOperationInfos": {
+    "SetCurPos": {
+      "operationName": "SetCurPos",
+      "parameterNames": [
+        "x",
+        "y"
+      ],
+      "outputParameterNames": [],
+      "topLevel": true,
+      "type": "CLASSICAL_B",
+      "readVariables": [],
+      "writtenVariables": [
+        "curx",
+        "cury"
+      ],
+      "nonDetWrittenVariables": [],
+      "typeMap": {
+        "x": "integer",
+        "y": "integer"
+      }
+    },
+    "SetEmpty": {
+      "operationName": "SetEmpty",
+      "parameterNames": [],
+      "outputParameterNames": [],
+      "topLevel": true,
+      "type": "CLASSICAL_B",
+      "readVariables": [],
+      "writtenVariables": [
+        "Board"
+      ],
+      "nonDetWrittenVariables": [],
+      "typeMap": {
+        "'Board'": "set(couple(integer,set(couple(integer,integer))))"
+      }
+    },
+    "SetPuzzle": {
+      "operationName": "SetPuzzle",
+      "parameterNames": [],
+      "outputParameterNames": [],
+      "topLevel": true,
+      "type": "CLASSICAL_B",
+      "readVariables": [
+        "PuzzleBoard"
+      ],
+      "writtenVariables": [
+        "Board"
+      ],
+      "nonDetWrittenVariables": [],
+      "typeMap": {
+        "'Board'": "set(couple(integer,set(couple(integer,integer))))",
+        "'PuzzleBoard'": "set(couple(integer,set(couple(integer,integer))))"
+      }
+    },
+    "ClearCurPos": {
+      "operationName": "ClearCurPos",
+      "parameterNames": [],
+      "outputParameterNames": [],
+      "topLevel": true,
+      "type": "CLASSICAL_B",
+      "readVariables": [
+        "Board",
+        "curx",
+        "cury"
+      ],
+      "writtenVariables": [
+        "Board"
+      ],
+      "nonDetWrittenVariables": [],
+      "typeMap": {
+        "'Board'": "set(couple(integer,set(couple(integer,integer))))"
+      }
+    },
+    "Solve": {
+      "operationName": "Solve",
+      "parameterNames": [
+        "SBoard"
+      ],
+      "outputParameterNames": [],
+      "topLevel": true,
+      "type": "CLASSICAL_B",
+      "readVariables": [
+        "Board",
+        "conflict_pos_sym"
+      ],
+      "writtenVariables": [
+        "Board"
+      ],
+      "nonDetWrittenVariables": [],
+      "typeMap": {
+        "'SBoard'": "set(couple(integer,set(couple(integer,integer))))",
+        "'Board'": "set(couple(integer,set(couple(integer,integer))))"
+      }
+    },
+    "SetBoard": {
+      "operationName": "SetBoard",
+      "parameterNames": [
+        "val"
+      ],
+      "outputParameterNames": [],
+      "topLevel": true,
+      "type": "CLASSICAL_B",
+      "readVariables": [
+        "Board",
+        "curx",
+        "cury"
+      ],
+      "writtenVariables": [
+        "Board"
+      ],
+      "nonDetWrittenVariables": [],
+      "typeMap": {
+        "val": "integer",
+        "'Board'": "set(couple(integer,set(couple(integer,integer))))"
+      }
+    },
+    "GetPossibleVals": {
+      "operationName": "GetPossibleVals",
+      "parameterNames": [],
+      "outputParameterNames": [
+        "res"
+      ],
+      "topLevel": true,
+      "type": "CLASSICAL_B",
+      "readVariables": [
+        "Board",
+        "conflict_pos",
+        "curx",
+        "cury"
+      ],
+      "writtenVariables": [],
+      "nonDetWrittenVariables": [],
+      "typeMap": {
+        "res": "set(integer)",
+        "'Board'": "set(couple(integer,set(couple(integer,integer))))"
+      }
+    }
+  },
+  "globalIdentifierTypes": {
+    "conflict_pos_sym": "set(couple(couple(integer,integer),set(couple(integer,integer))))",
+    "curx": "integer",
+    "cury": "integer",
+    "conflict_pos": "set(couple(couple(integer,integer),set(couple(integer,integer))))"
+  },
+  "metadata": {
+    "fileType": "Trace",
+    "formatVersion": 4,
+    "savedAt": "2021-06-30T17:11:00.133336Z",
+    "creator": "traceReplay",
+    "proB2KernelVersion": "4.0.0-SNAPSHOT",
+    "proBCliVersion": "1.11.0-nightly",
+    "modelName": "SudokuEvent"
+  }
+}
\ No newline at end of file