LCOV - code coverage report
Current view: top level - lps/include/mcrl2/lps/detail - move_constants_to_substitution.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 23 23 100.0 %
Date: 2020-02-19 00:44:21 Functions: 2 2 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Jan Friso Groote 
       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 mcrl2/lps/detail/move_constants_to_substitution.h
      10             : /// \brief This file contains a function that replaces constant
      11             : ///        non trivial terms in an lps by variables, and assigns
      12             : ///        the normal forms corresponding to the variables to a
      13             : ///        substitution. The purpose of this is to avoid rewriting
      14             : ///        these non trivial constant iteratively, when for instance
      15             : ///        generating a state space. 
      16             : 
      17             : #ifndef MCRL2_LPS_MOVE_CONSTANTS_TO_SUBSTITUTION_H
      18             : #define MCRL2_LPS_MOVE_CONSTANTS_TO_SUBSTITUTION_H
      19             : 
      20             : #include "mcrl2/data/detail/move_constants_to_substitution.h"
      21             : #include "mcrl2/lps/stochastic_specification.h"
      22             : 
      23             : namespace mcrl2
      24             : {
      25             : 
      26             : namespace lps
      27             : {
      28             : 
      29             : namespace detail
      30             : {
      31             : 
      32             : 
      33             : // For an explanation see move_constants_to_substitution below.
      34             : template <class SUBSTITUTION>
      35         181 : void move_constants_to_substitution_helper(lps::stochastic_specification& spec,
      36             :                                            data::rewriter& r,
      37             :                                            SUBSTITUTION& sigma,
      38             :                                            std::unordered_map<data::data_expression, data::variable>& expression_to_variable_map,
      39             :                                            data::set_identifier_generator& identifier_generator
      40             :                                           )
      41             : {
      42         604 :   for(stochastic_action_summand& s: spec.process().action_summands())
      43             :   {
      44         846 :     process::action_vector new_actions;
      45         804 :     for(const process::action& a: s.multi_action().actions())
      46             :     {
      47         762 :       data::data_expression_vector new_parameters;
      48         699 :       for(const data::data_expression& e: a.arguments())
      49             :       {
      50         318 :         new_parameters.emplace_back(data::detail::move_constants_to_substitution(e,r,sigma,expression_to_variable_map,identifier_generator));
      51             :       }
      52         381 :       new_actions.emplace_back(a.label(),data::data_expression_list(new_parameters.begin(),new_parameters.end()));
      53             :     }
      54         846 :     lps::multi_action new_multi_action(process::action_list(new_actions.begin(), new_actions.end()),
      55         423 :                                        data::detail::move_constants_to_substitution(s.multi_action().time(),
      56             :                                                                                     r,
      57             :                                                                                     sigma,
      58             :                                                                                     expression_to_variable_map,
      59             :                                                                                     identifier_generator));
      60             : 
      61         846 :     data::assignment_vector new_assignments;
      62        1512 :     for(const data::assignment&a: s.assignments())
      63             :     {
      64        1089 :       new_assignments.emplace_back(a.lhs(),
      65             :                                    data::detail::move_constants_to_substitution(a.rhs(),r,sigma,expression_to_variable_map,identifier_generator));
      66             :     }
      67             : 
      68        1269 :     s=stochastic_action_summand(s.summation_variables(), 
      69         423 :                                 data::detail::move_constants_to_substitution(s.condition(),r,sigma,expression_to_variable_map,identifier_generator),
      70             :                                 new_multi_action,
      71             :                                 data::assignment_list(new_assignments.begin(),new_assignments.end()),
      72         423 :                                 stochastic_distribution(s.distribution().variables(),
      73         423 :                                                         data::detail::move_constants_to_substitution(s.distribution().distribution(),
      74             :                                                                                                      r,
      75             :                                                                                                      sigma,
      76             :                                                                                                      expression_to_variable_map,
      77             :                                                                                                      identifier_generator)));
      78             :   }
      79         181 : }
      80             : 
      81             : 
      82             : } // namespace detail
      83             : 
      84             : 
      85             : /// \brief Replace non trivial constants c in the lps by variables and add assignments x:=normal_form(c) to the substitution.
      86             : /// \details This operation is useful when terms in the lps are very often rewritten. Constant expressions in the lps are 
      87             : ///          brought to normal form whenever they are encountered. This happens very often when generating a state space.
      88             : ///          In the substitution they are considered a normal form, and not rewritten. This can save more than 50% of the time
      89             : ///          to generate a state space.
      90             : /// \param lpsspec A linear process specification.
      91             : /// \param r The rewriter used to calculate a normal form.
      92             : /// \param sigma The substitution into which it is stored which variables represent which terms. 
      93             : template <class SUBSTITUTION>
      94         181 : void move_constants_to_substitution(lps::stochastic_specification& spec,
      95             :                                     data::rewriter& r,
      96             :                                     SUBSTITUTION& sigma)
      97             : {
      98         362 :   std::unordered_map<data::data_expression, data::variable> expression_to_variable_map;
      99         362 :   data::set_identifier_generator identifier_generator;
     100         181 :   detail::move_constants_to_substitution_helper(spec,r,sigma,expression_to_variable_map,identifier_generator);
     101         181 : }
     102             : 
     103             : } // namespace lps
     104             : 
     105             : } // namespace mcrl2
     106             : 
     107             : #endif // MCRL2_LPS_MOVE_CONSTANTS_TO_SUBSTITUTION_H

Generated by: LCOV version 1.13