Adds the reset variables procedure to the stategraph algorithm. More...

#include <stategraph_local_reset_variables.h>

Inheritance diagram for mcrl2::pbes_system::detail::local_reset_variables_algorithm:

Public Types
using	super = stategraph_local_algorithm

Public Types inherited from mcrl2::pbes_system::detail::stategraph_local_algorithm
using	super = stategraph_algorithm

Public Member Functions
pbes_expression	reset_variable (const propositional_variable_instantiation &x, const stategraph_equation &eq_X, std::size_t i)

void	reset_variables_to_original (pbes &p)

	local_reset_variables_algorithm (const pbes &p, const pbesstategraph_options &options)

void	execute_postprocessing () override

const pbes &	result () const

Public Member Functions inherited from mcrl2::pbes_system::detail::stategraph_local_algorithm
	stategraph_local_algorithm (const pbes &p, const pbesstategraph_options &options)

void	execute_core () override

void	execute_local_graphs_step ()

void	execute_belongs_step ()

void	execute_extra_graph_step ()

void	execute_marking_step ()

const std::vector< belongs_relation > &	belongs () const

Public Member Functions inherited from mcrl2::pbes_system::detail::stategraph_algorithm
void	simplify (stategraph_pbes &p) const

const std::map< core::identifier_string, std::vector< bool > > &	get_GCFP () const

void	compute_control_flow_parameters ()

template<typename T >
std::string	print_control_flow_parameters (const std::string &msg, T &is_CFP)

std::string	print_LCFP ()

std::string	print_GCFP ()

template<typename Map >
bool	is_undefined (const Map &m, const typename Map::key_type &key) const

template<typename Map >
bool	is_mapped_to (const Map &m, const typename Map::key_type &key, const typename Map::mapped_type &value) const

bool	maps_to_and_is_GFCP (const std::map< std::size_t, std::size_t > &m, std::size_t value, const core::identifier_string &X)

void	compute_local_control_flow_parameters ()

void	compute_global_control_flow_parameters ()

bool	is_LCFP_parameter (const core::identifier_string &X, std::size_t i) const

bool	is_GCFP_parameter (const core::identifier_string &X, std::size_t i) const

bool	is_global_control_flow_parameter (const core::identifier_string &X, std::size_t i) const

void	relate_GCFP_vertices (const core::identifier_string &X, std::size_t n, const core::identifier_string &Y, std::size_t m)

std::string	print_cfp (const core::identifier_string &X, std::size_t i) const

std::string	log_related_parameters (const core::identifier_string &X, std::size_t n, const core::identifier_string &Y, std::size_t m, const predicate_variable &Ye, const std::string &reason="") const

void	compute_related_GCFP_parameters ()

bool	is_valid_connected_component (const std::set< std::size_t > &component) const

std::string	print_connected_component (const std::set< std::size_t > &component) const

void	print_connected_components () const

std::set< std::size_t >	compute_connected_component (std::size_t i, std::vector< bool > &done) const

void	compute_connected_components ()

void	remove_invalid_connected_components ()

bool	is_not_only_copied (const core::identifier_string &X, std::size_t m) const

bool	has_only_copied_CFPs (const std::set< std::size_t > &component) const

void	remove_only_copy_components ()

const std::vector< bool > &	is_GCFP (const core::identifier_string &X) const

std::set< data::variable >	control_flow_parameters (const core::identifier_string &X) const

std::vector< std::size_t >	control_flow_parameter_indices (const core::identifier_string &X) const

std::string	print_data_parameters (const core::identifier_string &X, const std::set< std::size_t > &I) const

void	set_parameters (const stategraph_pbes &p)

void	print_final_control_flow_parameters () const

	stategraph_algorithm (const pbes &p, const pbesstategraph_options &options)
	Constructor.

virtual	~stategraph_algorithm ()=default
	Destructor.

const std::vector< std::set< std::size_t > > &	connected_components () const
	Returns the connected components of the global control flow graph.

std::string	print (const GCFP_vertex &u) const

std::set< data::data_expression >	compute_connected_component_values (const std::set< std::size_t > &component)
	Computes the values that the CFPs in component can attain.

void	compute_connected_component_values ()

std::vector< data::data_expression >	compute_values (const core::identifier_string &X, std::size_t j) const

void	run ()

virtual void	execute_preprocessing ()

virtual void	execute_core ()

virtual void	execute_postprocessing ()

const stategraph_pbes &	get_pbes () const

const GCFP_graph &	GCFP () const

std::vector< local_control_flow_graph > &	local_graphs ()

const std::vector< local_control_flow_graph > &	local_graphs () const

Protected Member Functions
data::data_expression	default_value (const core::identifier_string &X, std::size_t j, const data::sort_expression &x)

void	compute_occurring_data_parameters ()

data::data_expression_list	reset_variable_parameters (const propositional_variable_instantiation &x, const stategraph_equation &eq_X, std::size_t i)

Protected Member Functions inherited from mcrl2::pbes_system::detail::stategraph_local_algorithm
std::vector< core::identifier_string >	binding_variable_names () const

void	compute_edge_index ()

std::string	print_edge_index ()

std::string	print_belong_set (const stategraph_equation &eq, const std::set< std::size_t > &belongs) const

std::string	print_parameters (const core::identifier_string &X, const std::set< std::size_t > &I) const

template<typename RulesPredicate >
belongs_relation	compute_belongs (const local_control_flow_graph &Vk, RulesPredicate rules)

void	compute_belongs ()

std::string	print_belongs (const belongs_relation &B) const

void	print_belongs () const

std::set< data::variable >	significant_variables (const local_control_flow_graph_vertex &u) const

