Generating counterexample behaviors with Interaction seems awkward?

[thoughtpolice]

Consider the DieHard example, but this goes for anything: a normal run yields

specification: model check: failure
refuted property: always "isSolved"
  * from: 0x5da6be4b
      #smallJug = 3
      #bigJug = 1
  * to: 0x9ef6be4b
      #smallJug = 0
      #bigJug = 4

This is a perfectly sensible counterexample, but the thing is, I generally don't want the inviolate state; it's the very temporal specification itself, so it's apparent. Instead, I want the behavior resulting in this state so that I can understand how it lead here. The specific use case is CI to record bad traces, but even in normal dev cycles, I'd want this.

So normally I would now run ./Spec.hs -tl and then look through the trace diagram for the ending state, then follow the trace backwards to the root. But why can't this simply be emitted immediately? Am I missing something? I don't think I've seen this functionality anywhere.

Part of it is that the API isn't quite set up for this just yet it seems. modelcheck fundamentally doesn't allow you to access the resulting Tree World trace; its type either gives you a Left Error for a counterexample or Right (Tree World) for a successful trace. So if there is a temporal violation then you can't even get the traces.

So in the above case you'd have to modelcheck, and in the case of an error re-modeltrace and look for the resulting inviolate state in the Tree and track the states leading there with a search. This seems suboptimal, but doable. 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.

But ultimately I just want a counterexample behavior. So if I have to modelcheck-then-modeltrace, I suppose that's fine, but this feels like something that should be handled natively. And this will certainly require a big API change between the two I'd think. Honestly, it feels like there should only be one API entry point with an abstract options record we could configure the model checker with to get these results, but this ticket is probably long enough for now and capable of starting a discussion.¹

Footnotes

1. I actually think Spectacle being API driven from Haskell is an absolutely massive advantage over something like TLA⁺ that isn't stressed enough, since it allows a lot of integration flexibility that TLA+ doesn't; for example generating HTML reports from counterexample traces for use in CI is my final goal, and that's just going to be massively easier. Model-based test case generation would be another good example. ↩

[ixmatus]

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!

[riz0id]

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.

[riz0id]

@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.