tla-edn.spec — io.github.pfeodrippe/tladeps-edn-module 0.4.0

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

defop clj macro

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

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 the var of a function which receives one argument.

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.