Skip to content

Add GraphPrinter plugin for DOT format graph output - #805

Draft
bahnwaerter wants to merge 1 commit into
ultimate-pa:devfrom
bahnwaerter:wip/mb/graph-printer-plugin
Draft

bahnwaerter wants to merge 1 commit into
ultimate-pa:devfrom
bahnwaerter:wip/mb/graph-printer-plugin

Conversation

@bahnwaerter

Copy link
Copy Markdown
Member

Create a new GraphPrinter plugin that prints IElement data structures (AST, CFG, interpolant automata, etc.) in DOT (Graphviz) format to files. The plugin works like JungVisualization but is headless (isGuiRequired() returns false), making it usable in both GUI and CLI modes.

The plugin uses the same IVisualizable -> VisualizationNode -> DFS traversal pattern as JungVisualization, but writes DOT output to a file instead of displaying in a JUNG viewer. Node labels use the full object's toString() without truncation.

Preferences follow Ultimate's well-known dump pattern:

  • Graph directory (default: current directory)
  • Graph filename (default: "graph")
  • Write graph besides input file (default: true)
  • Which models to print (default: LAST, configurable like JungVisualization)

An annotation output mode controls how metadata and annotations from VisualizationNode and VisualizationEdge payloads are included in the DOT output:

  • NONE: no annotations in the output (like before)
  • HTML_LABELS: annotations are embedded as DOT HTML-like labels on nodes and edges, showing the label followed by an HTML table of all annotation key-value pairs (default mode)
  • RECORD_NODES: annotations are rendered as separate record nodes connected to their parent node/edge with dashed edges

Create a new GraphPrinter plugin that prints IElement data structures
(AST, CFG, interpolant automata, etc.) in DOT (Graphviz) format to files.
The plugin works like JungVisualization but is headless (isGuiRequired()
returns false), making it usable in both GUI and CLI modes.

The plugin uses the same IVisualizable -> VisualizationNode -> DFS traversal
pattern as JungVisualization, but writes DOT output to a file instead of
displaying in a JUNG viewer. Node labels use the full object's toString()
without truncation.

Preferences follow Ultimate's well-known dump pattern:

  - Graph directory (default: current directory)
  - Graph filename (default: "graph")
  - Write graph besides input file (default: true)
  - Which models to print (default: LAST, configurable like JungVisualization)

An annotation output mode controls how metadata and annotations from
VisualizationNode and VisualizationEdge payloads are included in the DOT
output:

  - NONE:         no annotations in the output (like before)
  - HTML_LABELS:  annotations are embedded as DOT HTML-like labels on nodes
                  and edges, showing the label followed by an HTML table of
                  all annotation key-value pairs (default mode)
  - RECORD_NODES: annotations are rendered as separate record nodes
                  connected to their parent node/edge with dashed edges
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant