LCOV - code coverage report
Current view: top level - lps/include/mcrl2/lps/detail - specification_property_map.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 102 119 85.7 %
Date: 2024-03-08 02:52:28 Functions: 20 21 95.2 %
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/detail/specification_property_map.h
      10             : /// \brief A property map containing properties of an LPS specification.
      11             : 
      12             : #ifndef MCRL2_LPS_DETAIL_SPECIFICATION_PROPERTY_MAP_H
      13             : #define MCRL2_LPS_DETAIL_SPECIFICATION_PROPERTY_MAP_H
      14             : 
      15             : #include "mcrl2/data/detail/data_property_map.h"
      16             : #include "mcrl2/lps/specification.h"
      17             : #include <boost/algorithm/string/split.hpp>
      18             : #include <boost/algorithm/string/trim.hpp>
      19             : 
      20             : namespace mcrl2
      21             : {
      22             : 
      23             : namespace lps
      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>summand_count               </td><td>The number of summands                      </td><td>NUMBER                                </td></tr>
      33             : /// <tr><td>tau_summand_count           </td><td>The number of tau summands                  </td><td>NUMBER                                </td></tr>
      34             : /// <tr><td>delta_summand_count         </td><td>The number of delta summands                </td><td>NUMBER                                </td></tr>
      35             : /// <tr><td>declared_free_variables     </td><td>The declared free variables                 </td><td>NAME:SORT; ... ; NAME:SORT            </td></tr>
      36             : /// <tr><td>declared_free_variable_names</td><td>The names of the declared free variables    </td><td>NAME; ... ; NAME                      </td></tr>
      37             : /// <tr><td>declared_variable_count     </td><td>The number of declared free variables       </td><td>NUMBER                                </td></tr>
      38             : /// <tr><td>used_free_variables         </td><td>The used free variables                     </td><td>NAME:SORT; ... ; NAME:SORT            </td></tr>
      39             : /// <tr><td>used_free_variables_names   </td><td>The names of the used free variables        </td><td>NAME; ... ; NAME                      </td></tr>
      40             : /// <tr><td>used_free_variable_count    </td><td>The number of used free variables           </td><td>NUMBER                                </td></tr>
      41             : /// <tr><td>process_parameters          </td><td>The process parameters                      </td><td>NAME:SORT; ... ; NAME:SORT            </td></tr>
      42             : /// <tr><td>process_parameter_names     </td><td>The names of the process parameters         </td><td>NAME; ... ; NAME                      </td></tr>
      43             : /// <tr><td>process_parameter_count     </td><td>The number of process parameters            </td><td>NUMBER                                </td></tr>
      44             : /// <tr><td>declared_action_labels      </td><td>The names of the declared action labels     </td><td>NAME; ... ; NAME                      </td></tr>
      45             : /// <tr><td>declared_action_label_count </td><td>The number of declared action labels        </td><td>NUMBER                                </td></tr>
      46             : /// <tr><td>used_action_labels          </td><td>The names of the used action labels         </td><td>NAME; ... ; NAME                      </td></tr>
      47             : /// <tr><td>used_action_label_count     </td><td>The number of used action labels            </td><td>NUMBER                                </td></tr>
      48             : /// <tr><td>used_multi_actions          </td><td>The used multi-actions (sets of label names)</td><td>{NAME,...,NAME}; ... ; {NAME,...,NAME}</td></tr>
      49             : /// <tr><td>used_multi_action_count     </td><td>The number of used multi-actions            </td><td>NUMBER
      50             : /// </table>
      51             : template <typename Specification = specification>
      52             : class specification_property_map: protected mcrl2::data::detail::data_property_map<specification_property_map<Specification> >
      53             : {
      54             :   protected:
      55             : 
      56             :     // Allow base class access to protected functions
      57             :     friend class data::detail::data_property_map<specification_property_map<Specification> >;
      58             : 
      59             :     typedef data::detail::data_property_map<specification_property_map> super;
      60             : 
      61             :     using super::m_data;
      62             :     using super::names;
      63             :     using super::print;
      64             :     using super::parse_unsigned_int;
      65             :     using super::parse_set_string;
      66             :     using super::parse_set_multiset_string;
      67             : 
      68         171 :     std::string print(const process::action_label& l) const
      69             :     {
      70         171 :       return core::pp(l.name());
      71             :     }
      72             : 
      73             :     std::string print(const process::action& a) const
      74             :     {
      75             :       return process::pp(a);
      76             :     }
      77             : 
      78             :     std::string print(const deadlock& x) const
      79             :     {
      80             :       return lps::pp(x);
      81             :     }
      82             : 
      83             :     std::string print(const multi_action& x) const
      84             :     {
      85             :       return lps::pp(x);
      86             :     }
      87             : 
      88          34 :     std::string print(const std::set<std::multiset<process::action_label> >& v) const
      89             :     {
      90          34 :       std::set<std::string> elements;
      91          83 :       for (const auto& s: v)
      92             :       {
      93          49 :         elements.insert(print(s));
      94             :       }
      95          68 :       return utilities::string_join(elements, "; ");
      96          34 :     }
      97             : 
      98             :     // super class compare functions
      99             :     using super::compare;
     100             : 
     101          41 :     std::string compare_property(std::string property, std::string x, std::string y) const
     102             :     {
     103          41 :       if (property == "summand_count")
     104             :       {
     105           1 :         return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
     106             :       }
     107          40 :       else if (property == "tau_summand_count")
     108             :       {
     109           1 :         return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
     110             :       }
     111          39 :       else if (property == "delta_summand_count")
     112             :       {
     113           1 :         return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
     114             :       }
     115          38 :       else if (property == "declared_free_variables")
     116             :       {
     117           0 :         return compare(property, parse_set_string(x), parse_set_string(y));
     118             :       }
     119          38 :       else if (property == "declared_free_variable_names")
     120             :       {
     121           1 :         return compare(property, parse_set_string(x), parse_set_string(y));
     122             :       }
     123          37 :       else if (property == "declared_free_variable_count")
     124             :       {
     125           1 :         return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
     126             :       }
     127          36 :       else if (property == "used_free_variables")
     128             :       {
     129           0 :         return compare(property, parse_set_string(x), parse_set_string(y));
     130             :       }
     131          36 :       else if (property == "used_free_variable_names")
     132             :       {
     133           1 :         return compare(property, parse_set_string(x), parse_set_string(y));
     134             :       }
     135          35 :       else if (property == "used_free_variable_count")
     136             :       {
     137           1 :         return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
     138             :       }
     139          34 :       else if (property == "process_parameters")
     140             :       {
     141           0 :         return compare(property, parse_set_string(x), parse_set_string(y));
     142             :       }
     143          34 :       else if (property == "process_parameter_names")
     144             :       {
     145          26 :         return compare(property, parse_set_string(x), parse_set_string(y));
     146             :       }
     147           8 :       else if (property == "process_parameter_count")
     148             :       {
     149           2 :         return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
     150             :       }
     151           6 :       else if (property == "declared_action_labels")
     152             :       {
     153           1 :         return compare(property, parse_set_string(x), parse_set_string(y));
     154             :       }
     155           5 :       else if (property == "declared_action_label_count")
     156             :       {
     157           1 :         return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
     158             :       }
     159           4 :       else if (property == "used_action_labels")
     160             :       {
     161           1 :         return compare(property, parse_set_string(x), parse_set_string(y));
     162             :       }
     163           3 :       else if (property == "used_action_label_count")
     164             :       {
     165           1 :         return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
     166             :       }
     167           2 :       else if (property == "used_multi_actions")
     168             :       {
     169           1 :         return compare(property, parse_set_multiset_string(x), parse_set_multiset_string(y));
     170             :       }
     171           1 :       else if (property == "used_multi_action_count")
     172             :       {
     173           1 :         return compare(property, parse_unsigned_int(x), parse_unsigned_int(y));
     174             :       }
     175           0 :       return "ERROR: unknown property " + property + " encountered!";
     176             :     }
     177             : 
     178             :     //--------------------------------------------//
     179             :     // compute functions
     180             :     //--------------------------------------------//
     181             :     // TODO: the compute functions can be combined for efficiency
     182          34 :     std::set<std::multiset<process::action_label> > compute_used_multi_actions(const Specification& spec) const
     183             :     {
     184          34 :       std::set<std::multiset<process::action_label> > result;
     185          91 :       for (auto i = spec.process().action_summands().begin(); i != spec.process().action_summands().end(); ++i)
     186             :       {
     187          57 :         std::multiset<process::action_label> labels;
     188         167 :         for (const process::action& a: i->multi_action().actions())
     189             :         {
     190          53 :           labels.insert(a.label());
     191             :         }
     192          57 :         result.insert(labels);
     193             :       }
     194          34 :       return result;
     195           0 :     }
     196             : 
     197          34 :     std::set<process::action_label> compute_used_action_labels(const Specification& spec) const
     198             :     {
     199          34 :       std::set<process::action_label> result;
     200          91 :       for (auto i = spec.process().action_summands().begin(); i != spec.process().action_summands().end(); ++i)
     201             :       {
     202         167 :         for (const process::action& a: i->multi_action().actions())
     203             :         {
     204          53 :           result.insert(a.label());
     205             :         }
     206             :       }
     207          34 :       return result;
     208           0 :     }
     209             : 
     210          34 :     std::size_t compute_tau_summand_count(const Specification& spec) const
     211             :     {
     212          34 :       std::size_t result = 0;
     213          34 :       auto const& summands = spec.process().action_summands();
     214          91 :       for (auto i = summands.begin(); i != summands.end(); ++i)
     215             :       {
     216          57 :         if (i->is_tau())
     217             :         {
     218           4 :           result++;
     219             :         }
     220             :       }
     221          34 :       return result;
     222             :     }
     223             : 
     224          34 :     std::set<data::variable> compute_used_free_variables(const Specification& spec) const
     225             :     {
     226          34 :       return lps::find_free_variables(spec.process());
     227             :     }
     228             : 
     229             :   public:
     230             :     /// \brief Constructor.
     231             :     /// The strings may appear in a random order, and not all of them need to be present
     232          27 :     specification_property_map(const std::string& text)
     233          27 :       : super(text)
     234          27 :     {}
     235             : 
     236             :     /// \brief Constructor
     237             :     /// Initializes the specification_property_map with a linear process specification
     238          34 :     specification_property_map(const Specification& spec)
     239          34 :     {
     240          34 :       std::size_t                            summand_count           = spec.process().summand_count();
     241          34 :       std::size_t                            tau_summand_count       = compute_tau_summand_count(spec);
     242          34 :       std::size_t                            delta_summand_count     = spec.process().deadlock_summands().size();
     243          34 :       const std::set<data::variable>&               declared_free_variables = spec.global_variables();
     244          34 :       std::set<data::variable>               used_free_variables     = compute_used_free_variables(spec);
     245          34 :       auto const&                            params                  = spec.process().process_parameters();
     246          34 :       std::set<data::variable>               process_parameters(params.begin(), params.end());
     247          34 :       auto const&                            action_labels = spec.action_labels();
     248          34 :       std::set<process::action_label>        declared_action_labels(action_labels.begin(),action_labels.end());
     249          34 :       std::set<process::action_label>        used_action_labels      = compute_used_action_labels(spec);
     250          34 :       auto                                   used_multi_actions      = compute_used_multi_actions(spec);
     251             : 
     252          34 :       m_data["summand_count"               ] = print(summand_count);
     253          34 :       m_data["tau_summand_count"           ] = print(tau_summand_count);
     254          34 :       m_data["delta_summand_count"         ] = print(delta_summand_count);
     255          34 :       m_data["declared_free_variables"     ] = print(declared_free_variables, false);
     256          34 :       m_data["declared_free_variable_names"] = print(names(declared_free_variables), false);
     257          34 :       m_data["declared_free_variable_count"] = print(declared_free_variables.size());
     258          34 :       m_data["used_free_variables"         ] = print(used_free_variables, false);
     259          34 :       m_data["used_free_variable_names"    ] = print(names(used_free_variables), false);
     260          34 :       m_data["used_free_variable_count"    ] = print(used_free_variables.size());
     261          34 :       m_data["process_parameters"          ] = print(process_parameters, false);
     262          34 :       m_data["process_parameter_names"     ] = print(names(process_parameters), false);
     263          34 :       m_data["process_parameter_count"     ] = print(process_parameters.size());
     264          34 :       m_data["declared_action_labels"      ] = print(declared_action_labels, false);
     265          34 :       m_data["declared_action_label_count" ] = print(declared_action_labels.size());
     266          34 :       m_data["used_action_labels"          ] = print(used_action_labels, false);
     267          34 :       m_data["used_action_label_count"     ] = print(used_action_labels.size());
     268          34 :       m_data["used_multi_actions"          ] = print(used_multi_actions);
     269          34 :       m_data["used_multi_action_count"     ] = print(used_multi_actions.size());
     270          34 :     }
     271             : 
     272             :     using super::to_string;
     273             :     using super::data;
     274             :     using super::operator[];
     275             : 
     276          27 :     std::string compare(const specification_property_map<Specification>& other) const
     277             :     {
     278          27 :       return super::compare(other);
     279             :     }
     280             : 
     281             :     /// \brief Returns a textual overview of some properties of an LPS
     282           0 :     std::string info() const
     283             :     {
     284           0 :       std::ostringstream out;
     285           0 :       out << "Number of summands                  : " << (*this)["summand_count"               ] << "\n";
     286           0 :       out << "Number of tau-summands              : " << (*this)["tau_summand_count"           ] << "\n";
     287           0 :       out << "Number of declared global variables : " << (*this)["declared_free_variable_count"] << "\n";
     288           0 :       out << "Number of process parameters        : " << (*this)["process_parameter_count"     ] << "\n";
     289           0 :       out << "Number of declared action labels    : " << (*this)["declared_action_label_count" ] << "\n";
     290           0 :       out << "Number of used actions              : " << (*this)["used_action_label_count"     ] << "\n";
     291           0 :       out << "Number of used multi-actions        : " << (*this)["used_multi_action_count"     ] << "\n";
     292           0 :       return out.str();
     293           0 :     }
     294             : };
     295             : 
     296             : } // namespace detail
     297             : 
     298             : } // namespace lps
     299             : 
     300             : } // namespace mcrl2
     301             : 
     302             : #endif // MCRL2_LPS_DETAIL_SPECIFICATION_PROPERTY_MAP_H

Generated by: LCOV version 1.14