recife.core — pfeodrippe/recife 0.4.0

all-done? clj

(all-done? db)

checker clj

(checker identifier expr)

context-from-state clj

(context-from-state state)

defconstraint clj macro

(defconstraint name f)

definvariant clj macro

(definvariant name f)

defproc clj macro

(defproc name params steps)

Defines a process and its multiple instances (:procs).

name is a symbol for this var.

params is a map of: :procs - set of arbitrary idenfiers (keywords); :local - map with local variables, :pc is required.

:pc - initial step from the steps key (keyword).

steps is a map of keywords (or vector) to functions. Each of these functions receives one argument (db) which contains the global state (namespaced keywords) plus any local state (unamespaced keywords) merged. E.g. in the example below, the function of ::check-funds will have :amount available in it's input (besides all global state, which it uses only :account/alice).

The keys in steps also can be a vector with two elements, the first one is the step identifier (keyword) and the second is some non-deterministic source (Recife model checker checks all the possibilities), e.g. if we want to model a failure, we can have [::read {:notify-failure? #{true false}}] instead of only ::read, :notify-failure will be assoc'ed to into db of the associated function.

;; Example (r/defproc wire {:procs #{:x :y} :local {:amount (r/one-of (range 5)) :pc ::check-funds}} {::check-funds (fn [{:keys [:amount :account/alice] :as db}] (if (< amount alice) (r/goto db ::withdraw) (r/done db)))

::withdraw (fn [db] (-> db (update :account/alice - (:amount db)) (r/goto ::deposit)))

::deposit (fn [db] (-> db (update :account/bob + (:amount db)) r/done))})

defproperty clj macro

(defproperty name expr)

done clj

(done db)

EdnStateWriter clj

FileStateWriter clj

goto clj

(goto db identifier)

implies clj macro

(implies condition & body)

Like when, but it returns true if condition is falsy.

invariant clj

(invariant identifier expr)

one-of clj

(one-of values)

(one-of identifier values)

Tells Recife to choose one of the values as its initial value.

operator-local clj multimethod

Used for helper functions (e.g. to help with non-determinism). Instead of creating a new operator, we create a unique one, recife-operator-local, and dispatch it based on :step and :key fields.

print-timeline-diff clj

(print-timeline-diff result-map)

process-config-operator clj

(process-config-operator f main-var-tla)

process-operator clj

(process-operator identifier f self-tla extra-args-tla main-var-tla)

random-traces-from-states clj

(random-traces-from-states states)

(random-traces-from-states states max-number-of-paths)

recife_operator_local clj

(recife_operator_local self params main-var)

recorder-info clj

reg clj

(reg identifier expr)

(reg identifier opts expr)

run-model clj

(run-model init-global-state components)

(run-model init-global-state components opts)

simulate clj multimethod

state-constraint clj

(state-constraint identifier expr)

states-from-result clj

(states-from-result {:keys [:recife/transit-states-file-path]})

temporal-property clj

(temporal-property identifier expr)

timeline-diff clj

(timeline-diff result-map)

tla clj

(tla identifier expr)

tlc clj

tlc-result-handler clj

(tlc-result-handler tlc-runner)

This function is a implementation detail, you should not use it. It handles the TLC object and its result, generating the output we see when calling run-model.

tlc-result-printer-handler clj

(tlc-result-printer-handler tlc-runner)