From cc91cd814f29d3d2be17d2b13d61a877f483855d Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Tue, 18 Feb 2020 15:35:01 +0100
Subject: [PATCH] Don't display dot command availability in :help :dot
The :help message shouldn't be state-dependent.
---
notebooks/tests/dot.ipynb | 24 +++++++++----------
.../de/prob2/jupyter/commands/DotCommand.java | 5 ----
2 files changed, 12 insertions(+), 17 deletions(-)
diff --git a/notebooks/tests/dot.ipynb b/notebooks/tests/dot.ipynb
index 66c0b52..5a41d15 100644
--- a/notebooks/tests/dot.ipynb
+++ b/notebooks/tests/dot.ipynb
@@ -17,7 +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",
- "* `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model (**Not available for this machine/state**: only available for Event-B models)\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",
"* `current_state` - Current State in State Space: Show current state and successors in state space\n",
@@ -27,19 +27,19 @@
"* `transition_diagram` - State Space Expression Projection...: Project state space onto expression values and show transition diagram\n",
"* `enable_graph` - Enable Graph: Show enabling graph of events\n",
"* `state_as_graph` - Current State as Graph: Show values in current state as a graph\n",
- "* `custom_graph` - Customized Current State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES (**Not available for this machine/state**: only available when CUSTOM_GRAPH_NODES and CUSTOM_GRAPH_EDGES are defined in the DEFINITIONS of a B machine)\n",
+ "* `custom_graph` - Customized Current State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES\n",
"* `expr_as_graph` - (Relational) Expression as Graph...: Show (relational) expression value as a graph\n",
"* `formula_tree` - Custom Predicate/Expression Formula Tree...: Show predicate/expressions and sub-formulas as a tree\n",
- "* `invariant` - Invariant Formula Tree: Show invariant as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n",
+ "* `invariant` - Invariant Formula Tree: Show invariant as a formula tree\n",
"* `properties` - Properties Formula Tree: Show properties as a formula tree\n",
"* `assertions` - Assertions Formula Tree: Show assertions as a formula tree\n",
- "* `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n",
- "* `goal` - Goal Formula Tree: Show GOAL as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models with a GOAL DEFINITION)\n",
+ "* `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree\n",
+ "* `goal` - Goal Formula Tree: Show GOAL as a formula tree\n",
"* `dependence_graph` - Dependence Graph: Show dependence graph of events\n",
"* `variable_modification_graph` - Variable Read/Write Graph: Show variable modification by operations and reading in guards\n",
"* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS\n",
"* `predicate_dependency` - Predicate Dependency Graph...: Show dependence graph of conjuncts of a predicate\n",
- "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree (**Not available for this machine/state**: only available when error occured)\n"
+ "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree\n"
],
"text/plain": [
":dot COMMAND [FORMULA]\n",
@@ -48,7 +48,7 @@
"The following dot visualisation commands are available:\n",
"\n",
"* `machine_hierarchy` - Machine Hierarchy: Shows the machine hierarchy of a classical B model\n",
- "* `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model (**Not available for this machine/state**: only available for Event-B models)\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",
"* `current_state` - Current State in State Space: Show current state and successors in state space\n",
@@ -58,19 +58,19 @@
"* `transition_diagram` - State Space Expression Projection...: Project state space onto expression values and show transition diagram\n",
"* `enable_graph` - Enable Graph: Show enabling graph of events\n",
"* `state_as_graph` - Current State as Graph: Show values in current state as a graph\n",
- "* `custom_graph` - Customized Current State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES (**Not available for this machine/state**: only available when CUSTOM_GRAPH_NODES and CUSTOM_GRAPH_EDGES are defined in the DEFINITIONS of a B machine)\n",
+ "* `custom_graph` - Customized Current State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES\n",
"* `expr_as_graph` - (Relational) Expression as Graph...: Show (relational) expression value as a graph\n",
"* `formula_tree` - Custom Predicate/Expression Formula Tree...: Show predicate/expressions and sub-formulas as a tree\n",
- "* `invariant` - Invariant Formula Tree: Show invariant as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n",
+ "* `invariant` - Invariant Formula Tree: Show invariant as a formula tree\n",
"* `properties` - Properties Formula Tree: Show properties as a formula tree\n",
"* `assertions` - Assertions Formula Tree: Show assertions as a formula tree\n",
- "* `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n",
- "* `goal` - Goal Formula Tree: Show GOAL as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models with a GOAL DEFINITION)\n",
+ "* `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree\n",
+ "* `goal` - Goal Formula Tree: Show GOAL as a formula tree\n",
"* `dependence_graph` - Dependence Graph: Show dependence graph of events\n",
"* `variable_modification_graph` - Variable Read/Write Graph: Show variable modification by operations and reading in guards\n",
"* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS\n",
"* `predicate_dependency` - Predicate Dependency Graph...: Show dependence graph of conjuncts of a predicate\n",
- "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree (**Not available for this machine/state**: only available when error occured)\n"
+ "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree\n"
]
},
"execution_count": 1,
diff --git a/src/main/java/de/prob2/jupyter/commands/DotCommand.java b/src/main/java/de/prob2/jupyter/commands/DotCommand.java
index e42637c..ec00c63 100644
--- a/src/main/java/de/prob2/jupyter/commands/DotCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/DotCommand.java
@@ -68,11 +68,6 @@ public final class DotCommand implements Command {
sb.append(item.getName());
sb.append(": ");
sb.append(item.getDescription());
- if (!item.isAvailable()) {
- sb.append(" (**Not available for this machine/state**: ");
- sb.append(item.getAvailable());
- sb.append(')');
- }
sb.append('\n');
}
return sb.toString();
--
GitLab