A small library to write TLA+ (TLC) Operators and to convert TLA+ values to/from EDN data.
Add the following dependency to your project.clj
file
It's not ready for production (and maybe never will), but you should use it only for testing anyway.
Check an example here.
Let's say you have one TLA+ operator called Inc
which you would like to
override using Clojure.
(* module "Incrementer", this name is important as it will be referenced later *)
Inc(n) == n + 1
The required steps are the following, you create a overriding operator
with defoperator
. Please, add the folder classes
to your project file
classpath (project.clj or deps.edn or boot.clj).
(ns my-ns.core
(:require
[tla-edn.core :as tla-edn]
[tla-edn.spec :as spec]))
(spec/defop Inc {:module "Incrementer"}
[x]
(-> (tla-edn/to-edn x)
inc
tla-edn/to-tla-value))
defop
makes use of gen-class
, so at first time you run it, the operators
will be compiled, then any change is automatically loaded when run again.
(defn -main
[]
;; this will run the TLA+ spec with its config file
(spec/run-spec "path/to/Incrementer.tla" "Incrementer.cfg")
(System/exit 0))
Then from the terminal
;; assuming you are using `deps.edn`
$ clj -A:test -m my-ns.core # this will compile (just at first time)
# OK
$ clj -A:test -m my-ns.core
# TLA+ output (it will run the spec with the overrides, hopefully)
(require '[tla-edn.core :as tla-edn])
;; converting from edn to TLA+ values
(str
(tla-edn/to-tla-value [{:a 3}
2
#{"look" '(1 2)}
[[#{{"b" {:c #{6 4 5}}}}]]]))
;; => "<<[a |-> 3], 2, {<<1, 2>>, \"look\"}, <<<<{[b |-> [c |-> {4, 5, 6}]]}>>>>>>"
;; converting from TLA+ values to edn (metadata is created so you can refer to the original TLA type)
(import '(tlc2.value.impl Value IntValue RecordValue BoolValue FcnRcdValue
StringValue TupleValue SetEnumValue BoolValue)
'(util UniqueString))
(let [tla-value (RecordValue.
(into-array UniqueString [(UniqueString/uniqueStringOf "eita")])
(into-array Value
[(TupleValue. (into-array Value [(IntValue/gen 4)
(IntValue/gen 100)]))])
false)]
(binding [*print-meta* true]
(prn (tla-edn/to-edn tla-value))))
;; => ^{:tla-plus-type tlc2.value.impl.RecordValue}
;; {"eita" ^{:tla-plus-type tlc2.value.impl.TupleValue}
;; (4 100)}
You can extend the protocol tla_edn.core.TLAPlusEdn
for conversion to edn
data.
;; example of extension
(extend-protocol TLAPlusEdn
tlc2.value.impl.BoolValue
(to-edn [v]
(.getVal v)))
You can create a defmethod
for tla-edn.core/to-tla-value
for conversion
from edn data.
;; example of dispatch using defmethod for tla-edn
(defmethod to-tla-value Boolean
[v]
(BoolValue. v))
The people working at https://github.com/tlaplus/tlaplus =D