Maude bindings documentation

The maude package allows manipulating terms, modules, and other entities of the Maude specification language as Python objects, whose methods expose the operations available as commands in the Maude interpreter. This documentation describes the Python bindings, but most of the API is available for other languages supported by SWIG. These bindings are based on the latest Maude release extended with a model checker for systems controlled by the Maude strategy language, which is accessible via the StrategyRewriteGraph.modelCheck() method.

See also

Maude 3.4 manual · Source code · Package at PyPI · Bindings for other languages

First steps

After loading the maude module, the first step should be calling the init() function to initialize Maude and load its prelude. Other modules can be loaded from file with the load() function or inserted verbatim with input(). Any loaded module can be obtained as a Module object with getModule() or getCurrentModule(), which allow parsing terms with their parseTerm() method. The usual Maude commands are represented as homonym methods of the Term class, except unify(), variant_unify() and variant_match() that belong to the Module class.

import maude
maude.init()
m = maude.getModule('NAT')
t = m.parseTerm('2 * 3')
t.reduce()
print(t)

For example, the snippet above parses the term 2 * 3 in the NAT module (defined in the Maude prelude) and reduces it equationally. The result 6 is printed to the standard output.

Note

Loading the package attaches a single session of Maude to the Python process that cannot be refreshed or unloaded. Finer control on the session lifetime and multiple simultaneous instances can be achieved using the multiprocessing module.

maude.downModule(term)

Get a module object from its metarepresentation in this module, which must include the META-LEVEL module.

Parameters:

term (Term) – The metarepresentation of a module, that is, a valid element of the Module sort in META-MODULE. The term will be reduced.

Return type:

VisibleModule

Returns:

The module object or null if the given term was not a valid module metarepresentation.

maude.getCurrentModule()

Get the current module (the last module inserted or explicitly selected, like in the Maude interpreter).

maude.getModule(name)

Get a module or theory by name.

Parameters:

name (string) – Name of the module or theory (module expressions are not allowed).

maude.getModules()

Get the list of loaded modules.

Return type:

list of ModuleHeader

Returns:

A list of module headers (this may change).

maude.getView(name)

Get a view by name.

Parameters:

name (string) – Name of the view (view expressions are not allowed).

maude.getViews()

Get the list of loaded views.

maude.init(loadPrelude=True, randomSeed=0, advise=True, handleInterrupts=False)

Init Maude.

This function must be called before anything else.

Parameters:

  • loadPrelude (boolean, optional) – Whether the Maude prelude should be loaded.

  • randomSeed (int, optional) – Seed for the pseudorandom number generator in the RANDOM module.

  • advise (boolean, optional) – Whether debug messages should be printed.

  • handleInterrupts (boolean, optional) – Whether interrupts are handled by Maude.

maude.input(text)

Process the given text as direct input to Maude.

Parameters:

text (string) – Maude modules or commands.

maude.load(name)

Load the file with the given name.

Parameters:

name (string) – The name of the file (absolute or relative to the current working directory or MAUDE_LIB).

maude.setAllowDir(flag)

Allow or disallow operations on directories from Maude code.

Parameters:

flag (boolean) – Whether directory access should be allowed.

maude.setAllowFiles(flag)

Allow or disallow operations on files from Maude code.

Parameters:

flag (boolean) – Whether file access should be allowed.

maude.setAllowProcesses(flag)

Allow or disallow running arbitrary executables from Maude code.

Parameters:

flag (boolean) – Whether process creation should be allowed.

maude.setAssocUnifDepth(m)

Set depth multiplier for associative unification.

Parameters:

seed – New depth multiplier (between 0 and 1e6).

maude.setRandomSeed(randomSeed)

Set the pseudorandom number generator seed.

Parameters:

seed – New pseudorandom number generator seed.

class maude.ModuleHeader

Module header information.

property name

Name of the module

property type

Type of the module (see Module class)

Terms

Term objects represent Maude terms in the context of a module. Their methods include observers (arguments(), equal(), …) and command-like operations (reduce(), rewrite(), …). Some of the latter are applied destructively, replacing the original term by the result, so a previous copy() may be required to preserve the original term if desired. Operations with multiple potential results return iterable objects over them.

Warning

Modules should be understood as closed compartments. In operations involving different terms, symbols or other module items, they must all belong to the same module. Mixing terms from different modules, even if related by inclusion, will not work.

class maude.Term(*args, **kwargs)

Maude term with its associated operations.

NO_CONDITION = Condition with 0 elements
apply(*args, **kwargs)

Apply any rule with the given label.

