knossos.model
A model specifies the behavior of a singlethreaded datatype, transitioning from one state to another given an operation.
A model specifies the behavior of a singlethreaded datatype, transitioning from one state to another given an operation.
cas-registerclj
(cas-register)(cas-register value)A compare-and-set register
A compare-and-set register
inconsistentclj
(inconsistent msg)Represents an invalid termination of a model; e.g. that an operation could not have taken place.
Represents an invalid termination of a model; e.g. that an operation could not have taken place.
inconsistent?clj
(inconsistent? model)Is a model inconsistent?
Is a model inconsistent?
multi-registerclj
(multi-register values)A register supporting read and write transactions over registers identified by keys. Takes a map of initial keys to values. Supports a single :f for ops, :txn, whose value is a transaction: a sequence of [f k v] tuples, where :f is :read or :write, k is a key, and v is a value. Nil reads are always legal.
A register supporting read and write transactions over registers identified by keys. Takes a map of initial keys to values. Supports a single :f for ops, :txn, whose value is a transaction: a sequence of [f k v] tuples, where :f is :read or :write, k is a key, and v is a value. Nil reads are always legal.
mutexclj
(mutex)A single mutex responding to :acquire and :release messages
A single mutex responding to :acquire and :release messages
noopclj
A model which always returns itself, unchanged.
A model which always returns itself, unchanged.
stepclj
(step model op)The job of a model is to validate that a sequence of operations applied to it is consistent. Each invocation of (step model op) returns a new state of the model, or, if the operation was inconsistent with the model's state, returns a (knossos/inconsistent msg). (reduce step model history) then validates that a particular history is valid, and returns the final state of the model.
Models should be a pure, deterministic function of their state and an operation's :f and :value.
The job of a model is to *validate* that a sequence of operations applied to it is consistent. Each invocation of (step model op) returns a new state of the model, or, if the operation was inconsistent with the model's state, returns a (knossos/inconsistent msg). (reduce step model history) then validates that a particular history is valid, and returns the final state of the model. Models should be a pure, deterministic function of their state and an operation's :f and :value.
cljdoc is a website building & hosting documentation for Clojure/Script libraries
× close