mcrl2::pbes_system::pbesinst_algorithm Class Reference

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

#include <pbesinst_algorithm.h>

Public Member Functions
	pbesinst_algorithm (data::data_specification const &data_spec, data::rewriter::strategy rewrite_strategy=data::rewrite_strategy::jitty, bool print_equations=false)
	Constructor.
void	run (pbes &p)
	Runs the algorithm. The result is obtained by calling the function get_result.
pbes	get_result ()
	Returns the computed bes in pbes format.
bool &	print_equations ()
	Returns the flag for printing the generated bes equations.
enumerate_quantifiers_rewriter &	rewriter ()

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

Protected Attributes
data::rewriter	datar
	Data rewriter.
enumerate_quantifiers_rewriter	R
	The rewriter.
std::size_t	m_equation_count = 0
	The number of generated equations.
std::set< propositional_variable_instantiation >	todo
	Propositional variable instantiations that need to be handled.
std::set< propositional_variable_instantiation >	done
	Propositional variable instantiations that have been handled.
std::vector< std::vector< pbes_equation > >	E
	Data structure for storing the result. E[i] corresponds to the equations generated from the i-th PBES equation.
propositional_variable_instantiation	init
	The initial value.
std::map< core::identifier_string, int >	equation_index
	A lookup map for PBES equations.
bool	m_print_equations
	Print the equations to standard out.

Detailed Description

Algorithm class for the pbesinst instantiation algorithm.

Definition at line 99 of file pbesinst_algorithm.h.

Constructor & Destructor Documentation

pbesinst_algorithm()

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

inlineexplicit

Constructor.

Parameters

data_spec	A data specification.
rewrite_strategy	A strategy for the data rewriter.
print_equations	If true, the generated equations are printed.

Definition at line 154 of file pbesinst_algorithm.h.

Member Function Documentation

get_result()

pbes mcrl2::pbes_system::pbesinst_algorithm::get_result ( )

inline

Returns the computed bes in pbes format.

Returns

The computed bes in pbes format

Definition at line 227 of file pbesinst_algorithm.h.

print_equation_count()

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

inlineprotected

Prints a log message for every 1000-th equation.

Definition at line 131 of file pbesinst_algorithm.h.

print_equations()

bool & mcrl2::pbes_system::pbesinst_algorithm::print_equations ( )

inline

Returns the flag for printing the generated bes equations.

Returns

The flag for printing the generated bes equations

Definition at line 240 of file pbesinst_algorithm.h.

rewriter()

enumerate_quantifiers_rewriter & mcrl2::pbes_system::pbesinst_algorithm::rewriter ( )

inline

Definition at line 245 of file pbesinst_algorithm.h.

rho()

pbes_expression mcrl2::pbes_system::pbesinst_algorithm::rho ( const pbes_expression &  x ) const

inlineprotected

Definition at line 143 of file pbesinst_algorithm.h.

run()

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

inline

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

Parameters

p

A PBES.

Definition at line 165 of file pbesinst_algorithm.h.

Member Data Documentation

datar

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

protected

Data rewriter.

Definition at line 103 of file pbesinst_algorithm.h.

done

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

protected

Propositional variable instantiations that have been handled.

Definition at line 115 of file pbesinst_algorithm.h.

E

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

protected

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

Definition at line 119 of file pbesinst_algorithm.h.

equation_index

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

protected

A lookup map for PBES equations.

Definition at line 125 of file pbesinst_algorithm.h.

init

propositional_variable_instantiation mcrl2::pbes_system::pbesinst_algorithm::init

protected

The initial value.

Definition at line 122 of file pbesinst_algorithm.h.

m_equation_count

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

protected

The number of generated equations.

Definition at line 109 of file pbesinst_algorithm.h.

m_print_equations

bool mcrl2::pbes_system::pbesinst_algorithm::m_print_equations

protected

Print the equations to standard out.

Definition at line 128 of file pbesinst_algorithm.h.

R

enumerate_quantifiers_rewriter mcrl2::pbes_system::pbesinst_algorithm::R

protected

The rewriter.

Definition at line 106 of file pbesinst_algorithm.h.

todo

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

protected

Propositional variable instantiations that need to be handled.

Definition at line 112 of file pbesinst_algorithm.h.

---

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

• pbes/include/mcrl2/pbes/pbesinst_algorithm.h