LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts/detail - liblts_swap_to_from_probabilistic_lts.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 19 21 90.5 %
Date: 2020-07-11 00:44:39 Functions: 2 3 66.7 %
Legend: Lines: hit not hit

          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         108 : 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         108 :   static_cast<lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE>& >(l_probabilistic).swap(l_plain);
      33             :   
      34         108 :   assert(l_probabilistic.initial_probabilistic_state().size()!=0);
      35         108 :   if (l_probabilistic.initial_probabilistic_state().size()==1)
      36             :   { 
      37         108 :     l_plain.set_initial_state(l_probabilistic.initial_probabilistic_state().begin()->state());
      38             :   }
      39             :   else
      40             :   {
      41           0 :     throw mcrl2::runtime_error("Initial state is probabilistic and cannot be transformed into a non probabilistic state.");
      42             :   }
      43             :   
      44             :   // Adapt the probabilistic target states to non probabilistic target states.
      45         108 :   std::size_t transition_number=1;
      46        1640 :   for(transition& t: l_plain.get_transitions())
      47             :   {
      48        1532 :     std::size_t probabilistic_target_state_number=t.to();
      49        1532 :     assert(l_probabilistic.probabilistic_state(probabilistic_target_state_number).size()!=0);
      50        1532 :     if (l_probabilistic.probabilistic_state(probabilistic_target_state_number).size()>1)
      51             :     {
      52           0 :       throw mcrl2::runtime_error("Transition " + std::to_string(transition_number) + " is probabilistic.");
      53             :     }
      54             :     else
      55             :     {
      56        1532 :       t=transition(t.from(), t.label(), l_probabilistic.probabilistic_state(probabilistic_target_state_number).begin()->state());
      57             :     }
      58        1532 :     transition_number++;
      59             :   }
      60             : 
      61             :   
      62         108 : }
      63             : 
      64             : template < class STATE_LABEL_T, class ACTION_LABEL_T, class PROBABILISTIC_STATE_T, class LTS_BASE >
      65          54 : void translate_to_probabilistic_lts(
      66             :         const lts<STATE_LABEL_T,ACTION_LABEL_T, LTS_BASE>& l_plain,
      67             :         probabilistic_lts<STATE_LABEL_T,ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE>& l_probabilistic) 
      68             : {
      69          54 :   static_cast<lts<STATE_LABEL_T,ACTION_LABEL_T, LTS_BASE>& >(l_probabilistic)=l_plain;
      70          54 :   l_probabilistic.set_initial_probabilistic_state(PROBABILISTIC_STATE_T(l_plain.initial_state()));
      71         430 :   for(std::size_t i=0; i<l_plain.num_states(); ++i)
      72             :   {
      73         376 :     l_probabilistic.add_probabilistic_state(PROBABILISTIC_STATE_T(i));
      74             :   }
      75          54 : }
      76             : 
      77             : } // detail
      78             : } // lts
      79             : } // mcrl2
      80             : 
      81             : #endif  // MCRL2_LTS_DETAIL_SWAP_TO_FROM_PROBABILISTIC_LTS_H

Generated by: LCOV version 1.13