lpsparunfold

Include file:

#include "mcrl2/lps/lpsparunfoldlib.h
class lpsparunfold

Private attributes

mcrl2::data::basic_sort fresh_basic_sort

The fresh sort of the unfolded process parameter used the case function.

mcrl2::process::action_label_list m_action_label_list

The initialization of a linear process.

bool m_add_distribution_laws

Boolean to indicate if additional distribution laws need to be generated.

std::map<mcrl2::data::sort_expression, lspparunfold::unfold_cache_element> *m_cache
mcrl2::data::data_specification m_data_specification

The data_specification used for manipulation.

std::set<mcrl2::data::variable> m_glob_vars

The global variables of the specification.

mcrl2::data::set_identifier_generator m_identifier_generator

set of identifiers to use during fresh variable generation

mcrl2::lps::stochastic_process_initializer m_init_process

The initialization of a linear process used for manipulation.

mcrl2::lps::stochastic_linear_process m_lps

The linear process used for manipulation.

mcrl2::data::representative_generator m_representative_generator

a generator for default data expressions of a give sort;

mcrl2::data::sort_expression m_unfold_process_parameter

The sort of the process parameter that needs to be unfold.

std::set<mcrl2::core::identifier_string> mapping_and_constructor_names

The set of constructor and mapping names occurring in the process specification.

std::map<mcrl2::data::variable, mcrl2::data::variable_vector> proc_par_to_proc_par_inj

Mapping of the unfold process parameter to a vector process parameters.

std::set<mcrl2::core::identifier_string> sort_names

The set of sort names occurring in the process specification.

std::string unfold_parameter_name

The name of the process parameter that needs to be unfold.

Public member functions

mcrl2::lps::stochastic_specification algorithm(std::size_t parameter_at_index)

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

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 mCRL process specification.

Returns: The process specification in which the process parameter at parameter_at_index is unfolded.

lpsparunfold(mcrl2::lps::stochastic_specification spec, std::map<mcrl2::data::sort_expression, lspparunfold::unfold_cache_element> *cache, bool add_distribution_laws = false)

Constructor for lpsparunfold algorithm.

Parameters:

  • spec which is a valid mCRL2 process specification.
  • cache Cache to store information for reuse.
  • add_distribution_laws If true, additional rewrite rules are introduced.

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

~lpsparunfold()

Destructor for lpsparunfold algorithm.

Private member functions

void add_new_equation(const mcrl2::data::data_expression &lhs, const mcrl2::data::data_expression &rhs)

Add a new equation to m_data_specification.

std::map<function_symbol, data_expression_vector> create_arguments_map(const mcrl2::data::function_symbol_vector &functions)

Create a mapping from function symbols to a list of fresh variables that can act as its arguments.

mcrl2::data::function_symbol create_case_function(std::size_t k)

Creates the case function.

Parameters:

  • k a integer value. The value represents the number of constructors of the unfolded process parameter.

Returns: A function that returns the corresponding constructor given the case selector and constructors.

void create_data_equations(const mcrl2::data::function_symbol_vector &projection_functions, const mcrl2::data::function_symbol &case_function, mcrl2::data::function_symbol_vector elements_of_new_sorts, const mcrl2::data::function_symbol_vector &affected_constructors, const mcrl2::data::function_symbol &determine_function)

Creates the needed equations for the unfolded process parameter. The equations are added to m_data_specification.

Parameters:

  • projection_functions a vector with projection functions.
  • case_function the case function.
  • elements_of_new_sorts set of fresh sorts.
  • affected_constructors vector of affected constructors.
  • determine_function the determine function.

Returns: A set of equations for the unfolded process parameter.

mcrl2::data::function_symbol create_determine_function()

Creates the determine function.

Returns: A function that maps a constructor to the fresh basic sort

mcrl2::data::data_equation create_distribution_law_over_case(const mcrl2::data::function_symbol &function_for_distribution, const mcrl2::data::function_symbol &case_function, const bool add_case_function_to_data_type)

Create distribution rules for distribution_functions over case_functions.

mcrl2::data::function_symbol_vector create_projection_functions(mcrl2::data::function_symbol_vector k)

