LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts - probabilistic_lts.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 37 37 100.0 %
Date: 2019-09-14 00:54:39 Functions: 28 36 77.8 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Muck van Weerdenburg, 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 probabilistic_lts.h
      11             :  *
      12             :  * \brief The file containing the core class for transition systems.
      13             :  * \details This is the LTS library's main header file. It declares all publicly
      14             :  * accessible data structures that form the interface of the library.
      15             :  * \author Muck van Weerdenburg, Jan Friso Groote
      16             :  */
      17             : 
      18             : #ifndef MCRL2_LTS_PROBABILISTIC_LTS_H
      19             : #define MCRL2_LTS_PROBABILISTIC_LTS_H
      20             : 
      21             : #include <string>
      22             : #include <vector>
      23             : #include <map>
      24             : #include <cstdio>
      25             : #include "mcrl2/lts/lts.h"
      26             : #include "mcrl2/lts/probabilistic_state.h"
      27             : 
      28             : 
      29             : namespace mcrl2
      30             : {
      31             : 
      32             : namespace lts
      33             : {
      34             : 
      35             : /** \brief A class that contains a labelled transition system.
      36             :     \details The state labels and action labels can be any type.
      37             :         Essentially, a labelled transition system consists of a
      38             :         vector of transitions. Each transition is a triple of
      39             :         three numbers <from, label, to>. For these numbers, there
      40             :         can be associated state labels (for 'from' and 'to'), and
      41             :         action labels (for 'label'). But it is also possible, that
      42             :         no state or action labels are provided. For all action labels
      43             :         it is maintained whether this action label is an internal
      44             :         'tau' action. This can be indicated for each action label
      45             :         separately. Finally, the number of states is recalled as
      46             :         a separate variable.
      47             : */
      48             : 
      49             : template < class STATE_LABEL_T, class ACTION_LABEL_T, class PROBABILISTIC_STATE_T, class LTS_BASE >
      50         682 : class probabilistic_lts: public lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE>
      51             : {
      52             :   public:
      53             : 
      54             :     typedef lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE> super;
      55             : 
      56             :     /** \brief The type of probabilistic labels.
      57             :     */
      58             :     typedef PROBABILISTIC_STATE_T probabilistic_state_t;
      59             : 
      60             :     typedef typename super::state_label_t         state_label_t        ;
      61             :     typedef typename super::action_label_t        action_label_t       ;
      62             :     typedef typename super::base_t                base_t               ;
      63             :     typedef typename super::states_size_type      states_size_type     ;
      64             :     typedef typename super::labels_size_type      labels_size_type     ;
      65             :     typedef typename super::transitions_size_type transitions_size_type;
      66             : 
      67             :   protected:
      68             : 
      69             :     std::vector<PROBABILISTIC_STATE_T> m_probabilistic_states;
      70             :     PROBABILISTIC_STATE_T m_init_probabilistic_state;
      71             : 
      72             :     /* This function is made protected to prevent its use in a probabilistic transition system */  
      73             :     states_size_type initial_state() const
      74             :     {
      75             :       return super::initial_state();
      76             :     }
      77             : 
      78             :     /* This function is made protected to prevent its use in a probabilistic transition system */  
      79         568 :     void set_initial_state(const states_size_type s)
      80             :     {
      81         568 :       super::set_initial_state(s);
      82         568 :     }
      83             : 
      84             :   public:
      85             : 
      86             :     /** \brief Creates an empty LTS.
      87             :      */
      88         675 :     probabilistic_lts()
      89         675 :     {}
      90             : 
      91             :     /** \brief Creates a copy of the supplied LTS.
      92             :      * \param[in] l The LTS to copy. */
      93           7 :     probabilistic_lts(const probabilistic_lts& l)
      94             :       : super(l),
      95           7 :         m_probabilistic_states(l.m_probabilistic_states)
      96           7 :     {}
      97             : 
      98             :     /** \brief Swap this lts with the supplied supplied LTS.
      99             :      * \param[in] l The LTS to swap. */
     100             :     void swap(probabilistic_lts& l)
     101             :     {
     102             :       super::swap(l);
     103             :       m_probabilistic_states.swap(l.m_probabilistic_states);
     104             :     }
     105             : 
     106             :     /** \brief Gets the initial state number of this LTS.
     107             :       * \return The number of the initial state of this LTS. */
     108         834 :     const PROBABILISTIC_STATE_T& initial_probabilistic_state() const
     109             :     {
     110         834 :       return m_init_probabilistic_state;
     111             :     }
     112             : 
     113             :     /** \brief Sets the probabilistic initial state number of this LTS.
     114             :      * \param[in] state The number of the state that will become the initial
     115             :      * state. */
     116         568 :     void set_initial_probabilistic_state(const PROBABILISTIC_STATE_T& state)
     117             :     {
     118             :       // Prevent that the initial state of the lts, which is not used in a probabilistic state
     119             :       // has a random value.
     120         568 :       set_initial_state(0);
     121         568 :       m_init_probabilistic_state = state;
     122         568 :     }
     123             : 
     124             : 
     125             :     /** \brief Gets the number of probabilistic states of this LTS.
     126             :      * \return The number of action labels of this LTS. */
     127        1857 :     labels_size_type num_probabilistic_states() const
     128             :     {
     129        1857 :       return m_probabilistic_states.size();
     130             :     }
     131             : 
     132             :     /** \brief Adds a probabilistic state to this LTS.
     133             :      * \details It is not checked whether this probabilistic state already exists.
     134             :      * \param[in] s The probabilistic state.
     135             :      * \return The index of the added probabilistic. */
     136        7207 :     states_size_type add_probabilistic_state(const PROBABILISTIC_STATE_T& s)
     137             :     {
     138        7207 :       const states_size_type label_index=m_probabilistic_states.size();
     139        7207 :       m_probabilistic_states.push_back(s);
     140        7207 :       return label_index;
     141             :     }
     142             : 
     143             :     /** \brief Adds a probabilistic state to this LTS and resets the state to empty.
     144             :      * \details This is more efficient than using add_probabilistic state, as this variant
     145             :      *          does not copy the probabilistic state. It is not checked whether this probabilistic state already exists.
     146             :      * \param[in] s The probabilistic state.
     147             :      * \return The index of the added probabilistic state. */
     148         477 :     states_size_type add_and_reset_probabilistic_state(PROBABILISTIC_STATE_T& s)
     149             :     {
     150         477 :       const states_size_type label_index=m_probabilistic_states.size();
     151         477 :       m_probabilistic_states.emplace_back();
     152         477 :       m_probabilistic_states.back().swap(s);
     153         477 :       return label_index;
     154             :     }
     155             : 
     156             :     /** \brief Sets the probabilistic label corresponding to some index.
     157             :      * \param[in] index The index of the state.
     158             :      * \param[in] s The new probabilistic state belonging to this index. */
     159             :     void set_probabilistic_state(const states_size_type index, const PROBABILISTIC_STATE_T& s)
     160             :     {
     161             :       assert(index<m_probabilistic_states.size());
     162             :       m_probabilistic_states[index] = s;
     163             :     }
     164             : 
     165             :     /** \brief Gets the probabilistic label of an index.
     166             :      *  \param[in] index The index of an action.
     167             :      *  \return The probabilistic state belonging to the index. */
     168        8418 :     const PROBABILISTIC_STATE_T& probabilistic_state(const states_size_type index) const
     169             :     {
     170        8418 :       assert(index < m_probabilistic_states.size());
     171        8418 :       return m_probabilistic_states[index];
     172             :     }
     173             : 
     174             :     /** \brief Clear the probabilistic states in this probabilistic transitions system.
     175             :     */
     176         122 :     void clear_probabilistic_states()
     177             :     {
     178         122 :       m_probabilistic_states.clear();
     179         122 :     }
     180             : 
     181             :     /** \brief Clear the transitions system.
     182             :      *  \details The state values, action values and transitions are
     183             :      *  reset. The number of states, actions and transitions are set to 0. */
     184         111 :     void clear()
     185             :     {
     186         111 :       super::clear();
     187         111 :       m_probabilistic_states.clear();
     188         111 :       m_probabilistic_states.shrink_to_fit();
     189         111 :     }
     190             : };
     191             : 
     192             : }
     193             : }
     194             : 
     195             : #endif // MCRL2_LTS_LTS_H

Generated by: LCOV version 1.12