Skip to content
Snippets Groups Projects
Commit 3f62e185 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add use of :pref DOT_ENGINE to example

parent 812e1ac5
Branches
Tags
No related merge requests found
%% Cell type:code id: tags:
``` prob
:help :dot
```
%% Output
```
: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
* `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)
* `state_space` - State Space: Show state space
* `state_space_sfdp` - State Space (Fast): Show state space (fast)
* `signature_merge` - Signature Merge: Show signature-merged reduced state space
* `dfa_merge` - DFA Merge: Show state space as deterministic automaton (DFA)
* `state_as_graph` - State Graph: Show values in current state as a graph
* `custom_graph` - Customized 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)
* `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)
* `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 (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)
* `goal` - Goal Formula Tree: Show GOAL as a formula tree
* `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)
* `enable_graph` - Enable Graph: Show enabling graph of events
* `dependence_graph` - Dependence Graph: Show dependence graph of events
* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS
* `expr_as_graph` - Expression Graph: Show expression value as a graph
* `formula_tree` - Formula Tree: Show predicate and sub-expressions as a tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)
* `formula_tree` - Formula Tree: Show predicate and sub-expressions as a tree
* `transition_diagram` - Transition Diagram Projection: Project state space onto expression values
* `predicate_dependency` - Predicate Dependency Graph: Show dependence graph of conjuncts of a predicate
```
: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
* `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)
* `state_space` - State Space: Show state space
* `state_space_sfdp` - State Space (Fast): Show state space (fast)
* `signature_merge` - Signature Merge: Show signature-merged reduced state space
* `dfa_merge` - DFA Merge: Show state space as deterministic automaton (DFA)
* `state_as_graph` - State Graph: Show values in current state as a graph
* `custom_graph` - Customized 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)
* `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)
* `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 (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)
* `goal` - Goal Formula Tree: Show GOAL as a formula tree
* `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)
* `enable_graph` - Enable Graph: Show enabling graph of events
* `dependence_graph` - Dependence Graph: Show dependence graph of events
* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS
* `expr_as_graph` - Expression Graph: Show expression value as a graph
* `formula_tree` - Formula Tree: Show predicate and sub-expressions as a tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)
* `formula_tree` - Formula Tree: Show predicate and sub-expressions as a tree
* `transition_diagram` - Transition Diagram Projection: Project state space onto expression values
* `predicate_dependency` - Predicate Dependency Graph: Show dependence graph of conjuncts of a predicate
%% Cell type:code id: tags:
``` prob
:pref DOT=/opt/local/bin/dot
:pref DOT=/usr/local/bin/dot
```
%% Output
Preference changed: DOT = /usr/local/bin/dot
%% Cell type:code id: tags:
``` prob
:dot state_space
```
%% Output
<Dot visualization: state_space []>
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 0: $initialise_machine()
%% Cell type:code id: tags:
``` prob
:dot state_space
```
%% Output
<Dot visualization: state_space []>
%% Cell type:code id: tags:
``` prob
:dot invariant
```
%% Output
<Dot visualization: invariant []>
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph {1|->2, 2|->3, 3|->1}
```
%% Output
<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
<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
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
<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
Preference changed: DOT_ENGINE = dot
%% Cell type:code id: tags:
``` prob
:dot formula_tree 1*2 + 3/4 = card({1, 2})
```
%% Output
<Dot visualization: formula_tree [1*2+3/4=card({1,2})]>
%% Cell type:code id: tags:
``` prob
```
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment