Skip to content
Snippets Groups Projects
Commit 9aba132d authored by dgelessus's avatar dgelessus
Browse files

Add initial VisB support to :show

parent bbb74533
Branches
No related tags found
No related merge requests found
Pipeline #117106 passed
...@@ -7,6 +7,7 @@ ...@@ -7,6 +7,7 @@
## [1.4.1](https://stups.hhu-hosting.de/downloads/prob2-jupyter/prob2-jupyter-kernel-1.4.1-all.jar) ## [1.4.1](https://stups.hhu-hosting.de/downloads/prob2-jupyter/prob2-jupyter-kernel-1.4.1-all.jar)
* Updated to ProB 1.12.1 (ProB Java API version 4.12.1). * Updated to ProB 1.12.1 (ProB Java API version 4.12.1).
* `:show` now also supports VisB visualizations in addition to the classical `ANIMATION_FUNCTION`.
## [1.4.0](https://stups.hhu-hosting.de/downloads/prob2-jupyter/prob2-jupyter-kernel-1.4.0-all.jar) ## [1.4.0](https://stups.hhu-hosting.de/downloads/prob2-jupyter/prob2-jupyter-kernel-1.4.0-all.jar)
......
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:help :show :help :show
``` ```
%% Output %% Output
``` ```
:show :show
``` ```
Show the machine's animation function visualisation for the current state. Show the machine's visualization for the current state.
The visualisation is static, any defined right-click options cannot be viewed or used. Only the current state is visualized. Interactively executing operations is not supported.
Both VisB and the classical `ANIMATION_FUNCTION` are supported. The visualization type is detected automatically (if both are defined, VisB is preferred).
:show :show
Show the machine's animation function visualisation for the current state. Show the machine's visualization for the current state.
Only the current state is visualized. Interactively executing operations is not supported.
The visualisation is static, any defined right-click options cannot be viewed or used. Both VisB and the classical `ANIMATION_FUNCTION` are supported. The visualization type is detected automatically (if both are defined, VisB is preferred).
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:load Hanoi.mch :load Hanoi.mch
``` ```
%% Output %% Output
Loaded machine: Hanoi Loaded machine: Hanoi
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:show :show
``` ```
%% Output %% Output
:show: Machine is not initialised, cannot show animation function visualisation :show: Model is not initialized, cannot show visualization (or no visualization is defined)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants :constants
``` ```
%% Output %% Output
Executed operation: SETUP_CONSTANTS() Executed operation: SETUP_CONSTANTS()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:show :show
``` ```
%% Output %% Output
:show: Machine is not initialised, cannot show animation function visualisation :show: Model is not initialized, cannot show visualization (or no visualization is defined)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:init :init
``` ```
%% Output %% Output
Executed operation: INITIALISATION() Executed operation: INITIALISATION()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:show :show
``` ```
%% Output %% Output
<table style="font-family:monospace"><tbody> <table style="font-family:monospace"><tbody>
<tr> <tr>
<td style="padding:0px"><img alt="1" src="images/Disc1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/Disc1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="2" src="images/Disc2.gif"/></td> <td style="padding:0px"><img alt="2" src="images/Disc2.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="3" src="images/Disc3.gif"/></td> <td style="padding:0px"><img alt="3" src="images/Disc3.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="4" src="images/Disc4.gif"/></td> <td style="padding:0px"><img alt="4" src="images/Disc4.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="5" src="images/Disc5.gif"/></td> <td style="padding:0px"><img alt="5" src="images/Disc5.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualization>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Move :exec Move
``` ```
%% Output %% Output
Executed operation: Move(orig,dest,1) Executed operation: Move(orig,dest,1)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:show :show
``` ```
%% Output %% Output
<table style="font-family:monospace"><tbody> <table style="font-family:monospace"><tbody>
<tr> <tr>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="2" src="images/Disc2.gif"/></td> <td style="padding:0px"><img alt="2" src="images/Disc2.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="3" src="images/Disc3.gif"/></td> <td style="padding:0px"><img alt="3" src="images/Disc3.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="4" src="images/Disc4.gif"/></td> <td style="padding:0px"><img alt="4" src="images/Disc4.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="5" src="images/Disc5.gif"/></td> <td style="padding:0px"><img alt="5" src="images/Disc5.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Disc1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/Disc1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualization>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Move :exec Move
``` ```
%% Output %% Output
Executed operation: Move(orig,Stakes3,2) Executed operation: Move(orig,Stakes3,2)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:show :show
``` ```
%% Output %% Output
<table style="font-family:monospace"><tbody> <table style="font-family:monospace"><tbody>
<tr> <tr>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="3" src="images/Disc3.gif"/></td> <td style="padding:0px"><img alt="3" src="images/Disc3.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="4" src="images/Disc4.gif"/></td> <td style="padding:0px"><img alt="4" src="images/Disc4.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:0px"><img alt="0" src="images/Disc_empty.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="5" src="images/Disc5.gif"/></td> <td style="padding:0px"><img alt="5" src="images/Disc5.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Disc1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/Disc1.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Disc2.gif"/></td> <td style="padding:0px"><img alt="2" src="images/Disc2.gif"/></td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualization>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
The image padding preference is respected. The image padding preference is respected.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:pref TK_CUSTOM_STATE_VIEW_PADDING=8 :pref TK_CUSTOM_STATE_VIEW_PADDING=8
``` ```
%% Output %% Output
Preference changed: TK_CUSTOM_STATE_VIEW_PADDING = 8 Preference changed: TK_CUSTOM_STATE_VIEW_PADDING = 8
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:show :show
``` ```
%% Output %% Output
<table style="font-family:monospace"><tbody> <table style="font-family:monospace"><tbody>
<tr> <tr>
<td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:8px"><img alt="3" src="images/Disc3.gif"/></td> <td style="padding:8px"><img alt="3" src="images/Disc3.gif"/></td>
<td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:8px"><img alt="4" src="images/Disc4.gif"/></td> <td style="padding:8px"><img alt="4" src="images/Disc4.gif"/></td>
<td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td>
<td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td> <td style="padding:8px"><img alt="0" src="images/Disc_empty.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:8px"><img alt="5" src="images/Disc5.gif"/></td> <td style="padding:8px"><img alt="5" src="images/Disc5.gif"/></td>
<td style="padding:8px"><img alt="1" src="images/Disc1.gif"/></td> <td style="padding:8px"><img alt="1" src="images/Disc1.gif"/></td>
<td style="padding:8px"><img alt="2" src="images/Disc2.gif"/></td> <td style="padding:8px"><img alt="2" src="images/Disc2.gif"/></td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualization>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Text labels are supported. Text labels are supported.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:load CrosswordPuzzle.mch :load CrosswordPuzzle.mch
``` ```
%% Output %% Output
Loaded machine: CrosswordPuzzle Loaded machine: CrosswordPuzzle
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants :constants
``` ```
%% Output %% Output
Executed operation: SETUP_CONSTANTS() Executed operation: SETUP_CONSTANTS()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:init :init
``` ```
%% Output %% Output
Executed operation: INITIALISATION() Executed operation: INITIALISATION()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:show :show
``` ```
%% Output %% Output
<table style="font-family:monospace"><tbody> <table style="font-family:monospace"><tbody>
<tr> <tr>
<td style="padding:10px">S</td> <td style="padding:10px">S</td>
<td style="padding:10px">T</td> <td style="padding:10px">T</td>
<td style="padding:10px">E</td> <td style="padding:10px">E</td>
<td style="padding:10px">E</td> <td style="padding:10px">E</td>
<td style="padding:10px">R</td> <td style="padding:10px">R</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">-</td> <td style="padding:10px">-</td>
<td style="padding:10px">-</td> <td style="padding:10px">-</td>
<td style="padding:10px">A</td> <td style="padding:10px">A</td>
<td style="padding:10px">-</td> <td style="padding:10px">-</td>
<td style="padding:10px">U</td> <td style="padding:10px">U</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">-</td> <td style="padding:10px">-</td>
<td style="padding:10px">I</td> <td style="padding:10px">I</td>
<td style="padding:10px">R</td> <td style="padding:10px">R</td>
<td style="padding:10px">O</td> <td style="padding:10px">O</td>
<td style="padding:10px">N</td> <td style="padding:10px">N</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">-</td> <td style="padding:10px">-</td>
<td style="padding:10px">-</td> <td style="padding:10px">-</td>
<td style="padding:10px">N</td> <td style="padding:10px">N</td>
<td style="padding:10px">O</td> <td style="padding:10px">O</td>
<td style="padding:10px">-</td> <td style="padding:10px">-</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualization>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
The text padding preference is respected. The text padding preference is respected.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:pref TK_CUSTOM_STATE_VIEW_STRING_PADDING=2 :pref TK_CUSTOM_STATE_VIEW_STRING_PADDING=2
``` ```
%% Output %% Output
Preference changed: TK_CUSTOM_STATE_VIEW_STRING_PADDING = 2 Preference changed: TK_CUSTOM_STATE_VIEW_STRING_PADDING = 2
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:show :show
``` ```
%% Output %% Output
<table style="font-family:monospace"><tbody> <table style="font-family:monospace"><tbody>
<tr> <tr>
<td style="padding:2px">S</td> <td style="padding:2px">S</td>
<td style="padding:2px">T</td> <td style="padding:2px">T</td>
<td style="padding:2px">E</td> <td style="padding:2px">E</td>
<td style="padding:2px">E</td> <td style="padding:2px">E</td>
<td style="padding:2px">R</td> <td style="padding:2px">R</td>
</tr> </tr>
<tr> <tr>
<td style="padding:2px">-</td> <td style="padding:2px">-</td>
<td style="padding:2px">-</td> <td style="padding:2px">-</td>
<td style="padding:2px">A</td> <td style="padding:2px">A</td>
<td style="padding:2px">-</td> <td style="padding:2px">-</td>
<td style="padding:2px">U</td> <td style="padding:2px">U</td>
</tr> </tr>
<tr> <tr>
<td style="padding:2px">-</td> <td style="padding:2px">-</td>
<td style="padding:2px">I</td> <td style="padding:2px">I</td>
<td style="padding:2px">R</td> <td style="padding:2px">R</td>
<td style="padding:2px">O</td> <td style="padding:2px">O</td>
<td style="padding:2px">N</td> <td style="padding:2px">N</td>
</tr> </tr>
<tr> <tr>
<td style="padding:2px">-</td> <td style="padding:2px">-</td>
<td style="padding:2px">-</td> <td style="padding:2px">-</td>
<td style="padding:2px">N</td> <td style="padding:2px">N</td>
<td style="padding:2px">O</td> <td style="padding:2px">O</td>
<td style="padding:2px">-</td> <td style="padding:2px">-</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualization>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
The font name and size preferences are supported. The font name and size preferences are supported.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:pref TK_CUSTOM_STATE_VIEW_FONT_NAME=Arial TK_CUSTOM_STATE_VIEW_FONT_SIZE=18 :pref TK_CUSTOM_STATE_VIEW_FONT_NAME=Arial TK_CUSTOM_STATE_VIEW_FONT_SIZE=18
``` ```
%% Output %% Output
Preference changed: TK_CUSTOM_STATE_VIEW_FONT_SIZE = 18 Preference changed: TK_CUSTOM_STATE_VIEW_FONT_SIZE = 18
Preference changed: TK_CUSTOM_STATE_VIEW_FONT_NAME = Arial Preference changed: TK_CUSTOM_STATE_VIEW_FONT_NAME = Arial
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:show :show
``` ```
%% Output %% Output
<table style="font-family:"Arial" monospace;font-size:18px"><tbody> <table style="font-family:"Arial" monospace;font-size:18px"><tbody>
<tr> <tr>
<td style="padding:2px">S</td> <td style="padding:2px">S</td>
<td style="padding:2px">T</td> <td style="padding:2px">T</td>
<td style="padding:2px">E</td> <td style="padding:2px">E</td>
<td style="padding:2px">E</td> <td style="padding:2px">E</td>
<td style="padding:2px">R</td> <td style="padding:2px">R</td>
</tr> </tr>
<tr> <tr>
<td style="padding:2px">-</td> <td style="padding:2px">-</td>
<td style="padding:2px">-</td> <td style="padding:2px">-</td>
<td style="padding:2px">A</td> <td style="padding:2px">A</td>
<td style="padding:2px">-</td> <td style="padding:2px">-</td>
<td style="padding:2px">U</td> <td style="padding:2px">U</td>
</tr> </tr>
<tr> <tr>
<td style="padding:2px">-</td> <td style="padding:2px">-</td>
<td style="padding:2px">I</td> <td style="padding:2px">I</td>
<td style="padding:2px">R</td> <td style="padding:2px">R</td>
<td style="padding:2px">O</td> <td style="padding:2px">O</td>
<td style="padding:2px">N</td> <td style="padding:2px">N</td>
</tr> </tr>
<tr> <tr>
<td style="padding:2px">-</td> <td style="padding:2px">-</td>
<td style="padding:2px">-</td> <td style="padding:2px">-</td>
<td style="padding:2px">N</td> <td style="padding:2px">N</td>
<td style="padding:2px">O</td> <td style="padding:2px">O</td>
<td style="padding:2px">-</td> <td style="padding:2px">-</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualization>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Empty cells are supported. Empty cells are supported.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:load AnimationFunctionTestProB2.mch :load AnimationFunctionTestProB2.mch
``` ```
%% Output %% Output
Loaded machine: AnimationFunctionTestProB2 Loaded machine: AnimationFunctionTestProB2
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants :constants
``` ```
%% Output %% Output
Executed operation: SETUP_CONSTANTS() Executed operation: SETUP_CONSTANTS()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:init :init
``` ```
%% Output %% Output
Executed operation: INITIALISATION() Executed operation: INITIALISATION()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:show :show
``` ```
%% Output %% Output
<table style="font-family:"Arial" monospace;font-size:18px"><tbody> <table style="font-family:"Arial" monospace;font-size:18px"><tbody>
<tr> <tr>
<td style="padding:2px">Overview</td> <td style="padding:2px">Overview</td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:8px"><img alt="0" src="images/small_empty_w.gif"/></td> <td style="padding:8px"><img alt="0" src="images/small_empty_w.gif"/></td>
<td style="padding:8px"><img alt="1" src="images/small_wqueen_w.gif"/></td> <td style="padding:8px"><img alt="1" src="images/small_wqueen_w.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:8px"><img alt="1" src="images/small_wqueen_w.gif"/></td> <td style="padding:8px"><img alt="1" src="images/small_wqueen_w.gif"/></td>
<td style="padding:8px"><img alt="0" src="images/small_empty_w.gif"/></td> <td style="padding:8px"><img alt="0" src="images/small_empty_w.gif"/></td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualization>
......
...@@ -12,9 +12,12 @@ import com.google.inject.Provider; ...@@ -12,9 +12,12 @@ import com.google.inject.Provider;
import de.prob.animator.command.GetAnimationMatrixForStateCommand; import de.prob.animator.command.GetAnimationMatrixForStateCommand;
import de.prob.animator.command.GetImagesForMachineCommand; import de.prob.animator.command.GetImagesForMachineCommand;
import de.prob.animator.command.GetPreferenceCommand; import de.prob.animator.command.GetPreferenceCommand;
import de.prob.animator.command.GetVisBHtmlForStates;
import de.prob.animator.command.GetVisBLoadedJsonFileCommand;
import de.prob.animator.command.LoadVisBCommand;
import de.prob.animator.domainobjects.AnimationMatrixEntry; import de.prob.animator.domainobjects.AnimationMatrixEntry;
import de.prob.statespace.AnimationSelector; import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace; import de.prob.statespace.State;
import de.prob2.jupyter.Command; import de.prob2.jupyter.Command;
import de.prob2.jupyter.ParameterCompleters; import de.prob2.jupyter.ParameterCompleters;
import de.prob2.jupyter.ParameterInspectors; import de.prob2.jupyter.ParameterInspectors;
...@@ -26,6 +29,7 @@ import de.prob2.jupyter.UserErrorException; ...@@ -26,6 +29,7 @@ import de.prob2.jupyter.UserErrorException;
import io.github.spencerpark.jupyter.kernel.display.DisplayData; import io.github.spencerpark.jupyter.kernel.display.DisplayData;
import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class ShowCommand implements Command { public final class ShowCommand implements Command {
private final @NotNull AnimationSelector animationSelector; private final @NotNull AnimationSelector animationSelector;
...@@ -56,29 +60,23 @@ public final class ShowCommand implements Command { ...@@ -56,29 +60,23 @@ public final class ShowCommand implements Command {
@Override @Override
public @NotNull String getShortHelp() { public @NotNull String getShortHelp() {
return "Show the machine's animation function visualisation for the current state."; return "Show the machine's visualization for the current state.";
} }
@Override @Override
public @NotNull String getHelpBody() { public @NotNull String getHelpBody() {
return "The visualisation is static, any defined right-click options cannot be viewed or used."; return "Only the current state is visualized. Interactively executing operations is not supported.\n\n"
} + "Both VisB and the classical `ANIMATION_FUNCTION` are supported. The visualization type is detected automatically (if both are defined, VisB is preferred).";
@Override
public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
if (!trace.getCurrentState().isInitialised()) {
throw new UserErrorException("Machine is not initialised, cannot show animation function visualisation");
} }
private @Nullable DisplayData getAnimationFunctionVisualization(final @NotNull State state) {
final GetImagesForMachineCommand cmdImages = new GetImagesForMachineCommand(); final GetImagesForMachineCommand cmdImages = new GetImagesForMachineCommand();
final GetAnimationMatrixForStateCommand cmdMatrix = new GetAnimationMatrixForStateCommand(trace.getCurrentState()); final GetAnimationMatrixForStateCommand cmdMatrix = new GetAnimationMatrixForStateCommand(state);
final GetPreferenceCommand cmdImagePadding = new GetPreferenceCommand("TK_CUSTOM_STATE_VIEW_PADDING"); final GetPreferenceCommand cmdImagePadding = new GetPreferenceCommand("TK_CUSTOM_STATE_VIEW_PADDING");
final GetPreferenceCommand cmdStringPadding = new GetPreferenceCommand("TK_CUSTOM_STATE_VIEW_STRING_PADDING"); final GetPreferenceCommand cmdStringPadding = new GetPreferenceCommand("TK_CUSTOM_STATE_VIEW_STRING_PADDING");
final GetPreferenceCommand cmdFontName = new GetPreferenceCommand("TK_CUSTOM_STATE_VIEW_FONT_NAME"); final GetPreferenceCommand cmdFontName = new GetPreferenceCommand("TK_CUSTOM_STATE_VIEW_FONT_NAME");
final GetPreferenceCommand cmdFontSize = new GetPreferenceCommand("TK_CUSTOM_STATE_VIEW_FONT_SIZE"); final GetPreferenceCommand cmdFontSize = new GetPreferenceCommand("TK_CUSTOM_STATE_VIEW_FONT_SIZE");
trace.getStateSpace().execute( state.getStateSpace().execute(
cmdImages, cmdImages,
cmdMatrix, cmdMatrix,
cmdImagePadding, cmdImagePadding,
...@@ -87,8 +85,8 @@ public final class ShowCommand implements Command { ...@@ -87,8 +85,8 @@ public final class ShowCommand implements Command {
cmdFontSize cmdFontSize
); );
if (cmdMatrix.getMatrix() == null) { if (cmdMatrix.getMatrix().isEmpty()) {
throw new UserErrorException("No animation function visualisation available"); return null;
} }
final Path machineDirectory = this.proBKernelProvider.get().getCurrentMachineDirectory(); final Path machineDirectory = this.proBKernelProvider.get().getCurrentMachineDirectory();
...@@ -146,11 +144,55 @@ public final class ShowCommand implements Command { ...@@ -146,11 +144,55 @@ public final class ShowCommand implements Command {
} }
tableBuilder.append("\n</tbody></table>"); tableBuilder.append("\n</tbody></table>");
final DisplayData result = new DisplayData("<Animation function visualisation>"); final DisplayData result = new DisplayData("<Animation function visualization>");
result.putMarkdown(tableBuilder.toString()); result.putMarkdown(tableBuilder.toString());
return result; return result;
} }
private static @Nullable DisplayData getVisBVisualization(final @NotNull State state) {
GetVisBLoadedJsonFileCommand loadedCmd = new GetVisBLoadedJsonFileCommand();
state.getStateSpace().execute(loadedCmd);
if (loadedCmd.getPath() == null) {
// Load VisB visualization defined inside the model itself
state.getStateSpace().execute(new LoadVisBCommand(""));
}
state.getStateSpace().execute(loadedCmd);
if (loadedCmd.getPath() == null) {
// The model doesn't contain any VisB visualization
return null;
}
GetVisBHtmlForStates htmlCmd = new GetVisBHtmlForStates(state);
state.getStateSpace().execute(htmlCmd);
final DisplayData result = new DisplayData("<VisB visualization>");
result.putHTML(htmlCmd.getHtml());
return result;
}
@Override
public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final State state = this.animationSelector.getCurrentTrace().getCurrentState();
final DisplayData visBResult = getVisBVisualization(state);
if (visBResult != null) {
return visBResult;
}
DisplayData animationFunctionResult = this.getAnimationFunctionVisualization(state);
if (animationFunctionResult != null) {
return animationFunctionResult;
}
if (state.isInitialised()) {
throw new UserErrorException("No VisB visualization or ANIMATION_FUNCTION defined in the model");
} else {
throw new UserErrorException("Model is not initialized, cannot show visualization (or no visualization is defined)");
}
}
@Override @Override
public @NotNull ParameterInspectors getParameterInspectors() { public @NotNull ParameterInspectors getParameterInspectors() {
return ParameterInspectors.NONE; return ParameterInspectors.NONE;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment