Soundness Checker

Verifies an accepting Petri net: is it a workflow net, and is it sound? Reports the three classical requirements — every case can still finish, finishes with nothing left over, and every transition can fire — plus boundedness, each decided exactly on the reachability graph and each failure carrying the firing sequence that demonstrates it. Discovery plugins produce nets; this is what says whether the net produced is one you can trust.