Creates projection functions for the unfolded process parameter.

Parameters:

  • k a integer value. The value represents the number of constructors of the unfolded process parameter.

Returns: A function that returns the projection functions for the constructor of the unfolded process parameter.

function_symbol_vector determine_affected_constructors()

Determines the constructors that are affected with the unfold process parameter.

Returns: The constructors that are affected with the unfold process parameter

void generate_case_functions(mcrl2::data::function_symbol_vector elements_of_new_sorts, const mcrl2::data::function_symbol &case_function)
mcrl2::data::basic_sort generate_fresh_basic_sort(const std::string &str)

Generates a fresh basic sort given an string.

Parameters:

  • str a string value. The value is used to generate a fresh basic sort.

Post: A fresh basic sort is generated, for which the name is unique with respect to the set of sort names (sort_names).

Returns: A fresh basic sort.

mcrl2::core::identifier_string generate_fresh_constructor_and_mapping_name(std::string str)

Generates a fresh name for a constructor or mapping.

Parameters:

  • str a string value. The value is used to generate a fresh name for a constructor or mapping.

Post: A fresh name for a constructor or mapping is generated, for which the name is unique with respect to the set of mapping and constructors (mapping_and_constructor_names).

Returns: A fresh name for a constructor or mapping.

mcrl2::core::identifier_string generate_fresh_process_parameter_name(std::string str, std::set<mcrl2::core::identifier_string> &process_parameter_names)

Generates a process parameter name given an string.

Parameters:

  • str a string value. The value is used to generate a fresh process parameter name.
  • process_parameter_names The context to use for generating fresh names.

Post: A fresh process parameter name is generated, which has an unique name with respect to the set of process parameters (process_parameter_names).

Returns: A fresh process parameter name.

function_symbol_vector new_constructors(mcrl2::data::function_symbol_vector k)

Creates a set of constructors for the fresh basic sort.

Returns: The constructors that are created for the fresh basic sort

std::map<mcrl2::data::variable, mcrl2::data::data_expression> parameter_substitution(std::map<mcrl2::data::variable, mcrl2::data::variable_vector> proc_par_to_proc_par_inj, mcrl2::data::function_symbol_vector k, const mcrl2::data::function_symbol &case_function)

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

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

mcrl2::data::sort_expression sort_at_process_parameter_index(std::size_t parameter_at_index)

Get the sort of the process parameter at given index.

Parameters:

  • parameter_at_index The index of the parameter for which the sort must be obtained.

Returns: the sort of the process parameter at given index.

mcrl2::data::data_expression_vector unfold_constructor(const mcrl2::data::data_expression &de, const mcrl2::data::function_symbol &determine_function, mcrl2::data::function_symbol_vector pi)

unfolds a data expression into a vector of process parameters

Parameters:

  • de the data expression
  • determine_function the determine function
  • pi the projection functions

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

void unfold_summands(mcrl2::lps::stochastic_action_summand_vector &summands, const mcrl2::data::function_symbol &determine_function, const mcrl2::data::function_symbol_vector &pi)
mcrl2::lps::stochastic_linear_process update_linear_process(const mcrl2::data::function_symbol &case_function, mcrl2::data::function_symbol_vector affected_constructors, const mcrl2::data::function_symbol &determine_function, std::size_t parameter_at_index, const mcrl2::data::function_symbol_vector &pi)

substitute unfold process parameter in the linear process

Parameters:

  • case_function the case function
  • affected_constructors vector of affected constructors
  • determine_function the determine function
  • parameter_at_index the parameter index
  • pi the projection functions

Returns: a new linear process in which the process parameter at given index is unfolded

mcrl2::lps::stochastic_process_initializer update_linear_process_initialization(const mcrl2::data::function_symbol &determine_function, std::size_t parameter_at_index, const mcrl2::data::function_symbol_vector &pi)

substitute unfold process parameter in the initialization of the linear process

Parameters:

  • determine_function the determine function
  • parameter_at_index the parameter index
  • pi the projection functions

Returns: a new initialization for the linear process in which the process parameter at given index is unfolded

Private static member functions

static bool char_filter(char c)