apalache icon indicating copy to clipboard operation
apalache copied to clipboard

Published 20 hours ago • verified publisher icon apalache-mc

Repurpose `CounterexampleWriter`

Open thpani opened this issue 2 years ago • 0 comments

CounterexampleWriter is used by DumpFilesModelCheckerListener to write all sorts of traces (not just counterexamples).

It should be adapted for this purpose by appropriate renaming, adapting the Scaladoc, etc.

Also, its API is still geared towards counterexamples, e.g, it still takes and writes a "negated invariant" (true) on positive traces:

https://github.com/informalsystems/apalache/blob/96aa8207853d5459b04d19289b96c0cacd5b92f8/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/DumpFilesModelCheckerListener.scala#L31-L32

thpani avatar Aug 10 '22 06:08 thpani