Generalize postcondition

[edsko]

This allows postcondition to return a string explaining the failure, rather than just a Bool. This will help with debugging.

I didn't bother taking advantage of this in the registry test, just added a function that turns a Bool into a Maybe String.

[ch1bo]

This looks very helpful! I used monitoring in the past to explain postcondition failures by:

monitoring (s, s') action l result =
  decoratePostconditionFailure
 where
  decoratePostconditionFailure
    | postcondition s action l result = id
    | otherwise =
        counterexample "postcondition failed"
          -- TODO: . counterexample ("Result: " <> show result)
          . counterexample ("Action: " <> show action)
          . counterexample ("State: " <> show s)

But having individual failures described by the model itself, good idea! 👍

[ch1bo]

Only issue with this.. it's a breaking change 😄 Version 2.0.0 incoming? 🤔 @abailly

[edsko]

Re version numbering, as far as the PVP is concerned, version 1.2 would suffice :)

[edsko]

If you are going to up the version number, might want to hold off, I'm working on some stuff, I may or may not have further PRs :)

[ghost]

I don't have any fetish with version numbers, they are, well, just numbers, so if this change is immediately useful and breaking then so be it :) Of course, if you have some other stuff coming @edsko it's also fine to wait a bit.

[ghost]

And thanks a lot for your contribution BTW !

[ghost]

Suggestion: Just fill in an example here? I agree we shouldn't bother with the other branches of the alternative.

[edsko]

Sure, can do! :)

[UlfNorell]

Having the ability to explain a failing postcondition is a good feature, but I'm not very fond of Maybe String.

• It's not immediately obvious (without reading the documentation) that Just means failure and Nothing means success.
• There's a lack of combinators (like && and ==) to use with Maybe String. Forcing every user to add a checkBool function is not very nice.

It would suggest defining a new type (isomorphic to Maybe String) and a set of combinators to work with it that include conjunction, equality checking (like ===), and conversion from Bool.

Backwards compatibility could be saved by adding this functionality in a new method postconditionBikeShed with default implementations in both directions.

[edsko]

Ok, will give that a stab later.

[ghost]

Out of curiosity, what are you using q-d for @edsko ?

[edsko]

I'm investigating whether I can use it for lockstep-style testing with q-d instead of q-s-m, so I'm trying to build some infrastructure on top of StateModel that allows me to do that. If I succeed, will probably write a blog post about it.

Now that we're on the topic: if successful, this infrastructure will probably consist of a new module that users can use, that provides a class on top of StateModel with some functions that provide default implementations for methods of StateModel. Would you guys in theory be interested in perhaps having that as part of the repo itself? If so, I'll send you a link to a draft blog post once I have it and you can assess if it's at all of interest; if you then decide it's of interest, I'll submit a PR.

[ghost]

Interesting! I don't see why we would not be interested in your contributions :) BTW, a few people are interested in understanding what are the differences between q-d and q-s-m and it seems your insights would be much appreciated. At the very least, pointing at your blog post could be a good first answer to that question.

[edsko]

Ok! Will send you a draft once it's done.

And yes, people have been asking me the same question, hence the blog post :)

[MaximilianAlgehed]

This is a welcome idea. We have the monitoring function but that suffers from not being the postcondition so you would have to repeat logic to move the logging entirely to monitoring.

Also see #12 - we have some breaking changes coming up so I suggest waiting a little bit with merging this PR (after the important suggestion from @UlfNorell) until we've settled the dust on that.

[edsko]

Yes, I will make that change, and maybe also propose one other (very minor) one. I am nearly done with my experiment, will report back hopefully tomorrow.

[edsko]

Ok, draft blog post implementing a "lockstep-style testing" abstraction on top of quickcheck-dynamic , and comparing it to a similar abstraction in quickcheck-state-machine, now available at https://www-staging.well-typed.com/staging-lockstep-eyohtj/blog/2022/09/lockstep-with-quickcheck-dynamic/ . The code for the abstraction itself can be found at https://github.com/well-typed/qsm-in-depth/blob/master/src/StateModel/Lockstep.hs ; it depends on this PR.

