lts_fsm.h

Go to the documentation of this file.

// Author(s): 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_LTS_FSM_H
#define MCRL2_LTS_LTS_FSM_H
 
#include "mcrl2/utilities/probabilistic_arbitrary_precision_fraction.h"
#include "mcrl2/lts/probabilistic_lts.h"
#include "mcrl2/lts/action_label_string.h"
 
namespace mcrl2
{
namespace lts
{
 
class state_label_fsm:  public std::vector < std::size_t >
{
  public:
    state_label_fsm()
    {}
 
    state_label_fsm(const state_label_fsm& )=default;
 
    state_label_fsm& operator=(const state_label_fsm& )=default;
 
    explicit state_label_fsm(const std::vector < std::size_t >& v):
      std::vector < std::size_t >(v)
    {}
 
    state_label_fsm operator+(const state_label_fsm& l) const
    {
      if ((*this).empty())
      {
        return l;
      }
      return (*this); 
    }
 
    static state_label_fsm number_to_label(const std::size_t n)
    {
      return state_label_fsm(std::vector < std::size_t >(1,n));
    }
};
 
inline std::string pp(const state_label_fsm& label)
{
  std::string s;
  for(const std::size_t& l: label)
  {
    s += std::to_string(l) + " ";
  }
  return s;
}
 
namespace detail
{
class lts_fsm_base
{
  public:
    typedef mcrl2::lts::probabilistic_state<std::size_t, mcrl2::utilities::probabilistic_arbitrary_precision_fraction> probabilistic_state;
    typedef mcrl2::lps::state_probability_pair<std::size_t, mcrl2::utilities::probabilistic_arbitrary_precision_fraction> state_probability_pair;
 
  protected:
 
    std::vector < std::vector < std::string > > m_state_element_values;
 
    std::vector < std::pair < std::string, std::string > > m_parameters;
 
  public:
 
    bool operator==(const lts_fsm_base& other) const
    {
      return m_state_element_values==other.m_state_element_values &&
             m_parameters==other.m_parameters;
    }
 
    lts_type type() const
    {
      return lts_fsm;
    }
 
    void swap(lts_fsm_base& other)
    {
      m_state_element_values.swap(other.m_state_element_values);
      m_parameters.swap(other.m_parameters);
    }
 
    void
    clear()
    {
      m_state_element_values.clear();
      m_parameters.clear();
    }
 
    const std::vector < std::string >& state_element_values(std::size_t idx) const
    {
      assert(idx<m_state_element_values.size());
      return m_state_element_values[idx];
    }
 
    inline std::string state_label_to_string(const state_label_fsm& l) const
    {
      std::string s;
      s = "(";
      for (std::size_t i=0; i<l.size(); ++i)
      {
        s += state_element_value(i,l[i]);
        if (i+1<l.size())
        {
          s += ",";
        }
      }
      s += ")";
      return s;
    }
 
    std::size_t add_state_element_value(std::size_t idx, const std::string& s)
    {
      assert(idx<m_state_element_values.size());
      m_state_element_values[idx].push_back(s);
      return m_state_element_values[idx].size();
    }
 
    std::string state_element_value(std::size_t parameter_index, std::size_t element_index) const
    {
      assert(parameter_index<m_state_element_values.size());
      if (m_state_element_values[parameter_index].size()==0)
      {
        // The domain for this parameter has no string; return the string "i"
        return std::to_string(element_index); 
      }
      assert(element_index<m_state_element_values[parameter_index].size());
      return m_state_element_values[parameter_index][element_index];
    }
 
    std::vector < std::pair < std::string, std::string > > process_parameters() const
    {
      return m_parameters;
    }
 
    std::pair < std::string, std::string > process_parameter(std::size_t i) const
    {
      assert(i<m_parameters.size());
      return m_parameters[i];
    }
 
    void clear_process_parameters()
    {
      m_parameters.clear();
      m_state_element_values.clear();
    }
 
    void add_process_parameter(const std::string& name, const std::string& sort)
    {
      assert(m_parameters.size()==m_state_element_values.size());
      m_parameters.push_back(std::pair<std::string,std::string>(name,sort));
      m_state_element_values.push_back(std::vector < std::string >());
    }
 
 
};
 
} // end namespace detail
 
class lts_fsm_t : public lts< state_label_fsm, action_label_string, detail::lts_fsm_base >
{
  public:
    typedef lts< state_label_fsm, action_label_string, detail::lts_fsm_base > super;
 
    void load(const std::string& filename);
 
    void save(const std::string& filename) const;
};
 
class probabilistic_lts_fsm_t : 
        public probabilistic_lts< state_label_fsm, 
                                  action_label_string, 
                                  probabilistic_state< std::size_t, mcrl2::utilities::probabilistic_arbitrary_precision_fraction >,
                                  detail::lts_fsm_base >
{
  public:
 
    typedef probabilistic_lts< state_label_fsm, action_label_string, probabilistic_state_t, detail::lts_fsm_base > super;
 
    void load(const std::string& filename);
 
    void save(const std::string& filename) const;
};
 
} // namespace lts
} // namespace mcrl2
 
#endif