tla-edn.spec

Liking cljdoc? Tell your friends :D

Clojure only.

-main
classes-loaded?
classes-to-be-loaded
compile-operators
defop
get-class-non-final-static-fields
run
run-spec
try-to-reset-tlc-state!

-main^clj

(-main model-path cfg-path tlc-result-handler-str namespaces-str cli-opts-str)

classes-loaded?^clj

(classes-loaded?)

classes-to-be-loaded^clj

compile-operators^clj

(compile-operators ns)

ns is a symbol (e.g 'my-ns.core). Does not compile if all classes are already loaded.

`ns` is a symbol (e.g 'my-ns.core).
Does not compile if all classes are already loaded.

raw docstring

defop^cljmacro

(defop
  name
  {:keys [:module :identifier :warn :prefix] :or {warn true prefix ""} :as opts}
  doc-string?
  attr-map?
  [params*]
  prepost-map?
  body)

Generates a class and a function which should be used to override a TLA+ operator.

Generates a class and a function which should be used to override
a TLA+ operator.

raw docstring

get-class-non-final-static-fields^clj

(get-class-non-final-static-fields klass)

run^clj

(run model-path cfg-path)

(run model-path cfg-path cli-opts)

(run model-path
     cfg-path
     cli-opts
     {:keys [:tlc-result-handler :complete-response? :loaded-classes :raw-args]
      :or {loaded-classes (vals (clojure.core/deref classes-to-be-loaded))}})

Like run-spec, but starts a new JVM and runs TLC from there. If you use it, :tlc-result-handler should be a var of a function which receives one argument.

Like `run-spec`, but starts a new JVM and runs TLC from there.
If you use it, `:tlc-result-handler` should be a var of a function which
receives one argument.

raw docstring

run-spec^clj

(run-spec model-path cfg-path)

(run-spec model-path cfg-path cli-opts)

(run-spec model-path cfg-path cli-opts {:keys [:run?] :or {run? true}})

try-to-reset-tlc-state!^clj

(try-to-reset-tlc-state!)

We try to reset TLC to a good state here, certainly it will not work for all (or even most) cases. If you run same things twice and they behaviour differently, you have to track down in TLC which static field is the corrupt.

We try to reset TLC to a good state here, certainly it will not work for all
(or even most) cases. If you run same things twice and they behaviour differently,
you have to track down in TLC which static field is the corrupt.

raw docstring