Include file:

#include "mcrl2/pbes/pbesinst_algorithm.h
class mcrl2::pbes_system::pbesinst_algorithm

Algorithm class for the pbesinst instantiation algorithm.

Protected attributes

data::rewriter mcrl2::pbes_system::pbesinst_algorithm::datar

Data rewriter.

std::set<propositional_variable_instantiation> mcrl2::pbes_system::pbesinst_algorithm::done

Propositional variable instantiations that have been handled.

std::vector<std::vector<pbes_equation>> mcrl2::pbes_system::pbesinst_algorithm::E

Data structure for storing the result. E[i] corresponds to the equations generated from the i-th PBES equation.

std::map<core::identifier_string, int> mcrl2::pbes_system::pbesinst_algorithm::equation_index

A lookup map for PBES equations.

propositional_variable_instantiation mcrl2::pbes_system::pbesinst_algorithm::init

The initial value.

std::size_t mcrl2::pbes_system::pbesinst_algorithm::m_equation_count

The number of generated equations.

bool mcrl2::pbes_system::pbesinst_algorithm::m_print_equations

Print the equations to standard out.

enumerate_quantifiers_rewriter mcrl2::pbes_system::pbesinst_algorithm::R

The rewriter.

std::set<propositional_variable_instantiation> mcrl2::pbes_system::pbesinst_algorithm::todo

Propositional variable instantiations that need to be handled.

Protected member functions

std::string print_equation_count(std::size_t size) const

Prints a log message for every 1000-th equation.

pbes_expression rho(const pbes_expression &x) const

Public member functions

pbes get_result()

Returns the computed bes in pbes format.

Returns: The computed bes in pbes format

pbesinst_algorithm(data::data_specification const &data_spec, data::rewriter::strategy rewrite_strategy = data::jitty, bool print_equations = false)



  • data_spec A data specification.
  • rewrite_strategy A strategy for the data rewriter.
  • print_equations If true, the generated equations are printed.
bool &print_equations()

Returns the flag for printing the generated bes equations.

Returns: The flag for printing the generated bes equations

enumerate_quantifiers_rewriter &rewriter()
void run(pbes &p)

Runs the algorithm. The result is obtained by calling the function get_result.


  • p A PBES.