Ubuntu 20.04上でGraphvizを用いる

はじめに_

グラフを簡単に描画するためのソフトウェアGraphvizを利用する。

インストール_

aptでインストールする。まず、パッケージにあるかどうか確かめる。

% sudo apt search ^graphviz$
ソート中... 完了
全文検索... 完了  
graphviz/focal,now 2.42.2-3build2 amd64 
  rich set of graph drawing tool

インストールする。

% sudo apt install -y graphviz

Graphvizはdotというコマンド名でインストールされている。

% which dot
/usr/bin/dot

% dot -V       
dot - graphviz version 2.43.0 (0)

例題：証明木の作成_

埼玉大学工学部情報工学科２年生向け講義「プログラミング言語論」で登場する、評価意味論の証明木を描画してみる。

作業ディレクトリの作成_

作業ディレクトリを作成する。

% cd 
% mkdir -p ~/Sandbox/Graphviz
% cd ~/Sandbox/Graphviz

DOT言語での記述_

GraphvizではDOT言語という形式言語で描画するグラフを指定する。 以下のページでは詳しく説明してくれている。

DOTファイルを用意する。

% touch example.dot

Graphvizとdot言語でグラフを描く方法のまとめを参考に証明木を書いてみた。example.dotの中身を以下のものにする。（ダウンロード）

digraph graph_name {
  graph [
    charset = "UTF-8";
    label = "証明木",
    labelloc = "t",
    labeljust = "c",
    bgcolor = "#343434",
    fontcolor = white,
    fontsize = 18,
    style = "filled",
    rankdir = TB,
    margin = 0.2,
    splines = spline,
    ranksep = 1.0,
    nodesep = 0.9
  ];

  node [
    colorscheme = "rdylgn11"
    style = "solid,filled",
    fontsize = 16,
    fontcolor = 6,
    fontname = "Migu 1M",
    color = 7,
    fillcolor = 11,
    fixedsize = true,
    height = 0.6,
    width = 3,
  ];

  edge [
    style = solid,
    fontsize = 14,
    fontcolor = white,
    fontname = "Migu 1M",
    color = white,
    labelfloat = true,
    labeldistance = 2.5,
    labelangle = 70
  ];

  // node define
  alpha [label = "ρ |- (x * z) - (y + z) => 3\n(OpR)",shape = box];
  beta [label = "ρ |- (x * z) => 8\n(OpR)",shape = box];
  gamma [label = "ρ |- (y + z) => 5\n(OpR)",shape = box];
  delta [label = "ρ |- x => 4 \n(VarR)",shape = box];
  epsilon [label = "ρ |- z => 2 \n(VarR)",shape = box];
  zeta [label = "ρ |- y => 3 \n(VarR)",shape = box];
  eta [label = "ρ |- z => 2 \n(VarR)",shape = box];


  // edge define
  alpha -> beta [arrowhead = normal];
  alpha -> gamma [arrowhead = normal];
  beta -> delta [arrowhead = normal];
  beta -> epsilon [arrowhead = normal];
  gamma -> zeta  [arrowhead = normal];
  gamma -> eta  [arrowhead = normal];
}

画像ファイルを生成する_

画像ファイルは以下のように生成する。

% dot -T画像形式 DOTファイル名 -o 出力する画像ファイル名

SVG画像（Webブラウザなどで閲覧できる）の場合は以下のようにする。

% dot -Tsvg example.dot -o example.svg

生成される画像は以下のようになる。

PNG画像の場合は以下のようにする。

% dot -Tpng example.dot -o example.png

生成される画像は以下のようになる。

JPEG画像の場合は以下のようにする。

% dot -Tjpg example.dot -o example.jpg

生成される画像は以下のようになる。

戻る_