stateful_check_output.txt

new-state
new-state
new-model
new-state
new-state
new-model
new-state
new-args
node-ids ()
new-state
new-model
new-state
apply ([:no-op nil] [:node 2])
new-args
node-ids ()
new-state
new-model
new-state
apply ([:no-op nil])
new-args
node-ids ()
new-state
new-model
new-state
apply ([:no-op nil] [:no-op nil] [:no-op nil])
new-args
node-ids ()
new-args
node-ids (0 1 4)
new-args
node-ids (0 1 4)
new-args
node-ids (0 1 4 5 4)
new-args
node-ids (0 1 4 5 4)
new-state
new-model
new-state
apply ([:no-op nil] [:node 0] [:node 1] [:node 4])
apply ()
apply ([:node 5] [:node 4] [:request 4])
apply ([:request 1] [:request 4])
new-state
new-state
new-state
new-state
new-state
new-model
new-state
apply ()
apply ([:node 5] [:node 4] [:request 4])
apply ([:request 1] [:request 4])
new-model
new-state
apply ([:no-op nil] [:node 0] [:node 1] [:node 4])
apply ([:node 5] [:node 4] [:request 4])
apply ([:request 1] [:request 4])
new-model
new-state
apply ([:no-op nil] [:node 0] [:node 1] [:node 4])
apply ()
apply ([:request 1] [:request 4])
new-model
new-state
apply ([:no-op nil] [:node 0] [:node 1] [:node 4])
apply ()
apply ([:node 5] [:node 4] [:request 4])
apply ([:node 3] [:node 5] [:request 4] [:node 4])
new-model
new-state
apply ([:no-op nil] [:node 0] [:node 1] [:node 4])
apply ()
apply ([:node 5] [:node 4] [:request 4])
apply ([:request 1] [:request 4])
new-state
new-state
new-state
new-state
new-model
new-state
apply ([:node 5] [:node 4] [:request 4])
apply ([:request 1] [:request 4])
new-model
new-state
apply ()
apply ([:request 1] [:request 4])
new-model
new-state
apply ()
apply ([:node 5] [:node 4] [:request 4])
apply ([:node 3] [:node 5] [:request 4] [:node 4])
new-model
new-state
apply ()
apply ([:node 5] [:node 4] [:request 4])
apply ([:request 1] [:request 4])
new-state
new-state
new-state
new-model
new-state
apply ([:request 1] [:request 4])
new-model
new-state
apply ([:node 5] [:node 4] [:request 4])
apply ([:node 3] [:node 5] [:request 4] [:node 4])
new-model
new-state
apply ([:node 5] [:node 4] [:request 4])
apply ([:request 1] [:request 4])
new-state
new-state
new-model
new-state
apply ([:node 3] [:node 5] [:request 4] [:node 4])
new-model
new-state
apply ([:request 1] [:request 4])
new-state
new-state
new-model
new-state
apply ([:request 4])
new-model
new-state
apply ([:request 1])
new-state
new-model
new-state
new-state
new-state
new-model
new-state
apply ([:request 4])
new-model
new-state
apply ([:request 1])
new-state
new-model
new-state
new-state
new-model
new-state
apply ()
new-state
new-model
new-state
apply ([:node 5])
new-state
new-model
new-state
apply ([:request 0])
new-state
new-model
new-state
apply ([:request 1])
new-state
new-model
new-state
new-state
new-model
new-state
apply ()
new-state
new-model
new-state

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

expected: :pass
  actual: :fail
  

stateful_check_sample.clj

(ns stateful-check-sample
  (:require [clojure.test :refer [is]]
            [clojure.test.check.generators :as gen]
            [stateful-check.core :refer [specification-correct?]]))

(def node-gen
  (gen/fmap
    (fn [n] {:type :node, :id n})
    gen/nat))

(defn request-gen [nodes]
  (let [node-ids (map :id nodes)]
    (prn 'node-ids node-ids)
    (if (seq node-ids)
      (gen/fmap
        (fn [n] {:type :request, :id n})
        (gen/elements node-ids))
      (gen/return {:type :no-op}))))

(def add-ops-spec
  {:model/args (fn [{:keys [model nodes], :as state}]
                 (prn 'new-args)
                 (let [ops (gen/vector
                             (gen/one-of [node-gen (request-gen nodes)]))]
                   [model ops]))
   :real/command (fn [model ops]
                   (prn 'apply (map (juxt :type :id) ops))
                   (as-> model %
                     (reduce (fn [m op] (conj m (:id op)))
                             %
                             (filter (comp #{:node} :type) ops))
                     (reduce (fn [m op]
                               (assert (contains? m (:id op))) m)
                             %
                             (filter (comp #{:request} :type) ops))))
   :next-state (fn [state [model ops] _]
                 (loop [[op & more] ops
                        state state]
                   (if-not op
                     state

                     (if (#{:node} (:type op))
                       (recur more (update-in state [:nodes] conj op))
                       (recur more state)))))})

(def model-spec
  {:commands {:add-ops #'add-ops-spec}
   :real/setup (fn []
                 (prn 'new-model)
                 {})
   :initial-state (fn [model]
                    (prn 'new-state)
                    {:model #{}
                     :nodes []})})

(comment
  (is (specification-correct? model-spec)))