czan / stateful-check Goto Github PK

I came across this talk that was given at ClojuTRE in Sep 2019:

• How to do Stateful Property Testing in Clojure – Magnus Kvalevåg

The presenter begins talking about stateful-check at this time in the video.

Maybe it would be worth adding a reference to in the README.org?

Hi there! Thanks for this wonderful tool!

It appears that using it in conjunction with test.check 0.9.0 throws incompatibility errors. Running the test suite for stateful-check produces an exception that IPersistentVector can't be cast to a RoseTree. I did some digging around, but wasn't able to come up with a solution.

Let's say you are testing a system where records are stored and the system assigns and returns a generated id. You can get back records by their id.

During retrieve-record command args generation, I want to randomly pick one of the generated ids, but the :args fn works on symbolic values and then the system will get called with a symbolic value.

How can you make this work?

Hi @czan,

first, thanks for this nice library. It is a really cool way of testing things. I saw you have this feature about using the clojure.test is form in post conditions in the development branch. This is something I was longing for and I was about to look into myself. Luckily you already seemed to have solved this issue. :)

What's the state of this? Is there a chance this could make it into a release?

Thanks, Roman.

I was trying to test a model and came across the following behavior. I'm not sure if this is the intended behavior, or if there's a better way to test this, or if my model isn't testable using this framework. Any suggestions are welcome.

The model is described as follows. I have a hashset that I can add nodes to. If a node is present in the set, I can request it and it will be returned. If the node has not been added, a request for it will throw an exception. There are two types of operations, one to add a node and one to request a node. These can be batched together such that multiple operations can be applied to the model at the same time. The expected behavior is to add all of the nodes first, and then evaluate any requests in the batch.

Now, for some examples...

; adds node 1
(model/apply [{:type :node, :id 1}])
; request node 1; all is ok
(model/apply [{:type :request, :id 1}])

; request node 2; throws exception because it doesn't exist
(model/apply [{:type :request, :id 2}])

; re-request node 1; add node 3 & immediately request it, all ok because nodes are added first
(model/apply [{:type :request, :id 1} {:type :request, :id 3} {:type :node, :id 3}])

Here's a gist with repro code and output: https://gist.github.com/mbossenbroek/b3eb82d7dd19d7dfbea5

When setting up the test, I'm storing the set of nodes that should be in the model within the state. I'm then using that information in the state to generate a set of requests for only those nodes. To say it another way, these generators should only ever generate requests for nodes that are in the model (and the state).

What I'm seeing is that it's preserving the :model/args generators across state/model resets. It will do a run that adds node 2, requests node 2, and all is good. Then it will reset the model & state, but continue to use a generator that thinks the model has a node 2, and comes up with a failure case of requesting only node 2. This isn't valid because we know the model doesn't have a node 2, so the exception is expected.

So, the primary question seems to be: why is it using an older generator? Is that a bug, or am I modeling it incorrectly?

Some secondary questions:

Why does it call the :initial-state function so often? It calls it much more frequently and in more places than I would expect.

The final output/failure shows what appears to be step #<3> in the process, which is odd. I was expecting a sequence of operations to apply to the model, starting with #<1>. If there's only one step, why #<3>?

FAIL in clojure.lang.PersistentList$EmptyList@1 (NO_SOURCE_FILE:1)
   #<3> = (:add-ops #{} [{:type :request, :id 0}])  =!!> #<AssertionError java.lang.AssertionError: Assert failed: (contains? m (:id op))>
Exception thrown while executing command 
Seed:  1445446106195
Visited:  14

Thanks,
Matt

The problem

I recently did a pretty large refactor in a codebase that was using already ~20 commands and I was running the specification-correct? assertion while I was refactoring to see if I had all the commands passing the postconditions as expected.
At some point the assertion was passing and returning the list of a bunch of commands with their corresponding frequency so everything seemed fine, however the issue was that some commands were not being executed at all, because the require function wasn't being satisfied, but this was not one of the main commands and only one among 20 was unnoticed at first.

Even without a large refactor, a command could stop running and go unnoticed because we usually don't check the cicd jobs output when everything is passing.

A proposal

I think it would be useful to add an exhaustive option to the specification-correct? assertion that will make it fail if some of the commands was not executed.
This flag could be turned on locally during refactors to check that every command is being executed or even use it in continuos integration.

Besides that, printing the commands that were not executed (aka frequency 0) even when the test passes and exhaustive is false, could be useful. So you can have at least some sort of "warning" that you are not running all the commands that you've specified but you might be fine with that (and that's why you don't want to turn on the exhaustive flag).

