test.carly.core — mvxcvi/test.carly 0.4.1

Suite of tests to verify that a given system implementation conforms to the spec during a sequence of operations performed on it.

check-system clj

(check-system message
              iteration-opts
              init-system
              ctx->op-gens
              &
              {:keys [context-gen init-model finalize! concurrency repetitions
                      search-threads]
               :or {context-gen (gen/return {})
                    init-model (constantly {})
                    concurrency 4
                    repetitions 5
                    search-threads (. (Runtime/getRuntime) availableProcessors)}
               :as opts})

Uses generative tests to validate the behavior of a system under a linear sequence of operations.

Takes a test message, a single-argument constructor function which takes the context and produces a new system for testing, and a function which will return a vector of operation generators when called with the test context. The remaining options control the behavior of the tests:

• :context-gen Generator for the operation test context.
• :init-model Function which returns a fresh model when called with the context.
• finalize! Called with the system after running all operations. This function may contain additional test assertions and should clean up any resources by stopping the system.
• concurrency Maximum number of operation threads to run in parallel.
• repetitions Number of times to run per generation to ensure repeatability.
• search-threads Number of threads to run to search for valid worldlines.
• report Options to override the default report configuration.

defop clj macro

(defop op-name attr-vec & forms)

Defines a new specification for a system operation test.

gen->Wait clj

(gen->Wait _)

Constructs a Wait operation generator.