add option to highlight non-determinism in dot output

I guess --dot=d would make sense.