std::size_t	find_parameter_index (const std::vector< data::variable > &d_Y, const data::variable &d) const

bool	belongs_contains (const belongs_relation &B, const core::identifier_string &X, const data::variable &d) const

std::set< data::variable >	belongs_intersection (const std::set< data::variable > &V, const belongs_relation &B, const core::identifier_string &X)

template<typename Substitution >
data::data_expression	rewr (const data::data_expression &x, Substitution sigma)

std::set< data::variable >	marking_update (const local_control_flow_graph_vertex &u, std::size_t i, const data::variable &d, const data::data_expression_list &e, const stategraph_equation &eq_Y, const belongs_relation &B)

void	print_marking_statistics ()

bool	update_marking_rule (const belongs_relation &B, const local_control_flow_graph_vertex &u, std::size_t i, const local_control_flow_graph_vertex &v, bool check_belongs)

bool	has_incoming_edge (const local_control_flow_graph &, const local_control_flow_graph_vertex &v, const core::identifier_string &X, std::size_t i) const

void	compute_control_flow_marking ()

void	add_equation_labels (std::set< equation_label_pair > &todo, const local_control_flow_graph_vertex &v)

void	compute_control_flow_marking_using_edge_index ()

void	compute_control_flow_marking_efficient ()

void	print_control_flow_marking () const

void	remove_belongs (std::set< data::variable > &B_X, const core::identifier_string &X, const belongs_relation &Bk, std::size_t k)

void	compute_extra_local_control_flow_graph ()

void	compute_local_control_flow_graph (const std::set< local_control_flow_graph_vertex > &U, const std::map< core::identifier_string, std::size_t > &C)

void	compute_local_control_flow_graph (const local_control_flow_graph_vertex &u, const std::map< core::identifier_string, std::size_t > &C)

void	compute_local_control_flow_graph (const std::set< std::size_t > &component, const std::set< data::data_expression > &component_values)

void	print_local_control_flow_graphs () const

void	compute_local_control_flow_graphs ()

Protected Member Functions inherited from mcrl2::pbes_system::detail::stategraph_algorithm
std::set< data::variable >	FV (const data::data_expression &x) const

void	start_timer (const std::string &msg) const

void	finish_timer (const std::string &msg) const

Protected Attributes
const pbes	m_original_pbes

pbes	m_transformed_pbes

bool	m_simplify

std::map< core::identifier_string, std::set< std::size_t > >	m_occurring_data_parameters

Protected Attributes inherited from mcrl2::pbes_system::detail::stategraph_local_algorithm
std::vector< belongs_relation >	m_belongs

bool	m_cache_marking_updates

std::size_t	m_marking_rewrite_count = 0

std::size_t	m_marking_rewrite_cached_count = 0

std::map< core::identifier_string, std::map< std::size_t, std::set< vertex_pair > > >	m_edge_index

Protected Attributes inherited from mcrl2::pbes_system::detail::stategraph_algorithm
stategraph_pbes	m_pbes

data::rewriter	m_datar

pbesstategraph_options	m_options

std::map< core::identifier_string, std::vector< bool > >	m_is_LCFP

std::map< core::identifier_string, std::vector< bool > >	m_is_GCFP

GCFP_graph	m_GCFP_graph

std::vector< std::set< std::size_t > >	m_connected_components

std::vector< std::set< data::data_expression > >	m_connected_components_values

std::vector< local_control_flow_graph >	m_local_control_flow_graphs

Detailed Description

Adds the reset variables procedure to the stategraph algorithm.

Definition at line 39 of file stategraph_local_reset_variables.h.

Member Typedef Documentation

◆ super

using mcrl2::pbes_system::detail::local_reset_variables_algorithm::super = stategraph_local_algorithm

Definition at line 42 of file stategraph_local_reset_variables.h.

Constructor & Destructor Documentation

◆ local_reset_variables_algorithm()

mcrl2::pbes_system::detail::local_reset_variables_algorithm::local_reset_variables_algorithm	(	const pbes &	p,
		const pbesstategraph_options &	options
	)

inline

Definition at line 126 of file stategraph_local_reset_variables.h.

Member Function Documentation

◆ compute_occurring_data_parameters()

void mcrl2::pbes_system::detail::local_reset_variables_algorithm::compute_occurring_data_parameters ( )

inlineprotected

Definition at line 68 of file stategraph_local_reset_variables.h.

◆ default_value()

data::data_expression mcrl2::pbes_system::detail::local_reset_variables_algorithm::default_value	(	const core::identifier_string &	X,
		std::size_t	j,
		const data::sort_expression &	x
	)

inlineprotected

Definition at line 55 of file stategraph_local_reset_variables.h.

◆ execute_postprocessing()

void mcrl2::pbes_system::detail::local_reset_variables_algorithm::execute_postprocessing ( )

inlineoverridevirtual

Reimplemented from mcrl2::pbes_system::detail::stategraph_algorithm.

Reimplemented in mcrl2::pbes_system::detail::lpsstategraph_algorithm.

Definition at line 132 of file stategraph_local_reset_variables.h.

◆ reset_variable()

pbes_expression mcrl2::pbes_system::detail::local_reset_variables_algorithm::reset_variable	(	const propositional_variable_instantiation &	x,
		const stategraph_equation &	eq_X,
		std::size_t	i
	)

inline

Definition at line 102 of file stategraph_local_reset_variables.h.

◆ reset_variable_parameters()

data::data_expression_list mcrl2::pbes_system::detail::local_reset_variables_algorithm::reset_variable_parameters	(	const propositional_variable_instantiation &	x,
		const stategraph_equation &	eq_X,
		std::size_t	i
	)