LCOV - code coverage report
Current view: top level - lps/include/mcrl2/lps - lpsparunfoldlib.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 7 7 100.0 %
Date: 2020-09-16 00:45:56 Functions: 6 6 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Frank Stappers
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file lpsparunfold/lpsparunfoldlib.h
      10             : /// \brief Unfold process parameters in mCRL2 process specifications.
      11             : 
      12             : #ifndef MCRL2_LPS_LPSPARUNFOLDLIB_H
      13             : //Fileinfo
      14             : #define MCRL2_LPS_LPSPARUNFOLDLIB_H
      15             : 
      16             : #include "mcrl2/data/representative_generator.h"
      17             : #include "mcrl2/lps/stochastic_specification.h"
      18             : 
      19             : namespace lspparunfold
      20             : {
      21           6 :   struct unfold_cache_element
      22             :   {
      23             :     mcrl2::data::basic_sort cached_fresh_basic_sort;
      24             :     mcrl2::data::function_symbol cached_case_function;
      25             :     mcrl2::data::function_symbol cached_determine_function;
      26             :     mcrl2::data::function_symbol_vector cached_k;
      27             :     mcrl2::data::function_symbol_vector cached_projection_functions;
      28             : 
      29             :     //mcrl2::data::function_symbol_vector elements_of_new_sorts;
      30             :     //mcrl2::data::data_equation_vector data_equations;
      31             :   };
      32             : } // namespace lspparunfold
      33             : 
      34             : class lpsparunfold
      35             : {
      36             :   public:
      37             : 
      38             :     /** \brief  Constructor for lpsparunfold algorithm.
      39             :       * \param[in] spec which is a valid mCRL2 process specification.
      40             :       * \param[in,out] cache Cache to store information for reuse.
      41             :       * \param[in] add_distribution_laws If true, additional rewrite rules are introduced.
      42             :       * \post   The content of mCRL2 process specification analysed for useful information and class variables are set.
      43             :       **/
      44             :     lpsparunfold(mcrl2::lps::stochastic_specification spec,
      45             :         std::map< mcrl2::data::sort_expression , lspparunfold::unfold_cache_element > *cache,
      46             :         bool add_distribution_laws=false
      47             :     );
      48             : 
      49             : 
      50             :     /** \brief  Destructor for lpsparunfold algorithm.
      51             :       **/
      52           1 :     ~lpsparunfold() {};
      53             : 
      54             :     /** \brief  Applies lpsparunfold algorithm on a process parameter an mCRL2 process specification .
      55             :       * \param[in] parameter_at_index An integer value that represents the index value of an process parameter.
      56             :       * \post   The process parameter at index parameter_at_index is unfolded in the mCRL process specification.
      57             :       * \return The process specification in which the process parameter at parameter_at_index is unfolded.
      58             :     **/
      59             :     mcrl2::lps::stochastic_specification algorithm(std::size_t parameter_at_index);
      60             : 
      61             :   private:
      62             :     /// set of identifiers to use during fresh variable generation
      63             :     mcrl2::data::set_identifier_generator m_identifier_generator;
      64             : 
      65             :     std::map< mcrl2::data::sort_expression , lspparunfold::unfold_cache_element >* m_cache;
      66             : 
      67             :     /// \brief The sort of the process parameter that needs to be unfold.
      68             :     mcrl2::data::sort_expression m_unfold_process_parameter;
      69             : 
      70             :     /// \brief The name of the process parameter that needs to be unfold.
      71             :     std::string unfold_parameter_name;
      72             : 
      73             :     /// \brief The data_specification used for manipulation
      74             :     mcrl2::data::data_specification m_data_specification;
      75             : 
      76             :     /// a generator for default data expressions of a give sort;
      77             :     mcrl2::data::representative_generator m_representative_generator;
      78             : 
      79             :     /// \brief The linear process used for manipulation
      80             :     mcrl2::lps::stochastic_linear_process m_lps;
      81             : 
      82             :     /// \brief The global variables of the specification
      83             :     std::set< mcrl2::data::variable > m_glob_vars;
      84             : 
      85             :     /// \brief The initialization of a linear process used for manipulation
      86             :     mcrl2::lps::stochastic_process_initializer m_init_process;
      87             : 
      88             :     /// \brief The initialization of a linear process
      89             :     mcrl2::process::action_label_list m_action_label_list;
      90             : 
      91             :     /// \brief The fresh sort of the unfolded process parameter used the case function.
      92             :     mcrl2::data::basic_sort fresh_basic_sort;
      93             : 
      94             :     /// \brief The set of sort names occurring in the process specification.
      95             :     std::set<mcrl2::core::identifier_string> sort_names;
      96             : 
      97             :     /// \brief The set of constructor and mapping names occurring in the process specification.
      98             :     std::set<mcrl2::core::identifier_string> mapping_and_constructor_names;
      99             : 
     100             :     /// \brief Mapping of the unfold process parameter to a vector process parameters.
     101             :     std::map<mcrl2::data::variable, mcrl2::data::variable_vector > proc_par_to_proc_par_inj;
     102             : 
     103             :     /// \brief Boolean to indicate if additional distribution laws need to be generated.
     104             :     bool m_add_distribution_laws;
     105             : 
     106             :     /** \brief  Generates a fresh basic sort given an string.
     107             :       * \param  str a string value. The value is used to generate a fresh
     108             :       *         basic sort.
     109             :       * \post   A fresh basic sort is generated, for which the name is unique
     110             :       *         with respect to the set of sort names (sort_names).
     111             :       * \return A fresh basic sort.
     112             :     **/
     113             :     mcrl2::data::basic_sort generate_fresh_basic_sort(const std::string& str);
     114             : 
     115             :     /** \brief  Generates a fresh name for a constructor or mapping.
     116             :       * \param  str a string value. The value is used to generate a fresh
     117             :       *         name for a constructor or mapping.
     118             :       * \post   A fresh name for a constructor or mapping is generated, for
     119             :       *         which the name is unique with respect to the set of mapping
     120             :       *         and constructors  (mapping_and_constructor_names).
     121             :       * \return A fresh name for a constructor or mapping.
     122             :     **/
     123             :     mcrl2::core::identifier_string generate_fresh_constructor_and_mapping_name(std::string str);
     124             : 
     125             :     /** \brief  Creates the case function.
     126             :       * \param  k a integer value. The value represents the number of
     127             :       *         constructors of the unfolded process parameter.
     128             :       * \return A function that returns the corresponding constructor given the
     129             :       *         case selector and constructors.
     130             :     **/
     131             :     mcrl2::data::function_symbol create_case_function(std::size_t k);
     132             : 
     133             :     /** \brief  Creates the determine function.
     134             :       * \return A function that maps a constructor to the fresh basic sort
     135             :     **/
     136             :     mcrl2::data::function_symbol create_determine_function();
     137             : 
     138             :     /** \brief  Creates projection functions for the unfolded process parameter.
     139             :       * \param  k a integer value. The value represents the number of
     140             :       *         constructors of the unfolded process parameter.
     141             :       * \return A function that returns the projection functions for the
     142             :       *         constructor of the unfolded process parameter.
     143             :     **/
     144             :     mcrl2::data::function_symbol_vector create_projection_functions(mcrl2::data::function_symbol_vector k);
     145             : 
     146             :     /** \brief  Creates the needed equations for the unfolded process parameter. The equations are added to m_data_specification.
     147             :       * \param  projection_functions a vector with projection functions.
     148             :       * \param  case_function the case function.
     149             :       * \param  elements_of_new_sorts set of fresh sorts.
     150             :       * \param  affected_constructors vector of affected constructors.
     151             :       * \param  determine_function the determine function.
     152             :       * \return A set of equations for the unfolded process parameter.
     153             :     **/
     154             :     void create_data_equations(
     155             :       const mcrl2::data::function_symbol_vector& projection_functions,
     156             :       const mcrl2::data::function_symbol& case_function,
     157             :       mcrl2::data::function_symbol_vector elements_of_new_sorts,
     158             :       const mcrl2::data::function_symbol_vector& affected_constructors,
     159             :       const mcrl2::data::function_symbol& determine_function);
     160             : 
     161             :     /** \brief  Determines the constructors that are affected with the unfold
     162             :       *         process parameter.
     163             :       * \return The constructors that are affected with the unfold
     164             :       *         process parameter
     165             :     **/
     166             :     mcrl2::data::function_symbol_vector determine_affected_constructors();
     167             : 
     168             :     /** \brief  Creates a set of constructors for the fresh basic sort
     169             :       * \return The constructors that are created for the fresh basic sort
     170             :     **/
     171             :     mcrl2::data::function_symbol_vector new_constructors(mcrl2::data::function_symbol_vector k);
     172             : 
     173             :     /** \brief  Generates a process parameter name given an string.
     174             :       * \param str a string value. The value is used to generate a fresh
     175             :       *         process parameter name.
     176             :       * \param process_parameter_names The context to use for generating fresh names.
     177             :       * \post   A fresh process parameter name is generated, which has an unique name
     178             :       *         with respect to the set of process parameters (process_parameter_names).
     179             :       * \return A fresh process parameter name.
     180             :     **/
     181             :     mcrl2::core::identifier_string generate_fresh_process_parameter_name(std::string str, std::set<mcrl2::core::identifier_string>& process_parameter_names);
     182             : 
     183             :     /** \brief  Get the sort of the process parameter at given index
     184             :       * \param  parameter_at_index The index of the parameter for which the sort must be obtained.
     185             :       * \return the sort of the process parameter at given index.
     186             :     **/
     187             :     mcrl2::data::sort_expression sort_at_process_parameter_index(std::size_t parameter_at_index);
     188             : 
     189             :     /** \brief  substitute function for replacing process parameters with unfolded process parameters functions.
     190             :       * \return substitute function for replacing process parameters with unfolded process parameters functions.
     191             :     **/
     192             :     std::map<mcrl2::data::variable, mcrl2::data::data_expression> parameter_substitution(
     193             :       std::map<mcrl2::data::variable, mcrl2::data::variable_vector > proc_par_to_proc_par_inj,
     194             :       mcrl2::data::function_symbol_vector k,
     195             :       const mcrl2::data::function_symbol& case_function);
     196             : 
     197             :     /** \brief unfolds a data expression into a vector of process parameters
     198             :       * \param  de the data expression
     199             :       * \param  determine_function the determine function
     200             :       * \param  pi the projection functions
     201             :       * \return The following vector: < det(de), pi_0(de), ... ,pi_n(de) >
     202             :     **/
     203             :     mcrl2::data::data_expression_vector unfold_constructor(
     204             :       const mcrl2::data::data_expression& de,
     205             :       const mcrl2::data::function_symbol& determine_function,
     206             :       mcrl2::data::function_symbol_vector pi);
     207             : 
     208             :     /** \brief substitute unfold process parameter in the linear process
     209             :       * \param  case_function the case function
     210             :       * \param  affected_constructors vector of affected constructors
     211             :       * \param  determine_function the determine function
     212             :       * \param  parameter_at_index the parameter index
     213             :       * \param  pi the projection functions
     214             :       * \return a new linear process in which the process parameter at given index is unfolded
     215             :     **/
     216             :     mcrl2::lps::stochastic_linear_process update_linear_process(
     217             :       const mcrl2::data::function_symbol& case_function,
     218             :       mcrl2::data::function_symbol_vector affected_constructors,
     219             :       const mcrl2::data::function_symbol& determine_function,
     220             :       std::size_t parameter_at_index,
     221             :       const mcrl2::data::function_symbol_vector& pi);
     222             : 
     223             :     /** \brief substitute unfold process parameter in the initialization of the linear process
     224             :       * \param  determine_function the determine function
     225             :       * \param  parameter_at_index the parameter index
     226             :       * \param  pi the projection functions
     227             :       * \return a new initialization for the linear process in which the process parameter at given index is unfolded
     228             :     **/
     229             :     mcrl2::lps::stochastic_process_initializer update_linear_process_initialization(
     230             :       const mcrl2::data::function_symbol& determine_function,
     231             :       std::size_t parameter_at_index,
     232             :       const mcrl2::data::function_symbol_vector& pi);
     233             : 
     234             :     /** \brief Create distribution rules for distribution_functions over case_functions
     235             :     **/
     236             :     mcrl2::data::data_equation create_distribution_law_over_case(
     237             :       const mcrl2::data::function_symbol& function_for_distribution,
     238             :       const mcrl2::data::function_symbol& case_function,
     239             :       const bool add_case_function_to_data_type);
     240             : 
     241             :     void generate_case_functions(
     242             :       mcrl2::data::function_symbol_vector elements_of_new_sorts,
     243             :       const mcrl2::data::function_symbol& case_function);
     244             : 
     245          44 :     static bool char_filter(char c)
     246             :     {
     247             :       // Put unwanted characters here
     248          44 :       return c==' ' || c==':' || c==',' || c=='|'
     249          44 :              || c=='>' || c=='[' || c==']' || c=='@'
     250          42 :              || c=='.' || c=='{' || c=='}' || c=='#'
     251          86 :              || c=='%' || c=='&' || c=='*' || c=='!'
     252             :              ;
     253             :     }
     254             :     /** \brief Add a new equation to m_data_specification. 
     255             :     **/
     256             :     void add_new_equation(const mcrl2::data::data_expression& lhs, const mcrl2::data::data_expression& rhs);
     257             : 
     258             :     /** \brief Create a mapping from function symbols to a list of fresh variables that can act as its arguments 
     259             :     **/
     260             :     std::map<mcrl2::data::function_symbol, mcrl2::data::data_expression_vector> 
     261             :               create_arguments_map(const mcrl2::data::function_symbol_vector& functions);
     262             : 
     263             :     // Applies 'process unfolding' to a sequence of summands.
     264             :     void unfold_summands(mcrl2::lps::stochastic_action_summand_vector& summands, const mcrl2::data::function_symbol& determine_function, const mcrl2::data::function_symbol_vector& pi);
     265             : };
     266             : 
     267             : 
     268             : 
     269             : #endif

Generated by: LCOV version 1.13