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

Generated by: LCOV version 1.12