mCRL2
Loading...
Searching...
No Matches
mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter > Class Template Reference

Algorithm class for the constelm algorithm. More...

#include <constelm.h>

Classes

class  edge
 Represents an edge of the dependency graph. The assignments are stored implicitly using the 'right' parameter. The condition determines under what circumstances the influence of the edge is propagated to its target vertex. More...
 
class  vertex
 Represents a vertex of the dependency graph. More...
 

Public Member Functions

 pres_constelm_algorithm (const DataRewriter &datar, const PresRewriter &presr)
 Constructor.
 
std::map< propositional_variable, std::vector< data::variable > > redundant_parameters () const
 Returns the parameters that have been removed by the constelm algorithm.
 
void run (pres &p, bool compute_conditions=false, bool check_quantifiers=true)
 Runs the constelm algorithm.
 

Protected Types

typedef std::map< data::variable, data::data_expressionconstraint_map
 A map with constraints on the vertices of the graph.
 
typedef std::list< detail::quantified_variableqvar_list
 
typedef std::map< core::identifier_string, vertexvertex_map
 The storage type for vertices.
 
typedef std::map< core::identifier_string, std::vector< edge > > edge_map
 The storage type for edges.
 

Protected Member Functions

std::string print_vertices () const
 Logs the vertices of the dependency graph.
 
std::string print_edges ()
 Logs the edges of the dependency graph.
 
std::string print_todo_list (const std::deque< propositional_variable > &todo)
 
std::string print_edge_update (const edge &e, const vertex &u, const vertex &v)
 
std::string print_condition (const edge &e, const vertex &u, const pres_expression &value)
 
std::string print_evaluation_failure (const edge &e, const vertex &u)
 
template<typename E >
std::list< E > concat (const std::list< E > a, const std::list< E > b)
 

Protected Attributes

const DataRewriter & m_data_rewriter
 Compares data expressions for equality.
 
const PresRewriter & m_pres_rewriter
 Compares data expressions for equality.
 
vertex_map m_vertices
 The vertices of the dependency graph. They are stored in a map, to support searching for a vertex.
 
edge_map m_edges
 The edges of the dependency graph. They are stored in a map, to easily access all out-edges corresponding to a particular vertex.
 
std::map< core::identifier_string, std::vector< std::size_t > > m_redundant_parameters
 The redundant parameters.
 

Detailed Description

template<typename DataRewriter, typename PresRewriter>
class mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >

Algorithm class for the constelm algorithm.

Definition at line 406 of file constelm.h.

Member Typedef Documentation

◆ constraint_map

template<typename DataRewriter , typename PresRewriter >
typedef std::map<data::variable, data::data_expression> mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::constraint_map
protected

A map with constraints on the vertices of the graph.

Definition at line 410 of file constelm.h.

◆ edge_map

template<typename DataRewriter , typename PresRewriter >
typedef std::map<core::identifier_string, std::vector<edge> > mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::edge_map
protected

The storage type for edges.

Definition at line 735 of file constelm.h.

◆ qvar_list

template<typename DataRewriter , typename PresRewriter >
typedef std::list<detail::quantified_variable> mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::qvar_list
protected

Definition at line 411 of file constelm.h.

◆ vertex_map

template<typename DataRewriter , typename PresRewriter >
typedef std::map<core::identifier_string, vertex> mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::vertex_map
protected

The storage type for vertices.

Definition at line 732 of file constelm.h.

Constructor & Destructor Documentation

◆ pres_constelm_algorithm()

template<typename DataRewriter , typename PresRewriter >
mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::pres_constelm_algorithm ( const DataRewriter &  datar,
const PresRewriter &  presr 
)
inline

Constructor.

Parameters
datarA data rewriter
presrA PRES rewriter

Definition at line 829 of file constelm.h.

Member Function Documentation

◆ concat()

template<typename DataRewriter , typename PresRewriter >
template<typename E >
std::list< E > mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::concat ( const std::list< E >  a,
const std::list< E >  b 
)
inlineprotected

Definition at line 817 of file constelm.h.

◆ print_condition()

template<typename DataRewriter , typename PresRewriter >
std::string mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::print_condition ( const edge e,
const vertex u,
const pres_expression value 
)
inlineprotected

Definition at line 798 of file constelm.h.

◆ print_edge_update()

template<typename DataRewriter , typename PresRewriter >
std::string mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::print_edge_update ( const edge e,
const vertex u,
const vertex v 
)
inlineprotected

Definition at line 789 of file constelm.h.

◆ print_edges()

template<typename DataRewriter , typename PresRewriter >
std::string mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::print_edges ( )
inlineprotected

Logs the edges of the dependency graph.

Definition at line 760 of file constelm.h.

◆ print_evaluation_failure()

template<typename DataRewriter , typename PresRewriter >
std::string mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::print_evaluation_failure ( const edge e,
const vertex u 
)
inlineprotected

Definition at line 807 of file constelm.h.

◆ print_todo_list()

template<typename DataRewriter , typename PresRewriter >
std::string mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::print_todo_list ( const std::deque< propositional_variable > &  todo)
inlineprotected

Definition at line 773 of file constelm.h.

◆ print_vertices()

template<typename DataRewriter , typename PresRewriter >
std::string mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::print_vertices ( ) const
inlineprotected

Logs the vertices of the dependency graph.

Definition at line 749 of file constelm.h.

◆ redundant_parameters()

template<typename DataRewriter , typename PresRewriter >
std::map< propositional_variable, std::vector< data::variable > > mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::redundant_parameters ( ) const
inline

Returns the parameters that have been removed by the constelm algorithm.

Returns
The removed parameters

Definition at line 835 of file constelm.h.

◆ run()

template<typename DataRewriter , typename PresRewriter >
void mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::run ( pres p,
bool  compute_conditions = false,
bool  check_quantifiers = true 
)
inline

Runs the constelm algorithm.

Parameters
pA pres
compute_conditionsIf true, propagation conditions are computed. Note that the currently implementation has exponential behavior.

Definition at line 856 of file constelm.h.

Member Data Documentation

◆ m_data_rewriter

template<typename DataRewriter , typename PresRewriter >
const DataRewriter& mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::m_data_rewriter
protected

Compares data expressions for equality.

Definition at line 414 of file constelm.h.

◆ m_edges

template<typename DataRewriter , typename PresRewriter >
edge_map mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::m_edges
protected

The edges of the dependency graph. They are stored in a map, to easily access all out-edges corresponding to a particular vertex.

Definition at line 743 of file constelm.h.

◆ m_pres_rewriter

template<typename DataRewriter , typename PresRewriter >
const PresRewriter& mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::m_pres_rewriter
protected

Compares data expressions for equality.

Definition at line 417 of file constelm.h.

◆ m_redundant_parameters

template<typename DataRewriter , typename PresRewriter >
std::map<core::identifier_string, std::vector<std::size_t> > mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::m_redundant_parameters
protected

The redundant parameters.

Definition at line 746 of file constelm.h.

◆ m_vertices

template<typename DataRewriter , typename PresRewriter >
vertex_map mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::m_vertices
protected

The vertices of the dependency graph. They are stored in a map, to support searching for a vertex.

Definition at line 739 of file constelm.h.


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