Parameters:

  • label (string) – Rule label (or null for any executable rule).

  • substitution (Substitution, optional) – Initial substitution that will be applied on the rule before matching.

  • minDepth (int, optional) – Minimum matching depth.

  • maxDepth (int, optional) – Maximum matching depth.

Return type:

RewriteSearchState

Returns:

An object to iterate through the rewritten terms.

arguments(normalize=True)

Iterate over the arguments of this term.

Parameters:

normalize (boolean, optional) – Whether to normalize before iterating over its arguments.

check()

Check an SMT formula.

Return type:

string

Returns:

A string, either sat, unsat or undecided.

copy()

Get a copy of this term.

equal(other)

Compare two terms for equality.

Parameters:

other (Term) – The second term to be compared.

erewrite(bound=-1, gas=-1)

Rewrite a term following the semantics of the erewrite command.

Parameters:

  • bound (int, optional) – An upper bound on the number of rule rewrites.

  • gas (int, optional) – An upper bound on the number of rule rewrites by position.

Return type:

(Term, int)

Returns:

The result and the total number of rewrites (the original term is not modified).

frewrite(bound=-1, gas=-1)

Rewrite a term following the semantics of the frewrite command.

Parameters:

  • bound (int, optional) – An upper bound on the number of rule rewrites.

  • gas (int, optional) – An upper bound on the number of rule rewrites per position.

Return type:

int

Returns:

The total number of rewrites.

getIterExponent()

Get the exponent of an iterable symbol or zero otherwise.

getSort()

Get the sort of this term.

getVarName()

Get the name of the variable if the current term is a variable or a null value otherwise.

get_variants(*args, **kwargs)

Compute the most general variants of this term.

Parameters:

  • irredundant (boolean, optional) – Whether to obtain irredundant variants (for theories with the finite variant property).

  • irreducible (list of Term, optional) – Irreducible terms constraint.

Return type:

VariantSearch

Returns:

An object to iterate through variants.

hash()

Get the hash value of the term.

isVariable()

Get whether the term is a variable.

leq(sort)

Check whether the sort of this term is a subtype of the given sort.

Parameters:

sort (Sort) – The pretended supertype.

match(*args, **kwargs)

Match this term into a given pattern.

Parameters:

  • pattern (Term) – Pattern term.

  • condition (Condition, optional) – Equational condition that solutions must satisfy.

  • withExtension (boolean, optional) – Whether the matching should be done with extension modulo axioms (deprecated, use maxDepth=0 instead).

  • minDepth (int, optional) – Minimum matching depth.

  • maxDepth (int, optional) – Maximum matching depth (-1 to match on top without extension, 0 to match on top with extension, UNBOUNDED to match anywhere, or any intermediate value).

Return type:

MatchSearchState

Returns:

An object to iterate through matches.

normalize(full=True)

Normalize this term modulo axioms.

Parameters:

full (boolean, optional) – Whether to normalize in depth.

prettyPrint(flags)

Pretty prints this term.

Parameters:

flags (int) – Flags that affect the term output.

reduce()

Reduce this term.

Return type:

int

Returns:

The total number of rewrites.

rewrite(bound=-1)

Rewrite a term following the semantics of the rewrite command.

Parameters:

bound (int, optional) – An upper bound on the number of rule rewrites.

Return type:

int

Returns:

The total number of rewrites.

search(type, target, strategy=None, condition=None, depth=-1)

Search states that match into a given pattern and satisfy a given condition by rewriting from this term.

Parameters:

  • type (int) – Type of search (number of steps).

  • target (Term) – Pattern term.

  • strategy (StrategyExpression, optional) – Strategy to control the search.

  • condition (Condition or sequence of condition fragments, optional) – Condition that solutions must satisfy.

  • depth (int, optional) – Depth bound

Return type:

either StrategySequenceSearch if a strategy is provided or RewriteSequenceSearch

Returns:

An object to iterate through matches.

srewrite(expr, depth=False)

Rewrite a term following a strategy.

Parameters:

  • expr (StrategyExpression) – A strategy expression.

  • depth (boolean, optional) – Whether to perform a depth-first search. By default, a fair search is used.

Return type:

StrategicSearch

Returns:

An object to iterate through strategy solutions.

symbol()

Get the top symbol of this term.

toFloat()

Get the floating-point number represented by the given term or zero otherwise.

toInt()

Get the integer number represented by the given term or zero otherwise.

toLatex()

Obtain the LaTeX representation of this term.

vu_narrow(type, target, depth=-1, fold=False, filter=False, delay=False)

Narrowing-based search of terms that unify with the given target.

