on DFS scan violation discovery, return better options

[michbarsinai]

The DfsBProgramVerifier.ProgressListener::violationFound violation listener should:

1. Accept a set of violations, not just one.
2. Return one of the following:

• CONTINUE
• PRUNE
• HALT

Effect of the return values:

• CONTINUE - mark current node as having a violation, go deeper into the graph.
• PRUNE - mark current node as having a violation, pop it (as in - go back and don't DFS into its descendants)
• HALT - mark current node as having a violation and stop the verification.

[achiyae]

I want different behaviors (Continue, prone, halt) for different violations. Will it be supported?

[michbarsinai]

Yes, your progress listener will get the violation can can then decide what to do.