What state are your properties in?

My last blog ‘Prop’ up your tests with test.check walked through an example of using Property Based Testing (PBT) on a very simple RESTful API.

However, this approach had limitations.

I could test the properties of each call on the API in isolation but what if I wanted to generate tests and assert about properties that spanned calls to the API.

I want to be able to generate random getpost and delete methods for randomly generated resources and be able to assert on these randomly generated commands. For example, if my PBT’s generate a post followed by a get for the same resource I should find the resource but if the tests generate a post, delete, get sequence for the same resource I should get a 404 (not found) on the get.

This gives me a couple of problems.

  1. How to generate random streams of commands with appropriate arguments.
  2. How to assert on properties based on the expected state of the resources on the server.


Fortunately there is a Clojure library for that.

Stateful.check allows me to model the state of any system and to generate random streams of commands with their associated pre and post conditions.

Due to a change in the implementation of the rose tree in the latest version of test.check I needed to use ‘Michael Drogalis’ fork of stateful.check

Stateful.check uses specification maps to model state, define how to generate arguments, check pre and post conditions, etc.

Stateful.check specifications have two parts: an abstract model (state) and a real execution. It took me some trial and error to work out that the abstract model stores the functions you define to operate on  either the model or the real values as symbols and records the order of commands and only during the execution phase does it replay this stack of functions but this time actually evaluating them against the real values.

The model (state) is defined as a hash map and you supply the initial value of the model in the :init-state value of the overall specification.

The state map is used to model the state of the actual implementation. In my case the state map models the state of Customer resources on the server for my simple Customer RESTful API.

To use stateful.check I need to include it in my project.clj file:

  {:dev {:dependencies [[javax.servlet/servlet-api "2.5"]
                        [ring/ring-mock "0.3.0"]
                        [cheshire "5.5.0"]
                        [org.clojure/test.check "0.9.0"]
                        [com.gfredericks/test.chuck "0.2.6"]
                        ; add stateful-check in dev profile
                        [mdrogalis/stateful-check "0.3.2"]]}})

Post method specification

Let’s start by specifying the post specification and a helper function to call the actual implementation.

;; helper functions to call post and get with a single argument
(defn- post-customer
  (post-resource-json (str "/customers") customer))

(def post-customer-specification
  {:model/args (fn [_]
                 [(gen/fmap (fn [cust] {:customer cust}) customer)])
   :real/command #'post-customer
   :real/postcondition (fn [_ _ _ {:keys [status]}]
                         (= 201 status))})
(def customer-resource-specification
  {:commands {:post #'post-customer-specification}
   :initial-state (constantly {})})

(deftest check-customer-resource-specification
 (is (specification-correct? customer-resource-specification {:num-tests 300})))

This is a simple specification for post command and a specification for the customer resource that defines the commands to execute and the initial state of the model. The specification-correct? function in the deftest uses the customer-resource-specification to generate commands based on the specifications listed. Here I am just generating tests for the post-customer-specification.

The post-customer-specification defines how to generate a sequence of arguments to the command function using a function defined against the :model/args key. The :model/args function must return a sequence of generators, one per argument for the command function. The :real/command key-value pair specifies the actual command to call – my helper function post-customer as a quoted var so it can be eval’ed later. The :real/postcondition defines a function that must return truthy if the post condition is valid.

post-customer-specification :model/args

I need to generate a single customer map argument to post-customer so I use the customer generator defined in the previous blog. As a reminder, sampling customer results in something like this:

user> (gen/sample customer)
({:name "", :email "p@microsoft.com", :age 12}
 {:name "", :email "6@yahoo.com", :age 85}
 {:name "", :email "P@yahoo.com", :age 60}
 {:name "·", :email "Qx9@hotmail.com", :age 31}
 {:name "", :email "zl2Y@gmail.com", :age 68}
 {:name "†cÙY", :email "z@zoho.com", :age 24}
 {:name "L ", :email "s0YG@hotmail.com", :age 56}
 {:name "ïàh", :email "n@gmail.com", :age 44}
 {:name "²", :email "mBIT7L1@hotmail.com", :age 34}
 {:name "‰¾ÿÚ", :email "4Q0@hotmail.com", :age 17})

The gen/fmap function maps the function (fn [cust] {:customer cust}) across the sequence of generated customer maps to make each generated customer map the value of the :customer key. I.e. {:customer {:name "", :email "p@microsoft.com", :age 12}. This is required as this structure, turned into JSON, is what the POST route is expecting.

post-customer-specification :real/postcondition

The :real/postcondition function:

  :real/postcondition (fn [_ _ _ {:keys [status]}]
                        (= 201 status))}

Takes four arguments: the previous state (before calling the real command in the execution phase), the next state (after calling the real command), a sequence of the arguments used in calling the command and the result of the command.

In this simple case I am ignore the previous & next states plus the arguments and I’m destructuring the map returned from the post-customer function to get the status and checking it’s created (201).

I also want to verify the Location header includes the generated id. So I can change my postcondition to this:

 :real/postcondition (fn [_ _ args {:keys [status] :as response}]
                         (= 201 status)
                         (not (nil? (extract-location-id response)))))