Parameters:

  • type (int) – Type of the search (number of steps).

  • target (Term) – The pattern that has to be reached.

  • depth (int, optional) – Depth bound (-1 for unbounded).

  • fold (boolean, optional) – Whether to activate folding (fvu-narrow command).

  • filter (boolean, optional) – Whether to activate filtered variant unification (filter option in the command).

  • delay (boolean, optional) – Whether variant unifiers are filtered before using the first one for narrowing (delay option in the command).

Return type:

NarrowingSequenceSearch3

Returns:

An object to iterate through solutions.

class maude.Symbol(*args, **kwargs)

A Maude symbol (operator at the kind level).

arity()

Get the number of arguments.

domainKind(argNr)

Get the kind for the given argument.

Parameters:

argNr (int) – The argument index.

equal(other)

Check whether two symbols are the same.

getFormat()

Get the format attribute of the symbol.

Return type:

list of str

Returns:

The sequence of instruction words of the format specification, each of them a string.

getFrozen()

Get the frozen attribute of the symbol.

Return type:

list of int

Returns:

The sequence of indices in the frozen attribute, where arguments are numbered from 0 instead of 1.

getIdHooks()

Get the id-hooks of the special operator (or an empty sequence otherwise).

Return type:

list of lists of str

Returns:

A sequence of string sequences representing each an id-hook of the operator with its name followed by its arguments.

getIdentity()

Get the identity element for this symbol (if any).

getLineNumber()

Get the line number information for this item as formatted by Maude.

The format of the string is usually filename, line line (module) where the second line is the integral line number, and module is the module type and name where this item was originally defined. The filename may be an actual quoted filename or some special name between angle brackets.

getMetadata(index)

Get the metadata attribute of the given declaration of this symbol.

Parameters:

index (int) – Index of the operator declaration.

getOpDeclarations()

Get the declarations of the symbol.

getOpHooks()

Get the operator hooks of the symbol as a dictionary.

getPrec()

Get the syntactic precedence of the symbol.

getRangeSort()

Get the range sort of the symbol.

getStrategy()

Get the reduction strategy of the symbol.

getTermHooks()

Get the term hooks of the symbol as a dictionary.

hasAttr(attr)

Whether the symbol has the given attribute.

Parameters:

attr (int) – One of the OP_* constants for operator attributes.

hash()

Get the hash value of the symbol.

isAssoc()

Whether the symbol is associative.

Deprecated: use hasAttr(OP_ASSOC) instead.

makeTerm(args)

Build a term with this symbol and the given terms as arguments.

class maude.OpDeclaration

Syntactical operator declaration.

getDomainAndRange()

Get domain and range sorts (range is last).

isConstructor()

Is the declared operator marked as a data constructor?

class maude.Substitution(*args)

Substitution (mapping from variables to terms).

Substitution are iterable, and the iterator returns pairs with each variable and value of the mapping.

find(name, sort=None)

Find the value of a given variable by name.

Parameters:

  • name (string) – Variable name (without sort).

  • sort (Sort, optional) – Sort of the variable (optional).

Return type:

Term

Returns:

The value of the variable or null if not found. If the sort of the variable is not given, multiple results are possible.

instantiate(term)

Instantiate a term with this substitution.

Parameters:

term (Term) – The term to be instantiated.

Return type:

Term

Returns:

The instantiated term.

matchedPortion()

Get the matched portion when matching with extension.

Return type:

Term

Returns:

The matched portion or null if the whole term matched.

size()

Get the number of variables in the substitution.

value(variable)

Get the value of a given variable.

Parameters:

variable (Term) – The variable whose value is looked up.

Search iterators

The following classes can be used as usual Python iterators, albeit some offer additional methods.

class maude.StrategicSearch(*args, **kwargs)

An iterator through the solutions of a strategy search.

It iterates over (Term, int) pairs including the solution term and the number of rewrites until it has been reached.

class maude.MatchSearchState(*args, **kwargs)

An iterator through the matching a term into a pattern.

It iterates over (Substitution, function) pairs including the matching substitution and a function from Term to Term that returns the matching context filled with the given term.

fillContext(term)

Get the context of the match filled with the given term.

Parameters:

term (Term) – Term to fill the context.

Return type:

Term

Returns:

The original term with the matched subterm replaced by the given term.

class maude.RewriteSearchState(*args, **kwargs)

An iterator through rewriting solutions.

It iterates over (Term, Substitution, function, Rule) tuples including the resulting term, the matching substitution, a Term to Term function that provides the matching context filled with the given term, and the rule that has been applied.

fillContext(term)

Get the context of the match filled with the given term.

Parameters:

term (Term) – Term to fill the context.

Return type:

Term

Returns:

The original term with the matched subterm replaced by the given term.

getRule()

Get the applied rule.

getSubstitution()

Get the matching substitution.

class maude.RewriteSequenceSearch(*args, **kwargs)

