API reference

The umaudemc.api package allows accessing part of the functionality of the umaudemc tool programmatically through the MaudeModel class.

class umaudemc.api.MaudeModel(initial, strategy=None, filename=None, module=None, metamodule=None, opaque=(), biased_matchrew=True, already_loaded=False, single_use=False)

Model of a Maude (strategy-controlled) rewriting system

check(formula, purge_fails='default', merge_states='default', backends=('maude', 'ltsmin', 'pymc', 'nusmv', 'spot', 'spin', 'builtin'), formula_str=None, logic=None, depth=-1, timeout=None, usermsgs=<module 'umaudemc.usermsgs' from '/home/portatil/Documentos/universidad/inves/software/umaudemc/umaudemc/usermsgs.py'>, extra_args=())

Model check a given temporal formula.

Parameters:

  • formula (str or list or maude.Term) – Formula

  • purge_fails (bool or str) – Whether failed states must be purged (by default, this value is selected depending on the logic)

  • merge_states (str) – Whether successors with a common term should be merged (edge, value or none, by default selected depending on the logic)

  • backends (str or list of str) – Prioritized list of model checking backends to be used

  • formula_str (str or None) – Formula given a string (in case formula is a list)

  • logic (str) – Logic (in case formula is a list)

  • depth (int) – Depth bound on the rewriting graph (only works for some backends)

  • timeout (int or None) – Timeout for the model-checking task (only works for some backends)

  • usermsgs (An object with print_error, print_warning and print_info methods) – Partially override default user message printing functions

  • extra_args (list of str) – Additional arguments to be passed to the backend

Returns:

the model-checking result and a dictionary with statistics

format_statistics(stats)

Format the statistics produced by the model checkers

Parameters:

stats (dict) – Statistics produced by the check method

Returns:

a formatted text with statistics

Return type:

str

pcheck(formula, purge_fails='default', merge_states='default', backends=('prism', 'storm'), timeout=None, usermsgs=<module 'umaudemc.usermsgs' from '/home/portatil/Documentos/universidad/inves/software/umaudemc/umaudemc/usermsgs.py'>, extra_args=(), assign='uniform', steps=False, reward=None)

Probabilistic model checking of a given temporal formula.

Parameters:

  • formula (str) – Formula

  • purge_fails (bool or str) – Whether failed states must be purged (by default, this value is selected depending on the logic)

  • merge_states (str) – Whether successors with a common term should be merged (edge, value or none, by default selected depending on the logic)

  • backends (str or list of str) – Prioritized list of model checking backends to be used

  • timeout (int or None) – Timeout for the model-checking task

  • usermsgs (An object with print_error, print_warning and print_info methods) – Partially override default user message printing functions

  • extra_args (list of str) – Additional arguments to be passed to the backend

  • assign (string) – Probability assignment method

  • steps (bool) – Whether the expected number of steps should be calculated

  • reward (str or maude.Term or None) – Reward term to calculate its expected value

Returns:

the probabilistic model-checking result and a dictionary with statistics

print_counterexample(stats, printer=None, sformat=None, eformat=None)

Pretty print a counterexample for a previous check (nothing is printed if no counterexample has been found)

Parameters:

  • stats (dict) – Statistics produced by the check method

  • printer (a counterexample printer or None) – Printer for the counterexample

  • sformat (str or function or None) – State formatter or format string

  • eformat (str or function or None) – Edge formatter or format string

Return type:

str

print_graph(outfile=<_io.TextIOWrapper name='<stdout>' mode='w' encoding='utf-8'>, sformat=None, eformat=None, depth=-1)

Print a graph for this model.

Parameters:

  • outfile (text stream) – Text stream where to write the graph (by default, the standard output)

  • sformat (str or function or None) – State formatter or format string

  • eformat (str or function or None) – Edge formatter or format string

  • depth (int) – Depth bound for the graph generation

scheck(quatex, assign='uniform', alpha=0.05, delta=0.5, block=30, nsims=(30, None), seed=None, jobs=1, usermsgs=<module 'umaudemc.usermsgs' from '/home/portatil/Documentos/universidad/inves/software/umaudemc/umaudemc/usermsgs.py'>, verbose=False, constants=None)

Statistical model checking of a given QuaTEx expression

Parameters:

  • quatex (str or text file object) – Quantitative temporal expression (file name or file object)

  • assign (string) – Probability assignment method

  • alpha (float (between 0.0 and 1.0)) – Complement of the confidence level (probability outside the confidence interval)

  • delta (float (positive)) – Maximum admissible radius for the confidence interval

  • block (int (positive)) – Number of simulations before checking the confidence interval

  • nsims ((int or None, int or None)) – Number of simulations (tuple of lower and upper limits)

  • seed (int) – Random seed

  • usermsgs (An object with print_error, print_warning and print_info methods) – Partially override default user message printing functions

  • verbose (bool) – Enable verbose messages about the simulation state between blocks

  • constants (dict[str, float]) – Constants to be used in the QuaTEx expression

Returns:

the probabilistic model-checking result and a dictionary with statistics