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 lts_dot.h
      11             :  *
      12             :  * \brief This file contains a class that contains labelled transition systems in dot format.
      13             :  * \details A labelled transition system in dot format is a transition system
      14             :  * with strings as state and transition labels.
      15             :  * \author Jan Friso Groote
      16             :  */
      17             : 
      18             : 
      19             : #ifndef MCRL2_LTS_LTS_DOT_H
      20             : #define MCRL2_LTS_LTS_DOT_H
      21             : 
      22             : #include "mcrl2/core/print.h"
      23             : #include "mcrl2/lts/probabilistic_arbitrary_precision_fraction.h"
      24             : #include "mcrl2/lts/probabilistic_lts.h"
      25             : #include "mcrl2/lts/action_label_string.h"
      26             : 
      27             : 
      28             : namespace mcrl2
      29             : {
      30             : namespace lts
      31             : {
      32             : 
      33             : /** \brief This class contains labels for states in dot format.
      34             :    \details A dot state label consists of two strings, the name of a state and a separate label.
      35             : */
      36             : class state_label_dot
      37             : {
      38             :   private:
      39             :     std::string m_state_name;
      40             :     std::string m_state_label;
      41             : 
      42             :   public:
      43             : 
      44             :     /** \brief The default constructor.
      45             :     */
      46           0 :     state_label_dot()
      47           0 :     {}
      48             : 
      49             :     /** \brief A constructor setting the name and label of this state label to the indicated values.
      50             :     */
      51           0 :     state_label_dot(const std::string& state_name,
      52           0 :                     const std::string& state_label):m_state_name(state_name),m_state_label(state_label)
      53           0 :     {}
      54             : 
      55             :     /** \brief This method sets the name of the state label to the string s.
      56             :     */
      57             :     void set_name(const std::string& s)
      58             :     {
      59             :       m_state_name=s;
      60             :     }
      61             : 
      62             :     /** \brief This method returns the string in the name field of a state label.
      63             :     */
      64           0 :     std::string name() const
      65             :     {
      66           0 :       return m_state_name;
      67             :     }
      68             : 
      69             :     /** \brief This method sets the label field of the state label to the string s.
      70             :     */
      71             :     void set_label(const std::string& s)
      72             :     {
      73             :       m_state_label=s;
      74             :     }
      75             : 
      76             :     /** \brief This method returns the label in the name field of a state label.
      77             :     */
      78           0 :     std::string label() const
      79             :     {
      80           0 :       return m_state_label;
      81             :     }
      82             : 
      83             :     /** \brief Standard comparison operator, comparing both the string in the name field, as well
      84             :               as the one in the label field.
      85             :     */
      86           0 :     bool operator ==(const state_label_dot& l) const
      87             :     {
      88           0 :       return m_state_name==l.name() && m_state_label==l.label();
      89             :     }
      90             : 
      91             :     /** \brief Standard inequality operator. Just the negation of equality
      92             :     */
      93           0 :     bool operator !=(const state_label_dot& l) const
      94             :     {
      95           0 :       return !(*this==l);
      96             :     }
      97             : };
      98             : 
      99             : /** \brief Pretty print function for a state_label_dot. Only prints the label field.
     100             : */
     101             : inline std::string pp(const state_label_dot& l)
     102             : {
     103             :   return l.label();
     104             : }
     105             : 
     106             : /** \brief A base class for the lts_dot labelled transition system.
     107             : */
     108             : 
     109             : namespace detail
     110             : {
     111             : 
     112             : class lts_dot_base
     113             : {
     114             :   public:
     115             :     /** \brief The lts_type of state_label_dot. In this case lts_dot.
     116             :     */
     117             :     lts_type type() const
     118             :     {
     119             :       return lts_dot;
     120             :     }
     121             : 
     122             :     /** \brief The standard swap function.
     123             :     */
     124             :     void swap(lts_dot_base&)
     125             :     {
     126             :       // Intentionally empty.
     127             :     }
     128             : 
     129             : };
     130             : 
     131             : } // end namespace detail
     132             : 
     133             : /** \brief A class to contain labelled transition systems in graphviz format.
     134             :     \details Action labels are strings, and state labels are pairs with a name field
     135             :              and an action fields. */
     136             : class lts_dot_t : public lts< state_label_dot, action_label_string, detail::lts_dot_base >
     137             : {
     138             : 
     139             :   public:
     140             : 
     141             :     /** \brief Save the labelled transition system to a stream.
     142             :      *  \param[in] os Stream which to write the lts to.
     143             :      */
     144             :     void save(std::ostream& os) const;
     145             : 
     146             :     /** \brief Save the labelled transition system to a file.
     147             :      *  \details Throws an error when the file cannot be opened.
     148             :      *  \param[in] filename Name of the file to which this lts is written.
     149             :      */
     150             :     void save(const std::string& filename) const;
     151             : };
     152             : 
     153             : 
     154             : /** \brief A class to contain labelled transition systems in graphviz format.
     155             :     \details Action labels are strings, and state labels are pairs with a name field
     156             :              and an action fields. */
     157             : class probabilistic_lts_dot_t : 
     158             :            public probabilistic_lts< 
     159             :                      state_label_dot, 
     160             :                      action_label_string, 
     161             :                      probabilistic_state<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction>,
     162             :                      detail::lts_dot_base >
     163             : {
     164             : 
     165             :   public:
     166             : 
     167             :     /** \brief Save the labelled transition system to a stream.
     168             :      *  \param[in] os Stream which to write the lts to.
     169             :      */
     170             :     void save(std::ostream& os) const;
     171             : 
     172             :     /** \brief Save the labelled transition system to a file.
     173             :      *  \details Throws an error when the file cannot be opened.
     174             :      *  \param[in] filename Name of the file to which this lts is written.
     175             :      */
     176             :     void save(const std::string& filename) const;
     177             : };
     178             : 
     179             : 
     180             : 
     181             : } // namespace lts
     182             : } // namespace mcrl2
     183             : 
     184             : #endif