An iterator through the solutions of a search.

It iterates over (Term, Substitution, function, int) tuples consisting of the solution term, the matching substitution, and the number of rewrites until it has been found. The third coordinate is a function that returns, when called without arguments, a path to the solution, as described in pathTo().

getRewriteCount()

Get the number of rewrites until this term has been found.

getRule(stateNr=-1)

Get the rule leading to the given state.

Parameters:

stateNr (int, optional) – The number of a state in the search graph or -1 for the current one.

getStateNr()

Get an internal state number that allows reconstructing the path to this term.

getStateParent(stateNr)

Get the parent state.

Parameters:

stateNr (int) – The number of a state in the search graph.

Return type:

int

Returns:

The number of the parent or -1 for the root.

getStateTerm(stateNr)

Get the term of a given state.

Parameters:

stateNr (int) – The number of a state in the search graph.

getSubstitution()

Get the matching substitution of the solution into the pattern.

pathTo(stateNr)

Get the path from the initial to the given state.

Parameters:

stateNr (int) – State index.

Return type:

list of Term and Rule

Returns:

A list interleaving terms and rules that connect them from the initial to the given state.

class maude.StrategySequenceSearch(*args, **kwargs)

An iterator through the solutions of a strategy-controlled search.

It iterates over (Term, Substitution, function, StrategyExpression, int) tuples consisting of the solution term, the matching substitution, the next strategy to be executed from the current term, and the number of rewrites until it has been found. The third coordinate is a function that returns, when called without arguments, a path to the solution, as described in pathTo().

getRewriteCount()

Get the number of rewrites until this term has been found.

getStateNr()

Get an internal state number that allows reconstructing the path to this term.

getStateParent(stateNr)

Get the parent state.

Parameters:

stateNr (int) – The number of a state in the search graph.

Return type:

int

Returns:

The number of the parent or -1 for the root.

getStateTerm(stateNr)

Get the term of a given state.

Parameters:

stateNr (int) – The number of a state in the search graph.

getStrategyContinuation(stateNr=-1)

Get the next strategy to be executed from the given state.

Parameters:

stateNr (int, optional) – The number of a state in the search graph or -1 for the current one.

getSubstitution()

Get the matching substitution of the solution into the pattern.

getTransition(stateNr=-1)

Get the transition leading to the given state.

Parameters:

stateNr (int, optional) – The number of a state in the search graph or -1 for the current one.

Return type:

StrategyGraphTransition

Returns:

The transition between the parent of the given state and the state itself.

pathTo(stateNr)

Get the path from the initial to the given state.

Parameters:

stateNr (int) – State index.

Return type:

list of Term and StrategyGraphTransition

Returns:

A list interleaving terms and transitions that connect them from the initial to the given state.

class maude.NarrowingSequenceSearch(*args, **kwargs)

An iterator through narrowing solutions.

It iterates over (Term, Substitution, Substitution) tuples, consisting of the solution, the accumulated substitution, and the variant unifer.

getSubstitution()

Get the accumulated substitution.

getUnifier()

Get the variant unifier.

isIncomplete()

Whether some solutions may have been missed due to incomplete unification algorithms.

class maude.VariantSearch(*args, **kwargs)

An iterator through variants.

It iterates over (Term, Substitution) pairs describing the variants.

isIncomplete()

Whether some variants may have been missed due to incomplete unification algorithms.

class maude.UnificationProblem(*args, **kwargs)

An iterator through unifiers.

It iterates over unifiers of type Substitution.

class maude.VariantUnifierSearch(*args, **kwargs)

An iterator through unifiers or matchers for variant unification or matching.

It iterates over unifiers of type Substitution.

filteringIncomplete()

Whether filetering was incomplete due to incomplete unification algorithms.

isIncomplete()

Whether some unifiers may have been missed due to incomplete unification algorithms.

class maude.ArgumentIterator(*args, **kwargs)

An iterator through the arguments of a term.

It iterates over subterms of type Term.

Search types

maude.ANY_STEPS

->*

maude.AT_LEAST_ONE_STEP

->+

maude.ONE_STEP

->1

maude.NORMAL_FORM

->!

maude.BRANCH

->#

Conditions

Conditions are sequences of condition fragments of any of the four types described below. They should be provided as Python lists to methods like Term.search(), and they are returned as Maude internal vectors in other methods like Rule.getCondition(). Maude internal vectors are read-only iterable objects, whose elements can also be accessed by index.

class maude.Condition(*args, **kwargs)

Internal Maude vector.

empty()

Is the vector empty?

size()

Size of the vector.

class maude.EqualityCondition(lhs, rhs)

Bases: ConditionFragment

An equality t = t' condition.

getLhs()

