recife.core — pfeodrippe/recife 0.3.0

_COLON_recife___core_SLASH_show_example_invariant2 clj

(_COLON_recife___core_SLASH_show_example_invariant2 main-var)

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)

defproperty clj macro

(defproperty name expr)

done clj

(done db)

EdnStateWriter 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.

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)

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)

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)

tlc-result-printer-handler clj

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