example.clj

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

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

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

(def nodes (atom nil))

(def add-ops-spec
  {:model/args (fn [state]
                 [(gen/vector (gen/one-of [node-gen (request-gen state)]))])
   :model/precondition (fn [state [ops]]
                         (let [all-nodes (->> ops
                                              (filter (comp #{:node} :type))
                                              (map :id)
                                              (into state))
                               requests (->> ops
                                             (filter (comp #{:request} :type))
                                             (map :id))]
                           (every? all-nodes requests)))
   :real/command (fn [ops]
                   (doseq [node (filter (comp #{:node} :type) ops)]
                     (swap! nodes conj (:id node)))
                   (doseq [request (filter (comp #{:request} :type) ops)]
                     (assert (get @nodes (:id request)))))
   :next-state (fn [state [ops] _]
                 (->> ops
                      (filter (comp #{:node} :type))
                      (map :id)
                      (into state)))})

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

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