mcrl2::pbes_system::pbesinst_finite_algorithm

Include file:

#include "mcrl2/pbes/pbesinst_finite_algorithm.h

class mcrl2::pbes_system::pbesinst_finite_algorithm

Algorithm class for the finite pbesinst algorithm.

Protected attributes

std::size_t mcrl2::pbes_system::pbesinst_finite_algorithm::m_equation_count

The number of generated equations.

data::enumerator_identifier_generator mcrl2::pbes_system::pbesinst_finite_algorithm::m_id_generator

Identifier generator for the enumerator.

data::rewriter::strategy mcrl2::pbes_system::pbesinst_finite_algorithm::m_rewriter_strategy

The strategy of the data rewriter.

Protected member functions

void compute_index_map(const std::vector<pbes_equation> &equations, const pbesinst_variable_map &variable_map, pbesinst_index_map &index_map)

Returns true if the container contains the given element.

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

Prints a message for every 1000-th equation.

Public member functions

pbesinst_finite_algorithm(data::rewriter::strategy rewriter_strategy = data::jitty)

Constructor.

Parameters:

• rewriter_strategy Strategy to be used for the data rewriter.

void run(pbes &p)

Runs the algorithm.

Parameters:

• p A PBES

void run(pbes &pbesspec, const pbesinst_variable_map &variable_map)

Runs the algorithm.

Parameters:

• pbesspec A PBES
• variable_map A map containing the finite parameters that should be expanded by the algorithm.