Question about :real/postcondition and :next-state

[lbradstreet]

Hi,

Thanks for stateful-check, it's the missing piece in my test.check use! I'm a bit confused about how to compare the result of :next-state against the result of :real/postcondition without duplicating a lot of logic between :next-state and :real/postcondition.

For example, if I have

{:next-state (fn [state, val, _] (inc state))
 :real/postcondition (fn [state, args, real] (= real state))}

where the result of :real/command is incrementing the real state, I'm getting the previous version of state in :real/postcondition, and I have duplicate the (inc state) logic in both :next-state and postcondition. I can see that this is the result of run-commands calling postcondition with the current state value, rather than the next state value.

The example is contrived but I'm finding that this is causing me to duplicate a lot of logic where I could simply look at the model state and compare it to the real state. Would you consider adding an extra arg to :real/postcondition, containing the next-state value?

Thanks again

[czan]

I understand the pain you're feeling, and to be honest I just copied the way it's done in QuickCheck/PropEr.

I want to think a bit about this before I say yes to it, but in the meantime you should be able to extract the common logic into a function in a fairly mechanical way:

(let [next-state (fn [state, args, val] (inc state))]
  {:next-state next-state
   :real/postcondition (fn [state, args, real]
                         (= real (next-state state args real)))})

You could even make a macro to do the work of this for you:

(defmacro command [map]
  `(let [~'next-state ~(:next-state map)]
     ~(assoc map
             :next-state 'next-state)))

(command {:next-state (fn [state, args, val]
                        (inc state))
          :real/postcondition (fn [state, args, val]
                                (= val (next-state state args val)))})

Of course, these examples are assuming that you're only ever using the single form of next-state. If you are using both :real/next-state and :model/next-state then it would be a bit trickier.

[lbradstreet]

Fair enough and totally understandable why you'd why to think on it. That's a pretty great suggestion which will do the trick for now. The main downside is that next-state will be called twice, and thus it will be slower, but I can live with that.

I keep feeling like there's something I'm missing, and the fact that QuickCheck/PropEr both do it this way isn't helping matters!

Cheers

[czan]

I imagine QuickCheck/PropEr was built with the idea that we can always go from state i to state i+1 by calling the next-state function, but we can't always go from i+1 back to i. (As a trivial example of this, imagine testing a queue's "pop" operation.) This means the most general option is to pass in state i and let the user construct state i+1 if they need it.

I'm a bit hesitant to add another parameter to the postcondition function without thought because it already feels "cluttered" to me. I can't see a good reason not to construct the next state before testing the postcondition (it just means that next-state functions can't assume the postcondition holds, which isn't a guarantee I've given thus far anyway).

[czan]

After thinking more about it I've decided to go ahead with this. As of ad72194dd62aee15eeba89cb9aa9880f88fee959 the :next-state function is called prior to :real/postcondition and the result is passed to the postcondition.

The parameters for the postcondition are now [prev-state next-state args result].

To use your example:

{:next-state (fn [state, _, _] (inc state))
 :real/postcondition (fn [_, next-state, _, real] (= real next-state))}

If you want to start using this now you'll need to move to 0.3.0-SNAPSHOT (also note that I have renamed reality-matches-model? to reality-matches-model as it's not a predicate and that name has been annoying me for a while).

[lbradstreet]

That's fantastic. Thanks for your consideration - I really do think it makes life easier!

On 22 May 2015, at 2:30 pm, Carlo Zancanaro notifications@github.com wrote:

After thinking more about it I've decided to go ahead with this. As of ad72194 the :next-state function is called prior to :real/postcondition and the result is passed to the postcondition.

The parameters for the postcondition are now [prev-state next-state args result].

To use your example:

{:next-state (fn [state, , ](inc state)) :real/postcondition (fn [, next-state, , real](= real next-state))} If you want to start using this now you'll need to move to 0.3.0-SNAPSHOT (also note that I have renamed reality-matches-model? to reality-matches-model as it's not a predicate and that name has been annoying me for a while).

— Reply to this email directly or view it on GitHub.

[lbradstreet]

The snapshot is working great. Thanks again.

[firesofmay]

Hi, Will you be pushing the new version anytime soon? This looks interesting and I am wondering if you'll be pushing 0.3.0 stable version or I'll need to use snapshot for now?

Thanks for your effort.

[czan]

I'm planning on pushing an 0.3.0 release within the next week. Probably this weekend.

[firesofmay]

Awesome! Thanks!

[czan]

I've just pushed a release of 0.3.0, so this issue should be resolved for real now.