Get the left-hand-side term.

getRhs()

Get the right-hand-side term.

class maude.AssignmentCondition(lhs, rhs)

Bases: ConditionFragment

An assignment t := t' condition.

getLhs()

Get the left-hand-side term.

getRhs()

Get the right-hand-side term.

class maude.SortTestCondition(lhs, rhs)

Bases: ConditionFragment

A sort test t : s condition.

getLhs()

Get the term of the sort test.

getSort()

Get the sort of the sort test.

class maude.RewriteCondition(lhs, rhs)

Bases: ConditionFragment

A rewrite t => t' condition.

getLhs()

Get the left-hand-side term.

getRhs()

Get the right-hand-side term.

Modules

The Module class gives access to module information including its components: Sort, Kind, Equation, MembershipAxiom, Rule, RewriteStrategy (strategy declarations) and StrategyDefinition. Terms and strategy expressions can be parsed by means of the parseTerm() and parseStrategy() functions. Modules can be obtained with getCurrentModule(), getModule(), downModule(), and some other specific functions.

class maude.Module(*args, **kwargs)

A Maude module.

FUNCTIONAL_MODULE = 0

Functional module (fmod)

FUNCTIONAL_THEORY = 2

Functional theory (fth)

OBJECT_ORIENTED_MODULE = 9

Object-oriented module (omod)

OBJECT_ORIENTED_THEORY = 11

Object-oriented theory (oth)

STRATEGY_MODULE = 5

Strategy module (smod)

STRATEGY_THEORY = 7

Strategy theory (sth)

SYSTEM_MODULE = 1

System module (mod)

SYSTEM_THEORY = 3

System theory (th)

downStrategy(term)

Get a strategy expression in this module from its metarepresentation in (possibly) another module.

Parameters:

term (Term) – The metarepresentation of a strategy, that is, a valid element of the Strategy sort in META-STRATEGY. This term must belong to a module where the META-LEVEL module is included. The term will be reduced.

Return type:

StrategyExpression

Returns:

The strategy expression or null if the metarepresentation was not valid.

downTerm(term)

Get a term in this module from its metarepresentation in (possibly) another module.

Parameters:

term (Term) – The metarepresentation of a term, that is, a valid element of the Term sort in META-TERM. This term must belong to a module where the META-LEVEL module is included. The term will be reduced.

Return type:

Term

Returns:

The term or null if the metarepresentation was not valid.

findSort(name)

Finds a sort by its name in the module.

Parameters:

name (string) – The name of the sort.

Return type:

Sort

Returns:

The sort or null if it does not exist.

findSymbol(name, domainKinds, rangeKind)

Find a symbol by its name and signature in the module.

Parameters:

  • name (string) – The name of the sort.

  • domainKinds (list of Kind) – Kinds of the symbol domain.

  • rangeKind (Kind) – Range kind of the symbol.

Return type:

Symbol

Returns:

The symbol or null if it does not exist.

getEquations()

Get the equations defined in the module.

getKinds()

Get the kinds defined in the module.

getMembershipAxioms()

Get the membership axioms defined in the module.

getModuleType()

Get the module type.

This allows distinguishing modules from theories, and the functional, system and strategy variants within them.

getNrImportedSorts()

Number of sorts imported from other modules or parameters.

getNrImportedStrategies()

Number of strategies imported from other modules or parameters.

getNrImportedSymbols()

Number of symbols imported from other modules or parameters.

getNrOriginalEquations()

Number of equations from this module.

getNrOriginalRules()

Number of rules from this module.

getNrOriginalStrategyDefinitions()

Number of strategy definitions from this module.

getNrParameters()

Number of parameters of the parameterized module.

getParameterName(index)

Get the name of a module parameter.

Parameters:

index (int) – Index of the parameter.

getParameterTheory(index)

Get the theory of the given parameter.

getRules()

Get the rules defined in the module.

getSorts()

Get the sorts declared in the module.

getStrategies()

Get the strategies declared in the module.

getStrategyDefinitions()

Get the strategy definitions defined in the module.

getSymbols()

Get the symbols declared in the module.

hasFreeParameters()

Is this a parameterized module with free parameters?

parseStrategy(*args, **kwargs)

Parse a strategy expression.

Parameters:

  • term_str – A strategy represented as a string.

  • vars (list of Term, optional) – Variables that may appear without explicit type annotation in the strategy.

parseTerm(*args)

Overload 1:

Parse a term.

Parameters:

  • bubble (list of Token) – Tokenized term.

  • kind (Kind, optional) – Restrict parsing to terms of the given kind.


Overload 2:

Parse a term.