Where the extract-location-id is the function I defined in the previous blog that extracts the id from the location header value:

(defn extract-location-id
  (second (re-find #"customers/([0-9|-[a-f]]+)" 
            (get-in response [:headers "Location"]))))

This is useful but this is simply reimplementing the same test I implemented in the previous post using test.check. We haven’t seen why modelling the state of the server might be useful. Let’s use a model of the state to store the customer resources returned from the server:

(def customer-resource-specification
  {:commands {:post #'post-customer-specification}
  :initial-state (constantly {:customers {}})})

First I add a map to hold the customers to the state map in the :initial-state for the customer resource specification under test. Now let’s change the post-customer-specification to store the customer posted.

(def post-customer-specification
  {:model/args (fn [_]
                 [(gen/fmap (fn [cust] {:customer cust}) customer)])
   :real/command #'post-customer
   :next-state (fn [state _ {:keys [body]}]
                 (let [id (:id body)]
                   (-> state
                     (update-in [:customers] assoc id body))))
   :real/postcondition (fn [_ _ args {:keys [status body] :as response}]
                           (= 201 status)
                           (not (nil? (extract-location-id response)))
                           (= (:customer (first args))
                              (dissoc body :id))))})

The :next-state function takes three arguments: the current model state (prior to the call to the command), the sequence of arguments to the command, and the result of the command and returns the model of the state after the command executes. In this case I destructure the result of the command to extract the body of the request and add the customer resource map returned in the request body to the :customers map keyed by it’s :id. The updated state map is returned.

I’ve also updated the postcondition function to check the customer map returned from the command with that passed into the command as an argument.

Get method specification

Let’s implement the get method specification for the customers resource. In order to make it easier to generate customer ids for a mixture of customers that exist and customers I will introduce a vector of all generated customer ids into the model that I can select from.

