Skip to content
GitLab
Commit a654e73e authored by dgelessus's avatar dgelessus
Browse files

Use new ProB 2 method for dot visualization without manual temp file

parent df4aa861
Pipeline #50786 passed with stage
in 7 minutes and 35 seconds
Hide whitespace changes
Inline Side-by-side
notebooks/tests/dot.ipynb
View file @ a654e73e
......@@ -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|&#45;&gt;2),(2|&#45;&gt;3),(3|&#45;&gt;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})]>"
......
%% Cell type:code id: tags:
``` prob
:help :dot
```
%%%% Output: execute_result
```
:dot COMMAND [FORMULA]
```
Execute and show a dot visualisation.
The following dot visualisation commands are available:
* `machine_hierarchy` - Machine Hierarchy: Shows the machine hierarchy of a classical B model
* `operations` - Operation Call Graph: Shows the call graph of a classical B model
* `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model
* `state_space` - State Space: Show state space
* `state_space_sfdp` - State Space (Fast): Show state space (fast)
* `current_state` - Current State in State Space: Show current state and successors in state space
* `history` - Path to Current State: Show a path leading to current state
* `signature_merge` - Signature Merge: Show signature-merged reduced state space
* `dfa_merge` - DFA Merge: Show state space as deterministic automaton (DFA)
* `transition_diagram` - State Space Expression Projection...: Project state space onto expression values and show transition diagram
* `enable_graph` - Enable Graph: Show enabling graph of events
* `state_as_graph` - Current State as Graph: Show values in current state as a graph
* `custom_graph` - Customized Current State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES
* `expr_as_graph` - (Relational) Expression as Graph...: Show (relational) expression value as a graph
* `formula_tree` - Custom Predicate/Expression Formula Tree...: Show predicate/expressions and sub-formulas as a tree
* `invariant` - Invariant Formula Tree: Show invariant as a formula tree
* `properties` - Properties Formula Tree: Show properties as a formula tree
* `assertions` - Assertions Formula Tree: Show assertions as a formula tree
* `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree
* `goal` - Goal Formula Tree: Show GOAL as a formula tree
* `dependence_graph` - Dependence Graph: Show dependence graph of events
* `variable_modification_graph` - Variable Read/Write Graph: Show variable modification by operations and reading in guards
* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS
* `predicate_dependency` - Predicate Dependency Graph...: Show dependence graph of conjuncts of a predicate
* `last_error` - Last Error Formula Tree: Show last error source as a formula tree
:dot COMMAND [FORMULA]
Execute and show a dot visualisation.
The following dot visualisation commands are available:
* `machine_hierarchy` - Machine Hierarchy: Shows the machine hierarchy of a classical B model
* `operations` - Operation Call Graph: Shows the call graph of a classical B model
* `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model
* `state_space` - State Space: Show state space
* `state_space_sfdp` - State Space (Fast): Show state space (fast)
* `current_state` - Current State in State Space: Show current state and successors in state space
* `history` - Path to Current State: Show a path leading to current state
* `signature_merge` - Signature Merge: Show signature-merged reduced state space
* `dfa_merge` - DFA Merge: Show state space as deterministic automaton (DFA)
* `transition_diagram` - State Space Expression Projection...: Project state space onto expression values and show transition diagram
* `enable_graph` - Enable Graph: Show enabling graph of events
* `state_as_graph` - Current State as Graph: Show values in current state as a graph
* `custom_graph` - Customized Current State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES
* `expr_as_graph` - (Relational) Expression as Graph...: Show (relational) expression value as a graph
* `formula_tree` - Custom Predicate/Expression Formula Tree...: Show predicate/expressions and sub-formulas as a tree
* `invariant` - Invariant Formula Tree: Show invariant as a formula tree
* `properties` - Properties Formula Tree: Show properties as a formula tree
* `assertions` - Assertions Formula Tree: Show assertions as a formula tree
* `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree
* `goal` - Goal Formula Tree: Show GOAL as a formula tree
* `dependence_graph` - Dependence Graph: Show dependence graph of events
* `variable_modification_graph` - Variable Read/Write Graph: Show variable modification by operations and reading in guards
* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS
* `predicate_dependency` - Predicate Dependency Graph...: Show dependence graph of conjuncts of a predicate
* `last_error` - Last Error Formula Tree: Show last error source as a formula tree
%% Cell type:code id: tags:
``` prob
:dot state_space
```
%%%% Output: execute_result
<Dot visualization: state_space []>
%% Cell type:code id: tags:
``` prob
:init
```
%%%% Output: execute_result
Machine initialised using operation 0: $initialise_machine()
Executed operation: INITIALISATION()
%% Cell type:code id: tags:
``` prob
:dot state_space
```
%%%% Output: execute_result
<Dot visualization: state_space []>
%% Cell type:code id: tags:
``` prob
:dot invariant
```
%%%% Output: execute_result
<Dot visualization: invariant []>
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph {1|->2, 2|->3, 3|->1}
```
%%%% Output: execute_result
<Dot visualization: expr_as_graph [{(1,2),(2,3),(3,1)}]>
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("gt",{x,y|x:1..5 & y:1..5 & x>y},"half",{y,x|x:1..5 & y:1..5 & x+x=y})
```
%%%% Output: execute_result
<Dot visualization: expr_as_graph [("gt",{x,y|x:1..5 & y:1..5 & x>y})]>
%% Cell type:code id: tags:
``` prob
:pref DOT_ENGINE=circo
```
%%%% Output: execute_result
Preference changed: DOT_ENGINE = circo
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("gt",{x,y|x:1..5 & y:1..5 & x>y},"half",{y,x|x:1..5 & y:1..5 & x+x=y})
```
%%%% Output: execute_result
<Dot visualization: expr_as_graph [("gt",{x,y|x:1..5 & y:1..5 & x>y})]>
%% Cell type:code id: tags:
``` prob
:pref DOT_ENGINE=dot
```
%%%% Output: execute_result
Preference changed: DOT_ENGINE = dot
%% Cell type:code id: tags:
``` prob
:dot formula_tree 1*2 + 3/4 = card({1, 2})
```
%%%% Output: execute_result
<Dot visualization: formula_tree [1*2+3/4=card({1,2})]>
%% Cell type:markdown id: tags:
Local variables can be used in dot visualisation parameters.
%% Cell type:code id: tags:
``` prob
:let thing 1*2 + 3/4
```
%%%% Output: execute_result
$2$
2
%% Cell type:code id: tags:
``` prob
:dot formula_tree thing = card({1, 2})
```
%%%% Output: execute_result
<Dot visualization: formula_tree [thingthing=2thing=card({1,2})]>
......
src/main/java/de/prob2/jupyter/commands/DotCommand.java
View file @ a654e73e
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);
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment