Ioannis Filippidis

This error is due to a syntax error in https://github.com/tlaplus/Examples/blob/fbdf8db1b52ea932b16c52e79fbfb516158291e3/specifications/ewd840/EWD840_proof.tla#L41-L42. SANY raises for `EWD840_proof.tla` (paths of modules adjusted in the below messages): ``` ****** SANY2 Version 2.1 created 24 February...

It might also be relevant to list `"3.10"` in the [section "Specifying Python versions"](https://docs.travis-ci.com/user/languages/python/#specifying-python-versions).

If reordering to given variable levels, `bdd.configure(reordering=False)` is needed, so that the variables are shifted to the given levels, without using automated reordering. The following works without errors: ```py bdd.configure(reordering=False)...

May I ask, just to make sure, if implemented in the other touchpad driver that already exists in the kernel, the driver would support both usb and bluetooth (not only...

Calling `dd.cudd.BDD.apply()` calls `Cudd_bddXor()`, `dd.cudd.BDD.add_expr()` also calls the parser.

As of `dd == 0.6.0`: ```sh pip install --upgrade wheel cython export DD_FETCH=1 DD_CUDD=1 pip install dd -vvv --use-pep517 --no-build-isolation ```

The modules `dd.cudd` and `download.py` are written to build on Linux. Building on Windows would need configuring the build differently, relevant: #68 and https://github.com/tulip-control/dd/issues/78#issuecomment-843647033.

The operator `EnabledWrapper` is defined in the module `TLAPS.tla`, and used in `src/expr/e_action.ml`, in an intermediate representation. Maybe the module `TLAPS` is not found?

Not sure about PPXs. It may be simpler to have an implementation as a function.

I will try to rebase the changes. The prefix "ENH" stands for "enhancement" (in the sense of a new feature), and is among acronyms listed in `numpy`'s documentation .