Improved file naming

This commit is contained in:
2017-06-12 15:38:51 +02:00
parent 9e6707b08f
commit f94ce2d73c
7 changed files with 131 additions and 79 deletions
+16 -6
View File
@@ -92,17 +92,27 @@ public class Graph {
return text;
}
public static synchronized void generateImage(Automata<String> a, String fileName) {
public static synchronized File generateImage(Automata<String> a)
{
return generateImage(a, null);
}
public static synchronized File generateImage(Automata<String> a, String fileName) {
File f;
if (fileName != null) {
f = new File("images/" + fileName + ".png");
} else {
f = new File("images/" + a.hashCode() + ".png");
}
try {
MutableGraph g = Parser.read(Graph.generateImageString(a));
if (fileName != null) {
Graphviz.fromGraph(g).width(Math.max(a.states.size() * 150, 750)).render(Format.PNG).toFile(new File("images/" + fileName + ".png"));
} else {
Graphviz.fromGraph(g).width(Math.max(a.states.size() * 150, 750)).render(Format.PNG).toFile(new File("images/" + a.hashCode() + ".png"));
}
Graphviz.fromGraph(g).width(Math.max(a.states.size() * 150, 750)).render(Format.PNG).toFile(f);
} catch (IOException e) {
e.printStackTrace();
}
return f;
}
}