If you guys think that this InLockstep is something you'd like to merge into the main library, let me know, and then I will create a PR for that. Either way, I will take care of the remaining PR review on this PR probably next week.

[ghost]

Thanks a lot @edsko. I had a quick look at the blog post and it's really great. This comparison is really useful and I wish you later have the time to investigate the dynamic logic part. The Lockstep might indeed be an interesting addition to the library. I will try to go through it over the week-and, and I think it would be great if @UlfNorell and @MaximilianAlgehed who are the bright minds behind this library could chime in and provide their insights.
I like the idea of keeping the library compact but having some "batteries included" does no harm.

[edsko]

Ok, I have pushed another commit that introduces a proper abstraction for postconditions, and I've modified the postcondition in the registry to take advantage of it.

Re lockstep, I will wait for the final verdict before submitting a PR on that :)

[ghost]

I like the PostCondition type :) I think we're all good and I would like to merge this PR. These changes somewhat conflict with #12 but I am happy dealing with the changes which are pretty much automatic. Alternatively, if you want you can rebase this branch on #12 @edsko as this will make your code compatible with soon-to-be-released version 2.0.0.

Regarding the LockStep abstraction, I think we can add it in a later PR. It's not a breaking change anyhow.

[edsko]

Sure, I can rebase.

[MaximilianAlgehed]

I would be much happier with a Assertable type class here (just like how QuickCheck has Testable). That way you can return a boolean if you want.

[ghost]

Also, the comment is now obsolete.

[MaximilianAlgehed]

Please add infix versions of these operators.

[MaximilianAlgehed]

This is why I want infix operators...

[edsko]

This is getting into bikeshedding territory; there are many ways that this type can be defined. Happy to make changes if there are specific requirements, or happy to leave this to you guys to modify as you see fit, but I'd like to avoid an endless back and forth if we can.

[MaximilianAlgehed]

I understand wanting to avoid endless back and forth - but this PR currently makes the examples more difficult to read so I'm not super comfortable merging it until that's been fixed.

In my humble opinion right way to implement new features is not to introduce a skeleton idea and leave it up to the maintainers to "modify as we see fit" - it's to introduce a coherent and complete package.

[edsko]

Ok, I see. Fair enough. I tried to give you a nice PR and tried to incorporate your suggestions, but if you consider this to be merely a "skeleton idea" where I am leaving the "actual implementation" up to you guys, I see that I am mistaken. My apologies.

[ghost]

@edsko Is your blog post published? At least, I would like to point at it in the README and fix #8

[edsko]

Not yet, will probably be early this week.

[MaximilianAlgehed]

@edsko I'm sorry if I hurt your feelings. I certainly didn't mean to imply that you haven't done useful work here - I just mean that I think there is more we can do with this to make sure we arrive at the right long-term solution that does everything we want. I think the fact that you were willing to pull this thread and start the discussion is great and I really want to include the work you've done in the repo so let's be friends and have an open discussion about the best way to pull it off. And let's perhaps have that discussion over in #15 to avoid it just being an endless series of requested edits to this PR, because I completely agree that such a process is super frustrating!

[edsko]

@abailly-iohk I have updated the draft blog post as well as my code to be compatible with current main of quickcheck-dynamic (the Realized stuff primarily). I have also put my code in a repository at https://github.com/well-typed/quickcheck-lockstep ; once you guys release a new version of quickcheck-dynamic to Hackage, I can follow suit for quickcheck-lockstep. The blog post should also be released soon.

[edsko]

(I now use monitoring to record the more detailed postcondition, so I don't depend on a solution to #15 .)

[edsko]

Blog post is live! https://well-typed.com/blog/2022/09/lockstep-with-quickcheck-dynamic/ Thanks for the assist, and the library. I think lockstep-style testing is much nicer with quickcheck-dynamic/quickcheck-lockstep rather than with quickcheck-state-machine :)

[abailly]

Thanks a lot @edsko for being our first external contributor and putting in the effort to work on this! I will make sure we reference the blog post in the documentation real quick and spread the word.