probabilistic_lts.h

Go to the documentation of this file.

// Author(s): Muck van Weerdenburg, Jan Friso Groote
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef MCRL2_LTS_PROBABILISTIC_LTS_H
#define MCRL2_LTS_PROBABILISTIC_LTS_H
 
#include "mcrl2/lts/lts.h"
#include "mcrl2/lts/probabilistic_state.h"
 
 
namespace mcrl2
{
 
namespace lts
{
 
template < class STATE_LABEL_T, class ACTION_LABEL_T, class PROBABILISTIC_STATE_T, class LTS_BASE >
class probabilistic_lts: public lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE>
{
  public:
 
    typedef lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE> super;
 
    typedef PROBABILISTIC_STATE_T probabilistic_state_t;
 
    typedef typename super::state_label_t         state_label_t        ;
    typedef typename super::action_label_t        action_label_t       ;
    typedef typename super::base_t                base_t               ;
    typedef typename super::states_size_type      states_size_type     ;
    typedef typename super::labels_size_type      labels_size_type     ;
    typedef typename super::transitions_size_type transitions_size_type;
 
    static constexpr bool is_probabilistic_lts=true;
 
  protected:
 
    std::vector<PROBABILISTIC_STATE_T> m_probabilistic_states;
    PROBABILISTIC_STATE_T m_init_probabilistic_state;
 
    /* This function is made protected to prevent its use in a probabilistic transition system */  
    states_size_type initial_state() const
    {
      return super::initial_state();
    }
 
    /* This function is made protected to prevent its use in a probabilistic transition system */  
    void set_initial_state(const states_size_type s)
    {
      super::set_initial_state(s);
    }
 
  public:
 
    probabilistic_lts()
    {}
 
    probabilistic_lts(const probabilistic_lts& other) = default;
 
    probabilistic_lts(probabilistic_lts&& other) = default;
 
    probabilistic_lts& operator=(const probabilistic_lts& other) = default;
 
    probabilistic_lts& operator=(probabilistic_lts&& other) = default;
 
    bool operator==(const probabilistic_lts& other) const
    {
      return super::operator==(static_cast<const super&>(other)) &&
             m_probabilistic_states==other.m_probabilistic_states &&
             m_init_probabilistic_state==other.m_init_probabilistic_state;
    }
 
    void swap(probabilistic_lts& other)
    {
      super::swap(other);
      m_probabilistic_states.swap(other.m_probabilistic_states);
      m_init_probabilistic_state.swap(other.m_init_probabilistic_state);
    }
 
    const PROBABILISTIC_STATE_T& initial_probabilistic_state() const
    {
      return m_init_probabilistic_state;
    }
 
    void set_initial_probabilistic_state(const PROBABILISTIC_STATE_T& state)
    {
      // Prevent that the initial state of the lts, which is not used in a probabilistic state
      // has an arbitrary value.
      set_initial_state(0);
      m_init_probabilistic_state = state;
    }
 
 
    labels_size_type num_probabilistic_states() const
    {
      return m_probabilistic_states.size();
    }
 
    states_size_type add_probabilistic_state(const PROBABILISTIC_STATE_T& s)
    {
      const states_size_type label_index=m_probabilistic_states.size();
      m_probabilistic_states.push_back(s);
      return label_index;
    }
 
    states_size_type add_and_reset_probabilistic_state(PROBABILISTIC_STATE_T& s)
    {
      const states_size_type label_index=m_probabilistic_states.size();
      m_probabilistic_states.emplace_back();
      m_probabilistic_states.back().swap(s);
      return label_index;
    }
 
    void set_probabilistic_state(const states_size_type index, const PROBABILISTIC_STATE_T& s)
    {
      assert(index<m_probabilistic_states.size());
      m_probabilistic_states[index] = s;
    }
 
    const PROBABILISTIC_STATE_T& probabilistic_state(const states_size_type index) const
    {
      assert(index < m_probabilistic_states.size());
      return m_probabilistic_states[index];
    }
 
    void clear_probabilistic_states()
    {
      m_probabilistic_states.clear();
    }
 
    void clear()
    {
      super::clear();
      m_probabilistic_states.clear();
      m_probabilistic_states.shrink_to_fit();
    }
};
 
}
}
 
#endif // MCRL2_LTS_LTS_H