Umaudemc

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.

All changes in this release are related to the statistical model-checking command `scheck`:

* Parametric queries à la [MultiVeSta](https://github.com/andrea-vandin/MultiVeStA) are supported in QuaTEx formulae. They are written `eval parametric(E[expr], name, start, step, stop)` where `expr` is a QuaTEx expression containing the variable `name`. It will be evaluated in every point `start + k * step` that is lower or equal to `stop`.
* New option `--plot` to plot the confidence intervals obtained from parametric queries using [Matplotlib](https://matplotlib.org/) (which should be installed for this option).
* QuaTEx expressions containing the logical operators `&&` and `||` are now supported.
* Fixed a bug in the execution of simultaneous queries that may produce wrong results.
* Fixed a bug in the parser of QuaTEx expressions that did not allow consecutive line comments.
* Fixed some ungraceful-termination bugs when the given assignment method argument is not valid or the input file contains no queries.

* Fixed a bug in the `strategy` assignment method related to states where both a strategy solution and a rewrite are possible.
* Fixed a bug in the `scheck` command where integer observations under the `pmaude` assignment method were not properly handled.
* Fixed a bug in the `prism` and `storm` backends that cause them to fail when an atomic proposition contains characters that are not admitted within PRISM labels.

* New command `scheck` for statistical model checking using the Quantitative Temporal Expressions (QuaTEx) query language of the [Vesta](https://doi.org/10.1109/QEST.2005.42) tool family. Probabilities can be expressed using the same methods supported by the probabilistic model-checking command `pcheck` (with some natural exceptions and additions) and the separate tool [`mvmaude`](https://github.com/fadoss/multivesta-maude) based on [MultiVeSta](https://doi.org/10.4108/icst.valuetools.2013.254377). There is a new assignment method `pmaude` for operating with [PMaude](https://doi.org/10.1016/j.entcs.2005.10.040) specifications.
* [JANI](https://jani-spec.org/) models can be obtained from probabilistic specifications by passing the `--format jani` option to `umaudemc graph`.
* [Spin](https://spinroot.com/) has been added as another qualitative model-checking backend for LTL. Notice that the communication with Spin relies on writing a Promela file with the low-level description of the Kripke structure. Hence, this backend is likely less efficient and scalable than the others.

* Probabilistic model checking is now possible through the `umaudemc gui --web` interface.
* The wheel package now installs a command `umaudemc` for calling the tool as with `python -m umaudemc`.
* Other minor improvements.

* Raw formulae are rewritten the atomic propositions to acceptable PRISM labels.
* Features introduced in Python 3.9 are no longer used for compatibility with Python 3.7.