(def customer-resource-specification
  {:commands {:post #'post-customer-specification
              :get #'get-customer-specification}
   :initial-state (constantly {:customers {} :all-customer-ids []})})

I have also referenced my, as yet, unwritten get-customer-specification in the commands.

In order to populate this new vector of all customer ids I need to store the ids of created customer resources once they’ve been returned from the post action. This means I need to update the :next-state function to update the vector of all customer ids.

 :next-state (fn [state _ {:keys [body]}]
               (let [id (:id body)]
                 (-> state
                   (update-in [:customers] assoc id body)
                   (update-in [:all-customer-ids] conj id))))

Now I can add my get-customer-specification:

(defn- get-customer
  (get-resource-json (str "/customers/" id)))


(def get-customer-specification
  {:model/args (fn [state]
                 (if (seq (:all-customer-ids state))
                   [(gen/frequency [[9 (gen/elements (:all-customer-ids state))]
                                    [1 gen/int]])]
   :real/command #'get-customer
   :real/postcondition (fn [{:keys [customers]} _ args {:keys [status body]}]
                         (let [id (first args)]
                           (if (customers id)
                               (= 200 status)
                               (= body (customers id)))
                             (= 404 status))))})

Let’s break this specification down and examine what I’m doing here.

The :real/command I’m going to call is a ‘helper’ function that takes a customer id, creates the appropriate URL, generates a request using the get method that gets submitted to the app, lastly, the body of the response returned is parsed form JSON to a Clojure map to make it easier to examine.

As get-customer takes a single argument of customer id I need to create a sequence of one generator for this argument. If the :all-customer-ids map in the state model has entries (i.e. seq return not nil) then I have customer id’s I expect to be present on the server. I can pick an id for a customer I expect to exist using gen/elements on the :all-customer-ids map. I use gen/frequency to generate a random int for one in 10 cases so that I get some not found edge cases. If I don’t have any customer id’s already stored in my model I just generate a random int.

In the :real/postcondition I destructure the :customers map from the state previous to the call to get and I extract the status and body from the result of the call to get. I check if the customer whose id is passed to get-customer exists in the model of customers and if it does I expect to find the customer (status 200 and the body of the response matches the customer in the model). If there is no customer for that id in the model then there should be no customer for that id on the server so I check for a status 404.

Delete method

Up to this point, apart from randomly generating get‘s and post‘s I haven’t added much to what I implemented previously using test.check alone.

What happens if we add a delete method for the customer resource? Let’s model that in our specification.

(defn- delete-customer
 (delete-resource-json "/customers/" id))


(def delete-customer-specification
  {:model/args (if (seq (:all-customer-ids state))
                        [[9 (gen/elements (:all-customer-ids state))]
                         [1 gen/int]])]
   :real/command #'delete-customer
   :next-state (fn [state args _]
                 (let [id (first args)]
                   (update-in state [:customers] dissoc id)))
   :real/postcondition (fn [{:keys [customers]} _ args {:keys [status]}]
                         (let [id (first args)]
                           (if (customers id)
                             (= 204 status)
                             (= 404 status))))})

Again, I’ve created a ‘helper’ function to call delete customer for an id.

The argument in this case is a random int if I have no customer ids in my model, or 9 times out of 10 a random id already posted and 1 time out of 10 a random int.

The :next-state function gets the customer id argument passed to the command and dissoc’s (removes) the customer for that id from the model.

You may have noticed that I don’t remove deleted customer id’s from the :all-customer-ids map in the model. This is intentional as I want to generate cases where the customer had been posted, deleted and then another command executed on the deleted customer.

The :real/postcondition function checks if the customer id to be deleted was the customers in the model prior to the delete command and if so I expect a ‘no content’ response (status 204) otherwise the customer should have been deleted so I expect a ‘not found’ (status 404).

I also need to add the delete-customer-specification to my tests:

(def customer-resource-specification
  {:commands {:post #'post-customer-specification
              :get #'get-customer-specification
              :delete #'delete-customer-specification} ; added delete
   :initial-state (constantly {:customers {} :all-customer-ids []})})

What happens if I implement the delete method route on the server like so:

(defn- delete-customer
  (let [customer (get-in @datastore [:customers id])]
    (if customer
      (resp/status (resp/response nil) 204)

(defroutes app-routes
  (DELETE "/customers/:id" [id]
    (delete-customer id))
  (route/not-found "Not Found"))

If I run the tests with this implementation I get something like this:

user> (run-tests 'blogpbt.handler-state-pb-tests)

Testing blogpbt.handler-state-pb-tests

FAIL in (check-customer-resource-specification) (handler_state_pb_tests.clj:125)
    #<2> = (:post {:customer {:name "", :email "0@gmail.com", :age 10}}) => {:status 201, :headers {"Location" "/customers/0a3794e7-c1d3-4ca2-b048-0ff247aefbbe", "Content-Type" "application/json"}, :body {:name "", :email "0@gmail.com", :age 10, :id "0a3794e7-c1d3-4ca2-b048-0ff247aefbbe"}}
    #<5> = (:delete (get (get #<2> :body) :id)) => {:status 204, :headers {"Content-Type" "application/octet-stream"}, :body nil}
    #<12> = (:get (get (get #<2> :body) :id)) => {:status 200, :headers {"Content-Type" "application/json"}, :body {:name "", :email "0@gmail.com", :age 10, :id "0a3794e7-c1d3-4ca2-b048-0ff247aefbbe"}}
Error while checking postcondition
Seed: 1460361271954
Visited: 103

expected: :pass
 actual: :fail

Ran 2 tests containing 2 assertions.
1 failures, 0 errors.
{:test 2, :pass 1, :fail 1, :error 0, :type :summary}

Whoops! I get an error if my tests generate a post for a customer, followed by a delete followed by a get. Why? Hmmm, my get is returning a status 200 which is an ‘OK’ but if I do a get after a delete for the same customer I should get a 404 (not found) of course.

My implementation of delete doesn’t remove the customer from my datastore atom! Let’s fix that:

(defn- delete-customer
  (let [customer (get-in @datastore [:customers id])]
    (if customer
        (swap! datastore update-in [:customers] dissoc id)
        (resp/status (resp/response nil) 204))

That looks better. Let me re-run the tests.

user> (run-tests 'blogpbt.handler-state-pb-tests)
Testing blogpbt.handler-state-pb-tests
Ran 2 tests containing 2 assertions.
 0 failures, 0 errors.
 {:test 2, :pass 2, :fail 0, :error 0, :type :summary}

That, looks better.

So in this blog you’ve seen how to use stateful.check to generate random sequences of commands and use a model to maintain the expected state so that you can generate appropriate arguments and assert against the expected state.

If you want to run or explore the code for this blog you will find it in the pbt-stateful branch of my blogpbt git repo.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s