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

Generated by: LCOV version 1.13