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             : /// \details This file contains two functions to efficiently transform 
      10             : //           a plain_lts into a probabilistic lts and vice versa. The
      11             : //           lts from which the transformation takes place is destroyed.
      12             : 
      13             : #ifndef MCRL2_LTS_DETAIL_SWAP_TO_FROM_PROBABILISTIC_LTS_H
      14             : #define MCRL2_LTS_DETAIL_SWAP_TO_FROM_PROBABILISTIC_LTS_H
      15             : 
      16             : #include "mcrl2/lts/probabilistic_lts.h"
      17             : #include "mcrl2/utilities/exception.h"
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : namespace lts
      22             : {
      23             : 
      24             : namespace detail
      25             : {
      26             : 
      27             : template < class STATE_LABEL_T, class ACTION_LABEL_T, class PROBABILISTIC_STATE_T, class LTS_BASE >
      28          54 : void swap_to_non_probabilistic_lts(
      29             :         probabilistic_lts<STATE_LABEL_T,ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE>& l_probabilistic, 
      30             :         lts<STATE_LABEL_T,ACTION_LABEL_T, LTS_BASE>& l_plain)
      31             : {
      32          54 :   static_cast<lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE>& >(l_probabilistic).swap(l_plain);
      33             :   
      34          54 :   if (l_probabilistic.initial_probabilistic_state().size()<=1)
      35             :   { 
      36          54 :     l_plain.set_initial_state(l_probabilistic.initial_probabilistic_state().get());
      37             :   }
      38             :   else
      39             :   {
      40           0 :     throw mcrl2::runtime_error("Initial state is probabilistic and cannot be transformed into a non probabilistic state.");
      41             :   }
      42             :   
      43             :   // Adapt the probabilistic target states to non probabilistic target states.
      44          54 :   std::size_t transition_number=1;
      45         820 :   for(transition& t: l_plain.get_transitions())
      46             :   {
      47         766 :     std::size_t probabilistic_target_state_number=t.to();
      48         766 :     if (l_probabilistic.probabilistic_state(probabilistic_target_state_number).size()>1)
      49             :     {
      50           0 :       throw mcrl2::runtime_error("Transition " + std::to_string(transition_number) + " is probabilistic.");
      51             :     }
      52             :     else
      53             :     {
      54         766 :       t=transition(t.from(), t.label(), l_probabilistic.probabilistic_state(probabilistic_target_state_number).get());
      55             :     }
      56         766 :     transition_number++;
      57             :   }
      58             : 
      59             :   
      60          54 : }
      61             : 
      62             : template < class STATE_LABEL_T, class ACTION_LABEL_T, class PROBABILISTIC_STATE_T, class LTS_BASE >
      63          54 : void translate_to_probabilistic_lts(
      64             :         const lts<STATE_LABEL_T,ACTION_LABEL_T, LTS_BASE>& l_plain,
      65             :         probabilistic_lts<STATE_LABEL_T,ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE>& l_probabilistic) 
      66             : {
      67          54 :   static_cast<lts<STATE_LABEL_T,ACTION_LABEL_T, LTS_BASE>& >(l_probabilistic)=l_plain;
      68          54 :   l_probabilistic.set_initial_probabilistic_state(PROBABILISTIC_STATE_T(l_plain.initial_state()));
      69         430 :   for(std::size_t i=0; i<l_plain.num_states(); ++i)
      70             :   {
      71         376 :     l_probabilistic.add_probabilistic_state(PROBABILISTIC_STATE_T(i));
      72             :   }
      73          54 : }
      74             : 
      75             : } // detail
      76             : } // lts
      77             : } // mcrl2
      78             : 
      79             : #endif  // MCRL2_LTS_DETAIL_SWAP_TO_FROM_PROBABILISTIC_LTS_H