#include <lpsparunfoldlib.h>
Definition at line 571 of file lpsparunfoldlib.h.
◆ case_func_replacement
◆ super
◆ lpsparunfold()
Constructor for lpsparunfold algorithm.
Constructor.
- Parameters
-
[in] | spec | which is a valid mCRL2 process specification. |
[in,out] | cache | Cache to store information for reuse. |
[in] | alt_case_placement | If true, case functions are placed at a higher level. |
[in] | 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. |
- Postcondition
- The content of mCRL2 process specification analysed for useful information and class variables are set.
Definition at line 462 of file lpsparunfoldlib.cpp.
◆ 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_index | An 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()
◆ parameter_case_function()
◆ 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.
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
-
index | The 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()
unfolds a data expression into a vector of process parameters
- Parameters
-
- Returns
- The following vector: < det(de), pi_0(de), ... ,pi_n(de) >
Definition at line 764 of file lpsparunfoldlib.cpp.
◆ unfold_summands()
◆ 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_index | the 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_index | the 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.
◆ 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
Bookkeeper for recogniser and projection functions.
Definition at line 607 of file lpsparunfoldlib.h.
◆ m_injected_parameters
◆ m_pattern_unfolder
◆ 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
◆ 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: