Line data    Source code

       1             : // Author(s): Wieger Wesselink
       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             : /// \file mcrl2/pbes/detail/lts2pbes_lts.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_DETAIL_LTS2PBES_LTS_H
      13             : #define MCRL2_PBES_DETAIL_LTS2PBES_LTS_H
      14             : 
      15             : #include "mcrl2/lts/lts_lts.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace pbes_system {
      20             : 
      21             : namespace detail {
      22             : 
      23             : inline
      24             : std::ostream& operator<<(std::ostream& out, const lts::lts_lts_t& ltsspec)
      25             : {
      26             :   const auto& action_labels = ltsspec.action_labels();
      27             :   out << "LTS" << std::endl;
      28             :   for (const auto& tr: ltsspec.get_transitions())
      29             :   {
      30             :     out << tr.from() << " --" << action_labels[tr.label()] << "--> " << tr.to() << std::endl;
      31             :   }
      32             :   return out;
      33             : }
      34             : 
      35             : // custom LTS type that maps states to a vector of outgoing edges
      36             : class lts2pbes_lts
      37             : {
      38             :   public:
      39             :     typedef std::size_t state_type;
      40             :     typedef std::size_t label_type;
      41             : 
      42             :     struct edge
      43             :     {
      44          25 :       edge(label_type label_, state_type state_, std::size_t index_)
      45          25 :         : label(label_),
      46          25 :           state(state_),
      47          25 :           index(index_)
      48          25 :       {}
      49             : 
      50             :       label_type label;
      51             :       state_type state;
      52             :       std::size_t index;
      53             :     };
      54             : 
      55             :     typedef std::vector<edge> edge_list;
      56             : 
      57             :   protected:
      58             :     std::map<state_type, edge_list> m_state_map;
      59             :     std::vector<lps::multi_action> m_action_labels;
      60             :     std::size_t m_state_count;
      61             :     edge_list m_empty_edge_list;
      62             : 
      63             :   public:
      64           4 :     lts2pbes_lts(const lts::lts_lts_t& ltsspec)
      65           4 :     {
      66           4 :       const auto& transitions = ltsspec.get_transitions();
      67          29 :       for (std::size_t i = 0; i < transitions.size(); i++)
      68             :       {
      69          25 :         const auto& transition = transitions[i];
      70          25 :         state_type s = transition.from();
      71          25 :         label_type a = transition.label();
      72          25 :         state_type t = transition.to();
      73          25 :         m_state_map[s].emplace_back(a, t, i);
      74             :       }
      75             : 
      76          16 :       for (const auto& a: ltsspec.action_labels())
      77             :       {
      78          12 :         m_action_labels.emplace_back(a.actions(), a.time());
      79             :       }
      80           4 :       m_state_count = ltsspec.num_states();
      81           4 :     }
      82             : 
      83             :     // returns the outgoing edges of state s
      84         217 :     const edge_list& edges(state_type s) const
      85             :     {
      86         217 :       auto i = m_state_map.find(s);
      87         217 :       if (i == m_state_map.end())
      88             :       {
      89          40 :         return m_empty_edge_list;
      90             :       }
      91             :       else
      92             :       {
      93         177 :         return i->second;
      94             :       }
      95             :     }
      96             : 
      97         283 :     const std::vector<lps::multi_action>& action_labels() const
      98             :     {
      99         283 :       return m_action_labels;
     100             :     }
     101             : 
     102         144 :     std::size_t state_count() const
     103             :     {
     104         144 :       return m_state_count;
     105             :     }
     106             : 
     107           0 :     const std::map<state_type, edge_list>& state_map() const
     108             :     {
     109           0 :       return m_state_map;
     110             :     }
     111             : };
     112             : 
     113           0 : std::ostream& operator<<(std::ostream& out, const lts2pbes_lts& ltsspec)
     114             : {
     115           0 :   const auto& action_labels = ltsspec.action_labels();
     116           0 :   out << "pbes-LTS" << std::endl;
     117           0 :   for (const auto& p: ltsspec.state_map())
     118             :   {
     119           0 :     for (const auto& edge: p.second)
     120             :     {
     121           0 :       out << edge.index << " " << p.first << " --" << action_labels[edge.label] << "--> " << edge.state << std::endl;
     122             :     }
     123             :   }
     124           0 :   return out;
     125             : }
     126             : 
     127             : } // namespace detail
     128             : 
     129             : } // namespace pbes_system
     130             : 
     131             : } // namespace mcrl2
     132             : 
     133             : #endif // MCRL2_PBES_DETAIL_LTS2PBES_LTS_H