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

Add :show command to show animation function

parent c5b40c14
No related branches found
No related tags found
No related merge requests found
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
notebooks/tests/images/Disc1.gif

990 B

notebooks/tests/images/Disc2.gif

1000 B

notebooks/tests/images/Disc3.gif

1009 B

notebooks/tests/images/Disc4.gif

1010 B

notebooks/tests/images/Disc5.gif

1018 B

notebooks/tests/images/Disc_empty.gif

981 B

%% Cell type:code id: tags:
``` prob
:help :show
```
%% Output
```
:show
```
Show the machine's animation function visualisation for the current state.
:show
Show the machine's animation function visualisation for the current state.
%% Cell type:code id: tags:
``` prob
:load Hanoi.mch
```
%% Output
Loaded machine: Hanoi : []
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table><tbody>
<tr>
<td style="padding:0">![null](null)</td>
<td style="padding:0">![null](null)</td>
</tr>
<tr>
<td style="padding:0">![null](null)</td>
<td style="padding:0">![null](null)</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table><tbody>
<tr>
<td style="padding:0">![null](null)</td>
<td style="padding:0">![null](null)</td>
</tr>
<tr>
<td style="padding:0">![null](null)</td>
<td style="padding:0">![null](null)</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 1: $initialise_machine()
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table><tbody>
<tr>
<td style="padding:0">![1](images/Disc1.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
</tr>
<tr>
<td style="padding:0">![2](images/Disc2.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
</tr>
<tr>
<td style="padding:0">![3](images/Disc3.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
</tr>
<tr>
<td style="padding:0">![4](images/Disc4.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
</tr>
<tr>
<td style="padding:0">![5](images/Disc5.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec Move
```
%% Output
Executed operation 2: Move(orig,dest,1)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table><tbody>
<tr>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
</tr>
<tr>
<td style="padding:0">![2](images/Disc2.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
</tr>
<tr>
<td style="padding:0">![3](images/Disc3.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
</tr>
<tr>
<td style="padding:0">![4](images/Disc4.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
</tr>
<tr>
<td style="padding:0">![5](images/Disc5.gif)</td>
<td style="padding:0">![1](images/Disc1.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec Move
```
%% Output
Executed operation 4: Move(orig,Stakes3,2)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table><tbody>
<tr>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
</tr>
<tr>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
</tr>
<tr>
<td style="padding:0">![3](images/Disc3.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
</tr>
<tr>
<td style="padding:0">![4](images/Disc4.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
<td style="padding:0">![0](images/Disc_empty.gif)</td>
</tr>
<tr>
<td style="padding:0">![5](images/Disc5.gif)</td>
<td style="padding:0">![1](images/Disc1.gif)</td>
<td style="padding:0">![2](images/Disc2.gif)</td>
</tr>
</tbody></table>
<Animation function visualisation>
......@@ -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));
......
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\">![%d](%s)</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;
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment