jd823592 / ic3 Goto Github PK

Because this is a lazy implementation, it is worth considering to modify the algorithm so that it collects all the counterexamples that it can find.

How this would be implemented:

1. Disallow Counterexample to be thrown. Drop the middle monad from bad and block and store a list of already discovered counterexamples in the state. Every time a real counterexample is found, remember it but block it as well. This would probably not work if there were infinitely many counterexamples as even if we read just one it would still have to wait for termination, which would not occur.
2. Counterexample is still thrown but the outermost loop collects it and uses guarded recursion to construct lazily a list of all counterexamples. Then depending on how many counterexamples were read, that many would be generated. But where would one include the resulting invariant? The counterexample would have to be blocked just before throwing it.