LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes/detail - pbes_property_map.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 75 77 97.4 %
Date: 2024-03-08 02:52:28 Functions: 7 7 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/pbes/detail/pbes_property_map.h
      10             : /// \brief A property map containing properties of an LPS specification.
      11             : 
      12             : #ifndef MCRL2_PBES_DETAIL_PBES_PROPERTY_MAP_H
      13             : #define MCRL2_PBES_DETAIL_PBES_PROPERTY_MAP_H
      14             : 
      15             : #include "mcrl2/data/detail/data_property_map.h"
      16             : #include "mcrl2/pbes/pbes.h"
      17             : #include <boost/algorithm/string/split.hpp>
      18             : #include <boost/algorithm/string/trim.hpp>
      19             : 
      20             : namespace mcrl2
      21             : {
      22             : 
      23             : namespace pbes_system
      24             : {
      25             : 
      26             : namespace detail
      27             : {
      28             : 
      29             : /// \brief Stores the following properties of a linear process specification:
      30             : /// <table>
      31             : /// <tr><th>property                    </th><th>description                             </th><th>format                               </th></tr>
      32             : /// <tr><td>equation_count              </td><td>The number of equation                  </td><td>NUMBER                               </td></tr>
      33             : /// <tr><td>mu_equation_count           </td><td>The number of mu equations              </td><td>NUMBER                               </td></tr>
      34             : /// <tr><td>nu_equation_count           </td><td>The number of nu equations              </td><td>NUMBER                               </td></tr>
      35             : /// <tr><td>block_nesting_depth         </td><td>The number of mu/nu alternations        </td><td>NUMBER                               </td></tr>
      36             : /// <tr><td>declared_free_variables     </td><td>The declared free variables             </td><td>PARAMLIST                            </td></tr>
      37             : /// <tr><td>declared_free_variable_names</td><td>The names of the declared free variables</td><td>NAME, ..., NAME                      </td></tr>
      38             : /// <tr><td>declared_variable_count     </td><td>The number of declared free variables   </td><td>NUMBER                               </td></tr>
      39             : /// <tr><td>used_free_variables         </td><td>The used free variables                 </td><td>PARAMLIST                            </td></tr>
      40             : /// <tr><td>used_free_variables_names   </td><td>The names of the used free variables    </td><td>NAME, ..., NAME                      </td></tr>
      41             : /// <tr><td>used_free_variable_count    </td><td>The number of used free variables       </td><td>NUMBER                               </td></tr>
      42             : /// <tr><td>binding_variables           </td><td>The binding variables                   </td><td>NAME(PARAMLIST), ..., NAME(PARAMLIST)</td></tr>
      43             : /// <tr><td>binding_variable_names      </td><td>The names of the binding variables      </td><td>NAME, ..., NAME                      </td></tr>
      44             : /// <tr><td>occurring_variables         </td><td>The occurring variables                 </td><td>NUMBER                               </td></tr>
      45             : /// <tr><td>occurring_variable_names    </td><td>The names of the occurring variables    </td><td>NAME(PARAMLIST), ..., NAME(PARAMLIST)</td></tr>
      46             : /// </table>
      47             : /// where <tt>PARAMLIST</tt> is defined as <tt>NAME:SORT, ... ,NAME:SORT</tt>.
      48             : class pbes_property_map : public mcrl2::data::detail::data_property_map< pbes_property_map >
      49             : {
      50             :   protected:
      51             : 
      52             :     // Allow base class access to protected functions
      53             :     friend class data::detail::data_property_map< pbes_property_map >;
      54             : 
      55             :     typedef data::detail::data_property_map< pbes_property_map > super;
      56             : 
      57             :     using super::print;
      58             : 
      59          77 :     std::string print(const propositional_variable& v) const
      60             :     {
      61          77 :       return pbes_system::pp(v);
      62             :     }
      63             : 
      64             :     // super class compare functions
      65             :     using super::compare;
      66             : 
      67          36 :     std::string compare_property(const std::string& property, const std::string& x, const std::string& y) const
      68             :     {
      69          36 :       if (property == "equation_count")
      70             :       {
      71           1 :         return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
      72             :       }
      73          35 :       else if (property == "mu_equation_count")
      74             :       {
      75           1 :         return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
      76             :       }
      77          34 :       else if (property == "nu_equation_count")
      78             :       {
      79           1 :         return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
      80             :       }
      81          33 :       else if (property == "block_nesting_depth")
      82             :       {
      83           0 :         return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
      84             :       }
      85          33 :       else if (property == "declared_free_variables")
      86             :       {
      87           2 :         return compare(property, parse_set_string(x), parse_set_string(y));
      88             :       }
      89          32 :       else if (property == "declared_free_variable_names")
      90             :       {
      91           2 :         return compare(property, parse_set_string(x), parse_set_string(y));
      92             :       }
      93          31 :       else if (property == "declared_variable_count")
      94             :       {
      95           1 :         return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
      96             :       }
      97          30 :       else if (property == "used_free_variables")
      98             :       {
      99           2 :         return compare(property, parse_set_string(x), parse_set_string(y));
     100             :       }
     101          29 :       else if (property == "used_free_variables_names")
     102             :       {
     103           2 :         return compare(property, parse_set_string(x), parse_set_string(y));
     104             :       }
     105          28 :       else if (property == "used_free_variable_count")
     106             :       {
     107           1 :         return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
     108             :       }
     109          27 :       else if (property == "binding_variables")
     110             :       {
     111          44 :         return compare(property, parse_set_string(x), parse_set_string(y));
     112             :       }
     113           5 :       else if (property == "binding_variable_names")
     114             :       {
     115           6 :         return compare(property, parse_set_string(x), parse_set_string(y));
     116             :       }
     117           2 :       else if (property == "occurring_variables")
     118             :       {
     119           2 :         return compare(property, parse_set_string(x), parse_set_string(y));
     120             :       }
     121           1 :       else if (property == "occurring_variable_names")
     122             :       {
     123           2 :         return compare(property, parse_set_string(x), parse_set_string(y));
     124             :       }
     125           0 :       return "ERROR: unknown property " + property + " encountered!";
     126             :     }
     127             : 
     128             :     //--------------------------------------------//
     129             :     // compute functions
     130             :     //--------------------------------------------//
     131             :     /// \brief Computes the number of mu and nu equations and returns them as a pair
     132          23 :     std::pair<std::size_t, std::size_t> compute_equation_counts(const pbes& p) const
     133             :     {
     134          23 :       std::size_t mu_count = 0;
     135          23 :       std::size_t nu_count = 0;
     136          62 :       for (const pbes_equation& eqn: p.equations())
     137             :       {
     138          39 :         if (eqn.symbol().is_mu())
     139             :         {
     140          15 :           mu_count++;
     141             :         }
     142             :         else
     143             :         {
     144          24 :           nu_count++;
     145             :         }
     146             :       }
     147          46 :       return std::make_pair(mu_count, nu_count);
     148             :     }
     149             : 
     150             :     // number of changes from mu to nu or vice versa
     151          23 :     std::size_t compute_block_nesting_depth(const pbes& p) const
     152             :     {
     153          23 :       std::size_t block_nesting_depth = 0;
     154          23 :       bool last_symbol_is_mu = false;
     155             : 
     156          62 :       for (auto i = p.equations().begin(); i != p.equations().end(); ++i)
     157             :       {
     158          39 :         if (i != p.equations().begin())
     159             :         {
     160          16 :           if (i->symbol().is_mu() != last_symbol_is_mu)
     161             :           {
     162          10 :             block_nesting_depth++;
     163             :           }
     164             :         }
     165          39 :         last_symbol_is_mu = i->symbol().is_mu();
     166             :       }
     167          23 :       return block_nesting_depth;
     168             :     }
     169             : 
     170             :   public:
     171             :     /// \brief Constructor.
     172             :     /// The strings may appear in a random order, and not all of them need to be present
     173          24 :     pbes_property_map(const std::string& text)
     174          24 :       : super(text)
     175          24 :     {}
     176             : 
     177             :     /// \brief Constructor
     178             :     /// Initializes the pbes_property_map with a linear process specification
     179          23 :     explicit pbes_property_map(const pbes& p)
     180          23 :     {
     181          23 :       std::pair<std::size_t, std::size_t>  equation_counts              = compute_equation_counts(p);
     182          23 :       std::size_t block_nesting_depth                                    = compute_block_nesting_depth(p);
     183          23 :       const std::set<data::variable>&           declared_free_variables      = p.global_variables();
     184          23 :       std::set<data::variable>               used_free_variables          = pbes_system::find_free_variables(p);
     185          23 :       std::set<propositional_variable>       binding_variables            = p.binding_variables();
     186          23 :       std::set<propositional_variable>       occurring_variables          = p.occurring_variables();
     187             : 
     188          23 :       m_data["equation_count"              ] = print(equation_counts.first + equation_counts.second);
     189          23 :       m_data["mu_equation_count"           ] = print(equation_counts.first);
     190          23 :       m_data["nu_equation_count"           ] = print(equation_counts.second);
     191          23 :       m_data["block_nesting_depth"         ] = print(block_nesting_depth);
     192          23 :       m_data["declared_free_variables"     ] = print(declared_free_variables, false);
     193          23 :       m_data["declared_free_variable_names"] = print(names(declared_free_variables), false);
     194          23 :       m_data["declared_variable_count"     ] = print(declared_free_variables.size());
     195          23 :       m_data["used_free_variables"         ] = print(used_free_variables, false);
     196          23 :       m_data["used_free_variables_names"   ] = print(names(used_free_variables), false);
     197          23 :       m_data["used_free_variable_count"    ] = print(used_free_variables.size());
     198          23 :       m_data["binding_variables"           ] = print(binding_variables, false);
     199          23 :       m_data["binding_variable_names"      ] = print(names(binding_variables), false);
     200          23 :       m_data["occurring_variables"         ] = print(occurring_variables, false);
     201          23 :       m_data["occurring_variable_names"    ] = print(names(occurring_variables), false);
     202          23 :     }
     203             : 
     204             :     using super::to_string;
     205             :     using super::data;
     206             : 
     207          24 :     std::string compare(const pbes_property_map& other) const
     208             :     {
     209          24 :       return super::compare(other);
     210             :     }
     211             : };
     212             : 
     213             : } // namespace detail
     214             : 
     215             : } // namespace pbes_system
     216             : 
     217             : } // namespace mcrl2
     218             : 
     219             : #endif // MCRL2_PBES_DETAIL_PBES_PROPERTY_MAP_H

Generated by: LCOV version 1.14