diff --git a/notebooks/tests/dot.ipynb b/notebooks/tests/dot.ipynb index 66c0b525c54d0885820e8f2f26c841f89870dc21..5a41d151179502c7cf27af4edbf39b57bab83075 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 e42637c9e086baca4bc817fbac55f0ea0976f3c7..ec00c63712e806c2532a1560c1cf81e1f77de89d 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();