Umaudemc

* Fixed a bug that causes an internal error when the observation of a QuaTEx expression is a constant.
* Fixed a bug in the parallel statistical simulator that affects macOS and Windows due to a different default behavior of the [`multiprocessing`](https://docs.python.org/3/library/multiprocessing.html#contexts-and-start-methods) package.

* The model checker for the Kleene-star semantics of the iteration (`--kleene-iteration` flag) now uses the more efficient builtin implementation of the strategy language introduced for the `pcheck` command when using Spot as backend. Opaque strategies are not supported yet, and the previous implementation is still used for other backends.
* New option `--kleene-iteration` to the `graph` command. It prints the graph used in the Kleene-aware model checker, where edges starting or terminating an iteration are annotated with an opaque identifier of the iteration.
* Fixed a bug in the `graph` command when printing probabilistic strategy-controlled graphs.
* The number of rewrites printed by `pcheck` with the `strategy` assignment method is more accurate.
* The web-based interface does no longer depend on the deprecated `cgi` module.
* The unmaintained GTK-based interface has been replaced by a thin wrapper around the web-based interface. Its only advantage is that a more confortable native file chooser is used for selecting Maude files. It requires GTK 4 and WebKitGTK 6.
* Removed backward compatibility code for very old versions of the `maude` Python library.

* Fixed a bug in the translation from QuaTEx to Python.
* Fixed a bug in the web interface when the result of a query is infinity.
* Test specifications in TOML are also admitted for Python ≥ 3.11.
* Switching to PEP 621 build system (pyproject.toml).

<details>
<summary><b>Changes in previous versions</b></summary>

* In `scheck`, the `strategy` assignment method has been renamed to `strategy-fast` and `strategy-full` has been renamed to `strategy`. Warnings are now printed by `strategy-fast` when local unquantified nondeterminism or conditional expressions are detected. However, conditional expressions whose conditions only contain tests can now safely used.

* The connection with the probabilistic model checker Storm now uses its Python bindings [StormPy](https://moves-rwth.github.io/stormpy/) if available. Otherwise, it falls back to the previous command-line communication.
* Weight annotations for `metadata` assignment method can now be terms depending on the matching substitution also in strategy-controlled models.
* The `graph` command can now show transition labels for models whose probabilities/rates have been assigned with the `strategy` method (it was the only case were edge labels were not printed).
* New method `MaudeModel.scheck` in the Python API for statistical model checking.
* Bug fixes related to the normalization of probabilities under the `strategy` method.

All changes are related to the probabilistic and statistical model-checking commands `pcheck` and `scheck`:

* Support for the new `matchrew with weight` operator of the probabilistic Maude strategy language.
* Support for checking continuous-time Markov chains (CTMC) in the `pcheck` command by prepending `ctmc-` to the existing probability assignment methods. Weights obtained by these methods are interpreted as firing rates instead of unnormalized probabilities (the only practical difference with respect to DTMC is the measurement of time).
* In the `scheck` command, the special observation `time` now returns the elapsed time as calculated for a CTMC (regardless of whether `ctmc-` is prepended to the assignment method name or not). The previous behavior, i.e. obtaining the number of rewrites, can be achieved with the special observation `steps`, and it is also maintained for the `step` and `strategy` methods.
* Weight annotations for the probability assignment method `metadata` can now be terms of sort `Nat` or `Float` on the variables of the matching substitution, in addition to numeric literals. For the moment, this does not work for strategy-controlled models.
* QuaTEx expressions containing the logical negation operator `!` are now supported.