From a654e73efd252fa227abd37af04d07c1be110c14 Mon Sep 17 00:00:00 2001 From: dgelessus <dgelessus@users.noreply.github.com> Date: Fri, 4 Dec 2020 17:31:07 +0100 Subject: [PATCH] Use new ProB 2 method for dot visualization without manual temp file --- notebooks/tests/dot.ipynb | 20 ++++++++------- .../de/prob2/jupyter/commands/DotCommand.java | 25 ++++--------------- 2 files changed, 16 insertions(+), 29 deletions(-) diff --git a/notebooks/tests/dot.ipynb b/notebooks/tests/dot.ipynb index 5a41d15..66fd9bc 100644 --- a/notebooks/tests/dot.ipynb +++ b/notebooks/tests/dot.ipynb @@ -17,6 +17,7 @@ "The following dot visualisation commands are available:\n", "\n", "* `machine_hierarchy` - Machine Hierarchy: Shows the machine hierarchy of a classical B model\n", + "* `operations` - Operation Call Graph: Shows the call graph of a classical B model\n", "* `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model\n", "* `state_space` - State Space: Show state space\n", "* `state_space_sfdp` - State Space (Fast): Show state space (fast)\n", @@ -48,6 +49,7 @@ "The following dot visualisation commands are available:\n", "\n", "* `machine_hierarchy` - Machine Hierarchy: Shows the machine hierarchy of a classical B model\n", + "* `operations` - Operation Call Graph: Shows the call graph of a classical B model\n", "* `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model\n", "* `state_space` - State Space: Show state space\n", "* `state_space_sfdp` - State Space (Fast): Show state space (fast)\n", @@ -108,7 +110,7 @@ "<text text-anchor=\"middle\" x=\"44.3223\" y=\"-17.9\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">root</text>\n", "</g>\n", "</g>\n", - "</svg>" + "</svg>\n" ], "text/plain": [ "<Dot visualization: state_space []>" @@ -131,7 +133,7 @@ { "data": { "text/plain": [ - "Machine initialised using operation 0: $initialise_machine()" + "Executed operation: INITIALISATION()" ] }, "execution_count": 3, @@ -184,7 +186,7 @@ "<text text-anchor=\"middle\" x=\"90.3223\" y=\"-101.4\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">INITIALISATION</text>\n", "</g>\n", "</g>\n", - "</svg>" + "</svg>\n" ], "text/plain": [ "<Dot visualization: state_space []>" @@ -226,7 +228,7 @@ "<text text-anchor=\"middle\" x=\"27\" y=\"-7.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">true</text>\n", "</g>\n", "</g>\n", - "</svg>" + "</svg>\n" ], "text/plain": [ "<Dot visualization: invariant []>" @@ -300,7 +302,7 @@ "<text text-anchor=\"middle\" x=\"249.5\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{(1|->2),(2|->3),(3|->1)}</text>\n", "</g>\n", "</g>\n", - "</svg>" + "</svg>\n" ], "text/plain": [ "<Dot visualization: expr_as_graph [{(1,2),(2,3),(3,1)}]>" @@ -449,7 +451,7 @@ "<text text-anchor=\"middle\" x=\"107.8366\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n", "</g>\n", "</g>\n", - "</svg>" + "</svg>\n" ], "text/plain": [ "<Dot visualization: expr_as_graph [(\"gt\",{x,y|x:1..5 & y:1..5 & x>y})]>" @@ -618,7 +620,7 @@ "<text text-anchor=\"middle\" x=\"21.5\" y=\"-111.9736\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n", "</g>\n", "</g>\n", - "</svg>" + "</svg>\n" ], "text/plain": [ "<Dot visualization: expr_as_graph [(\"gt\",{x,y|x:1..5 & y:1..5 & x>y})]>" @@ -718,7 +720,7 @@ "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"154.295,-20.0001 144.295,-23.5 154.2949,-27.0001 154.295,-20.0001\"/>\n", "</g>\n", "</g>\n", - "</svg>" + "</svg>\n" ], "text/plain": [ "<Dot visualization: formula_tree [1*2+3/4=card({1,2})]>" @@ -828,7 +830,7 @@ "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"154.295,-20.0001 144.295,-23.5 154.2949,-27.0001 154.295,-20.0001\"/>\n", "</g>\n", "</g>\n", - "</svg>" + "</svg>\n" ], "text/plain": [ "<Dot visualization: formula_tree [thingthing=2thing=card({1,2})]>" diff --git a/src/main/java/de/prob2/jupyter/commands/DotCommand.java b/src/main/java/de/prob2/jupyter/commands/DotCommand.java index d7242cd..07ad616 100644 --- a/src/main/java/de/prob2/jupyter/commands/DotCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/DotCommand.java @@ -1,14 +1,10 @@ package de.prob2.jupyter.commands; -import java.io.IOException; -import java.io.UncheckedIOException; -import java.nio.file.Files; -import java.nio.file.Path; import java.util.Arrays; import java.util.Collections; import java.util.List; +import java.util.function.Supplier; import java.util.stream.Collectors; -import java.util.stream.Stream; import com.google.common.collect.ImmutableMap; import com.google.inject.Inject; @@ -111,24 +107,13 @@ public final class DotCommand implements Command { .findAny() .orElseThrow(() -> new UserErrorException("No such dot command: " + command)); - final Path outPath; - try { - outPath = Files.createTempFile(null, "svg"); - } catch (final IOException e) { - throw new UncheckedIOException("Failed to create temp file", e); - } // Provide source code (if any) to error highlighter - final Runnable execute = () -> dotCommand.visualizeAsSvgToFile(outPath, dotCommandArgs); + final Supplier<String> execute = () -> dotCommand.visualizeAsSvgToString(dotCommandArgs); + final String svg; if (code != null) { - CommandUtils.withSourceCode(code, execute); + svg = CommandUtils.withSourceCode(code, execute); } else { - execute.run(); - } - final String svg; - try (final Stream<String> lines = Files.lines(outPath)) { - svg = lines.collect(Collectors.joining("\n")); - } catch (final IOException e) { - throw new UncheckedIOException("Failed to read dot output", e); + svg = execute.get(); } final DisplayData result = new DisplayData(String.format("<Dot visualization: %s %s>", command, dotCommandArgs)); result.putSVG(svg); -- GitLab