What do you think about this proposal? Does it make sense to you?
I could implement it if you think is useful, I've already did a local implementation and helped me to discover broken require functions during a refactor.

Note: My implementation only modified the report-result but if might be misleading to have result being true and then make the assertion fail. Also it is probably hardest to test at this level.

Thanks a lot for your work on this library, it's very useful.

One thing I noticed is that when a test fails, the seed doesn't appear to be printed, so if I want to reproduce the test run (after, say, applying a fix for the bug), my only choice is to run a large number of tests and hope the same sequence is generated.

Is there a way to do this?

Hi @czan,

I'm experimenting with an Emacs Mode for stateful-check.

Right now I have the following features planned:

• Enhance the clojure.test machinery to report more information about stateful-check test runs, so NREPL middleware can reach it
• Render the failed/shrunk executions in a buffer similar to what we have now. But ...
• Render command arguments and results via the Cider inspect value machinery (larger data structures are truncated)
• Functionality to open command arguments and results in the Cider inspector
• Functionality to open the state/model of each execution step
• Some kind of debugger/execution stepper, that allows to live step one execution after the other and inspect the state.

It's all work in progress, but this is where I am right now:

https://github.com/r0man/stateful-check/tree/nrepl
https://github.com/r0man/cider/tree/stateful-check
https://github.com/r0man/cider-nrepl/tree/stateful-check

Since you also seem to use know a bit about Emacs and NREPL middleware (I just discovered wingman), do you have any other ideas?

Roman

Hey there!
First and foremost, thank you for this amazing lib, it has been a blast using it 🎉

So, I've been having this error at the end of the executions and I'm not sure how to solve it, would you mind taking a look? Maybe it is something on my test configuration that's causing it, but I haven't been able to figure out 😬

OS info: MacOS Catalina - 10.15.3

ERROR in () (core.clj:200)
expected: (specification-correct? conn-spec {:report {:first-case? true, :stacktrace? true}})
  actual: java.lang.ClassCastException: class java.io.StringWriter cannot be cast to class java.io.PrintWriter (java.io.StringWriter and java.io.PrintWriter are in module java.base of loader 'bootstrap')
 at stateful_check.core$report_result$fn__12635.invoke (core.clj:200)
    stateful_check.core$report_result.invokeStatic (core.clj:193)
    stateful_check.core$report_result.invoke (core.clj:182)
    pocket_conn_pool.core_test$eval12667.invokeStatic (form-init869914851329692435.clj:1)
    pocket_conn_pool.core_test$eval12667.invoke (form-init869914851329692435.clj:1)
    clojure.lang.Compiler.eval (Compiler.java:7177)
    clojure.lang.Compiler.eval (Compiler.java:7132)
    clojure.core$eval.invokeStatic (core.clj:3214)
    clojure.core$eval.invoke (core.clj:3210)
    clojure.main$repl$read_eval_print__9086$fn__9089.invoke (main.clj:437)
    clojure.main$repl$read_eval_print__9086.invoke (main.clj:437)
    clojure.main$repl$fn__9095.invoke (main.clj:458)
    clojure.main$repl.invokeStatic (main.clj:458)
    clojure.main$repl.doInvoke (main.clj:368)
    clojure.lang.RestFn.invoke (RestFn.java:1523)
    nrepl.middleware.interruptible_eval$evaluate.invokeStatic (interruptible_eval.clj:79)
    nrepl.middleware.interruptible_eval$evaluate.invoke (interruptible_eval.clj:55)
    nrepl.middleware.interruptible_eval$interruptible_eval$fn__10569$fn__10573.invoke (interruptible_eval.clj:142)
    clojure.lang.AFn.run (AFn.java:22)
    nrepl.middleware.session$session_exec$main_loop__10670$fn__10674.invoke (session.clj:171)
    nrepl.middleware.session$session_exec$main_loop__10670.invoke (session.clj:170)
    clojure.lang.AFn.run (AFn.java:22)
    java.lang.Thread.run (Thread.java:834)

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

Hello, when a test fails, the errors and the seed are printed and the following data is returned:

{:test 1, :pass 0, :fail 1, :error 0, :type :summary}

Is there a way to get access to the commands and system responses as data? It would be really useful to have this for debugging the system when a test fails.
Accessing the generated commands so you can execute them against the system manually is really useful. Currently the only way to do this is by copy-pasting them.