Parameters:

  • term_str (string) – A term represented as a string.

  • kind (Kind, optional) – Restrict parsing to terms of the given kind.

  • vars (list of Term, optional) – Variables that may appear without explicit type annotation in the strategy.

toLatex(all=False)

Obtain the LaTeX representation of this module.

Parameters:

all (boolean, optional) – Whether to show all statements by transitivity.

unify(problem, irredundant=False)

Solves the given unification problem.

Parameters:

  • problem (list of (Term, Term)) – A list of pairs of terms to be unified.

  • irredundant (boolean, optional) – Whether to compute a minimal set of unifiers.

Return type:

UnificationProblem

Returns:

An object to iterate through unifiers.

upStrategy(expr)

Get the metarepresentation in this module of a strategy expression in (possibly) another module. This module must contain META-LEVEL.

Parameters:

expr (StrategyExpression) – Any strategy expression.

Return type:

Term

Returns:

The metarepresented strategy or null.

upTerm(term)

Get the metarepresentation in this module of a term in (possibly) another module. This module must contain META-LEVEL.

Parameters:

term (Term) – Any term.

Return type:

Term

Returns:

The metarepresentation term or null.

variant_match(*args)

Computes a complete set of order-sorted matches modulo the equations declared with the variant attribute (which must satisfy the finite variant property) plus the (supported) equational axioms in the given module.

Parameters:

  • problem (list of (Term, Term)) – A list of pairs of terms to be matched.

  • irreducible (list of Term, optional) – Irreducible terms.

Return type:

VariantUnifierSearch

Returns:

An object to iterate through unifiers.

variant_unify(*args, **kwargs)

Solves the given unification problem using variants.

Parameters:

  • problem (list of (Term, Term)) – A list of pairs of terms to be unified.

  • irreducible (list of Term, optional) – Irreducible terms.

  • filtered (boolean, optional) – Whether to compute a minimal set of unifiers.

Return type:

VariantUnifierSearch

Returns:

An object to iterate through unifiers.

Module items

class maude.Sort(*args, **kwargs)

A Maude sort.

getLineNumber()

Get the line number information for this item as formatted by Maude.

The format of the string is usually filename, line line (module) where the second line is the integral line number, and module is the module type and name where this item was originally defined. The filename may be an actual quoted filename or some special name between angle brackets.

getSubsorts()

Get the subsorts of this sort.

getSupersorts()

Get the supersorts of this sort.

kind()

Get the kind this sort belongs to.

leq(rhs)

Check if this sort is a subsort of the given sort.

Parameters:

rhs (Sort) – The right-hand side of the comparison.

class maude.Kind(*args, **kwargs)

A Maude kind (connected component of sorts).

This is an iterable object over its sorts.

errorFree()

Whether the kind contains error terms.

nrMaximalSorts()

Get the number of maximal sorts in this kind.

nrSorts()

Get the number of sorts in this kind.

sort(index)

Get the sort with a given index in this kind.

Parameters:

index (int) – Sort index.

class maude.MembershipAxiom(*args, **kwargs)

A sort membership axiom.

getCondition()

Get the condition of the membership axiom.

getLabel()

Get the label attribute.

getLhs()

Get the term of the membership axiom.

getLineNumber()

Get the line number information for this item as formatted by Maude.

The format of the string is usually filename, line line (module) where the second line is the integral line number, and module is the module type and name where this item was originally defined. The filename may be an actual quoted filename or some special name between angle brackets.

getMetadata()

Get the free text metadata attribute of this statement.

getSort()

Get the sort of the membership axiom.

isNonexec()

Whether the membership axiom has the nonexec attribute.

class maude.Equation(*args, **kwargs)

A Maude equation.

getCondition()

Get the condition of the equation.

getLabel()

Get the label attribute.

getLhs()

Get the left-hand-side term.

getLineNumber()

Get the line number information for this item as formatted by Maude.

The format of the string is usually filename, line line (module) where the second line is the integral line number, and module is the module type and name where this item was originally defined. The filename may be an actual quoted filename or some special name between angle brackets.

getMetadata()

Get the free text metadata attribute of this statement.

getRhs()

Get the right-hand-side term.

hasCondition()

Whether the equation has a condition.

isNonexec()

Whether the equation has the nonexec attribute.

isOwise()

Whether the equation has the owise attribute.

isVariant()

Whether the equation has the variant attribute.

class maude.Rule(*args, **kwargs)

A Maude rewrite rule.

getCondition()

Get the condition of the rule.

getLabel()

Get the label attribute.

getLhs()

Get the left-hand-side term.

getLineNumber()

Get the line number information for this item as formatted by Maude.

The format of the string is usually filename, line line (module) where the second line is the integral line number, and module is the module type and name where this item was originally defined. The filename may be an actual quoted filename or some special name between angle brackets.

