mcrl2::pbes_system::pbesinst_finite_algorithm Class Reference

Algorithm class for the finite pbesinst algorithm. More...

#include <pbesinst_finite_algorithm.h>

Public Member Functions
	pbesinst_finite_algorithm (data::rewriter::strategy rewriter_strategy=data::jitty)
	Constructor.
void	run (pbes &pbesspec, const pbesinst_variable_map &variable_map)
	Runs the algorithm.
void	run (pbes &p)
	Runs the algorithm.

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.

Protected Attributes
data::rewriter::strategy	m_rewriter_strategy
	The strategy of the data rewriter.
std::size_t	m_equation_count = 0
	The number of generated equations.
data::enumerator_identifier_generator	m_id_generator
	Identifier generator for the enumerator.

Detailed Description

Algorithm class for the finite pbesinst algorithm.

Definition at line 265 of file pbesinst_finite_algorithm.h.

Constructor & Destructor Documentation

pbesinst_finite_algorithm()

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

inlineexplicit

Constructor.

Parameters

rewriter_strategy

Strategy to be used for the data rewriter.

Definition at line 321 of file pbesinst_finite_algorithm.h.

Member Function Documentation

compute_index_map()

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

inlineprotected

Returns true if the container contains the given element.

Definition at line 278 of file pbesinst_finite_algorithm.h.

print_equation_count()

std::string mcrl2::pbes_system::pbesinst_finite_algorithm::print_equation_count ( std::size_t  size ) const

inlineprotected

Prints a message for every 1000-th equation.

Definition at line 306 of file pbesinst_finite_algorithm.h.

run() [1/2]

void mcrl2::pbes_system::pbesinst_finite_algorithm::run ( pbes &  p )

inline

Runs the algorithm.

Parameters

p

A PBES

Definition at line 389 of file pbesinst_finite_algorithm.h.

run() [2/2]

void mcrl2::pbes_system::pbesinst_finite_algorithm::run ( pbes &  pbesspec, const pbesinst_variable_map &  variable_map  )

inline

Runs the algorithm.

Parameters

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

Definition at line 328 of file pbesinst_finite_algorithm.h.

Member Data Documentation

m_equation_count

std::size_t mcrl2::pbes_system::pbesinst_finite_algorithm::m_equation_count = 0

protected

The number of generated equations.

Definition at line 272 of file pbesinst_finite_algorithm.h.

m_id_generator

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

protected

Identifier generator for the enumerator.

Definition at line 275 of file pbesinst_finite_algorithm.h.

m_rewriter_strategy

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

protected

The strategy of the data rewriter.

Definition at line 269 of file pbesinst_finite_algorithm.h.

---

The documentation for this class was generated from the following file:

• pbes/include/mcrl2/pbes/pbesinst_finite_algorithm.h