Generating counterexample behaviors with Interaction seems awkward? about spectacle HOT 3 OPEN

@thoughtpolice oh, and as for this comment:

Alternatively, you could modeltrace from the start and simply look for any inviolate state according to the temporal property, but this seems like a delicate thing the API should handle for you? And it seems like there's probably a reason they're separate APIs, for now.

The motivation for having a separate modeltrace vs modelcheck is that this approach was the most direct path to providing both features. It turned out to be fairly difficult to implement both in features in way that shared the same model checker run without significant changes to the model checker's implementation being needed. Since the current CLI is a very simple tool primarily geared towards debugging issues with the model checker, I didn't feel comfortable making significant changes to the model checker in order to support the CLI. Especially since the model checker's correctness is so sensitive to changes.

from spectacle.

Hi @thoughtpolice! Thanks for writing a detailed ticket about what would be more useful for you 🙂 We're pretty busy at the moment so probably won't get around to properly responding to you for a little while.

And yeah, one of the reasons we chose to drive model checking from Haskell was to make integration with Git and CI much nicer. Thanks for affirming our design decisions 🙂

Also, if you do any of the work to generate HTML reports from traces, please contribute it (if you feel so inclined). PRs are welcome!

from spectacle.

I made some crude changes to the CLI to enable performing a trace with property checks within the same interaction call in #55, e.g.

$ cabal v2-repl integration-tests
ghci *> :set args --trace --diagram
ghci *> import Specifications.Bitclock
ghci *> check

The model checker will run in check-only mode by default as before. To disable property checking and only trace the specification you can use:

$ cabal v2-repl integration-tests
ghci *> :set args --no-check --trace --diagram
ghci *> import Specifications.Bitclock
ghci *> check

I know this still isn't ideal from the users perspective, but I understand how annoying it was to switch back and fourth between checking and tracing. Leaving this issue open as I think significant improvements can still be made to the CLI to make tracing more user-friendly.

from spectacle.