Allow effects in post-conditions?

[fisx]

I want to express as a post-condition that the state (say, the actual database) and the model (a pure value keeping track of some data in the database) are still in sync.

I can store the handle to the database in the model together with the pure value, but I cannot write an post-condition with Ensure that queries the database and compares the response with the model.

What would happen if we changed the type thusly:

data Callback input output state
    [...]
  | Ensure (state Concrete -> state Concrete -> input Concrete -> output -> TestT m ())

Is there a better way to do what I want to do that I missed?

I suspect it may be possible to wrap the commandExecute field in a hand-rolled invariant checker in all commands, but I feel there should be a more straight-forward way.

[fisx]

On second thought, I doubt commandExecute would work, because it does not provide access to the model. Anyway it would have been a weird confusion between testable post-condition and semantics.

[owickstrom]

I also hit this problem, but started wondering if effectful post-conditions wouldn't break the black box approach? As in @fisx's example with the database, to keep the database implementation a black box in our tests, we couldn't do any "extra queries" to validate its state. The only way to observe it would be through the API we model as commands and the outputs we get. Is this perhaps why Ensure does not allow IO? If so, this might be a good thing to document clearly in the Haddocks.

And, disclaimer: I've justed started using this library and I'm trying to understand the design, not sure what's best here. :slightly_smiling_face:

[spacekitteh]

I would really like to know the answer to this!

[ocharles]

@spacekitteh can you explain more about what it is you're trying to do, and why you want access to effects in post-conditions? I'm not convinced about the need for this functionality.

[spacekitteh]

To check STM stuff without having to put unsafePerformIO everywhere; for example, checking the contents of containers in stm-containers.

[ocharles]

I'm afraid that still doesn't convince me of the need for effects in post-conditions. I understand HH state machine testing as testing a black box - you probe the blackbox and get some kind of response when you talk to it in commandExecute. Then, you verify the response against what you expect the machine to be doing, in commandCallbacks. If you're using STM, then I'd assume a call to atomically in commandExecute, running the STM transaction and yielding a response you can inspect. Is this approach not possible for you?

[spacekitteh]

Nope. I'm trying to test an API which builds a sort of network/graph; each node (which can be from a number of different constructors) has references to other nodes in TVars and StmContainers.Set's. Further, these nodes have a StmContainers.Multimap of messages in them which, in turn, reference other messages, and the messages have a "history" tree of nodes which lead to the creation of them. The graph is supposed to be able to updated and process its messages concurrently. I can't test for graph consistency without essentially duplicating all this structure to have no STM stuff involved.

It's quite an interconnected mess, which is why it's so important to be able to test construction/manipulation/processing of it and, crucially, that involves consistency checking after every Command.

[ocharles]

Ok, unfortunately I'm still missing the reason why a call to atomically isn't possible/ergonomic. From what I can tell, you'd be equally stuck with QuickCheck-state-machine. This isn't to say "well these things are both doing this so you must be wrong", but when I'm in a situation like this, it does give me pause for thought. I think it would be easier if we had a concrete bit of code to look at. It's difficult to make API decisions without putting the ideas into action.

[spacekitteh]

The call to atomically is fine; it's the unsafePerformIO I don't like :)

Here's what I'm working on: https://gitlab.com/spacekitteh/cosmothought/-/tree/master/core

Specifically, I want to test graphs produced by this: https://gitlab.com/spacekitteh/cosmothought/-/blob/master/core/src/Core/Rete/ReteBuilder.hs

Here's the code testing it: https://gitlab.com/spacekitteh/cosmothought/-/blob/master/core/test/Core/Rete/ReteNodeTests.hs