action_label_string.h

Go to the documentation of this file.

// Author(s): Jan Friso Groote
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef MCRL2_LTS_ACTION_LABEL_STRING_H
#define MCRL2_LTS_ACTION_LABEL_STRING_H
 
#include <set>
#include "mcrl2/utilities/exception.h"
#include "mcrl2/utilities/text_utility.h"
 
namespace mcrl2
{
namespace lts
{
 
class action_label_string: public std::string
{
  public:
 
    /* \brief Default constructor. The label will contain the default string.
     */
    action_label_string()
    {}
 
    action_label_string(const action_label_string& )=default;
 
    action_label_string& operator=(const action_label_string& )=default;
 
    /* \brief A constructor, where the string s is taken to become the action label.
     */
    explicit action_label_string(const std::string& s):std::string(sort_multiactions(s))
    {}
 
    /* \brief An auxiliary function to hide actions. Makes a best-effort attempt at
              parsing the string as an mCRL2 multi-action and hiding the actions
              with a name in string_vector. The format is assumed to be a1(args1)|...|an(argsn),
              and each action ai that occurs in string_vector will be renamed to tau. 
              If all actions are hidden, the resulting
              action name will be "tau". The effects of this operation on action 
              labels that are not generated by the pretty printer are undefined. */
    void hide_actions(const std::vector<std::string>& string_vector)
    {
      std::string ns;                    // New label after hiding.
      std::string::iterator b = begin(); // Start position of current action.
      std::string::iterator c = begin(); // End position of current action.
      while (c != end())
      {
        std::string a;
        // Parse action name into a
        while (c != end() && *c != '(' && *c != '|')
        {
          a.append(1, *c++);
        }
        // Skip over parameters of a, if any
        if (c != end() && *c == '(')
        {
          std::size_t nd = 0;
          do 
          {
            switch (*c++)
            {
              case '(': ++nd; break;
              case ')': --nd; break;
            }
          }
          while (nd > 0 && c != end());
        }
        // Search for the next occurrence of "|" or the end of the string. This is the end of the current action. 
        while (c != end() && *c != '|')
        {
          ++c;
        }
        // Add the appropriate action to the new action label string
        if (std::find(string_vector.begin(), string_vector.end(), a) == string_vector.end())
        {
          // This action is not hidden. 
          if (!ns.empty())
          {
            ns.append("|");
          }
          ns.append(b, c);
        }
        // Skip the multi-action operator, if any
        if (c != end() && *c == '|')
        {
          ++c;
        }
        // The start of the next action is pointed to by c.
        b = c;
      }
      if (ns.empty())
      {
        assign(tau_action());
      }
      else
      {
        assign(ns);
      }
    }
 
    /* \brief A comparison operator comparing the action_label_strings in the same way as strings.
    */
    bool operator<(const action_label_string& l) const
    {
      return std::string(*this)<std::string(l);
    }
 
    /* \brief The action label string that represents the internal action.
    */
    static const action_label_string& tau_action()
    {
      static action_label_string tau_action("tau");
      return tau_action;
    }
 
  protected:
    static std::string sort_multiactions(const std::string& s) 
    {
      // Split this multiaction in actions a1(...)  , a2(...), a3(...)
      static std::multiset<std::string> split_actions;  // Make a static variable to avoid this multiset being created often. 
      assert(split_actions.empty());
      size_t nested_bracket_counter=0;
      size_t start_of_current_action=0;
      for(size_t i=0; i<s.size(); ++i)
      {
        const char c=s[i];
        if (c==')')
        { if (nested_bracket_counter==0)
          {
            throw mcrl2::runtime_error("The transition label is not a proper multiaction (1): " + s);
          }
          else 
          {
            nested_bracket_counter--;
          }
        }
        else if (c=='(')
        {
          nested_bracket_counter++;
        }
        else if (c=='|' && nested_bracket_counter==0)
        {
          split_actions.insert(s.substr(start_of_current_action,i-start_of_current_action));
          start_of_current_action=i+1;
        }
      }
      if (start_of_current_action==s.size()) // In this case the multiaction ends with a "|".
      {
        throw mcrl2::runtime_error("The transition label is not a proper multiaction (2): " + s);
      }
      if (split_actions.size()==0)   // No actions were split off. No 
      {
        // This is not a multiaction. 
        return s;
      }
      split_actions.insert(s.substr(start_of_current_action,s.size()-start_of_current_action));
      std::string result;
      for(const std::string& s: split_actions)
      {
        if (result.size()>0)
        {
          result.append("|");
        }
        result.append(s);
      }
      split_actions.clear();
      return result;
    }
};
 
/* \brief A pretty print operator on action labels, returning it as a string.
*/
inline std::string pp(const action_label_string& l)
{
  return l;
}
 
} // namespace lts
} // namespace mcrl2
 
namespace std
{
 
template<>
struct hash< mcrl2::lts::action_label_string >
{
  std::size_t operator()(const mcrl2::lts::action_label_string& as) const
  {
    hash<std::string> hasher;
    return hasher(as);
  }
};
 
} // namespace std
 
 
#endif