It is convenient to program symbolic code using mathematics (TLA+). Multi-line Python strings and str.format are excellent for this job. For development, this works well. For stable code deployment, it is slow. Calling the parser and bitblaster takes long time compared to lightweight to medium size BDD operations (that don't last minutes). The delay becomes especially noticeable for TLA+ expressions that appear inside tight loops, and profiling showed that it dominates runtime.
The manual approach that addresses this problem is to simply write code calling directly functions that operate on BDDs, instead of a TLA+ string. Automate this conversion, so that it never need to happen in user code. This can be done by compiling TLA+ to Python code objects and using a decorator to memoize them. A similar approach was used in tulip.spec.form.GRSpec.compile_init.
A more traditional approach would be to translate the Python module and replace such strings by the equivalent Python code, but it introduces an inconvenient extra step and requires syntactically recognizing the strings to replace, which isn't a clearly defined problem (it is implicit). The proposed approach is explicit, and easier to implement.
It is convenient to program symbolic code using mathematics (TLA+). Multi-line Python strings and
str.formatare excellent for this job. For development, this works well. For stable code deployment, it is slow. Calling the parser and bitblaster takes long time compared to lightweight to medium size BDD operations (that don't last minutes). The delay becomes especially noticeable for TLA+ expressions that appear inside tight loops, and profiling showed that it dominates runtime.The manual approach that addresses this problem is to simply write code calling directly functions that operate on BDDs, instead of a TLA+ string. Automate this conversion, so that it never need to happen in user code. This can be done by compiling TLA+ to Python
codeobjects and using a decorator to memoize them. A similar approach was used intulip.spec.form.GRSpec.compile_init.A more traditional approach would be to translate the Python module and replace such strings by the equivalent Python code, but it introduces an inconvenient extra step and requires syntactically recognizing the strings to replace, which isn't a clearly defined problem (it is implicit). The proposed approach is explicit, and easier to implement.