LCOV - code coverage report
Current view: top level - lps/include/mcrl2/lps - linear_process.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 42 43 97.7 %
Date: 2024-03-08 02:52:28 Functions: 24 24 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Wieger Wesselink
       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/linear_process.h
      10             : /// \brief The class linear_process.
      11             : 
      12             : #ifndef MCRL2_LPS_LINEAR_PROCESS_H
      13             : #define MCRL2_LPS_LINEAR_PROCESS_H
      14             : 
      15             : #include "mcrl2/lps/action_summand.h"
      16             : #include "mcrl2/lps/deadlock_summand.h"
      17             : // #include "mcrl2/lps/process_initializer.h" Is not used in this file. 
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : 
      22             : namespace lps
      23             : {
      24             : 
      25             : namespace detail
      26             : {
      27             : 
      28             : // helper function for linear_process_base::linear_process_base(const atermpp::aterm_appl& lps)
      29             : template <typename Summand>
      30             : Summand make_action_summand(const data::variable_list&,
      31             :                             const data::data_expression&,
      32             :                             const multi_action&,
      33             :                             const data::assignment_list&,
      34             :                             const stochastic_distribution&
      35             :                            )
      36             : {
      37             :   throw mcrl2::runtime_error("make_action_summand is not defined!");
      38             : }
      39             : 
      40             : template <>
      41             : inline
      42             : action_summand make_action_summand<action_summand>(const data::variable_list& summation_variables,
      43             :                                                    const data::data_expression& condition,
      44             :                                                    const multi_action& a,
      45             :                                                    const data::assignment_list& assignments,
      46             :                                                    const stochastic_distribution& distribution
      47             :                                                   )
      48             : {
      49             :   (void)distribution;  // Suppress an unused variable warning. 
      50             :   assert(!distribution.is_defined());
      51             :   return action_summand(summation_variables, condition, a, assignments);
      52             : }
      53             : 
      54             : } // namespace detail
      55             : 
      56             : class linear_process; // prototype declaration
      57             : bool check_well_typedness(const linear_process& x);
      58             : 
      59             : class stochastic_linear_process; // prototype declaration
      60             : bool check_well_typedness(const stochastic_linear_process& x);
      61             : 
      62             : template <typename ActionSummand>
      63             : class linear_process_base
      64             : {
      65             :   protected:
      66             :     /// \brief The process parameters of the process
      67             :     data::variable_list m_process_parameters;
      68             : 
      69             :     /// \brief The deadlock summands of the process
      70             :     deadlock_summand_vector m_deadlock_summands;
      71             : 
      72             :     /// \brief The action summands of the process
      73             :     std::vector<ActionSummand> m_action_summands;
      74             : 
      75             :   public:
      76             :     /// \brief The action summand type
      77             :     typedef ActionSummand action_summand_type;
      78             : 
      79             :     /// \brief Constructor.
      80       14444 :     linear_process_base() = default;
      81             : 
      82             :     /// \brief Constructor.
      83        2032 :     linear_process_base(const data::variable_list& process_parameters,
      84             :                         const deadlock_summand_vector& deadlock_summands,
      85             :                         const std::vector<ActionSummand>& action_summands
      86             :                        )
      87             :        :
      88        2032 :       m_process_parameters(process_parameters),
      89        2032 :       m_deadlock_summands(deadlock_summands),
      90        2032 :       m_action_summands(action_summands)
      91        2032 :     { }
      92             : 
      93             :     /// \brief Constructor.
      94             :     /// \param lps A term.
      95             :     /// \param stochastic_distributions_allowed True when stochastic processes are allowed
      96             :     explicit linear_process_base(const atermpp::aterm_appl& lps, bool stochastic_distributions_allowed = true)
      97             :     {
      98             :       using atermpp::down_cast;
      99             :       assert(core::detail::check_term_LinearProcess(lps));
     100             :       m_process_parameters = down_cast<data::variable_list>(lps[0]);
     101             :       const auto& summands = atermpp::down_cast<atermpp::aterm_list>(lps[1]);
     102             :       for (const atermpp::aterm& summand: summands)
     103             :       {
     104             :         assert(core::detail::check_rule_LinearProcessSummand(summand));
     105             :         const auto& t = down_cast<atermpp::aterm_appl>(summand);
     106             : 
     107             :         const auto& summation_variables = down_cast<data::variable_list>(t[0]);
     108             :         const auto& condition = down_cast<data::data_expression>(t[1]);
     109             :         const auto& time = down_cast<data::data_expression>(t[3]);
     110             :         const auto& assignments = down_cast<data::assignment_list>(t[4]);
     111             :         const auto& distribution = down_cast<stochastic_distribution>(t[5]);
     112             :         if (!stochastic_distributions_allowed && distribution.is_defined())
     113             :         {
     114             :           throw mcrl2::runtime_error("Summand with stochastic distribution encountered, while this tool is not yet able to deal with stochastic distributions.");
     115             :         }
     116             :         if (down_cast<atermpp::aterm_appl>(t[2]).function() == core::detail::function_symbols::Delta)
     117             :         {
     118             :           m_deadlock_summands.push_back(deadlock_summand(summation_variables, condition, deadlock(time)));
     119             :         }
     120             :         else
     121             :         {
     122             :           assert(lps::is_multi_action(down_cast<atermpp::aterm_appl>(t[2])));
     123             :           const auto& actions = down_cast<process::action_list>(down_cast<atermpp::aterm_appl>(t[2])[0]);
     124             :           m_action_summands.push_back(detail::make_action_summand<ActionSummand>(summation_variables, condition, multi_action(actions, time), assignments, distribution));
     125             :         }
     126             :       }
     127             :     }
     128             : 
     129             :     /// \brief Returns the number of LPS summands.
     130             :     /// \return The number of LPS summands.
     131          41 :     std::size_t summand_count() const
     132             :     {
     133          41 :       return m_deadlock_summands.size() + m_action_summands.size();
     134             :     }
     135             : 
     136             :     /// \brief Returns the sequence of action summands.
     137             :     /// \return The sequence of action summands.
     138       35985 :     const std::vector<ActionSummand>& action_summands() const
     139             :     {
     140       35985 :       return m_action_summands;
     141             :     }
     142             : 
     143             :     /// \brief Returns the sequence of action summands.
     144             :     /// \return The sequence of action summands.
     145        6106 :     std::vector<ActionSummand>& action_summands()
     146             :     {
     147        6106 :       return m_action_summands;
     148             :     }
     149             : 
     150             :     /// \brief Returns the sequence of deadlock summands.
     151             :     /// \return The sequence of deadlock summands.
     152        6065 :     const deadlock_summand_vector& deadlock_summands() const
     153             :     {
     154        6065 :       return m_deadlock_summands;
     155             :     }
     156             : 
     157             :     /// \brief Returns the sequence of deadlock summands.
     158             :     /// \return The sequence of deadlock summands.
     159        3973 :     deadlock_summand_vector& deadlock_summands()
     160             :     {
     161        3973 :       return m_deadlock_summands;
     162             :     }
     163             : 
     164             :     /// \brief Returns the sequence of process parameters.
     165             :     /// \return The sequence of process parameters.
     166       18609 :     const data::variable_list& process_parameters() const
     167             :     {
     168       18609 :       return m_process_parameters;
     169             :     }
     170             : 
     171             :     /// \brief Returns the sequence of process parameters.
     172             :     /// \return The sequence of process parameters.
     173        5218 :     data::variable_list& process_parameters()
     174             :     {
     175        5218 :       return m_process_parameters;
     176             :     }
     177             : 
     178             :     /// \brief Returns true if time is available in at least one of the summands.
     179             :     /// \return True if time is available in at least one of the summands.
     180         316 :     bool has_time() const
     181             :     {
     182        1126 :       for (auto i = m_action_summands.begin(); i != m_action_summands.end(); ++i)
     183             :       {
     184         821 :         if (i->has_time())
     185             :         {
     186          11 :           return true;
     187             :         }
     188             :       }
     189         457 :       for (auto i = m_deadlock_summands.begin(); i != m_deadlock_summands.end(); ++i)
     190             :       {
     191         152 :         if (i->deadlock().has_time())
     192             :         {
     193           0 :           return true;
     194             :         }
     195             :       }
     196         305 :       return false;
     197             :     }
     198             : };
     199             : 
     200             : /// \brief linear process.
     201             : class linear_process: public linear_process_base<action_summand>
     202             : {
     203             :   typedef linear_process_base<action_summand> super;
     204             : 
     205             :   public:
     206             :     /// \brief Constructor.
     207         474 :     linear_process() = default;
     208             : 
     209             :     /// \brief Constructor.
     210         141 :     linear_process(const data::variable_list& process_parameters,
     211             :                    const deadlock_summand_vector& deadlock_summands,
     212             :                    const action_summand_vector& action_summands
     213             :                   )
     214         141 :       : super(process_parameters, deadlock_summands, action_summands)
     215         141 :     { }
     216             : 
     217             :     /// \brief Constructor.
     218             :     /// \param lps A term
     219             :     explicit linear_process(const atermpp::aterm_appl& lps, bool = false)
     220             :       : super(lps, false)
     221             :     { }
     222             : };
     223             : 
     224             : /// \brief Conversion to aterm_appl.
     225             : /// \return The action summand converted to aterm format.
     226             : template <typename ActionSummand>
     227         140 : atermpp::aterm_appl linear_process_to_aterm(const linear_process_base<ActionSummand>& p)
     228             : {
     229         140 :   atermpp::term_list<atermpp::aterm_appl> summands;
     230         172 :   for (auto i = p.deadlock_summands().rbegin(); i != p.deadlock_summands().rend(); ++i)
     231             :   {
     232          32 :     atermpp::aterm_appl s = deadlock_summand_to_aterm(*i);
     233          32 :     summands.push_front(s);
     234             :   }
     235         273 :   for (auto i = p.action_summands().rbegin(); i != p.action_summands().rend(); ++i)
     236             :   {
     237         133 :     atermpp::aterm_appl s = action_summand_to_aterm(*i);
     238         133 :     summands.push_front(s);
     239             :   }
     240             : 
     241             :   return atermpp::aterm_appl(core::detail::function_symbol_LinearProcess(),
     242         140 :            p.process_parameters(),
     243             :            summands
     244         280 :          );
     245         140 : }
     246             : 
     247             : //--- start generated class linear_process ---//
     248             : // prototype declaration
     249             : std::string pp(const linear_process& x);
     250             : 
     251             : /// \\brief Outputs the object to a stream
     252             : /// \\param out An output stream
     253             : /// \\param x Object x
     254             : /// \\return The output stream
     255             : inline
     256             : std::ostream& operator<<(std::ostream& out, const linear_process& x)
     257             : {
     258             :   return out << lps::pp(x);
     259             : }
     260             : //--- end generated class linear_process ---//
     261             : 
     262             : /// \brief Test for a linear_process expression
     263             : /// \param x A term
     264             : /// \return True if \a x is a linear process expression
     265             : inline
     266             : bool is_linear_process(const atermpp::aterm_appl& x)
     267             : {
     268             :   return x.function() == core::detail::function_symbols::LinearProcess;
     269             : }
     270             : 
     271             : // template function overloads
     272             : std::set<data::variable> find_all_variables(const lps::linear_process& x);
     273             : std::set<data::variable> find_free_variables(const lps::linear_process& x);
     274             : std::set<process::action_label> find_action_labels(const lps::linear_process& x);
     275             :  
     276             : } // namespace lps
     277             : 
     278             : } // namespace mcrl2
     279             : 
     280             : #endif // MCRL2_LPS_LINEAR_PROCESS_H

Generated by: LCOV version 1.14