From b685b03196d9f51f2fc9fe8f4ef36995c30adff1 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Thu, 21 Jun 2018 15:00:30 +0200
Subject: [PATCH] Add :show command to show animation function
---
notebooks/tests/Hanoi.mch | 37 ++
notebooks/tests/images/Disc1.gif | Bin 0 -> 990 bytes
notebooks/tests/images/Disc2.gif | Bin 0 -> 1000 bytes
notebooks/tests/images/Disc3.gif | Bin 0 -> 1009 bytes
notebooks/tests/images/Disc4.gif | Bin 0 -> 1010 bytes
notebooks/tests/images/Disc5.gif | Bin 0 -> 1018 bytes
notebooks/tests/images/Disc_empty.gif | Bin 0 -> 981 bytes
notebooks/tests/show.ipynb | 359 ++++++++++++++++++
.../java/de/prob2/jupyter/ProBKernel.java | 2 +
.../prob2/jupyter/commands/ShowCommand.java | 68 ++++
10 files changed, 466 insertions(+)
create mode 100644 notebooks/tests/Hanoi.mch
create mode 100644 notebooks/tests/images/Disc1.gif
create mode 100644 notebooks/tests/images/Disc2.gif
create mode 100644 notebooks/tests/images/Disc3.gif
create mode 100644 notebooks/tests/images/Disc4.gif
create mode 100644 notebooks/tests/images/Disc5.gif
create mode 100644 notebooks/tests/images/Disc_empty.gif
create mode 100644 notebooks/tests/show.ipynb
create mode 100644 src/main/java/de/prob2/jupyter/commands/ShowCommand.java
diff --git a/notebooks/tests/Hanoi.mch b/notebooks/tests/Hanoi.mch
new file mode 100644
index 0000000..d79869f
--- /dev/null
+++ b/notebooks/tests/Hanoi.mch
@@ -0,0 +1,37 @@
+MACHINE Hanoi
+SETS
+ Stakes
+DEFINITIONS
+ GOAL == (!s.(s:Stakes & s/=dest => on(s) = <>));
+/* 12.35 secs on PPC G4 1.25 GHz to find GOAL with hash_markers; 75 seconds on Alloy4 */
+ SET_PREF_SYMBOLIC == FALSE;
+ scope_Stakes == 1..3;
+
+ ANIMATION_IMG0 == "images/Disc_empty.gif";
+ ANIMATION_IMG1 == "images/Disc1.gif";
+ ANIMATION_IMG2 == "images/Disc2.gif";
+ ANIMATION_IMG3 == "images/Disc3.gif";
+ ANIMATION_IMG4 == "images/Disc4.gif";
+ ANIMATION_IMG5 == "images/Disc5.gif";
+ ANIMATION_FUNCTION == ({r,c,i|r:1..nrdiscs & c:Stakes & i=0} <+
+ {r,c,i|r:1..nrdiscs & c:Stakes & r-5+size(on(c)): dom(on(c)) &
+ i = on(c)(r-5+size(on(c))) }
+ )
+CONSTANTS orig,dest,nrdiscs
+PROPERTIES
+ orig: Stakes & dest:Stakes & orig /= dest & nrdiscs = 5
+VARIABLES on
+INVARIANT
+ on : Stakes --> seq(INTEGER)
+INITIALISATION
+ on := %s.(s:Stakes & s /= orig | <>) \/ {orig |-> %x.(x:1..nrdiscs|x)}
+OPERATIONS
+ Move(from,to,disc) = PRE from:Stakes & on(from) /= <> &
+ to:Stakes & to /= from &
+ disc:NATURAL1 & disc = first(on(from)) &
+ (on(to) /= <> => first(on(to))> disc )
+ THEN
+ on := on <+ { from |-> tail(on(from)), to |-> (disc -> on(to)) }
+ END
+END
+
diff --git a/notebooks/tests/images/Disc1.gif b/notebooks/tests/images/Disc1.gif
new file mode 100644
index 0000000000000000000000000000000000000000..d39538437af6cec2b3b7e8d695694f676d2cbec6
GIT binary patch
literal 990
zcmZ?wbhEHb>|;=7_|9VZ9}UDs{6CisLEn+VvE=Vy^d1@PO@0qU&ym62sOK<r4;ieD
zx(7qokia=)ur%l#3>`xPdy&9aWH7~RD;TXs20dPDVQ48bXmMH!LvxV86l73rIR%V*
zkU_C!4-B;+fof!sY*~#!hSkYXRE!Lw42xkX8wDh1XM<64ayASlBY`L+5QGA}f`UNE
z3k5iNdBKpAlNSOhdO5+6rJ@%YIUxf}MJFhdaIyp=Lq#VTvP1@k5|%Jzhzv9}4Pi)A
zQxS?3B{ZQ(KvNNf6j6YLq9PbcNGKwZfT9ExNeBqQ5Ql^S2nnD74gmoe;@}W~Ar2J4
zz`+4U45&Z{#0BLA29CoFj2to^8x|aF<`CA3;dn6ra66B(*Bp<Hi;i~l$U7Z5v2pS7
zeg#u27SByfPEO`^T@-V2(^992|6@+g*(s!UcD9A}turS#r@KwHYvz*OQM@8>o@>9>
z+?gdSFVAwA?`3<lWL4<g!1Y<Z5ersdU!QO|PgdJt&CSj6C*xdCe_L~FW$xo;wZB8w
z#qKJ7d+g}zkoR%>y#Fp@)d~F&b0~SWQr+qb!<)zYwmbFJlo~x<IZfaG?3zl==jYt*
Uo8`2sN-kVlR=ucBN`S!{06);9MgRZ+
literal 0
HcmV?d00001
diff --git a/notebooks/tests/images/Disc2.gif b/notebooks/tests/images/Disc2.gif
new file mode 100644
index 0000000000000000000000000000000000000000..8b97acec07c7ba8263ce7e07b6ffa3e517a24f32
GIT binary patch
literal 1000
zcmZ?wbhEHb>|;=7_|9VZ9~IbK^80@-8-l(ggJa3x!RS3Q*qi(whMpsXy;09$=pHgy
z8+8wct|5VQ$Y5#EIT$*I1ok3<t;k@C*H$oEiwt_a*22(IWYFTY6o%#?fhowK*m4RO
z^&o>{%N`hNK?2ptAlb4SfefpYp{N)cL>U&tP&Nuk&dvs-<m7A^N=5=vNFWFWcm)N4
zkQWMY^74WqCnqliQuK0yAxlLsFmgf$mWobLB;jNUMuv(`Fl31g3?(dK$PgK5Y8t|j
zrlukkDN1NUk$|Qm2q~ff2}MOPl8{hDAOS@QD3TBmfFTYE0T2>E0UQDXFvP(j07D!o
zfPsSpiWpFV4u}iN3k)1*85lWaJT@#i*vuiU6~pmh{^52WWv@9N8y6kz=8<<ga$@7+
z<NXSzRxF;ImYkf->$)iB<ff%g6aUAYnzK_#?d)s|>sx0|ZccZbYS+vqyQ6qT;5^rU
zt+_KxR$iXvFyG7eX345h2G&hkcTa6yeSLkx*0{Nn+t%FN9D975%js=v!?$YRJvEp6
z`;$Anb6(Fna(erkdy{IJ_y6?{+VGI6g;AbwPR0AAUA<GodgoLaJ>5S||N7ZAk-E>%
hh1)mJ)2jM%`O>oKi~MR!OkXct7th}N*F=HA8UV~-su%zO
literal 0
HcmV?d00001
diff --git a/notebooks/tests/images/Disc3.gif b/notebooks/tests/images/Disc3.gif
new file mode 100644
index 0000000000000000000000000000000000000000..11e467eab2debeeb7fae8d092b97a5cfec3c0b54
GIT binary patch
literal 1009
zcmZ?wbhEHb>|;=7_|9VZ9~H#Z|Nnn38-l(ggJa3x!RS3Q*qi(whMpsXy;09$=pHgy
z8+8wct|5VQ$Y5#EIT$*I1ok3<t;k@C*H$oEiwt_a*22(IWYFTY6o%#?fhowK*m4RO
z^&o>{%N`hNK?2ptAlb4SfefpYp{N)cL>U&tP&Nuk&dvs-<m7A^N=5=vNFWFWcm)N4
zkQWMY^74WqCnqliQuK0yAxlLsFmgf$mWobLB;jNUMuv(`Fl31g3?(dK$PgK5Y8t|j
zrlukkDN1NUk$|Qm2q~ff2}MOPl8{hDAOS@QD3TBmfFTYE0T2>E0UQDXFvP(j07D!o
zfPsSpiWpFV4u}iN3k)3B7#KNZJT@#i*vuiU6~pmh{^52WWv@9N8y6kz=8<<ga$@7+
z<NXSzRxF;ImYkf->$)iB<ff%g6aUAYnzK_#?d)s|>sx0|ZccZbYS+vqyQ6qT;5^rU
zt+_KxR$iXvFrQD?Ve6`^t0OjN-95E+^>wBo!8%#*ZEGUeCUVb<J-zMi)h*0-PtA=M
z(_`3G@i}el>h0^}_SG?;X4Tp8A#!&)ulBz#i;s_vXGmMO@kAP(TQ<#D`N*1`#ur!2
qbLM`cV`cpE(j@=IZfmMc?_67V_)y>960^5Ux8=*9l{Hgfum%7uRH_RA
literal 0
HcmV?d00001
diff --git a/notebooks/tests/images/Disc4.gif b/notebooks/tests/images/Disc4.gif
new file mode 100644
index 0000000000000000000000000000000000000000..bb575ca9046a842e7b3dbf8d7c91ff2d05bc5615
GIT binary patch
literal 1010
zcmZ?wbhEHb>|;=7_|9VZ9~B%EHTr)p8-l(ggJa3x!RS3Q*qi(whMpsXy;09$=pHgy
z8+8wct|5VQ$Y5#EIT$*I1ok3<t;k@C*H$oEiwt_a*22(IWYFTY6o%#?fhowK*m4RO
z^&o>{%N`hNK?2ptAlb4SfefpYp{N)cL>U&tP&Nuk&dvs-<m7A^N=5=vNFWFWcm)N4
zkQWMY^74WqCnqliQuK0yAxlLsFmgf$mWobLB;jNUMuv(`Fl31g3?(dK$PgK5Y8t|j
zrlukkDN1NUk$|Qm2q~ff2}MOPl8{hDAOS@QD3TBmfFTYE0T2>E0UQDXFvP(j07D!o
zfPsSpiWpFV4u}iN3k)3B85lWaJT@#i*vuiU6~pmh{^52WWv@9N8y6kz=8<<ga$@7+
z<NXSzRxF;ImYkf->$)iB<ff%g6aUAYnzK_#?d)s|>sx0|ZccZbYS+vqyQ6qT;5^rU
zt+_KxR$iXvFyG7eW{K8mrijg1cTa6yeSLkx;VxO}Z)!I;XIx$td%INa_V$9uo2F`R
zUw3zROzfk(r@ybgx37VDdamY<4G-6p@M}MNUA8fKcbdF+Shi^D)l)OH<IbJ=x%}9<
r1?qWxzOyo}Tw1}|=f_)Rntg6vd~%=eZLPPrg7P1it*Xv)V6X-NLTIh#
literal 0
HcmV?d00001
diff --git a/notebooks/tests/images/Disc5.gif b/notebooks/tests/images/Disc5.gif
new file mode 100644
index 0000000000000000000000000000000000000000..70ae3e90586fe8517046fb38c32558654c701b77
GIT binary patch
literal 1018
zcmZ?wbhEHb>|;=7_|9VZ9}S$#{trXnk-@R#?_l&E8SG7d4@1w9!QQCnFmw+Ytc|({
zL)VbNIb^Uj=o}0kLjrq|z*b~1#cL}VtwjbsUTa}!DKcnrS_(sRkiZmVP;5B`jCznk
zv1JbowIG3NWRPrGjX;Lg$xu{`45AE+VJI5~Bxh%XQF3xN3?(ChC?pVs0=$BPK*$RP
zIC*)&kdu=a0x5bq!H}h*7Z^Dq14~6GD3Wlp1S3O5Cm6Cs28I%rFl2}fG&K!jNK;c0
ziWDU@p-4be5rh;`fP|tV7)eMdB9MTh1QbaK2*41Bga8N$pa2d50T|-o5P%^L6u`j2
z0Ywa`KnKJH<pl<g`wWa6G9DWi9Bk$g){5bHF#m8nkFwVskBy6tcJs(P9XYXa@$r5I
zQ!5tFO-oKr=5<{Zb8^#Cr-}b#PR-dVq;__;h4rm7CpV|NO|@(0lHF0fB5<B-zt-HD
zB`Yt_a+qJF<FIwr)zuN3v+kbSy88P1gu_Ll8r#;~+?;WFm2N}9+S}U;9_QI=Y+rYG
zcN*`byQjD7hwiOo<}Tx|*zoXh0=IJ9nH#Gf9h<;^xz{JM;P$B*KPR0%Be^c5$Jf65
wnq=vg%nM8XSI?8E+WNX>ZTx99iRy1}Zf%Qyd~R=*`TNWJ>ihZZtP~im0eU60lmGw#
literal 0
HcmV?d00001
diff --git a/notebooks/tests/images/Disc_empty.gif b/notebooks/tests/images/Disc_empty.gif
new file mode 100644
index 0000000000000000000000000000000000000000..ff8c39534f1734b0594d1caee860a34f379b025d
GIT binary patch
literal 981
zcmZ?wbhEHb>|;=7_|9VZ9}UDs{6CisLEn+VvE=Vy^d1@PO@0qU&ym62sOK<r4;ieD
zx(7qokia=)ur%l#3>`xPdy&9aWH7~RD;TXs20dPDVQ48bXmMH!LvxV86l73rIR%V*
zkU_C!4-B;+fof!sY*~#!hSkYXRE!Lw42xkX8wDh1XM<64ayASlBY`L+5QGA}f`UNE
z3k5iNdBKpAlNSOhdO5+6rJ@%YIUxf}MJFhdaIyp=Lq#VTvP1@k5|%Jzhzv9}4Pi)A
zQxS?3B{ZQ(KvNNf6j6YLq9PbcNGKwZfT9ExNeBqQ5Ql^S2nnD74gmoe;@}W~Ar2J4
zz`+4U45&Z{#0BLA298|}j2to^8x|aF<`CA3;dn6ra66B(*Bp<Hi;i~l$U7Z5v2pS7
zeg#u27SByfPEO`^T@-V2(^992|6@+g*(s!UcD9A}turS#r@KwHYvz*OQM@8>o@>9>
z+?gdSFVAwA?`3<lWL4<g!1Y;2Pb^z~eQkn%)nBP?YmRJ;J-aHlW7^qU+u3g)nrj`P
zcXwym`+a9uhwI+om%5tio>s+&tB2Z_EBXB?F?_tVPhP%Pr&8nTDM$U}cPlH4&z+l>
L-&7|hz+epkq;sD4
literal 0
HcmV?d00001
diff --git a/notebooks/tests/show.ipynb b/notebooks/tests/show.ipynb
new file mode 100644
index 0000000..0523575
--- /dev/null
+++ b/notebooks/tests/show.ipynb
@@ -0,0 +1,359 @@
+{
+ "cells": [
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "```\n",
+ ":show\n",
+ "```\n",
+ "\n",
+ "Show the machine's animation function visualisation for the current state."
+ ],
+ "text/plain": [
+ ":show\n",
+ "\n",
+ "Show the machine's animation function visualisation for the current state."
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":help :show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Hanoi : []\n"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":load Hanoi.mch"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 1: $initialise_machine()"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation 2: Move(orig,dest,1)"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Move"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 9,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation 4: Move(orig,Stakes3,2)"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Move"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "<td style=\"padding:0\"></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 11,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "codemirror_mode": "prob2_jupyter_repl",
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob2-jupyter-repl",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index c71c8c1..94a6ce5 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -37,6 +37,7 @@ import de.prob2.jupyter.commands.NoSuchCommandException;
import de.prob2.jupyter.commands.PrefCommand;
import de.prob2.jupyter.commands.PrettyPrintCommand;
import de.prob2.jupyter.commands.RenderCommand;
+import de.prob2.jupyter.commands.ShowCommand;
import de.prob2.jupyter.commands.SolveCommand;
import de.prob2.jupyter.commands.TableCommand;
import de.prob2.jupyter.commands.TimeCommand;
@@ -149,6 +150,7 @@ public final class ProBKernel extends BaseKernel {
this.commands.put(":exec", injector.getInstance(ExecCommand.class));
this.commands.put(":constants", injector.getInstance(ConstantsCommand.class));
this.commands.put(":init", injector.getInstance(InitialiseCommand.class));
+ this.commands.put(":show", injector.getInstance(ShowCommand.class));
this.commands.put(":dot", injector.getInstance(DotCommand.class));
this.commands.put(":assert", injector.getInstance(AssertCommand.class));
this.commands.put(":time", injector.getInstance(TimeCommand.class));
diff --git a/src/main/java/de/prob2/jupyter/commands/ShowCommand.java b/src/main/java/de/prob2/jupyter/commands/ShowCommand.java
new file mode 100644
index 0000000..1b7fa92
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/commands/ShowCommand.java
@@ -0,0 +1,68 @@
+package de.prob2.jupyter.commands;
+
+import java.util.Map;
+
+import com.google.inject.Inject;
+
+import de.prob.animator.command.GetImagesForMachineCommand;
+import de.prob.animator.command.GetImagesForStateCommand;
+import de.prob.statespace.AnimationSelector;
+import de.prob.statespace.Trace;
+
+import de.prob2.jupyter.ProBKernel;
+import de.prob2.jupyter.UserErrorException;
+
+import io.github.spencerpark.jupyter.kernel.display.DisplayData;
+
+import org.jetbrains.annotations.NotNull;
+
+public final class ShowCommand implements Command {
+ private final @NotNull AnimationSelector animationSelector;
+
+ @Inject
+ private ShowCommand(final @NotNull AnimationSelector animationSelector) {
+ super();
+
+ this.animationSelector = animationSelector;
+ }
+
+ @Override
+ public @NotNull String getSyntax() {
+ return ":show";
+ }
+
+ @Override
+ public @NotNull String getShortHelp() {
+ return "Show the machine's animation function visualisation for the current state.";
+ }
+
+ @Override
+ public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+ if (!argString.isEmpty()) {
+ throw new UserErrorException("Expected no arguments");
+ }
+
+ final Trace trace = this.animationSelector.getCurrentTrace();
+
+ final GetImagesForMachineCommand cmd1 = new GetImagesForMachineCommand();
+ trace.getStateSpace().execute(cmd1);
+ final Map<Integer, String> images = cmd1.getImages();
+
+ final GetImagesForStateCommand cmd2 = new GetImagesForStateCommand(trace.getCurrentState().getId());
+ trace.getStateSpace().execute(cmd2);
+
+ final StringBuilder tableBuilder = new StringBuilder("<table><tbody>");
+ for (final Integer[] 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)));
+ }
+ tableBuilder.append("\n</tr>");
+ }
+ tableBuilder.append("\n</tbody></table>");
+
+ final DisplayData result = new DisplayData("<Animation function visualisation>");
+ result.putMarkdown(tableBuilder.toString());
+ return result;
+ }
+}
--
GitLab