mCRL2
Loading...
Searching...
No Matches
mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter > 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

 pbes_constelm_algorithm (const DataRewriter &datar, const PbesRewriter &pbesr)
 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 (pbes &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 pbes_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 PbesRewriter & m_pbes_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 PbesRewriter>
class mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >

Algorithm class for the constelm algorithm.

Definition at line 394 of file constelm.h.

Member Typedef Documentation

◆ constraint_map

template<typename DataRewriter , typename PbesRewriter >
typedef std::map<data::variable, data::data_expression> mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::constraint_map
protected

A map with constraints on the vertices of the graph.

Definition at line 398 of file constelm.h.

◆ edge_map

template<typename DataRewriter , typename PbesRewriter >
typedef std::map<core::identifier_string, std::vector<edge> > mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::edge_map
protected

The storage type for edges.

Definition at line 723 of file constelm.h.

◆ qvar_list

template<typename DataRewriter , typename PbesRewriter >
typedef std::list<detail::quantified_variable> mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::qvar_list
protected

Definition at line 399 of file constelm.h.

◆ vertex_map

template<typename DataRewriter , typename PbesRewriter >
typedef std::map<core::identifier_string, vertex> mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::vertex_map
protected

The storage type for vertices.

Definition at line 720 of file constelm.h.

Constructor & Destructor Documentation

◆ pbes_constelm_algorithm()

template<typename DataRewriter , typename PbesRewriter >
mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::pbes_constelm_algorithm ( const DataRewriter &  datar,
const PbesRewriter &  pbesr 
)
inline

Constructor.

Parameters
datarA data rewriter
pbesrA PBES rewriter

Definition at line 817 of file constelm.h.

Member Function Documentation

◆ concat()

template<typename DataRewriter , typename PbesRewriter >
template<typename E >
std::list< E > mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::concat ( const std::list< E >  a,
const std::list< E >  b 
)
inlineprotected

Definition at line 805 of file constelm.h.

◆ print_condition()

template<typename DataRewriter , typename PbesRewriter >
std::string mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::print_condition ( const edge e,
const vertex u,
const pbes_expression value 
)
inlineprotected

Definition at line 786 of file constelm.h.

◆ print_edge_update()

template<typename DataRewriter , typename PbesRewriter >
std::string mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::print_edge_update ( const edge e,
const vertex u,
const vertex v 
)
inlineprotected

Definition at line 777 of file constelm.h.

◆ print_edges()

template<typename DataRewriter , typename PbesRewriter >
std::string mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::print_edges ( )
inlineprotected

Logs the edges of the dependency graph.

Definition at line 748 of file constelm.h.

◆ print_evaluation_failure()

template<typename DataRewriter , typename PbesRewriter >
std::string mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::print_evaluation_failure ( const edge e,
const vertex u 
)
inlineprotected

Definition at line 795 of file constelm.h.

◆ print_todo_list()

template<typename DataRewriter , typename PbesRewriter >
std::string mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::print_todo_list ( const std::deque< propositional_variable > &  todo)
inlineprotected

Definition at line 761 of file constelm.h.

◆ print_vertices()

template<typename DataRewriter , typename PbesRewriter >
std::string mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::print_vertices ( ) const
inlineprotected

Logs the vertices of the dependency graph.

Definition at line 737 of file constelm.h.

◆ redundant_parameters()

template<typename DataRewriter , typename PbesRewriter >
std::map< propositional_variable, std::vector< data::variable > > mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::redundant_parameters ( ) const
inline

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

Returns
The removed parameters

Definition at line 823 of file constelm.h.

◆ run()

template<typename DataRewriter , typename PbesRewriter >
void mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::run ( pbes p,
bool  compute_conditions = false,
bool  check_quantifiers = true 
)
inline

Runs the constelm algorithm.

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

Definition at line 844 of file constelm.h.

Member Data Documentation

◆ m_data_rewriter

template<typename DataRewriter , typename PbesRewriter >
const DataRewriter& mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::m_data_rewriter
protected

Compares data expressions for equality.

Definition at line 402 of file constelm.h.

◆ m_edges

template<typename DataRewriter , typename PbesRewriter >
edge_map mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::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 731 of file constelm.h.

◆ m_pbes_rewriter

template<typename DataRewriter , typename PbesRewriter >
const PbesRewriter& mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::m_pbes_rewriter
protected

Compares data expressions for equality.

Definition at line 405 of file constelm.h.

◆ m_redundant_parameters

template<typename DataRewriter , typename PbesRewriter >
std::map<core::identifier_string, std::vector<std::size_t> > mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::m_redundant_parameters
protected

The redundant parameters.

Definition at line 734 of file constelm.h.

◆ m_vertices

template<typename DataRewriter , typename PbesRewriter >
vertex_map mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::m_vertices
protected

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

Definition at line 727 of file constelm.h.


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