LCOV - code coverage report
Current view: top level - lts/source - liblts_lts.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 137 152 90.1 %
Date: 2020-02-19 00:44:21 Functions: 24 24 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Muck van Weerdenburg; completely rewritten by 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             : /// \file liblts_lts.cpp
      10             : 
      11             : #include "mcrl2/lts/lts_lts.h"
      12             : 
      13             : #include <fstream>
      14             : 
      15             : namespace mcrl2
      16             : {
      17             : namespace lts
      18             : {
      19             : namespace detail
      20             : {
      21             : 
      22             : using namespace atermpp;
      23             : 
      24             : 
      25             : typedef term_list<state_label_lts> state_labels_t;               // The state labels listed consecutively.
      26             : typedef term_list<atermpp::aterm_appl> action_labels_t;          // A multiaction has the shape "multi_action(action_list,data_expression)
      27             : typedef term_list<data::data_expression> probabilistic_labels_t; // This contains a list of probabilities.
      28             : typedef term_list<data::function_symbol> boolean_list_t;         // A list with constants true or false, indicating
      29             :                                                                  // whether a state is probabilistic.
      30             : 
      31             : // Special function symbols to indicate the type of written terms.
      32             : 
      33             : // A header consisting of the data_specification, the process parameters, the list of action labels, the initial state and the number of states.
      34         224 : static atermpp::function_symbol lts_header()
      35             : {
      36         224 :   static atermpp::function_symbol lts_h("labelled_transition_system", 5);
      37         224 :   return lts_h;
      38             : }
      39             : 
      40             : // A simple transition of three aterm_int indicating the from, label and to states.
      41        5136 : static atermpp::function_symbol transition_header()
      42             : {
      43        5136 :   static atermpp::function_symbol t_h("transition", 3);
      44        5136 :   return t_h;
      45             : }
      46             : 
      47             : // A simple transition of two aterm_int indicating the from state and label, the last argument is a state_probability_list.
      48        3704 : static atermpp::function_symbol probabilistic_transition_header()
      49             : {
      50        3704 :   static atermpp::function_symbol t_h("probabilistic_transition", 3);
      51        3704 :   return t_h;
      52             : }
      53             : 
      54        2764 : static atermpp::function_symbol multi_action_header()
      55             : {
      56        2764 :   static atermpp::function_symbol ma_h("multi_action", 2);
      57        2764 :   return ma_h;
      58             : }
      59             : 
      60             : // Utility functions
      61             : 
      62             : /// \brief Converts a probabilistic state into an aterm that encodes it.
      63         216 : static aterm_list encode_probabilitistic_state(const probabilistic_lts_lts_t::probabilistic_state_t& target)
      64             : {
      65         216 :   aterm_list result;
      66         544 :   for(const auto& state : target)
      67             :   {
      68             :     // Push a (index, probability) pair into the list.
      69         328 :     result.push_front(state.probability());
      70         328 :     result.push_front(aterm_int(state.state()));
      71             :   }
      72             : 
      73         216 :   return result;
      74             : }
      75             : 
      76         216 : static probabilistic_lts_lts_t::probabilistic_state_t decode_probabilistic_state(const atermpp::aterm_list& list)
      77             : {
      78             :   // Convert the list into a vector of pairs.
      79         432 :   std::vector<lps::state_probability_pair<std::size_t, mcrl2::lps::probabilistic_data_expression>> result;
      80             : 
      81         544 :   for(auto it = list.begin(); it != list.end(); ++it)
      82             :   {
      83             :     // Read the (index, probability) pair from the list.
      84         328 :     const std::size_t state_number = down_cast<aterm_int>(*it).value();
      85         328 :     ++it;
      86             : 
      87             :     // The indices are already added to the header before.
      88         328 :     const lps::probabilistic_data_expression& probability = down_cast<lps::probabilistic_data_expression>(*it);
      89         328 :     result.emplace_back(state_number, probability);
      90             :   }
      91             : 
      92         432 :   return probabilistic_lts_lts_t::probabilistic_state_t(result.begin(), result.end());
      93             : }
      94             : 
      95          60 : static aterm encode_initial_state(const probabilistic_lts_lts_t& lts)
      96             : {
      97          60 :   return encode_probabilitistic_state(lts.initial_probabilistic_state());
      98             : }
      99             : 
     100          52 : static aterm encode_initial_state(const lts_lts_t& lts)
     101             : {
     102          52 :   return encode_probabilitistic_state(probabilistic_lts_lts_t::probabilistic_state_t(lts.initial_state()));
     103             : }
     104             : 
     105         104 : static void decode_initial_state(lts_lts_t& lts, const probabilistic_lts_lts_t::probabilistic_state_t& initial_state)
     106             : {
     107         104 :   if (initial_state.size() > 1)
     108             :   {
     109           0 :     throw mcrl2::runtime_error("The initial state of the non probabilistic input lts is probabilistic.");
     110             :   }
     111             : 
     112         104 :   lts.set_initial_state(initial_state.begin()->state());
     113         104 : }
     114             : 
     115           8 : static void decode_initial_state(probabilistic_lts_lts_t& lts, const probabilistic_lts_lts_t::probabilistic_state_t& initial_state)
     116             : {
     117           8 :   lts.set_initial_probabilistic_state(initial_state);
     118           8 : }
     119             : 
     120         762 : static aterm encode_transition(const lts_lts_t& lts, const transition& trans)
     121             : {
     122        1524 :   return atermpp::aterm_appl(transition_header(),
     123        1524 :     aterm_int(trans.from()),
     124        1524 :     aterm_int(lts.apply_hidden_label_map(trans.label())),
     125        2286 :     aterm_int(trans.to()));
     126             : }
     127             : 
     128         870 : static aterm encode_transition(const probabilistic_lts_lts_t& lts, const transition& trans)
     129             : {
     130         870 :   const probabilistic_lts_lts_t::probabilistic_state_t& probabilistic_state = lts.probabilistic_state(trans.to());
     131             : 
     132         870 :   if (probabilistic_state.size() == 1)
     133             :   {
     134             :     // Actually a non_probabilistic transition.
     135        1532 :     return atermpp::aterm_appl(transition_header(),
     136        1532 :       aterm_int(trans.from()),
     137        1532 :       aterm_int(lts.apply_hidden_label_map(trans.label())),
     138        2298 :       aterm_int(probabilistic_state.begin()->state()));
     139             :   }
     140             :   else
     141             :   {
     142         208 :     return atermpp::aterm_appl(probabilistic_transition_header(),
     143         208 :       aterm_int(trans.from()),
     144         208 :       aterm_int(lts.apply_hidden_label_map(trans.label())),
     145         312 :       encode_probabilitistic_state(probabilistic_state));
     146             :   }
     147             : 
     148             : }
     149             : 
     150        1524 : static void decode_transition(lts_lts_t& lts, const aterm_appl& appl)
     151             : {
     152        1524 :   if (appl.function() == probabilistic_transition_header())
     153             :   {
     154           0 :     throw mcrl2::runtime_error("Attempting to read a probabilistic lts as a regular lts.");
     155             :   }
     156             : 
     157        6096 :   lts.add_transition(transition(
     158        1524 :     static_cast<const aterm_int&>(appl[0]).value(),
     159        1524 :     static_cast<const aterm_int&>(appl[1]).value(),
     160        1524 :     static_cast<const aterm_int&>(appl[2]).value()));
     161        1524 : }
     162             : 
     163         108 : static void decode_transition(probabilistic_lts_lts_t& lts, const aterm_appl& appl)
     164             : {
     165         108 :   std::size_t target_index = 0;
     166             : 
     167             :   // Depending on the header its the index of a probabilistic state or an actual probabilistic state encoded as a list.
     168         108 :   if (appl.function() == transition_header())
     169             :   {
     170           8 :     auto target = probabilistic_lts_lts_t::probabilistic_state_t(static_cast<const aterm_int&>(appl[2]).value());
     171           4 :     target_index = lts.add_probabilistic_state(target);
     172             :   }
     173             :   else
     174             :   {
     175         104 :     assert(appl.function() == probabilistic_transition_header());
     176         208 :     auto target = decode_probabilistic_state(static_cast<const aterm_list&>(appl[2]));
     177         104 :     target_index = lts.add_probabilistic_state(target);
     178             :   }
     179             : 
     180         324 :   lts.add_transition(transition(
     181         108 :     static_cast<const aterm_int&>(appl[0]).value(),
     182         108 :     static_cast<const aterm_int&>(appl[1]).value(),
     183             :     target_index));
     184         108 : }
     185             : 
     186             : template <class LTS_TRANSITION_SYSTEM>     
     187         112 : static void read_from_lts(LTS_TRANSITION_SYSTEM& lts, const std::string& filename)
     188             : {
     189             :   static_assert(std::is_same<LTS_TRANSITION_SYSTEM,probabilistic_lts_lts_t>::value || 
     190             :                 std::is_same<LTS_TRANSITION_SYSTEM,lts_lts_t>::value,
     191             :                 "Function read_from_lts can only be applied to a (probabilistic) lts. ");
     192             : 
     193         224 :   std::ifstream fstream;
     194         112 :   if (!filename.empty())
     195             :   {
     196         112 :     fstream.exceptions ( std::ifstream::failbit | std::ifstream::badbit );
     197             :     try
     198             :     {  
     199         112 :       fstream.open(filename, std::ifstream::in | std::ifstream::binary);
     200             :     }
     201           0 :     catch (std::ifstream::failure&)
     202             :     {
     203           0 :       if (filename.empty())
     204             :       {
     205           0 :         throw mcrl2::runtime_error("Fail to open standard input to read an lts.");
     206             :       }
     207             :       else 
     208             :       {
     209           0 :         throw mcrl2::runtime_error("Fail to open file " + filename + " to read an lts.");
     210             :       }
     211             :     }
     212             :   }
     213             : 
     214             :   try
     215             :   {
     216         224 :     atermpp::binary_aterm_istream stream(filename.empty() ? std::cin : fstream);
     217         112 :     stream >> data::detail::add_index_impl;
     218             : 
     219        3500 :     while (true)
     220             :     {
     221        7112 :       aterm term = stream.get();
     222        3612 :       if (!term.defined())
     223             :       {
     224             :         // The default constructed term indicates the end of the stream.
     225         112 :         break;
     226             :       }
     227             : 
     228        3500 :       if (term.function() == transition_header() || term.function() == probabilistic_transition_header())
     229             :       {
     230        1632 :         const aterm_appl& appl = static_cast<const aterm_appl&>(term);
     231        1632 :         decode_transition(lts, appl);
     232             :       }
     233        1868 :       else if (term.function() == multi_action_header())
     234             :       {
     235         896 :         const aterm_appl& appl = static_cast<const aterm_appl&>(term);
     236             : 
     237        2688 :         const lps::multi_action action = lps::multi_action(
     238         896 :           down_cast<process::action_list>(appl[0]),
     239             :           down_cast<data::data_expression>(appl[1]));
     240             : 
     241         896 :         lts.add_action(action_label_lts(action));
     242             :       }
     243         972 :       else if (term.function() == atermpp::detail::g_term_pool().as_list())
     244             :       {
     245             :         // Lists always represent state labels, only need to add the indices.
     246         860 :         lts.add_state(reinterpret_cast<const state_label_lts&>(term));
     247             :       }
     248         112 :       else if (term.function() == lts_header())
     249             :       {
     250         112 :         const aterm_appl& header= static_cast<const aterm_appl&>(term);
     251             : 
     252         112 :         lts.set_data(data::data_specification(static_cast<const aterm_appl&>(header[0])));
     253         112 :         lts.set_process_parameters(static_cast<const data::variable_list&>(header[1]));
     254         112 :         lts.set_action_label_declarations(static_cast<const process::action_label_list&>(header[2]));
     255             : 
     256         112 :         if (lts.num_state_labels() == 0)
     257             :         {
     258           0 :           lts.set_num_states(static_cast<const aterm_int&>(header[4]).value());
     259             :         }
     260             :         else
     261             :         {
     262         112 :           assert(lts.num_states() == lts.num_state_labels());
     263             :         }
     264             : 
     265             :         // The initial state can only be set after the states are known.
     266         112 :         decode_initial_state(lts, decode_probabilistic_state(static_cast<const aterm_list&>(header[3])));
     267             :       }
     268             :     }
     269             :   }
     270           0 :   catch (std::ifstream::failure&)
     271             :   {
     272           0 :     if (filename.empty())
     273             :     {
     274           0 :       throw mcrl2::runtime_error("Fail to correctly read an lts from standard input.");
     275             :     }
     276             :     else
     277             :     {
     278           0 :       throw mcrl2::runtime_error("Fail to correctly read an lts from the file " + filename + ".");
     279             :     }
     280             :   }
     281         112 : }
     282             : 
     283             : template <class LTS_TRANSITION_SYSTEM>
     284         112 : static void write_to_lts(const LTS_TRANSITION_SYSTEM& lts, const std::string& filename)
     285             : {
     286             :   static_assert(std::is_same<LTS_TRANSITION_SYSTEM,probabilistic_lts_lts_t>::value ||
     287             :                 std::is_same<LTS_TRANSITION_SYSTEM,lts_lts_t>::value,
     288             :                 "Function read_from_lts can only be applied to a (probabilistic) lts. ");
     289             : 
     290         224 :   std::ofstream fstream;
     291         112 :   if (!filename.empty())
     292             :   {
     293         112 :     fstream.exceptions ( std::ofstream::failbit | std::ofstream::badbit );
     294             : 
     295             :     try
     296             :     {
     297         112 :       fstream.open(filename, std::ofstream::out | std::ofstream::binary);
     298             :     }
     299           0 :     catch (std::ofstream::failure&)
     300             :     {
     301           0 :       throw mcrl2::runtime_error("Fail to open file " + filename + " for writing.");
     302             :     }
     303             :   }
     304             : 
     305             :   try
     306             :   {
     307         224 :     atermpp::binary_aterm_ostream stream(filename.empty() ? std::cout : fstream);
     308         112 :     stream << data::detail::remove_index_impl;
     309             : 
     310         112 :     if (lts.has_state_info())
     311             :     {
     312         972 :       for (std::size_t i = 0; i < lts.num_state_labels(); ++i)
     313             :       {
     314             :         // Write state labels as such, we assume that all list terms without headers are state labels.
     315         860 :         stream << lts.state_label(i);
     316             :       }
     317             :     }
     318             : 
     319         112 :     if (lts.has_action_info())
     320             :     {
     321         988 :       for (std::size_t i = 1; i < lts.num_action_labels(); ++i)
     322             :       {
     323         896 :         stream << atermpp::aterm_appl(multi_action_header(), lts.action_label(i).actions(), lts.action_label(i).time());
     324             :       }
     325             :     }
     326             : 
     327        1744 :     for (auto& trans : lts.get_transitions())
     328             :     {
     329        1632 :       stream << encode_transition(lts, trans);
     330             :     }
     331             : 
     332             :     // Write the header of the labelled transition system at the end, because the initial state must be set of adding the transitions.
     333         224 :     aterm header = aterm_appl(lts_header(),
     334             :                 data::detail::data_specification_to_aterm(lts.data()),
     335             :                 lts.process_parameters(),
     336             :                 lts.action_label_declarations(),
     337             :                 encode_initial_state(lts),
     338             :                 aterm_int(lts.num_states()));
     339             : 
     340             :     // Write the header with the indices of dedicated terms removed.
     341         112 :     stream << header;
     342             :   }
     343           0 :   catch (std::ofstream::failure&)
     344             :   {
     345           0 :     throw mcrl2::runtime_error("Fail to write lts correctly to the file " + filename + ".");
     346             :   }
     347         112 : }
     348             : 
     349             : } // namespace detail
     350             : 
     351             : // Implementation of public functions.
     352             : 
     353          60 : void probabilistic_lts_lts_t::save(const std::string& filename) const
     354             : {
     355          60 :   mCRL2log(log::verbose) << "Starting to save a probabilistic lts to the file " << filename << ".\n";
     356          60 :   detail::write_to_lts(*this, filename);
     357          60 : }
     358             : 
     359          52 : void lts_lts_t::save(std::string const& filename) const
     360             : {
     361          52 :   mCRL2log(log::verbose) << "Starting to save an lts to the file " << filename << ".\n";
     362          52 :   detail::write_to_lts(*this, filename);
     363          52 : }
     364             : 
     365           8 : void probabilistic_lts_lts_t::load(const std::string& filename)
     366             : {
     367           8 :   mCRL2log(log::verbose) << "Starting to load a probabilistic lts from the file " << filename << ".\n";
     368           8 :   detail::read_from_lts(*this, filename);
     369           8 : }
     370             : 
     371         104 : void lts_lts_t::load(const std::string& filename)
     372             : {
     373         104 :   mCRL2log(log::verbose) << "Starting to load an lts from the file " << filename << ".\n";
     374         104 :   detail::read_from_lts(*this, filename);
     375         104 : }
     376             : 
     377             : }
     378          21 : }

Generated by: LCOV version 1.13