The formulas in automatons are hard to read at a glance. & is distracting, literals don't stand out from logical connectives and from one another.
Consider:
- use html code for logical connectives; classic logical connectives are cleaner and easier to recognize
- assign its own unique color to each literal
- bold the positive occurrence of a literal and italicize the negated occurrence of a literal