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

Generated by: LCOV version 1.12