Umaudemc

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.

* In the `pcheck` command, `--fraction` or `-f` can be used to show approximate fractions instead of floating-point numbers for probabilities and expected values.
* `PRISM_PATH` may point to a file instead of a directory to select the PRISM executable. This allows using `ngprism` for avoiding the initialization overhead of the Java virtual machine. For consistency, `STORM_PATH` can also point to a file.
* Fixed a bug in the parsing of steady-state probabilities from Storm, whose internal identifiers may not coincide with the state variables of the model.
* Fixed a bug in the implementation of the `strategy` assignment method that misses some execution cycles inside conditional expressions.
* Fixed some bugs in the Python API.