mcrl2::lps::lpsparunfold

Include file:

#include "mcrl2/lps/lpsparunfoldlib.h

class mcrl2::lps::lpsparunfold

Private types

type mcrl2::lps::lpsparunfold::super

typedef for detail::lps_algorithm< lps::stochastic_specification >

Public types

type mcrl2::lps::lpsparunfold::case_func_replacement

typedef for std::tuple< data::variable, std::map< data::sort_expression, data::function_symbol >, data::variable, data::data_expression_vector >

Private attributes

bool mcrl2::lps::lpsparunfold::m_alt_case_placement

Boolean to indicate if alternative placement of case functions should be used.

detail::unfold_data_manager mcrl2::lps::lpsparunfold::m_datamgr

Bookkeeper for recogniser and projection functions.

mcrl2::data::variable_vector mcrl2::lps::lpsparunfold::m_injected_parameters

The process parameters that are inserted.

detail::pattern_match_unfolder mcrl2::lps::lpsparunfold::m_pattern_unfolder

bool mcrl2::lps::lpsparunfold::m_run_before

set to true when the algorithm has been run once; as the algorithm should run only once…

mcrl2::data::variable mcrl2::lps::lpsparunfold::m_unfold_parameter

The process parameter that needs to be unfold.

bool mcrl2::lps::lpsparunfold::m_unfold_pattern_matching

Indicates whether functions defined by pattern matching that occur in the scope of a Det or pi in a state update should be unfolded.

Public member functions

void algorithm(const std::size_t parameter_at_index)

Applies lpsparunfold algorithm on a process parameter of an mCRL2 process specification .

Pre: algorithm has not been called before.

Parameters:

• parameter_at_index An integer value that represents the index value of an process parameter.

Post: The process parameter at index parameter_at_index is unfolded in the mCRL2 process specification.

lpsparunfold(lps::stochastic_specification &spec, std::map<data::sort_expression, unfold_cache_element> &cache, bool alt_case_placement = false, bool possibly_inconsistent = false, bool unfold_pattern_matching = true)

Constructor for lpsparunfold algorithm.

Constructor.

Parameters:

• spec which is a valid mCRL2 process specification.
• cache Cache to store information for reuse.
• alt_case_placement If true, case functions are placed at a higher level.
• possibly_inconsistent If true, case functions over Booleans are replaced by a disjunction of conjunctions. For this to be correct, the unfolded sort needs to satisfy some restrictions.

Post: The content of mCRL2 process specification analysed for useful information and class variables are set.

Private member functions

data::data_expression apply_function(const data::function_symbol &f, const data::data_expression &de) const

lpsparunfold::case_func_replacement parameter_case_function()

std::map<data::variable, data::data_expression> parameter_substitution()

substitute function for replacing process parameters with unfolded process parameters functions.

Returns: substitute function for replacing process parameters with unfolded process parameters functions.

data::variable process_parameter_at(const std::size_t index)

Get the process parameter at given index.

Parameters:

• index The index of the parameter which must be obtained.

Returns: the process parameter at given index.

data::data_expression_vector unfold_constructor(const mcrl2::data::data_expression &de)

unfolds a data expression into a vector of process parameters

Parameters:

• de the data expression

Returns: The following vector: < det(de), pi_0(de), … ,pi_n(de) >

void unfold_summands(mcrl2::lps::stochastic_action_summand_vector &summands)

void update_linear_process(std::size_t parameter_at_index)

substitute unfold process parameter in the linear process

Parameters:

• parameter_at_index the parameter index

Post: the process parameter at given index is unfolded in the the linear process

void update_linear_process_initialization(std::size_t parameter_at_index)

substitute unfold process parameter in the initialization of the linear process

Parameters:

• parameter_at_index the parameter index

Post: the initialization for the linear process is updated by unfolding the parameter at given index is unfolded