Latest release

The umaudemc file is a compressed bundle that can be run as an executable ./umaudemc in Linux and macOS, or with the python command as PYTHON_PATH=umaudemc python -m umaudemc.

Otherwise, the package can be installed through PyPI with pip install umaudemc or using the attached wheel with pip install umaudemc-0.13.1-py3-none-any.whl. (Outdated) Docker images are also available at ghcr.io/fadoss/umaudemc with tags latest for classical and qmaude for quantitative model checking.

Changes introduced in 0.13

• 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.

Bug fixes in 0.13.1

• 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 package.

Changes introduced in 0.12

• The connection with the probabilistic model checker Storm now uses its Python bindings 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.

Minor improvements in 0.12.1

• 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.

Bug fixes and minor improvements in 0.12.2

• 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).

Changes in previous versions

Changes introduced in 0.11

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.

Changes introduced in 0.10

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

• Parametric queries à la 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 (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.

Changes introduced in 0.9

• New command scheck for statistical model checking using the Quantitative Temporal Expressions (QuaTEx) query language of the Vesta 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 based on MultiVeSta. There is a new assignment method pmaude for operating with PMaude specifications.
• JANI models can be obtained from probabilistic specifications by passing the --format jani option to umaudemc graph.
• Spin 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.

Bug fixes and minor improvements in 0.9.1

• 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.

Changes introduced in 0.8

• 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.

Changes introduced in 0.7

• 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.

Bug fixes and minor improvements in 0.7.1

• 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...