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 empty state labels, and strings as transition labels.
      15             :  * \author Jan Friso Groote
      16             :  */
      17             : 
      18             : 
      19             : #ifndef MCRL2_LTS_LTS_AUT_H
      20             : #define MCRL2_LTS_LTS_AUT_H
      21             : 
      22             : #include "mcrl2/lts/probabilistic_arbitrary_precision_fraction.h"
      23             : #include "mcrl2/lts/state_label_empty.h"
      24             : #include "mcrl2/lts/action_label_string.h"
      25             : #include "mcrl2/lts/probabilistic_lts.h"
      26             : 
      27             : 
      28             : namespace mcrl2
      29             : {
      30             : namespace lts
      31             : {
      32             : 
      33             : namespace detail
      34             : {
      35             : 
      36             : 
      37             : 
      38             : class lts_aut_base
      39             : {
      40             :   public:
      41             :     /** \brief Provides the type of this lts, in casu lts_aut.  */
      42          76 :     lts_type type()
      43             :     {
      44          76 :       return lts_aut;
      45             :     }
      46             : 
      47             :     /** \brief Standard swap function. */
      48           7 :     void swap(lts_aut_base& )
      49             :     {
      50             :       // Does intentionally not provide any action.
      51           7 :     }
      52             : 
      53             :     /** \brief Standard equality function.
      54             :      *  \param[in] other Value to compare with. */
      55           7 :     bool operator==(const lts_aut_base&) const
      56             :     {
      57           7 :       return true;
      58             :     }
      59             : };
      60             : 
      61             : } // end namespace detail
      62             : 
      63             : 
      64             : /** \brief A simple labelled transition format with only strings as action labels.
      65             :  *  \details This lts format corresponds to the Ceasar/Aldebaran labelled transition
      66             :  *  system format. There are no state labels, only transition labels which are plain
      67             :  *  strings.
      68             :  */
      69             : class lts_aut_t : public lts< state_label_empty, action_label_string, detail::lts_aut_base>
      70             : {
      71             :   public:
      72             : 
      73             :     /** \brief Load the labelled transition system from a file.
      74             :      *  \details If the filename is empty, the result is read from stdin.
      75             :                  The input file must be in .aut format.
      76             :      *  \param[in] filename Name of the file from which this lts is read.
      77             :      */
      78             :     void load(const std::string& filename);
      79             : 
      80             :     /** \brief Load the labelled transition system from an input stream.
      81             :      *  \details The input stream must be in .aut format.
      82             :      *  \param[in] is The input stream.
      83             :      */
      84             :     void load(std::istream& is);
      85             : 
      86             :     /** \brief Save the labelled transition system to file.
      87             :      *  \details If the filename is empty, the result is written to stdout.
      88             :      *  \param[in] filename Name of the file to which this lts is written.
      89             :      */
      90             :     void save(const std::string& filename) const;
      91             : };
      92             : 
      93             : /** \brief A simple labelled transition format with only strings as action labels.
      94             :  *  \details This lts format corresponds to the Ceasar/Aldebaran labelled transition
      95             :  *  system format. There are no state labels, only transition labels which are plain
      96             :  *  strings.
      97             :  */
      98             : class probabilistic_lts_aut_t : 
      99             :             public probabilistic_lts< state_label_empty, 
     100             :                                       action_label_string, 
     101             :                                       mcrl2::lts::probabilistic_state<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction>,
     102             :                                       detail::lts_aut_base>
     103             : {
     104             :   public:
     105             : 
     106             :     /** \brief Load the labelled transition system from a file.
     107             :      *  \details If the filename is empty, the result is read from stdin.
     108             :                  The input file must be in .aut format.
     109             :      *  \param[in] filename Name of the file from which this lts is read.
     110             :      */
     111             :     void load(const std::string& filename);
     112             : 
     113             :     /** \brief Load the labelled transition system from an input stream.
     114             :      *  \details The input stream must be in .aut format.
     115             :      *  \param[in] is The input stream.
     116             :      */
     117             :     void load(std::istream& is);
     118             : 
     119             :     /** \brief Save the labelled transition system to file.
     120             :      *  \details If the filename is empty, the result is written to stdout.
     121             :      *  \param[in] filename Name of the file to which this lts is written.
     122             :      */
     123             :     void save(const std::string& filename) const;
     124             : };
     125             : 
     126             : } // namespace lts
     127             : } // namespace mcrl2
     128             : 
     129             : #endif