LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts - lts_fsm.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 37 41 90.2 %
Date: 2019-09-14 00:54:39 Functions: 18 21 85.7 %
Legend: Lines: hit not hit

          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_fsm.h
      11             :  *
      12             :  * \brief This file contains a class that contains labelled transition systems in fsm format.
      13             :  * \details A labelled transition system in fsm 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_LTS_FSM_H
      20             : #define MCRL2_LTS_LTS_FSM_H
      21             : 
      22             : #include <string>
      23             : #include <vector>
      24             : #include "mcrl2/lts/probabilistic_arbitrary_precision_fraction.h"
      25             : #include "mcrl2/lts/probabilistic_lts.h"
      26             : #include "mcrl2/lts/action_label_string.h"
      27             : 
      28             : namespace mcrl2
      29             : {
      30             : namespace lts
      31             : {
      32             : 
      33             : /** \brief This class contains state labels for the fsm format.
      34             :     \details An fsm state label is just a vector of integers. There is an array m_state_element
      35             :              values that contains strings corresponding to the integers in the vector.
      36             :              Each integer i at position j in the vector corresponds with the string
      37             :              m_state_element_values[j][i].
      38             : */
      39        7820 : class state_label_fsm:  public std::vector < std::size_t >
      40             : {
      41             :   public:
      42             :     /** \brief Default constructor. The label becomes an empty vector.
      43             :     */
      44        2470 :     state_label_fsm()
      45        2470 :     {}
      46             : 
      47             :     /** \brief Copy constructor. */
      48        4586 :     state_label_fsm(const state_label_fsm& )=default;
      49             : 
      50             :     /** \brief Copy assignment. */
      51             :     state_label_fsm& operator=(const state_label_fsm& )=default;
      52             : 
      53             :     /** \brief Default constructor. The label is set to the vector v.
      54             :     */
      55         764 :     explicit state_label_fsm(const std::vector < std::size_t >& v):
      56         764 :       std::vector < std::size_t >(v)
      57         764 :     {}
      58             : 
      59             :     /** \brief An operator to concatenate two state labels. Fsm labels cannot be concatenated. Therefore, only 
      60             :                the first label is returned, unless empty, in which case the second is returned. */
      61           0 :     state_label_fsm operator+(const state_label_fsm& l) const
      62             :     {
      63           0 :       if ((*this).empty())
      64             :       {
      65           0 :         return l;
      66             :       }
      67           0 :       return (*this); 
      68             :     }
      69             : };
      70             : 
      71             : /** \brief Pretty print an fsm state label. */
      72             : 
      73             : inline std::string pp(const state_label_fsm& label)
      74             : {
      75             :   std::string s;
      76             :   for(const std::size_t& l: label)
      77             :   {
      78             :     s += std::to_string(l) + " ";
      79             :   }
      80             :   return s;
      81             : }
      82             : 
      83             : namespace detail
      84             : {
      85         542 : class lts_fsm_base
      86             : {
      87             :   public:
      88             :     typedef mcrl2::lts::probabilistic_state<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction> probabilistic_state;
      89             :     typedef mcrl2::lps::state_probability_pair<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction> state_probability_pair;
      90             : 
      91             :   protected:
      92             : 
      93             :     /** \brief state_element_values contain the values that can occur at the i-th
      94             :        position of a state label */
      95             :     std::vector < std::vector < std::string > > m_state_element_values;
      96             : 
      97             :     /** \brief m_parameters contain the parameters corresponding to the
      98             :                consecutive elements of a state vector. A parameter consists
      99             :                of two strings: a variable name and a string indicating its sort. */
     100             :     std::vector < std::pair < std::string, std::string > > m_parameters;
     101             : 
     102             :   public:
     103             : 
     104             :     /** \brief The lts_type of this labelled transition system. In this case lts_fsm.
     105             :         \return Returns lts_fsm as type of this transition system.
     106             :     */
     107         108 :     lts_type type() const
     108             :     {
     109         108 :       return lts_fsm;
     110             :     }
     111             : 
     112             :     /** \brief Standard swap function */
     113          52 :     void swap(lts_fsm_base& other)
     114             :     {
     115          52 :       m_state_element_values.swap(other.m_state_element_values);
     116          52 :       m_parameters.swap(other.m_parameters);
     117          52 :     }
     118             : 
     119             :     /** \brief Clear the transitions system.
     120             :      *  \details The state values, action values and transitions are
     121             :      *  reset. The number of states, actions and transitions are set to 0.
     122             :      */
     123             :     void
     124             :     clear()
     125             :     {
     126             :       m_state_element_values.clear();
     127             :       m_parameters.clear();
     128             :     }
     129             : 
     130             :     /** \brief Provides the vector of strings that correspond to the values
     131             :                of the number at position idx in a vector.
     132             :         \param[in] idx The index of the parameter.
     133             :         \return A vector containing strings representing the possible values
     134             :                 that this parameter can have.
     135             :     */
     136         168 :     const std::vector < std::string >& state_element_values(std::size_t idx) const
     137             :     {
     138         168 :       assert(idx<m_state_element_values.size());
     139         168 :       return m_state_element_values[idx];
     140             :     }
     141             : 
     142             :     /** \brief Pretty print a state value of this FSM.
     143             :         \details The label l is printed as (t1,...,tn). It uses information from the lts.
     144             :         \param[in] l  The state value to pretty print.
     145             :         \return           The pretty-printed representation of value. */
     146             :     inline std::string state_label_to_string(const state_label_fsm& l) const
     147             :     {
     148             :       std::string s;
     149             :       s = "(";
     150             :       for (std::size_t i=0; i<l.size(); ++i)
     151             :       {
     152             :         s += state_element_value(i,l[i]);
     153             :         if (i+1<l.size())
     154             :         {
     155             :           s += ",";
     156             :         }
     157             :       }
     158             :       s += ")";
     159             :       return s;
     160             :     }
     161             : 
     162             :     /** \brief Adds a string to the state element values for the idx-th
     163             :                position in a state vector. Returns the number given to this string.
     164             :         \param[in] idx The parameter index.
     165             :         \param[in] s   String to be added as value for the indicate parameter.
     166             :         \return The index for the added parameter.
     167             :     */
     168         812 :     std::size_t add_state_element_value(std::size_t idx, const std::string& s)
     169             :     {
     170         812 :       assert(idx<m_state_element_values.size());
     171         812 :       m_state_element_values[idx].push_back(s);
     172         812 :       return m_state_element_values[idx].size();
     173             :     }
     174             : 
     175             :     /** \brief Returns the element_index'th element for the parameter with index
     176             :                parameter_index.
     177             :         \details If there are no values for the parameter_index, the element_index
     178             :                  is transformed to a string, and this string is returned.
     179             :         \param[in] parameter_index The index for this parameter.
     180             :         \param[in] element_index The index to the value string corresponding to this parameter.
     181             :         \return The string corresponding to the two given indices.
     182             :     */
     183             :     std::string state_element_value(std::size_t parameter_index, std::size_t element_index) const
     184             :     {
     185             :       assert(parameter_index<m_state_element_values.size());
     186             :       if (m_state_element_values[parameter_index].size()==0)
     187             :       {
     188             :         // The domain for this parameter has no string; return the string "i"
     189             :         return std::to_string(element_index); 
     190             :       }
     191             :       assert(element_index<m_state_element_values[parameter_index].size());
     192             :       return m_state_element_values[parameter_index][element_index];
     193             :     }
     194             : 
     195             :     /** \brief Return the parameters of the state vectors stored in this LTS.
     196             :     *   \return The state parameters stored in this LTS.
     197             :     */
     198         279 :     std::vector < std::pair < std::string, std::string > > process_parameters() const
     199             :     {
     200         279 :       return m_parameters;
     201             :     }
     202             : 
     203             :     /** \brief Returns the i-th parameter of the state vectors stored in this LTS.
     204             :         \param[in] i The index of the parameter.
     205             :         \return The variable/sort of the state parameter at index i.
     206             :     */
     207         336 :     std::pair < std::string, std::string > process_parameter(std::size_t i) const
     208             :     {
     209         336 :       assert(i<m_parameters.size());
     210         336 :       return m_parameters[i];
     211             :     }
     212             : 
     213             :     /** \brief Clear the state parameters for this LTS.
     214             :     */
     215         108 :     void clear_process_parameters()
     216             :     {
     217         108 :       m_parameters.clear();
     218         108 :       m_state_element_values.clear();
     219         108 :     }
     220             : 
     221             :     /** \brief Set the state parameters for this LTS.
     222             :        \param[in] name  The variable name of the added parameter.
     223             :        \param[in] sort  The sort of the added parameter.
     224             :     */
     225         332 :     void add_process_parameter(const std::string& name, const std::string& sort)
     226             :     {
     227         332 :       assert(m_parameters.size()==m_state_element_values.size());
     228         332 :       m_parameters.push_back(std::pair<std::string,std::string>(name,sort));
     229         332 :       m_state_element_values.push_back(std::vector < std::string >());
     230         332 :     }
     231             : 
     232             : 
     233             : };
     234             : 
     235             : } // end namespace detail
     236             : 
     237             : /** \brief The class lts_fsm_t contains labelled transition systems in .fsm format.
     238             :     \details The .fsm format consists of an labelled transition system where the
     239             :              action labels are strings, and the state labels are vectors of integers.
     240             :              The integers at position i corresponds to a string, which are maintained
     241             :              in a separate vector for memory efficiency.
     242             : */
     243         104 : class lts_fsm_t : public lts< state_label_fsm, action_label_string, detail::lts_fsm_base >
     244             : {
     245             :   public:
     246             :     typedef lts< state_label_fsm, action_label_string, detail::lts_fsm_base > super;
     247             : 
     248             :     /** \brief Save the labelled transition system to file.
     249             :      *  \details If the filename is empty, the result is read from stdout.
     250             :      *  \param[in] filename Name of the file from which this lts is read.
     251             :      */
     252             :     void load(const std::string& filename);
     253             : 
     254             :     /** \brief Save the labelled transition system to file.
     255             :      *  \details If the filename is empty, the result is written to stdout.
     256             :      *  \param[in] filename Name of the file to which this lts is written.
     257             :      */
     258             :     void save(const std::string& filename) const;
     259             : };
     260             : 
     261             : /** \brief The class lts_fsm_t contains labelled transition systems in .fsm format.
     262             :     \details The .fsm format consists of an labelled transition system where the
     263             :              action labels are strings, and the state labels are vectors of integers.
     264             :              The integers at position i corresponds to a string, which are maintained
     265             :              in a separate vector for memory efficiency.
     266             : */
     267         438 : class probabilistic_lts_fsm_t : 
     268             :         public probabilistic_lts< state_label_fsm, 
     269             :                                   action_label_string, 
     270             :                                   probabilistic_state< std::size_t, probabilistic_arbitrary_precision_fraction >,
     271             :                                   detail::lts_fsm_base >
     272             : {
     273             :   public:
     274             : 
     275             :     typedef probabilistic_lts< state_label_fsm, action_label_string, probabilistic_state_t, detail::lts_fsm_base > super;
     276             : 
     277             :     /** \brief Save the labelled transition system to file.
     278             :      *  \details If the filename is empty, the result is read from stdout.
     279             :      *  \param[in] filename Name of the file from which this lts is read.
     280             :      */
     281             :     void load(const std::string& filename);
     282             : 
     283             :     /** \brief Save the labelled transition system to file.
     284             :      *  \details If the filename is empty, the result is written to stdout.
     285             :      *  \param[in] filename Name of the file to which this lts is written.
     286             :      */
     287             :     void save(const std::string& filename) const;
     288             : };
     289             : 
     290             : } // namespace lts
     291             : } // namespace mcrl2
     292             : 
     293             : #endif

Generated by: LCOV version 1.12