getMetadata()

Get the free text metadata attribute of this statement.

getRhs()

Get the right-hand-side term.

hasCondition()

Whether the rule has a condition.

isNarrowing()

Whether the rule has the narrowing attribute.

isNonexec()

Whether the rule has the nonexec attribute.

class maude.RewriteStrategy(*args, **kwargs)

A named rewriting strategy.

arity()

Get the number of arguments of the strategy.

getDefinitions()

Get the definitions for this strategy.

getDomain()

Get the argument domain.

getLineNumber()

Get the line number information for this item as formatted by Maude.

The format of the string is usually filename, line line (module) where the second line is the integral line number, and module is the module type and name where this item was originally defined. The filename may be an actual quoted filename or some special name between angle brackets.

getMetadata()

Get the free text metadata attribute of this statement.

getName()
getSubjectSort()

Get the sort to which the strategy is intended to be applied.

class maude.StrategyDefinition(*args, **kwargs)

A Maude strategy definition.

getCondition()

Get the condition of the strategy definition.

getLabel()

Get the label attribute.

getLhs()

Get the left-hand side of the strategy definition as a term.

getLineNumber()

Get the line number information for this item as formatted by Maude.

The format of the string is usually filename, line line (module) where the second line is the integral line number, and module is the module type and name where this item was originally defined. The filename may be an actual quoted filename or some special name between angle brackets.

getMetadata()

Get the free text metadata attribute of this statement.

getRhs()

Get the strategy definition.

getStrategy()

Get the named strategy being defined.

hasCondition()

Whether the strategy definition has a condition.

isNonexec()

Whether the strategy definition has the nonexec attribute.

Operator attributes

maude.OP_ASSOC

associative

maude.OP_COMM

commutative

maude.OP_ITER

iterable

maude.OP_IDEM

idempotent

maude.OP_LEFT_ID

with left identity element

maude.OP_RIGHT_ID

with right identity element

maude.OP_MEMO

with memoization

maude.OP_SPECIAL

special

Rewriting graphs and model checking

These two classes give access to the reachable rewriting graphs from an initial term. Their nodes are terms indexed by integers and their edges are essentially rule applications. In StrategyRewriteGraph, rewriting is controlled by a strategy expression. LTL formulae can be model checked on these graphs using their modelCheck methods, obtaining the state indices of the counterexample in case the property is not satisfied.

class maude.RewriteGraph(term)

Complete rewriting graph from an initial state.

getNextState(stateNr, index)

List the successors of a state in the graph.

Parameters:

  • stateNr (int) – A state number.

  • index (int) – A child index (from zero).

Return type:

int

Returns:

The state number of a successor or -1.

getNrRewrites()

Get the number of rewrites used to generate this graph, including the evaluation of atomic propositions.

getNrStates()

Get the number of states in the graph.

getRule(origin, dest)

Get a rule that connects two states.

Parameters:

  • origin (int) – Origin state number.

  • dest (int) – Destination state number.

Return type:

Rule

Returns:

A rule that connects the two states or null if none.

getStateParent(stateNr)

Get the (one) parent of a given state.

Parameters:

stateNr (int) – A state number.

Return type:

int

Returns:

The state number of the parent or -1.

getStateTerm(stateNr)

Get the term of the given state.

Parameters:

stateNr (int) – A state number.

modelCheck(formula)

Model check a given LTL formula.

Parameters:

formula (Term) – Term of the Formula sort.

Return type:

ModelCheckResult

Returns:

The result of model checking.

class maude.StrategyRewriteGraph(*args)

Complete rewriting graph under the control of a strategy from an initial state.

OPAQUE_STRATEGY = 1

opaque strategy

RULE_APPLICATION = 0

rule application

SOLUTION = 2

self-loops for solutions

getNextState(stateNr, index)

List the successors of a state in the graph.

Parameters:

  • stateNr (int) – A state number.

  • index (int) – A child index (from zero).

Return type:

int

Returns:

The state number of a successor or -1.

getNrRealStates()

Get the number of real (not merged) states in the graph (in linear time).

getNrRewrites()

Get the number of rewrites used to generate this graph, including the evaluation of atomic propositions.

getNrStates()

Get the number of states in the graph.

getStateStrategy(stateNr)

Get the strategy that will be executed next from the given state.

Parameters:

stateNr (int) – A state number.

Return type:

StrategyExpression

Returns:

That strategy expression or null if there is no pending strategy in the current call or subsearch frame.

getStateTerm(stateNr)

Get the term of the given state.

Parameters:

stateNr (int) – A state number.

getTransition(origin, dest)

Get the transition that connects two states (if any).

