diff --git a/notebooks/tests/CrosswordPuzzle.mch b/notebooks/tests/CrosswordPuzzle.mch new file mode 100644 index 0000000000000000000000000000000000000000..99b4da8d18fd29135b8d977ecd2c1e7b5212fa31 --- /dev/null +++ b/notebooks/tests/CrosswordPuzzle.mch @@ -0,0 +1,69 @@ +MACHINE CrosswordPuzzle +/* Crossword puzzle taken from pages 3-4 of "Dechter, Rina. Constraint Processing, 2003." +*/ +SETS + Letters = {A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z} +CONSTANTS words, chosen +PROPERTIES + /* list of available words : */ + words = [ [H,O,S,E,S], [L,A,S,E,R], [S,H,E,E,T], [S,N,A,I,L], [S,T,E,E,R], + [A,L,S,O], [E,A,R,N], [H,I,K,E], [I,R,O,N], + [S,A,M,E], [E,A,T], [L,E,T], [R,U,N], [S,U,N], [T,E,N], [Y,E,S], + [B,E], [I,T], [N,O], [U,S] , [O,O] /* added OO as otherwise puzzle seems unsolvable ? */ + ] + & + chosen : 1..6 >-> dom(words) /* 1-3 vertical, 5-6 horizontal */ + & +/* length of the words: */ + size(words(chosen(1))) = 5 & + size(words(chosen(2))) = 4 & + size(words(chosen(3))) = 2 & + size(words(chosen(4))) = 4 & + size(words(chosen(5))) = 2 & + size(words(chosen(6))) = 3 & + +/* overlap constraints: */ + words(chosen(1))(3) = words(chosen(4))(1) & + words(chosen(1))(5) = words(chosen(6))(1) & + words(chosen(2))(2) = words(chosen(4))(3) & + words(chosen(2))(3) = words(chosen(5))(1) & + words(chosen(2))(4) = words(chosen(6))(3) & + words(chosen(3))(1) = words(chosen(4))(4) & + words(chosen(3))(2) = words(chosen(5))(2) +DEFINITIONS + ANIMATION_FUNCTION_DEFAULT == %(r,c).(r:1..4 & c:1..5|0); + ANIMATION_FUNCTION == %(r,c).(r=1&c:1..5|words(chosen(1))(c)) \/ + %(r,c).(r=3&c:2..5|words(chosen(2))(c-1)) \/ + %(r,c).(r=4&c:3..4|words(chosen(3))(c-2)) \/ + {(2,3,words(chosen(4))(2)), (2,5,words(chosen(6))(2))}; + ANIMATION_STR0 == "-"; + ANIMATION_STR1 == "A"; + ANIMATION_STR2 == "B"; + ANIMATION_STR3 == "C"; + ANIMATION_STR4 == "D"; + ANIMATION_STR5 == "E"; + ANIMATION_STR6 == "F"; + ANIMATION_STR7 == "G"; + ANIMATION_STR8 == "H"; + ANIMATION_STR9 == "I"; + ANIMATION_STR10 == "J"; + ANIMATION_STR11 == "K"; + ANIMATION_STR12 == "L"; + ANIMATION_STR13 == "M"; + ANIMATION_STR14 == "N"; + ANIMATION_STR15 == "O"; + ANIMATION_STR16 == "P"; + ANIMATION_STR17 == "Q"; + ANIMATION_STR18 == "R"; + ANIMATION_STR19 == "S"; + ANIMATION_STR20 == "T"; + ANIMATION_STR21 == "U"; + ANIMATION_STR22 == "V"; + ANIMATION_STR23 == "W"; + ANIMATION_STR24 == "X"; + ANIMATION_STR25 == "Y"; + ANIMATION_STR26 == "Z" +ASSERTIONS + %i.(i:1..6|size(words(chosen(i)))) = [5,4,2, 4,2,3] /* length of the words ; this is not good for constraint solving as lambda not expanded!?; TO DO : improve in ProB kernel */ +END + diff --git a/notebooks/tests/show.ipynb b/notebooks/tests/show.ipynb index de67d5392128eeeb723931c41ae102d31829d17f..9ee27a253e74bd9ee4665e1d9aaf3c5098647e7f 100644 --- a/notebooks/tests/show.ipynb +++ b/notebooks/tests/show.ipynb @@ -317,6 +317,125 @@ "source": [ ":show" ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Text labels are supported." + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Loaded machine: CrosswordPuzzle : []\n" + ] + }, + "execution_count": 12, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":load CrosswordPuzzle.mch" + ] + }, + { + "cell_type": "code", + "execution_count": 13, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Machine constants set up using operation 0: $setup_constants()" + ] + }, + "execution_count": 13, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":constants" + ] + }, + { + "cell_type": "code", + "execution_count": 14, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Machine initialised using operation 1: $initialise_machine()" + ] + }, + "execution_count": 14, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":init" + ] + }, + { + "cell_type": "code", + "execution_count": 15, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "<table><tbody>\n", + "<tr>\n", + "<td style=\"padding:0\">S</td>\n", + "<td style=\"padding:0\">T</td>\n", + "<td style=\"padding:0\">E</td>\n", + "<td style=\"padding:0\">E</td>\n", + "<td style=\"padding:0\">R</td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:0\">-</td>\n", + "<td style=\"padding:0\">-</td>\n", + "<td style=\"padding:0\">A</td>\n", + "<td style=\"padding:0\">-</td>\n", + "<td style=\"padding:0\">U</td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:0\">-</td>\n", + "<td style=\"padding:0\">I</td>\n", + "<td style=\"padding:0\">R</td>\n", + "<td style=\"padding:0\">O</td>\n", + "<td style=\"padding:0\">N</td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:0\">-</td>\n", + "<td style=\"padding:0\">-</td>\n", + "<td style=\"padding:0\">N</td>\n", + "<td style=\"padding:0\">O</td>\n", + "<td style=\"padding:0\">-</td>\n", + "</tr>\n", + "</tbody></table>" + ], + "text/plain": [ + "<Animation function visualisation>" + ] + }, + "execution_count": 15, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":show" + ] } ], "metadata": { diff --git a/src/main/java/de/prob2/jupyter/commands/ShowCommand.java b/src/main/java/de/prob2/jupyter/commands/ShowCommand.java index 66539e007ac1011965999a41f7ea4cfdb763bbbd..16db1723877dd31ae80e54b48e34cc6fe8122c66 100644 --- a/src/main/java/de/prob2/jupyter/commands/ShowCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/ShowCommand.java @@ -1,11 +1,12 @@ package de.prob2.jupyter.commands; +import java.util.List; import java.util.Map; import com.google.inject.Inject; +import de.prob.animator.command.GetAnimationMatrixForStateCommand; import de.prob.animator.command.GetImagesForMachineCommand; -import de.prob.animator.command.GetImagesForStateCommand; import de.prob.statespace.AnimationSelector; import de.prob.statespace.Trace; @@ -58,14 +59,26 @@ public final class ShowCommand implements Command { trace.getStateSpace().execute(cmd1); final Map<Integer, String> images = cmd1.getImages(); - final GetImagesForStateCommand cmd2 = new GetImagesForStateCommand(trace.getCurrentState().getId()); + final GetAnimationMatrixForStateCommand cmd2 = new GetAnimationMatrixForStateCommand(trace.getCurrentState()); trace.getStateSpace().execute(cmd2); + if (cmd2.getMatrix() == null) { + throw new UserErrorException("No animation function visualisation available"); + } + final StringBuilder tableBuilder = new StringBuilder("<table><tbody>"); - for (final Integer[] row : cmd2.getMatrix()) { + for (final List<Object> row : cmd2.getMatrix()) { tableBuilder.append("\n<tr>"); - for (final Integer id : row) { - tableBuilder.append(String.format("\n<td style=\"padding:0\"></td>", id, images.get(id))); + for (final Object entry : row) { + tableBuilder.append("\n<td style=\"padding:0\">"); + if (entry instanceof Integer) { + tableBuilder.append(String.format("", entry, images.get(entry))); + } else if (entry instanceof String) { + tableBuilder.append(entry); + } else { + throw new AssertionError("Unhandled animation matrix entry type: " + entry.getClass()); + } + tableBuilder.append("</td>"); } tableBuilder.append("\n</tr>"); }