"""
visualizations.py
=================
This module contains some adaptations e.g. of the standard ``networkx`` drawing routines \
to the standard input data formats used in the ``datatypes`` sub-module of ``ReSMT``.
"""
#####################################################################################
# %% setup of logging tool for providing various level of feedback to the user:
import logging
# NOTE: in order to alter the behavior of the logging tool *after* having once
# executed the code below, it is necessary to restart Python and load the module
# again! (-> possibly find a nicer method to allow "on-the-fly" changes...)
from resmt import datatypes
logging.basicConfig(format='%(asctime)s.%(msecs)03d %(message)s',
filename='visualizations.log',
# filemode='w',
# datefmt='%d/%m/%y %H:%M:%S',
datefmt='%H:%M:%S',
level=logging.INFO) # set to logging.INFO for less verbose mode
# uncomment the following if an output to the console is also desired:
# logging.getLogger().addHandler(logging.StreamHandler())
logging.info('---------->visualizations.py module loaded<----------')
#####################################################################################
# %% Initialization:
# support for intelligent type-aliases
from typing import Any, Dict, List, Set, Tuple, NamedTuple, TypeVar, Type, Optional
import os
from pprint import pformat
from IPython.display import SVG, display, HTML
# set the interactive Python shell to recognize the current working directory:
import sys
sys.path.append(os.getcwd())
from collections import OrderedDict, Counter
import timeit
import numpy
import networkx as nx
import z3
import mpmath
import resmt.datatypes
from jinja2 import FileSystemLoader
from latex.jinja2 import make_env
from latex import build_pdf
import subprocess
import signal
from network2tikz import plot
import seaborn as sns
#### some nice available styles:
# 'seaborn-whitegrid', 'seaborn-pastel', 'seaborn'
####################################
# for plotting runtimes etc.:
import matplotlib
import matplotlib.pyplot as plt
from matplotlib import style
style.use('seaborn-white')
from mpl_toolkits.mplot3d import Axes3D
# allow for TeX forumlas in labels etc.:
# source: https://stackoverflow.com/questions/46259617/how-does-one-use-latex-amsmath-with-matplotlib
matplotlib.rc('text', usetex=True)
matplotlib.rc('font', **{'family': "sans-serif"})
# method compatible with matplotlib >= 3.3:
latexPreambleParams = [r'\usepackage{amsmath,amssymb}',
r'\usepackage[english]{babel}',
r'\usepackage[utf8]{inputenc}',
r'\usepackage{sansmathfonts}',
r'\usepackage[scaled=0.95]{helvet}',
r'\renewcommand{\rmdefault}{\sfdefault}',
r'\usepackage[T1]{fontenc}']
params = {'text.latex.preamble': '\n'.join(map(str, latexPreambleParams))}
plt.rcParams.update(params)
##########################################################################################################
# %%
[docs]class nxTypedDirectedGraph:
"""Networkx representation of typed directed graphs."""
[docs] def __init__(self, G: datatypes.Z3TypedDirectedGraph,
drawGraph: bool = True,
writeGraph: bool = False,
fileName: str = None,
gLayout: str = 'neato') -> None:
"""Instantiating a Networkx representation of a Z3TypedDirectedGraph.
Args:
G: a ``Z3TypedDirectedGraph`` instance
drawGraph: (optional) a boolean controlling whether or not to draw the graph \
via the matplotlib plot commands after instantiation (default: ``True``)
writeGraph: (optional) controls whether or not the graph should be written \
to a file (default: False)
fileName: (optional) a filename for the graph, where the extension controls \
the output format (default: None)
gLayout: (optional) a string controlling the graph layout for the interactive \
display (default: 'neato'; alternative options are those of ``GraphViz``, e.g. \
``dot``, ``twopi``, ``fdp``, ``sfdp`` and ``circo``).
.. note:: The available file-formats for the graph visualizations are those supported \
by the ``GraphViz`` package, i.e. either of the following ones:
bmp canon cgimage cmap cmapx cmapx_np dot dot_json eps exr fig gd gd2 gif gv
icns ico imap imap_np ismap jp2 jpe jpeg jpg json json0 mp pct pdf pic
pict plain plain-ext png pov ps ps2 psd sgi svg svgz tga tif tiff
tk vdx vml vmlz vrml wbmp webp xdot xdot1.2 xdot1.4 xdot_json
"""
# vertex and edge sets (in format of dictionaries of the format 'elName':'elSrt')
self.vertices = G.vertices.els
self.edges = G.edges.els
# determine the number of vertex and edge sorts, and render suitable color palettes:
vSorts = list(set(G.vertices.els.values()))
eSorts = list(set(G.edges.els.values()))
vertexColors = sns.color_palette("dark", len(vSorts)).as_hex()
# render a version with alpha value of 0.5 for the node labels:
alphaVL = 0.5
vertexLabelColors = sns.color_palette(
[tuple(x + (1 - x) * (1 - alphaVL) for x in c)
for c in sns.color_palette("dark", len(vSorts))]
).as_hex()
edgeColors = sns.color_palette("dark", len(eSorts)).as_hex()
vSrtToColor = {vSorts[i]: vertexColors[i] for i in range(len(vSorts))}
vSrtToLabelColor = {vSorts[i]: vertexLabelColors[i] for i in range(len(vSorts))}
eSrtToColor = {eSorts[i]: edgeColors[i] for i in range(len(eSorts))}
# the incidence data:
# NOTE: we filter out any potential nil-element mappings!
self.stDict = {e:vs for e, vs in G.stDict.items() if e[:3] != 'nil'}
# instantiate an empty multidigraph:
self.graph = nx.MultiDiGraph()
self.graph.nodes(data=True)
# render the node sets from self.vertices and node color lists:
nodeColors = []
nodeLabelColors = []
for vName, vSrt in self.vertices.items():
if vName[:3] != 'nil':
self.graph.add_node(vName, sort=vSrt)
nodeColors += [vSrtToColor[vSrt]]
nodeLabelColors += [vSrtToLabelColor[vSrt]]
self.nodeLabels = {vName: vName for vName in self.graph.nodes()}
# render the edges from self.edges and self.stDict:
edgeColors = []
edgeNames = []
for eName, eSrt in self.edges.items():
if eName[:3] != 'nil':
vSrc, vTrgt = self.stDict[eName]
self.graph.add_edge(vSrc, vTrgt, sort=eSrt)
edgeColors += [eSrtToColor[eSrt]]
edgeNames += [eName]
self.edgeLabels = {self.stDict[eName]: eName for eName in self.edges.keys() if eName[:3] != 'nil'}
self.pos = nx.fruchterman_reingold_layout(self.graph)
# render a pydot visualization of the graph
self.pydot = nx.drawing.nx_pydot.to_pydot(self.graph)
# adjust the node styles:
for n in self.pydot.get_nodes():
vSrt = n.get('sort')
# Note: pydot requests rgb colors as a string with all three
# subcolor values separated by a space, hence the conversion below:
vColor = vSrtToColor[vSrt]
vLabelColor = vSrtToLabelColor[vSrt]
n.set_color('white')
n.set_fontcolor(vLabelColor)
n.set_fillcolor(vColor)
n.set_shape('circle')
n.set_style('filled')
n.set_fontsize('6pt')
n.set_fontname('Lato')
n.set_margin('0.05')
n.set_height('0.3')
n.set_width('0.3')
n.set_penwidth('0')
n.set_fixedsize('True')
# adjust the edge styles:
for idx, e in enumerate(self.pydot.get_edges()):
e.set_arrowsize('0.5')
eSrt = e.get('sort')
# Note: pydot requests rgb colors as a string with all three
# subcolor values separated by a space, hence the conversion below:
eColor = eSrtToColor[eSrt]
e.set_color(eColor)
e.set_fontcolor(eColor)
e.set_fontsize('6pt')
e.set_fontname('Lato')
# read out the edge name by edge index:
e.set_label(edgeNames[idx])
# write the graph to a file (if writeGraph == True and a non-empty filename is given):
if writeGraph:
if fileName is None:
raise ValueError('Please specify a filename!')
else:
# write the SVG image to a file:
fmt = fileName[-3:].lower() # format string
# NOTE: the following call will automatically raise a value-error if a
# format not supported by GraphViz is required (i.e. with supported formats
# possibly evolving via the updates to that package)
self.pydot.write(fileName, format=fmt, prog=gLayout)
# draw the graph to the interactive plot console (if drawGraph == True)
if drawGraph: # if drawGraph == True
self.display = SVG(self.pydot.create(prog=gLayout, format='svg'))
else:
self.display = None
[docs]def displaySVGtable(tabData: Dict[str, List[str]], width:str ="100%") -> None:
""""Display a set of SVG images in an HTML table.
This method is adapted from code by \
`Brian Naughton <http://blog.booleanbiotech.com/ipython_notebook_tips.html)>`_. \
It allows to render a table of SVG images (with table headers), which provides \
a nice extension to the funcitonalities of ``Jupyter`` notebooks (since the default \
SVG image display would only permit a sequential output of SVG images).
Args:
tabData: a dictionary with entries of the form ``'header entry': ['SVG filename 1',...]``, \
i.e. the data necessary to fill a column of the table
width: (optional) a string of the form ``"x%"``, with ``x`` an integer between ``0`` and ``100`` \
(default value: ``"100%"``)
"""
# initialize a HTML table specification:
html = ["<table width:{}'><tr>".format(width)]
# render the header entries:
html += ["<th style=\"text-align:center\">{}</th>".format(h) for h in tabData.keys()] + ["</tr>"]
# determine the maximal length of the columns:
numRows = max([len(val) for key, val in tabData.items()])
for r in range(numRows):
html += ["<tr>"]
for hStr, cList in tabData.items():
if (r + 1) <= len(cList):
html += ["<td style=\"align:center\"><img src='{}' /></td>".format(cList[r])]
else:
html += ["<td></td>"]
html += ["</tr>"]
html += ["</table>"]
display(HTML(''.join(html)))