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 thepcheck
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 thegraph
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 thestrategy
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 thestrategy
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
, thestrategy
assignment method has been renamed tostrategy-fast
andstrategy-full
has been renamed tostrategy
. Warnings are now printed bystrategy-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 prependingctmc-
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 observationtime
now returns the elapsed time as calculated for a CTMC (regardless of whetherctmc-
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 observationsteps
, and it is also maintained for thestep
andstrategy
methods. - Weight annotations for the probability assignment method
metadata
can now be terms of sortNat
orFloat
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)
whereexpr
is a QuaTEx expression containing the variablename
. It will be evaluated in every pointstart + k * step
that is lower or equal tostop
. - 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 commandpcheck
(with some natural exceptions and additions) and the separate toolmvmaude
based on MultiVeSta. There is a new assignment methodpmaude
for operating with PMaude specifications. - JANI models can be obtained from probabilistic specifications by passing the
--format jani
option toumaudemc 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 thepmaude
assignment method were not properly handled. - Fixed a bug in the
prism
andstorm
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 withpython -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 variablesUMAUDEMC_BACKEND
andUMAUDEMC_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 usingngprism
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.
Bug fixes in 0.7.2
- 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.
Changes introduced in 0.6
- New probability assignment method
strategy
for thepcheck
command using the probabilistic extension of the Maude strategy language (mainly thechoice
operator, since sampling continuous distributions withsample
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 as an alternative backend for probabilistic model checking.
- Removed artificial restrictions on the format of terms passed to the
term
assignment method ofpcheck
(an arbitrary term is allowed, not only a function call) and thereward
argument (any variable name is allowed, not onlyS
). - Fixed a bug in the translation of CTL and CTL* formulae for the Kleene star semantics of the iteration (in 0.6.1).
Changes introduced in 0.5
- New experimental command
pcheck
for probabilistic model checking. LTL, CTL, and PCTL formulae can be expressed in an extension of the syntax of the defaultLTL
module where bounded temporal operators are admitted like<> <= n
orU > n
. Probabilities are distributed among the successors of a state according to a method specified with the--assign
option. The default one isuniform
, but others are available such asuaction
where actions can be assigned weights or probabilities,metadata
where weights are read from the metadata attribute of rules and strategies, andterm
to obtain weights by reducing a Maude function of numerical range. All these methods exceptuaction
can be prefixed withmdp-
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 model checker. - Fixed the printing of an unwanted debugging message when using
--kleene-iteration
.
Bug fixes in 0.5.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.
Changes introduced in 0.4
- 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.
Changes introduced in 0.3
- 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.
Changes introduced in 0.2
- Other programs can use the model checkers and other auxiliary functions through an API.
- Model-checking jobs can be safely cancelled in the graphical interfaces.
- Alternative graphical interface based on Gtk.
- All the backends calculate and show the number of rewrites executed for their model-checking jobs, and the number of states of the Büchi automaton is shown when using Maude (in addition to LTSmin).
- Other bug fixes.