mCRL2
Loading...
Searching...
No Matches
mcrl2::lps::lpsparunfold Class Reference

#include <lpsparunfoldlib.h>

Inheritance diagram for mcrl2::lps::lpsparunfold:
mcrl2::lps::detail::lps_algorithm< lps::stochastic_specification >

Public Types

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

Public Member Functions

 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.
 
void algorithm (const std::size_t parameter_at_index)
 Applies lpsparunfold algorithm on a process parameter of an mCRL2 process specification .
 
- Public Member Functions inherited from mcrl2::lps::detail::lps_algorithm< lps::stochastic_specification >
 lps_algorithm (lps::stochastic_specification &spec)
 Constructor.
 
bool verbose () const
 Flag for verbose output.
 
data::data_expression next_state (const action_summand &s, const data::variable &v) const
 Applies the next state substitution to the variable v.
 
void instantiate_free_variables ()
 Attempts to eliminate the free variables of the specification, by substituting a constant value for them. If no constant value is found for one of the variables, an exception is thrown.
 
void remove_parameters (const std::set< data::variable > &to_be_removed)
 Removes formal parameters from the specification.
 
void remove_singleton_sorts ()
 Removes parameters with a singleton sort.
 
void remove_trivial_summands ()
 Removes summands with condition equal to false.
 
void remove_unused_summand_variables ()
 Removes unused summand variables.
 

Private Types

typedef detail::lps_algorithm< lps::stochastic_specificationsuper
 

Private Member Functions

case_func_replacement parameter_case_function ()
 
mcrl2::data::variable process_parameter_at (const std::size_t index)
 Get the process parameter at given index.
 
std::map< mcrl2::data::variable, mcrl2::data::data_expressionparameter_substitution ()
 substitute function for replacing process parameters with unfolded process parameters functions.
 
data::data_expression apply_function (const data::function_symbol &f, const data::data_expression &de) const
 
mcrl2::data::data_expression_vector unfold_constructor (const mcrl2::data::data_expression &de)
 unfolds a data expression into a vector of process parameters
 
void update_linear_process (std::size_t parameter_at_index)
 substitute unfold process parameter in 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
 
void unfold_summands (mcrl2::lps::stochastic_action_summand_vector &summands)
 

Private Attributes

bool m_run_before
 set to true when the algorithm has been run once; as the algorithm should run only once...
 
detail::unfold_data_manager m_datamgr
 Bookkeeper for recogniser and projection functions.
 
detail::pattern_match_unfolder m_pattern_unfolder
 
mcrl2::data::variable m_unfold_parameter
 The process parameter that needs to be unfold.
 
mcrl2::data::variable_vector m_injected_parameters
 The process parameters that are inserted.
 
bool m_alt_case_placement
 Boolean to indicate if alternative placement of case functions should be used.
 
bool 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.
 

Additional Inherited Members

- Protected Member Functions inherited from mcrl2::lps::detail::lps_algorithm< lps::stochastic_specification >
void sumelm_find_variables (const action_summand &s, std::set< data::variable > &result) const
 
void sumelm_find_variables (const deadlock_summand &s, std::set< data::variable > &result) const
 
void summand_remove_unused_summand_variables (SummandType &summand_)
 
- Protected Attributes inherited from mcrl2::lps::detail::lps_algorithm< lps::stochastic_specification >
lps::stochastic_specificationm_spec
 The specification that is processed by the algorithm.
 

Detailed Description

Definition at line 571 of file lpsparunfoldlib.h.

Member Typedef Documentation

◆ case_func_replacement

◆ super

Constructor & Destructor Documentation

◆ lpsparunfold()

lpsparunfold::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
[in]specwhich is a valid mCRL2 process specification.
[in,out]cacheCache to store information for reuse.
[in]alt_case_placementIf true, case functions are placed at a higher level.
[in]possibly_inconsistentIf 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.
Postcondition
The content of mCRL2 process specification analysed for useful information and class variables are set.

Definition at line 462 of file lpsparunfoldlib.cpp.

Member Function Documentation

◆ algorithm()

void lpsparunfold::algorithm ( const std::size_t  parameter_at_index)

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

Precondition
algorithm has not been called before.
Parameters
[in]parameter_at_indexAn integer value that represents the index value of an process parameter.
Postcondition
The process parameter at index parameter_at_index is unfolded in the mCRL2 process specification.

Definition at line 815 of file lpsparunfoldlib.cpp.

◆ apply_function()

data::data_expression lpsparunfold::apply_function ( const data::function_symbol f,
const data::data_expression de 
) const
private

Definition at line 750 of file lpsparunfoldlib.cpp.

◆ parameter_case_function()

lpsparunfold::case_func_replacement lpsparunfold::parameter_case_function ( )
private

Definition at line 508 of file lpsparunfoldlib.cpp.

◆ parameter_substitution()

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

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

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

Definition at line 709 of file lpsparunfoldlib.cpp.

◆ process_parameter_at()

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

Get the process parameter at given index.

Parameters
indexThe index of the parameter which must be obtained.
Returns
the process parameter at given index.

Definition at line 801 of file lpsparunfoldlib.cpp.

◆ unfold_constructor()

data::data_expression_vector lpsparunfold::unfold_constructor ( const mcrl2::data::data_expression de)
private

unfolds a data expression into a vector of process parameters

Parameters
dethe data expression
Returns
The following vector: < det(de), pi_0(de), ... ,pi_n(de) >

Definition at line 764 of file lpsparunfoldlib.cpp.

◆ unfold_summands()

void lpsparunfold::unfold_summands ( mcrl2::lps::stochastic_action_summand_vector summands)
private

Definition at line 486 of file lpsparunfoldlib.cpp.

◆ update_linear_process()

void lpsparunfold::update_linear_process ( std::size_t  parameter_at_index)
private

substitute unfold process parameter in the linear process

Parameters
parameter_at_indexthe parameter index
Postcondition
the process parameter at given index is unfolded in the the linear process

Definition at line 543 of file lpsparunfoldlib.cpp.

◆ update_linear_process_initialization()

void lpsparunfold::update_linear_process_initialization ( std::size_t  parameter_at_index)
private

substitute unfold process parameter in the initialization of the linear process

Parameters
parameter_at_indexthe parameter index
Postcondition
the initialization for the linear process is updated by unfolding the parameter at given index is unfolded

Definition at line 676 of file lpsparunfoldlib.cpp.

Member Data Documentation

◆ m_alt_case_placement

bool mcrl2::lps::lpsparunfold::m_alt_case_placement
private

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

Definition at line 617 of file lpsparunfoldlib.h.

◆ m_datamgr

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

Bookkeeper for recogniser and projection functions.

Definition at line 607 of file lpsparunfoldlib.h.

◆ m_injected_parameters

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

The process parameters that are inserted.

Definition at line 614 of file lpsparunfoldlib.h.

◆ m_pattern_unfolder

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

Definition at line 608 of file lpsparunfoldlib.h.

◆ m_run_before

bool mcrl2::lps::lpsparunfold::m_run_before
private

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

Definition at line 604 of file lpsparunfoldlib.h.

◆ m_unfold_parameter

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

The process parameter that needs to be unfold.

Definition at line 611 of file lpsparunfoldlib.h.

◆ m_unfold_pattern_matching

bool mcrl2::lps::lpsparunfold::m_unfold_pattern_matching
private

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

Definition at line 621 of file lpsparunfoldlib.h.


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