mcrl2/pbes/algorithms.h

Include file:

#include "mcrl2/pbes/algorithms.h"

add your file description here.

Functions

void instantiate_global_variables(pbes &p)

Attempts to eliminate the free variables of a PBES, by substituting a constant value for them. If no constant value is found for one of the variables, an exception is thrown.

bool is_bes(const pbes &x)

Returns true if a PBES is in BES form.

Parameters:

  • x a PBES
bool is_normalized(const pbes &x)

Checks if a PBEs is normalized.

Returns: True if the PBES is normalized

void normalize(pbes &x)

The function normalize brings (embedded) pbes expressions into positive normal form, i.e. a formula without any occurrences of ! or =>.

Parameters:

  • x an object containing pbes expressions
void pbesinst_finite(pbes &p, data::rewrite_strategy rewrite_strategy, const std::string &finite_parameter_selection)

Apply finite instantiation to the given PBES.

std::string print_removed_equations(const std::vector<propositional_variable> &removed)

Print removed equations.

void remove_parameters(pbes &x, const std::set<data::variable> &to_be_removed)

Removes parameters from propositional variable instantiations in a pbes expression.

Parameters:

  • x A PBES library object that does not derive from atermpp::aterm_appl
  • to_be_removed A set of parameters that are to be removed

Returns: The expression x with parameters removed according to the mapping to_be_removed

void remove_parameters(pbes &x, const std::map<core::identifier_string, std::vector<std::size_t>> &to_be_removed)

Removes parameters from propositional variable instantiations in a pbes expression.

Parameters:

  • x A PBES library object that does not derive from atermpp::aterm_appl
  • to_be_removed A mapping that maps propositional variable names to indices of parameters that are removed

Returns: The expression x with parameters removed according to the mapping to_be_removed

std::vector<propositional_variable> remove_unreachable_variables(pbes &p)

Removes equations that are not (syntactically) reachable from the initial state of a PBES.

Returns: The removed variables

std::set<data::variable> significant_variables(const pbes_expression &x)

Returns the significant variables of a pbes expression.