Umaudemc

* In the `pcheck` command, steady-state and transient probabilities can be calculated by writing `steady` or `transient(n)` instead of the temporal formula.
* The probability specification of the `--assign` argument can be loaded from file by passing `` followed by a file name to it.
* In the `graph` command, PRISM files can be exported with `--format prism`. The probability specification should be passed with the `--passign` option, and every atomic proposition passed to `--aprops` will be evaluated in the graph and set as a label, like for NuSMV output.
* Probabilistic models can also be exported in DOT format, where edges will be annotated with their corresponding probabilities.
* Edges labels may include the line number of the statement that causes the transition by using the template `%n` in the format string of the `--elabel` argument.
* The list of standard and probabilistic backends of the `--backend` option can be specified with the environment variables `UMAUDEMC_BACKEND` and `UMAUDEMC_PBACKEND`, respectively. The command-line option takes precedence over the environment variables.
* Some test cases have been included in the repository, and several minor bugs have been fixed.

* New probability assignment method `strategy` for the `pcheck` command using the probabilistic extension of the Maude strategy language (mainly the `choice` operator, since sampling continuous distributions with `sample` is not compatible with deriving discrete probabilistic models). The probabilistic strategy must be free of nondeterminism (to derive discrete-time Markov chains) or at least avoid nondeterminism between a quantified choice and a rewrite (to derive Markov decision processes).
* Added [Storm](https://www.stormchecker.org/) as an alternative backend for probabilistic model checking.
* Removed artificial restrictions on the format of terms passed to the `term` assignment method of `pcheck` (an arbitrary term is allowed, not only a function call) and the `reward` argument (any variable name is allowed, not only `S`).
* Fixed a bug in the translation of CTL and CTL* formulae for the Kleene star semantics of the iteration (in 0.6.1).

* Reading counterexamples from Maude led to crashes when using the `maude` library in its 0.7 version.
* `matchrew`s were not properly handled by the Kleene-star iteration semantics.

* New experimental command `pcheck` for probabilistic model checking. LTL, CTL, and PCTL formulae can be expressed in an extension of the syntax of the default `LTL` module where bounded temporal operators are admitted like `<> <= n` or `U > n`. Probabilities are distributed among the successors of a state according to a method specified with the `--assign` option. The default one is `uniform`, but others are available such as `uaction` where actions can be assigned weights or probabilities, `metadata` where weights are read from the metadata attribute of rules and strategies, and `term` to obtain weights by reducing a Maude function of numerical range. All these methods except `uaction` can be prefixed with `mdp-` to generate a Markov decision process, where actions (rule labels) are selected nondeterministically. By default, the result of the command is the probability that the given formulae is satisfied (or the minimum and maximum ones for MDPs), but the `--steps` and `--reward` attributes can be used to get the expected value of the number of steps or of a user-defined reward function on states. Currently, all features are directly supported by the [PRISM](https://www.prismmodelchecker.org/) model checker.
* Fixed the printing of an unwanted debugging message when using `--kleene-iteration`.

* Opaque strategy labels can be used as actions in μ-calculus formulae, as `opaque(`*name*`)` or directly as *name* if there is no homonym rule.
* Support for model checking against the Kleene-star semantics of the iteration strategy is extended to the other backends by transforming the LTL, CTL and CTL* formulae. However, branching-time properties of relatively small size may become too complex for an efficient verification.
* Improvements in the `test` subcommand that now measures the number of rewrites, the length of the counterexamples, the preparation time and the memory usage. Moreover, executions can be resumed from which they were interrupted and tests be bounded by a timeout.
* Fixed a bug that misdetects the logic of the formulae whose only temporal operator is `O` (next).
* Fixed a bug that produces wrong results when model checking under the Kleene-star semantics.
* Colors are disabled when the standard output is a file.
* Other minor bugs fixed.

* Recursive algorithms have been transformed to iterative ones due to the limited Python recursion.
* Spot has been added as a new model-checking backend for LTL properties.
* Initial support for checking LTL properties under the semantics of the strategy language whose iteration coincides with the Kleene star. It uses Streett automata from the Spot library.
* Improvements in the test and benchmarking subcommand with support for nested problem specifications, parameters, multiple executions, etc.
* The API is extended with a function to print graphs.
* Bug fixes and code cleanup.