Class DotUtil


  • public class DotUtil
    extends java.lang.Object
    utilities for interfacing with DOT
    • Constructor Detail

      • DotUtil

        public DotUtil()
    • Method Detail

      • dotify

        public static <T> void dotify​(Graph<T> g,
                                      NodeDecorator<T> labels,
                                      java.lang.String dotFile,
                                      java.lang.String outputFile,
                                      java.lang.String dotExe)
                               throws WalaException
        Type Parameters:
        T - the type of a graph node
        Throws:
        WalaException
      • dotify

        public static <T> void dotify​(Graph<T> g,
                                      NodeDecorator<T> labels,
                                      java.lang.String title,
                                      java.lang.String dotFile,
                                      java.lang.String outputFile,
                                      java.lang.String dotExe)
                               throws WalaException
        Type Parameters:
        T - the type of a graph node
        Throws:
        WalaException
      • spawnDot

        public static void spawnDot​(java.lang.String dotExe,
                                    java.lang.String outputFile,
                                    java.io.File dotFile)
                             throws WalaException
        Throws:
        WalaException
      • dotOutput

        public static <T> java.lang.StringBuffer dotOutput​(Graph<T> g,
                                                           NodeDecorator<T> labels,
                                                           java.lang.String title)
                                                    throws WalaException
        Returns:
        StringBuffer holding dot output representing G
        Throws:
        WalaException
      • getFontSize

        public static int getFontSize()
      • setFontSize

        public static void setFontSize​(int fontSize)