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             : 
      10             : /** \file
      11             :  *
      12             :  * \brief This file contains a class that contains labelled transition systems in aut format.
      13             :  * \details A labelled transition system in aut format is a transition system
      14             :  * with as state labels vectors of strings, and as transition labels strings.
      15             :  * \author Jan Friso Groote
      16             :  */
      17             : 
      18             : 
      19             : #ifndef MCRL2_LTS_ACTION_LABEL_STRING_H
      20             : #define MCRL2_LTS_ACTION_LABEL_STRING_H
      21             : 
      22             : #include <set>
      23             : #include "mcrl2/utilities/exception.h"
      24             : #include "mcrl2/utilities/text_utility.h"
      25             : 
      26             : namespace mcrl2
      27             : {
      28             : namespace lts
      29             : {
      30             : 
      31             : /** \brief This class contains strings to be used as values for action labels in lts's.
      32             :  *  \details These action labels are used in the aut, fsm, and dot format to represent
      33             :  *           values for the action labels in transitions. The string must have a pattern
      34             :  *           resemblinb multiactions, and these multiactions are always sorted. 
      35             :  */
      36             : class action_label_string: public std::string
      37             : {
      38             :   public:
      39             : 
      40             :     /* \brief Default constructor. The label will contain the default string.
      41             :      */
      42         456 :     action_label_string()
      43         456 :     {}
      44             : 
      45             :     /** \brief Copy constructor. */
      46       24953 :     action_label_string(const action_label_string& )=default;
      47             : 
      48             :     /** \brief Copy assignment. */
      49        1335 :     action_label_string& operator=(const action_label_string& )=default;
      50             : 
      51             :     /* \brief A constructor, where the string s is taken to become the action label.
      52             :      */
      53        5252 :     explicit action_label_string(const std::string& s):std::string(sort_multiactions(s))
      54        5252 :     {}
      55             : 
      56             :     /* \brief An auxiliary function to hide actions. Makes a best-effort attempt at
      57             :               parsing the string as an mCRL2 multi-action and hiding the actions
      58             :               with a name in string_vector. If all actions are hidden, the resulting
      59             :               action name will be "tau". The effects of this operation on action 
      60             :               labels that are not generated by the pretty printer are undefined. */
      61          30 :     void hide_actions(const std::vector<std::string>& string_vector)
      62             :     {
      63          30 :       std::string ns;                    // New label after hiding.
      64          30 :       std::string::iterator b = begin(); // Start position of current action.
      65          30 :       std::string::iterator c = begin(); // End position of current action.
      66          62 :       while (c != end())
      67             :       {
      68          32 :         std::string a;
      69             :         // Parse action name into a
      70         193 :         while (c != end() && *c != '(' && *c != '|')
      71             :         {
      72         161 :           a.append(1, *c++);
      73             :         }
      74             :         // Skip over parameters of a, if any
      75          32 :         if (c != end() && *c == '(')
      76             :         {
      77           0 :           std::size_t nd = 0;
      78             :           do 
      79             :           {
      80           0 :             switch (*c++)
      81             :             {
      82           0 :               case '(': ++nd; break;
      83           0 :               case ')': --nd; break;
      84             :             }
      85             :           }
      86           0 :           while (nd > 0 && c != end());
      87             :         }
      88             :         // Add the appropriate action to the new action label string
      89          32 :         if (std::find(string_vector.begin(), string_vector.end(), a) == string_vector.end())
      90             :         {
      91          28 :           if (!ns.empty())
      92             :           {
      93           0 :             ns.append("|");
      94             :           }
      95          28 :           ns.append(b, c);
      96             :         }
      97             :         // Skip the multi-action operator, if any
      98          32 :         if (c != end() && *c == '|')
      99             :         {
     100           2 :           ++c;
     101             :         }
     102             :         // The start of the next action is pointed to by c.
     103          32 :         b = c;
     104          32 :       }
     105          30 :       if (ns.empty())
     106             :       {
     107           2 :         assign(tau_action());
     108             :       }
     109             :       else
     110             :       {
     111          28 :         assign(ns);
     112             :       }
     113          30 :     }
     114             : 
     115             :     /* \brief A comparison operator comparing the action_label_strings in the same way as strings.
     116             :     */
     117        8010 :     bool operator<(const action_label_string& l) const
     118             :     {
     119        8010 :       return std::string(*this)<std::string(l);
     120             :     }
     121             : 
     122             :     /* \brief The action label string that represents the internal action.
     123             :     */
     124       69274 :     static const action_label_string& tau_action()
     125             :     {
     126       69274 :       static action_label_string tau_action("tau");
     127       69274 :       return tau_action;
     128             :     }
     129             :  
     130             :   protected:
     131             :     ///\brief Sort multiactions in a string.
     132             :     ///\details Take a string with a multi-action of the shape a1(...)|a2(...)|...|an(...).
     133             :     ///         Split it into different actions, and reassemble them such that the actions
     134             :     ///         are ordered. 
     135             :     ///\returns This action in which the multi-actions are ordered. 
     136        5252 :     static std::string sort_multiactions(const std::string& s) 
     137             :     {
     138             :       // Split this multiaction in actions a1(...)  , a2(...), a3(...)
     139        5252 :       static std::multiset<std::string> split_actions;  // Make a static variable to avoid this multiset being created often. 
     140        5252 :       assert(split_actions.empty());
     141        5252 :       size_t nested_bracket_counter=0;
     142        5252 :       size_t start_of_current_action=0;
     143      170368 :       for(size_t i=0; i<s.size(); ++i)
     144             :       {
     145      165116 :         const char c=s[i];
     146      165116 :         if (c==')')
     147        6859 :         { if (nested_bracket_counter==0)
     148             :           {
     149           0 :             throw mcrl2::runtime_error("The transition label is not a proper multiaction (1): " + s);
     150             :           }
     151             :           else 
     152             :           {
     153        6859 :             nested_bracket_counter--;
     154             :           }
     155             :         }
     156      158257 :         else if (c=='(')
     157             :         {
     158        6859 :           nested_bracket_counter++;
     159             :         }
     160      151398 :         else if (c=='|' && nested_bracket_counter==0)
     161             :         {
     162          14 :           split_actions.insert(s.substr(start_of_current_action,i-start_of_current_action));
     163          14 :           start_of_current_action=i+1;
     164             :         }
     165             :       }
     166        5252 :       if (start_of_current_action==s.size()) // In this case the multiaction ends with a "|".
     167             :       {
     168           0 :         throw mcrl2::runtime_error("The transition label is not a proper multiaction (2): " + s);
     169             :       }
     170        5252 :       if (split_actions.size()==0)   // No actions were split off. No 
     171             :       {
     172             :         // This is not a multiaction. 
     173        5238 :         return s;
     174             :       }
     175          14 :       split_actions.insert(s.substr(start_of_current_action,s.size()-start_of_current_action));
     176          14 :       std::string result;
     177          42 :       for(const std::string& s: split_actions)
     178             :       {
     179          28 :         if (result.size()>0)
     180             :         {
     181          14 :           result.append("|");
     182             :         }
     183          28 :         result.append(s);
     184             :       }
     185          14 :       split_actions.clear();
     186          14 :       return result;
     187          14 :     }
     188             : 
     189             : };
     190             : 
     191             : /* \brief A pretty print operator on action labels, returning it as a string.
     192             : */
     193        1657 : inline std::string pp(const action_label_string& l)
     194             : {
     195        1657 :   return l;
     196             : }
     197             : 
     198             : } // namespace lts
     199             : } // namespace mcrl2
     200             : 
     201             : namespace std
     202             : {
     203             : 
     204             : /// \brief specialization of the standard std::hash function for an action_label_string.
     205             : template<>
     206             : struct hash< mcrl2::lts::action_label_string >
     207             : {
     208       10670 :   std::size_t operator()(const mcrl2::lts::action_label_string& as) const
     209             :   {
     210             :     hash<std::string> hasher;
     211       10670 :     return hasher(as);
     212             :   }
     213             : };
     214             : 
     215             : } // namespace std
     216             : 
     217             : 
     218             : #endif
     219             : 
     220             :