[util] render start/stop states in graphviz as boxes, not as dots

..because dots can't contain text.

Change-Id: Ie38e59b17dd5c88fb00c0ae45f6e969335b51116
This commit is contained in:
Moritz Eysholdt 2015-02-03 19:41:04 +01:00
parent 53a95fc5aa
commit 54c6e2f1bf

View file

@ -21,7 +21,7 @@ public class NfaToDot<STATE> extends GraphvizDotBuilder {
protected Node create(Digraph result, Nfa<STATE> nfa, STATE state) {
Node n = new Node(state, stateToString(nfa, state));
if (state == nfa.getStart() || state == nfa.getStop())
n.setShape("point");
n.setShape("box");
return n;
}