LCOV - code coverage report
Current view: top level - lts/source - liblts_fsm.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 85 94 90.4 %
Date: 2020-09-16 00:45:56 Functions: 13 13 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Muck van Weerdenburg
       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 liblts_fsm.cpp
      10             : 
      11             : #include "mcrl2/lts/lts_io.h"
      12             : #include "mcrl2/lts/parse.h"
      13             : #include "mcrl2/lts/detail/liblts_swap_to_from_probabilistic_lts.h"
      14             : 
      15             : namespace mcrl2 {
      16             : 
      17             : namespace lts {
      18             : 
      19             : struct fsm_writer
      20             : {
      21             :   std::ostream& out;
      22             :   std::size_t number_of_initial_state;
      23             :   const probabilistic_lts_fsm_t& fsm;
      24             : 
      25         119 :   fsm_writer(std::ostream& out_, const probabilistic_lts_fsm_t& fsm_)
      26         119 :     : out(out_), number_of_initial_state(fsm_.initial_probabilistic_state().begin()->state()), fsm(fsm_)
      27             :   {
      28         119 :     assert(fsm_.initial_probabilistic_state().size()>0);
      29         119 :   }
      30             : 
      31             :   // This functions swaps 0 with the number number_of_initial_state of the initial state.
      32        4254 :   std::size_t swap_initial_state(const std::size_t i)
      33             :   {
      34        4254 :     if (i==number_of_initial_state)
      35             :     {
      36        1556 :       return 0;
      37             :     }
      38        2698 :     if (i==0)
      39             :     {
      40           0 :       return number_of_initial_state;
      41             :     }
      42        2698 :     return i;
      43             :   }
      44             : 
      45         119 :   void write_parameters()
      46             :   {
      47             :     // print parameters with used values
      48         119 :     mCRL2log(log::verbose) << "writing parameter table..." << std::endl;
      49         299 :     for (std::size_t i = 0; i < fsm.process_parameters().size(); i++)
      50             :     {
      51         180 :       const std::vector<std::string>& values = fsm.state_element_values(i);
      52         180 :       out << fsm.process_parameter(i).first << "(" << values.size() << ") " << fsm.process_parameter(i).second << " ";
      53         636 :       for (const std::string& s: values)
      54             :       {
      55         456 :         out << " \"" << s << "\"";
      56             :       }
      57         180 :       out << std::endl;
      58             :     }
      59         119 :   }
      60             : 
      61         119 :   void write_states()
      62             :   {
      63         119 :     mCRL2log(log::verbose) << "writing states..." << std::endl;
      64         119 :     assert(fsm.initial_probabilistic_state().size()>0);
      65         992 :     for (std::size_t i = 0; i < fsm.num_states(); i++)
      66             :     {
      67         873 :       if (fsm.has_state_info())
      68             :       {
      69        1640 :         const state_label_fsm& state_parameters = fsm.state_label(swap_initial_state(i));
      70        8040 :         for (std::size_t j = 0; j < state_parameters.size(); j++)
      71             :         {
      72        7220 :           if (j > 0)
      73             :           {
      74        6400 :             out << " ";
      75             :           }
      76        7220 :           out << state_parameters[j];
      77             :         }
      78         820 :         out << std::endl;
      79             :       }
      80             :     }
      81         119 :   }
      82             : 
      83             :   // If there is only a single state with probility 1, write a single state, otherwise 
      84             :   // write "[state1 probability1, state2 probability2, ..., state_n probability_n]".
      85        1665 :   void write_probabilistic_state(const detail::lts_fsm_base::probabilistic_state& probabilistic_state)
      86             :   {
      87        1665 :     if (probabilistic_state.size()==1)
      88             :     {
      89        1553 :       out << swap_initial_state(probabilistic_state.begin()->state())+1;
      90             :     }
      91             :     else
      92             :     {
      93         112 :       out << "[";
      94         112 :       bool first=true;
      95         336 :       for(const lps::state_probability_pair< std::size_t, probabilistic_arbitrary_precision_fraction>& p: probabilistic_state)
      96             :       {
      97         224 :         if (first)
      98             :         {
      99         112 :           first=false;
     100             :         }
     101             :         else
     102             :         {
     103         112 :           out << ' ';
     104             :         }
     105         224 :         out << swap_initial_state(p.state()) + 1 << " " << p.probability();
     106             :       }
     107         112 :       out << "]";
     108             :     }
     109        1665 :   }
     110             : 
     111         119 :   void write_transitions()
     112             :   {
     113         119 :     mCRL2log(log::verbose) << "writing transitions..." << std::endl;
     114        1776 :     for (const transition& t: fsm.get_transitions())
     115             :     {
     116             :       // correct state numbering, by adding 1.
     117        1657 :       out << swap_initial_state(t.from()) + 1 << " ";
     118        1657 :       write_probabilistic_state(fsm.probabilistic_state(t.to())); 
     119        1657 :       out << " \"" << mcrl2::lts::pp(fsm.action_label(fsm.apply_hidden_label_map(t.label()))) << "\"" << std::endl;
     120             :     }
     121         119 :   }
     122             : 
     123         119 :   void write()
     124             :   {
     125         119 :     write_parameters();
     126         119 :     out << "---" << std::endl;
     127         119 :     write_states();
     128         119 :     out << "---" << std::endl;
     129         119 :     write_transitions();
     130             :     // If there is a initial distribution with more than one state, write the initial distribution.
     131         119 :     if (fsm.initial_probabilistic_state().size()>1)
     132             :     {
     133           8 :       out << "---" << std::endl;
     134           8 :       write_probabilistic_state(fsm.initial_probabilistic_state()); 
     135           8 :       out << "\n" << std::endl;
     136             :     }
     137         119 :   }
     138             : };
     139             : 
     140         116 : void probabilistic_lts_fsm_t::load(const std::string& filename)
     141             : {
     142         116 :   if (filename.empty())
     143             :   {
     144             :     try
     145             :     {
     146           0 :       parse_fsm_specification(std::cin, *this);
     147             :     }
     148           0 :     catch (mcrl2::runtime_error& e)
     149             :     {
     150           0 :       throw mcrl2::runtime_error(std::string("Error parsing .fsm file from standard input.\n") + e.what());
     151             :     }
     152             :   }
     153             :   else
     154             :   {
     155         232 :     std::ifstream is(filename.c_str());
     156             : 
     157         116 :     if (!is.is_open())
     158             :     {
     159           0 :       throw mcrl2::runtime_error("Cannot open .fsm file " + filename + ".");
     160             :     }
     161             :     try
     162             :     {
     163         116 :       parse_fsm_specification(is, *this);
     164             :     }
     165           0 :     catch (mcrl2::runtime_error& e)
     166             :     {
     167           0 :       throw mcrl2::runtime_error(std::string("Error parsing .fsm file.\n") + e.what());
     168             :     }
     169         116 :     is.close();
     170             :   }
     171         116 : }
     172             : 
     173         119 : void probabilistic_lts_fsm_t::save(const std::string& filename) const
     174             : {
     175         119 :   if (filename=="")
     176             :   {
     177           0 :     fsm_writer(std::cout, *this).write();
     178             :   }
     179             :   else
     180             :   {
     181         238 :     std::ofstream os(filename.c_str());
     182             : 
     183         119 :     if (!os.is_open())
     184             :     {
     185           0 :       throw mcrl2::runtime_error("Cannot create .fsm file '" + filename + ".");
     186             :       return;
     187             :     }
     188             : 
     189         119 :     fsm_writer(os, *this).write();
     190         119 :     os.close();
     191             :   }
     192         119 : }
     193             : 
     194         108 : void lts_fsm_t::load(const std::string& filename)
     195             : {
     196         216 :   probabilistic_lts_fsm_t l;
     197         108 :   l.load(filename);
     198             :   detail::swap_to_non_probabilistic_lts
     199             :              <state_label_fsm,
     200             :               action_label_string,
     201             :               detail::lts_fsm_base::probabilistic_state,
     202         108 :               detail::lts_fsm_base>(l,*this);
     203         108 : }
     204             : 
     205          54 : void lts_fsm_t::save(const std::string& filename) const
     206             : {
     207         108 :   probabilistic_lts_fsm_t l;
     208             :   detail::translate_to_probabilistic_lts
     209             :             <state_label_fsm,
     210             :              action_label_string,
     211             :              detail::lts_fsm_base::probabilistic_state,
     212          54 :              detail::lts_fsm_base>(*this,l);
     213          54 :   l.save(filename);
     214          54 : }
     215             : 
     216             : 
     217             : } // namespace lts
     218             : 
     219          21 : } // namespace mcrl2

Generated by: LCOV version 1.13