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