Parameters:

  • origin (int) – Origin state number.

  • dest (int) – Destination state number.

Return type:

StrategyGraphTransition

Returns:

That transition if exists or a null pointer.

isSolutionState(stateNr)

Whether the state is a solution for the strategy.

Parameters:

stateNr (int) – A state number.

modelCheck(formula)

Model check a given LTL formula.

Parameters:

formula (Term) – Term of the Formula sort.

Return type:

ModelCheckResult

Returns:

The result of model checking.

class maude.StrategyGraphTransition(*args, **kwargs)

Structure describing a transition in the graph.

getRule()

Get the rule applied, in case the transition is a rule application.

Return type:

Rule

Returns:

That rule or a null pointer if the transition is not a rule application.

getStrategy()

Get the strategy executed, in case of an opaque transition.

Return type:

RewriteStrategy

Returns:

That strategy or a null pointer if the transition is not an opaque strategy.

getType()

Get the transition type (rule application, opaque strategy, or solution).

class maude.ModelCheckResult

Result of LTL model checking.

property cycle

The counterexample cycle.

property holds

Whether the property holds.

property leadIn

The counterexample path to the cycle.

property nrBuchiStates

Number of states in the Büchi automaton.

Custom special operators

Special operators in Maude are those whose semantics are given in the C++ code of its interpreter, as opposed to the usual ones that are defined by means of equations and rules. Using the elements described below, new special operators can be declared whose behavior is implemented in Python. The process involves three steps:

  1. Declaring in Maude the desired operator with a special attribute containing the fragment id-hook SpecialHubSymbol. Additionally, op-hook and term-hook bindings can be included in the attribute to let the Python implementation access some given symbols and terms through the HookData class.

  2. Defining in Python the behavior of the special operator whenever it is reduced equationally or rewritten. A subclass of Hook must define its run() method that produces the reduced or rewritten term.

  3. Associating a Hook instance with an special operator using the functions connectEqHook() for equational rewriting or connectRlHook() for rule rewriting.

For example, the following is the declaration in Maude of a function getenv to obtain the value of an environment variable:

op getenv : String ~> String [special (
    id-hook SpecialHubSymbol
)] .

This declaration alone makes getenv behave as a standard operator, and its special meaning should be given within Python:

class EnvironmentHook(maude.Hook):
    def run(self, term, data):
        module = term.symbol().getModule()
        term.reduce()
        envar = str(term)[1:-1]
        enval = os.getenv(envar)
        return module.parseTerm(f'"{enval}"') if enval is not None else None

envhook = EnvironmentHook()
maude.connectEqHook('getenv', envhook)

The terms passed to the Python implementation do not have their subterms reduced, but these arguments must be reduced if included in the resulting term. None is an admitted return value that is interpreted as the absence of rewrite at that symbol. In this case, getenv is a partial function that does not yield a string when the given environment variable does not exist.

Warning

This feature is experimental and may be subject to changes. Do not forget that Maude programs including these special operators will not be executable in the official Maude interpreter.

class maude.Hook

Special operators defined on the external language.

run(term, data)

Method called by the hook.

Parameters:

  • term (Term) – The term being reduced or rewritten.

  • data (HookData) – Data associated to the hook.

Return type:

Term

Returns:

The reduced or rewritten term, or a null value in case no rewrite is possible.

class maude.HookData(*args, **kwargs)

Data associated to a hook and passed to its callback.

getData()

Get the data associated to the hook.

getSymbol(name)

Get the symbol associated to the hook with the given name.

getTerm(name)

Get the term associated to the hook with the given name.

maude.connectEqHook(name, hook)

Connect a callback for the reduction of a special operator declared with the SpecialHubSymbol id-hook.

Parameters:

  • name (string) – The name of the operator to be bound to this callback. In case the id-hook contains arguments, the name is instead the first of these. A null value may be passed to assign a default callback for those operators without an explicitly associated one.

  • hook (Hook) – An instance of a subclass of Hook defining its run method. The object must be alive as long as the binding is active. A null value can be passed to disconnect the current one.

Return type:

boolean

Returns:

Whether this call overwrites a previous binding.

maude.connectRlHook(name, hook)

Connect a callback for rule rewriting a special operator declared with the SpecialHubSymbol id-hook.

Parameters:

  • name (string) – The name of the operator to be bound to this callback. In case the id-hook contains arguments, the name is instead the first of these. A null value may be passed to assign a default callback for those operators without an explicitly associated one.

  • hook (Hook) – An instance of a subclass of Hook defining its run method. The object must be alive as long as the binding is active. A null value can be passed to disconnect the current one.

Return type:

boolean

Returns:

Whether this call overwrites a previous binding.

Indices and tables