VN: Visualization of Nondeterminism

VN is a tool for studying nondeterministic finite automata (NDFA). It generates a Promela program from a representation of an NDFA (for example, one generated by JFLAP. The program can be executed randomly or guided interactively using the Erigone model checker. VN can find one or more accepting computations if they exist. The NDFA and the execution path are graphically displayed using the dot language and tool from GraphViz.

Download from GitHub: