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

#include <stategraph_global_reset_variables.h>

Inheritance diagram for mcrl2::pbes_system::detail::global_reset_variables_algorithm:

Public Types
using	super = stategraph_global_algorithm

Public Types inherited from mcrl2::pbes_system::detail::stategraph_global_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)

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

void	execute_core () override

const pbes &	result () const

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

void	execute_core () override

const global_control_flow_graph &	global_graph () 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 data::sort_expression &x)

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

template<typename Graph >
void	compute_global_control_flow_marking (Graph &G)

template<typename Vertex >
bool	location_possibly_reachable (const core::identifier_string &Y, const Vertex &u, const std::vector< data::data_expression > &e_X, const stategraph_equation &eq_X, std::size_t i)

Protected Member Functions inherited from mcrl2::pbes_system::detail::stategraph_global_algorithm
bool	enabled_edge (const global_control_flow_graph_vertex &u, const stategraph_equation &eq_X, const predicate_variable &Yf)

std::size_t	unproject (const predicate_variable &Yf, const std::vector< std::size_t > &cfp, std::size_t l) const

const global_control_flow_graph_vertex &	compute_vertex (global_control_flow_graph &G, const global_control_flow_graph_vertex &u, const stategraph_equation &eq_X, const predicate_variable &Yf, const stategraph_equation &eq_Y)

void	compute_significant_variables ()

void	compute_global_control_flow_graph ()

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

Protected Attributes inherited from mcrl2::pbes_system::detail::stategraph_global_algorithm
global_control_flow_graph	m_control_flow_graph

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 24 of file stategraph_global_reset_variables.h.

Member Typedef Documentation

◆ super

using mcrl2::pbes_system::detail::global_reset_variables_algorithm::super = stategraph_global_algorithm

Definition at line 27 of file stategraph_global_reset_variables.h.

Constructor & Destructor Documentation

◆ global_reset_variables_algorithm()

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

inline

Definition at line 260 of file stategraph_global_reset_variables.h.

Member Function Documentation

◆ compute_global_control_flow_marking()

template<typename Graph >

void mcrl2::pbes_system::detail::global_reset_variables_algorithm::compute_global_control_flow_marking ( Graph & G )

inlineprotected

Definition at line 52 of file stategraph_global_reset_variables.h.

◆ default_value()

data::data_expression mcrl2::pbes_system::detail::global_reset_variables_algorithm::default_value ( const data::sort_expression & x )

inlineprotected

Definition at line 36 of file stategraph_global_reset_variables.h.

◆ execute_core()

void mcrl2::pbes_system::detail::global_reset_variables_algorithm::execute_core ( )

inlineoverridevirtual

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

Definition at line 266 of file stategraph_global_reset_variables.h.

◆ location_possibly_reachable()

template<typename Vertex >

bool mcrl2::pbes_system::detail::global_reset_variables_algorithm::location_possibly_reachable	(	const core::identifier_string &	Y,
		const Vertex &	u,
		const std::vector< data::data_expression > &	e_X,
		const stategraph_equation &	eq_X,
		std::size_t	i
	)

inlineprotected

Definition at line 125 of file stategraph_global_reset_variables.h.

◆ propvar_parameters()

std::set< data::variable > mcrl2::pbes_system::detail::global_reset_variables_algorithm::propvar_parameters ( const core::identifier_string & X ) const

inlineprotected

Definition at line 44 of file stategraph_global_reset_variables.h.

◆ reset_variable()

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

inline

Definition at line 153 of file stategraph_global_reset_variables.h.

◆ reset_variables_to_original()

void mcrl2::pbes_system::detail::global_reset_variables_algorithm::reset_variables_to_original ( pbes & p )

inline

Definition at line 238 of file stategraph_global_reset_variables.h.

◆ result()

const pbes & mcrl2::pbes_system::detail::global_reset_variables_algorithm::result ( ) const

inline

Definition at line 277 of file stategraph_global_reset_variables.h.

Member Data Documentation

◆ m_original_pbes

const pbes& mcrl2::pbes_system::detail::global_reset_variables_algorithm::m_original_pbes

protected

Definition at line 30 of file stategraph_global_reset_variables.h.

◆ m_simplify

bool mcrl2::pbes_system::detail::global_reset_variables_algorithm::m_simplify

protected

Definition at line 34 of file stategraph_global_reset_variables.h.

◆ m_transformed_pbes

pbes mcrl2::pbes_system::detail::global_reset_variables_algorithm::m_transformed_pbes

protected

Definition at line 31 of file stategraph_global_reset_variables.h.

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

pbes/include/mcrl2/pbes/detail/stategraph_global_reset_variables.h

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ super

Constructor & Destructor Documentation

◆ global_reset_variables_algorithm()

Member Function Documentation

◆ compute_global_control_flow_marking()

◆ default_value()

◆ execute_core()

◆ location_possibly_reachable()

◆ propvar_parameters()

◆ reset_variable()

◆ reset_variables_to_original()

◆ result()

Member Data Documentation

◆ m_original_pbes

◆ m_simplify

◆ m_transformed_pbes