LCOV - code coverage report
Current view: top level - lts/source - liblts_lts.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 187 211 88.6 %
Date: 2020-09-16 00:45:56 Functions: 31 33 93.9 %
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             : #include "mcrl2/lts/lts_io.h"
      13             : 
      14             : #include <fstream>
      15             : #include <optional>
      16             : 
      17             : namespace mcrl2::lts
      18             : {
      19             : 
      20             : /// \brief Converts a probabilistic state into an aterm that encodes it.
      21         220 : atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const probabilistic_lts_lts_t::probabilistic_state_t& state)
      22             : {
      23         220 :   stream << atermpp::aterm_int(state.size());
      24             : 
      25         552 :   for(const auto& state : state)
      26             :   {
      27             :     // Push a (index, probability) pair into the list.
      28         332 :     stream << state.probability();
      29         332 :     stream << atermpp::aterm_int(state.state());
      30             :   }
      31             : 
      32         220 :   return stream;
      33             : }
      34             : 
      35         220 : atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, probabilistic_lts_lts_t::probabilistic_state_t& state)
      36             : {
      37         440 :   atermpp::aterm_int size;
      38         220 :   stream >> size;
      39             : 
      40         220 :   state = {};
      41         552 :   for (std::size_t i = 0; i < size.value(); ++i)
      42             :   {
      43         664 :     lps::probabilistic_data_expression probability;
      44         664 :     atermpp::aterm_int index;
      45             : 
      46         332 :     stream >> probability;
      47         332 :     stream >> index;
      48             : 
      49         332 :     state.add(index.value(), probability);
      50             :   }
      51             : 
      52         220 :   state.shrink_to_fit();
      53         440 :   return stream;
      54             : }
      55             : 
      56             : namespace detail
      57             : {
      58             : 
      59             : using namespace atermpp;
      60             : 
      61             : // Special terms to indicate the type of the following structure.
      62             : 
      63        4156 : static atermpp::aterm transition_mark()
      64             : {
      65        4156 :   static atermpp::aterm_appl mark(atermpp::function_symbol("transition", 0));
      66        4156 :   return mark;
      67             : }
      68             : 
      69        1188 : static atermpp::aterm probabilistic_transition_mark()
      70             : {
      71        1188 :   static atermpp::aterm_appl mark(atermpp::function_symbol("probabilistic_transition", 0));
      72        1188 :   return mark;
      73             : }
      74             : 
      75         232 : static atermpp::aterm initial_state_mark()
      76             : {
      77         232 :   static atermpp::aterm_appl mark(atermpp::function_symbol("initial_state", 0));
      78         232 :   return mark;
      79             : }
      80             : 
      81         232 : static atermpp::aterm labelled_transition_system_mark()
      82             : {
      83         232 :   return atermpp::aterm_appl(atermpp::function_symbol("labelled_transition_system", 0));
      84             : }
      85             : 
      86             : // Utility functions
      87             : 
      88         108 : static void set_initial_state(lts_lts_t& lts, const probabilistic_lts_lts_t::probabilistic_state_t& initial_state)
      89             : {
      90         108 :   if (initial_state.size() > 1)
      91             :   {
      92           0 :     throw mcrl2::runtime_error("The initial state of the non probabilistic input lts is probabilistic.");
      93             :   }
      94             : 
      95         108 :   lts.set_initial_state(initial_state.begin()->state());
      96         108 : }
      97             : 
      98           8 : static void set_initial_state(probabilistic_lts_lts_t& lts, const probabilistic_lts_lts_t::probabilistic_state_t& initial_state)
      99             : {
     100           8 :   lts.set_initial_probabilistic_state(initial_state);
     101           8 : }
     102             : 
     103             : template <class LTS>
     104         116 : static void read_lts(atermpp::aterm_istream& stream, LTS& lts)
     105             : {
     106             :   static_assert(std::is_same<LTS,probabilistic_lts_lts_t>::value ||
     107             :                 std::is_same<LTS,lts_lts_t>::value,
     108             :                 "Function read_lts can only be applied to a (probabilistic) lts. ");
     109             : 
     110         232 :   atermpp::aterm_stream_state state(stream);
     111         116 :   stream >> data::detail::add_index_impl;
     112             : 
     113         232 :   atermpp::aterm marker;
     114         116 :   stream >> marker;
     115             : 
     116         116 :   if (marker != labelled_transition_system_mark())
     117             :   {
     118           0 :     throw mcrl2::runtime_error("Stream does not contain a labelled transition system (LTS).");
     119             :   }
     120             : 
     121             :   // Read the header of the lts.
     122         232 :   data::data_specification spec;
     123         232 :   data::variable_list parameters;
     124         232 :   process::action_label_list action_labels;
     125             : 
     126         116 :   stream >> spec;
     127         116 :   stream >> parameters;
     128         116 :   stream >> action_labels;
     129             : 
     130         116 :   lts.set_data(spec);
     131         116 :   lts.set_process_parameters(parameters);
     132         116 :   lts.set_action_label_declarations(action_labels);
     133             : 
     134             :   // An indexed set to keep indices for multi actions.
     135         232 :   mcrl2::utilities::indexed_set<action_label_lts> multi_actions;
     136         116 :   multi_actions.insert(action_label_lts::tau_action()); // This action list represents 'tau'.
     137             : 
     138             :   // The initial state is stored and set as last.
     139         232 :   std::optional<probabilistic_lts_lts_t::probabilistic_state_t> initial_state;
     140             : 
     141             :   // Keep track of the number of states (derived from the transitions).
     142         116 :   std::size_t number_of_states = 1;
     143             : 
     144        2620 :   while (true)
     145             :   {
     146        5356 :     aterm term = stream.get();
     147        2736 :     if (!term.defined())
     148             :     {
     149             :       // The default constructed term indicates the end of the stream.
     150         116 :       break;
     151             :     }
     152             : 
     153        2620 :     if (term == transition_mark())
     154             :     {
     155        3072 :       aterm_int from;
     156        3072 :       process::timed_multi_action action;
     157        3072 :       aterm_int to;
     158             : 
     159        1536 :       stream >> from;
     160        1536 :       stream >> action;
     161        1536 :       stream >> to;
     162             : 
     163        3072 :       const action_label_lts lts_action(lps::multi_action(action.actions(),action.time()));
     164        1536 :       auto [index, inserted] = multi_actions.insert(lts_action);
     165             : 
     166        1536 :       std::size_t target_index = to.value();
     167             :       if constexpr (std::is_same<LTS, probabilistic_lts_lts_t>::value)
     168             :       {
     169             :         // For probabilistic lts it is necessary to add the state first (and use the returned index).
     170           4 :         target_index = lts.add_probabilistic_state(probabilistic_lts_lts_t::probabilistic_state_t(to.value()));
     171             :       }
     172             : 
     173             :       // Add the transition and update the number of states.
     174        1536 :       lts.add_transition(transition(from.value(), index, target_index));
     175        1536 :       number_of_states = std::max(number_of_states, std::max(from.value() + 1, to.value() + 1));
     176             : 
     177        1536 :       if (inserted)
     178             :       {
     179         868 :         std::size_t actual_index = lts.add_action(lts_action);
     180         868 :         utilities::mcrl2_unused(actual_index);
     181         868 :         assert(actual_index == index);
     182             :       }
     183             : 
     184             :     }
     185        1084 :     else if(term == probabilistic_transition_mark())
     186             :     {
     187             :       if constexpr (std::is_same<LTS, probabilistic_lts_lts_t>::value)
     188             :       {
     189         208 :         aterm_int from;
     190         208 :         process::timed_multi_action action;
     191         208 :         probabilistic_lts_lts_t::probabilistic_state_t to;
     192             : 
     193         104 :         stream >> from;
     194         104 :         stream >> action;
     195         104 :         stream >> to;
     196             : 
     197         208 :         const action_label_lts lts_action(lps::multi_action(action.actions(),action.time()));
     198         104 :         auto [index, inserted] = multi_actions.insert(lts_action);
     199             : 
     200             :         // Compute the index of the probabilistic state by adding it.
     201         104 :         std::size_t to_index = lts.add_probabilistic_state(to);
     202         104 :         lts.add_transition(transition(from.value(), index, to_index));
     203             : 
     204             :         // Update the number of states
     205         104 :         number_of_states = std::max(number_of_states, std::max(from.value() + 1, to_index + 1));
     206             : 
     207         104 :         if (inserted)
     208             :         {
     209          32 :           std::size_t actual_index = lts.add_action(action_label_lts(lps::multi_action(action.actions())));
     210          32 :           utilities::mcrl2_unused(actual_index);
     211          32 :           assert(actual_index == index);
     212             :         }
     213             :       }
     214             :       else
     215             :       {
     216           0 :         throw mcrl2::runtime_error("Attempting to read a probabilistic LTS as a regular LTS.");
     217             :       }
     218             :     }
     219         980 :     else if (term.function() == atermpp::detail::g_term_pool().as_list())
     220             :     {
     221             :       // Lists always represent state labels, only need to add the indices.
     222         864 :       lts.add_state(reinterpret_cast<const state_label_lts&>(term));
     223             :     }
     224         116 :     else if (term == initial_state_mark())
     225             :     {
     226             :       // Read the initial state.
     227         232 :       probabilistic_lts_lts_t::probabilistic_state_t state;
     228         116 :       stream >> state;
     229         116 :       initial_state = state;
     230             :     }
     231             :     else
     232             :     {
     233           0 :       throw mcrl2::runtime_error("Unknown mark in labelled transition system (LTS) stream.");
     234             :     }
     235             :   }
     236             : 
     237             :   // The initial state can only be set after the states are known.
     238         116 :   if (initial_state)
     239             :   {
     240             :     // If the lts has no state labels, we need to add empty states labels.
     241         116 :     lts.set_num_states(number_of_states, lts.has_state_info());
     242             : 
     243         116 :     set_initial_state(lts, initial_state.value());
     244             :   }
     245             :   else
     246             :   {
     247           0 :     throw mcrl2::runtime_error("Missing initial state in labelled transition system (LTS) stream.");
     248             :   }
     249         116 : }
     250             : 
     251             : template <class LTS_TRANSITION_SYSTEM>     
     252         116 : static void read_from_lts(LTS_TRANSITION_SYSTEM& lts, const std::string& filename)
     253             : {
     254             :   static_assert(std::is_same<LTS_TRANSITION_SYSTEM,probabilistic_lts_lts_t>::value || 
     255             :                 std::is_same<LTS_TRANSITION_SYSTEM,lts_lts_t>::value,
     256             :                 "Function read_from_lts can only be applied to a (probabilistic) lts. ");
     257             : 
     258         232 :   std::ifstream fstream;
     259         116 :   if (!filename.empty())
     260             :   {
     261         116 :     fstream.open(filename, std::ifstream::in | std::ifstream::binary);
     262         116 :     if (fstream.fail())
     263             :     {
     264           0 :       if (filename.empty())
     265             :       {
     266           0 :         throw mcrl2::runtime_error("Fail to open standard input to read an lts.");
     267             :       }
     268             :       else 
     269             :       {
     270           0 :         throw mcrl2::runtime_error("Fail to open file " + filename + " to read an lts.");
     271             :       }
     272             :     }
     273             :   }
     274             : 
     275             :   try
     276             :   {
     277         232 :     atermpp::binary_aterm_istream stream(filename.empty() ? std::cin : fstream);
     278         116 :     stream >> lts;
     279             :   }
     280           0 :   catch (const std::exception& ex)
     281             :   {
     282           0 :     mCRL2log(log::error) << ex.what() << "\n";
     283           0 :     if (filename.empty())
     284             :     {
     285           0 :       throw mcrl2::runtime_error("Fail to correctly read an lts from standard input.");
     286             :     }
     287             :     else
     288             :     {
     289           0 :       throw mcrl2::runtime_error("Fail to correctly read an lts from the file " + filename + ".");
     290             :     }
     291             :   }
     292         116 : }
     293             : 
     294          62 : void write_initial_state(atermpp::aterm_ostream& stream, const probabilistic_lts_lts_t& lts)
     295             : {
     296          62 :   stream << detail::initial_state_mark();
     297          62 :   stream << lts.initial_probabilistic_state();
     298          62 : }
     299             : 
     300          54 : void write_initial_state(atermpp::aterm_ostream& stream, const lts_lts_t& lts)
     301             : {
     302          54 :   stream << detail::initial_state_mark();
     303          54 :   stream << probabilistic_lts_lts_t::probabilistic_state_t(lts.initial_state());
     304          54 : }
     305             : 
     306             : template <class LTS>
     307         116 : static void write_lts(atermpp::aterm_ostream& stream, const LTS& lts)
     308             : {
     309             :   static_assert(std::is_same<LTS,probabilistic_lts_lts_t>::value ||
     310             :                 std::is_same<LTS,lts_lts_t>::value,
     311             :                 "Function write_lts can only be applied to a (probabilistic) lts. ");
     312             : 
     313             :   // Write the process related information.
     314         116 :   write_lts_header(stream,
     315             :    lts.data(),
     316             :    lts.process_parameters(),
     317             :    lts.action_label_declarations());
     318             : 
     319        1756 :   for (auto& trans : lts.get_transitions())
     320             :   {
     321        3280 :     lts_lts_t::action_label_t label = lts.action_label(lts.apply_hidden_label_map(trans.label()));
     322             : 
     323             :     if constexpr (std::is_same<LTS, probabilistic_lts_lts_t>::value)
     324             :     {
     325         874 :       write_transition(stream, trans.from(), process::timed_multi_action(label.actions(), label.time()), lts.probabilistic_state(trans.to()));
     326             :     }
     327             :     else
     328             :     {
     329         766 :       write_transition(stream, trans.from(), process::timed_multi_action(label.actions(), label.time()), trans.to());
     330             :     }
     331             :   }
     332             : 
     333         116 :   if (lts.has_state_info())
     334             :   {
     335         980 :     for (std::size_t i = 0; i < lts.num_state_labels(); ++i)
     336             :     {
     337             :       // Write state labels as such, we assume that all list terms without headers are state labels.
     338         864 :       stream << lts.state_label(i);
     339             :     }
     340             :   }
     341             : 
     342             :   // Write the initial state.
     343         116 :   write_initial_state(stream, lts);
     344         116 : }
     345             : 
     346             : template <class LTS_TRANSITION_SYSTEM>
     347         116 : static void write_to_lts(const LTS_TRANSITION_SYSTEM& lts, const std::string& filename)
     348             : {
     349             :   static_assert(std::is_same<LTS_TRANSITION_SYSTEM,probabilistic_lts_lts_t>::value ||
     350             :                 std::is_same<LTS_TRANSITION_SYSTEM,lts_lts_t>::value,
     351             :                 "Function write_to_lts can only be applied to a (probabilistic) lts. ");
     352             : 
     353         232 :   std::ofstream fstream;
     354         116 :   if (!filename.empty())
     355             :   {
     356         116 :     fstream.open(filename, std::ofstream::out | std::ofstream::binary);
     357         116 :     if (fstream.fail())
     358             :     {
     359           0 :       throw mcrl2::runtime_error("Fail to open file " + filename + " for writing.");
     360             :     }
     361             :   }
     362             : 
     363             :   try
     364             :   {
     365         232 :     atermpp::binary_aterm_ostream stream(filename.empty() ? std::cout : fstream);
     366         116 :     stream << lts;
     367             :   }
     368           0 :   catch (const std::exception& ex)
     369             :   {
     370           0 :     mCRL2log(log::error) << ex.what() << "\n";
     371           0 :     throw mcrl2::runtime_error("Fail to write lts correctly to the file " + filename + ".");
     372             :   }
     373         116 : }
     374             : 
     375             : } // namespace detail
     376             : 
     377             : // Implementation of public functions.
     378             : 
     379         108 : atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, lts_lts_t& lts)
     380             : {
     381         108 :   read_lts(stream, lts);
     382         108 :   return stream;
     383             : }
     384             : 
     385           8 : atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, probabilistic_lts_lts_t& lts)
     386             : {
     387           8 :   read_lts(stream, lts);
     388           8 :   return stream;
     389             : }
     390             : 
     391          54 : atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const lts_lts_t& lts)
     392             : {
     393          54 :   detail::write_lts(stream, lts);
     394          54 :   return stream;
     395             : }
     396             : 
     397          62 : atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const probabilistic_lts_lts_t& lts)
     398             : {
     399          62 :   detail::write_lts(stream, lts);
     400          62 :   return stream;
     401             : }
     402             : 
     403         116 : void write_lts_header(atermpp::aterm_ostream& stream,
     404             :   const data::data_specification& data_spec,
     405             :   const data::variable_list& parameters,
     406             :   const process::action_label_list& action_labels)
     407             : {
     408             :   // We set the transformer for all other elements (transitions, state labels and the initial state).
     409         116 :   stream << data::detail::remove_index_impl;
     410             : 
     411             :   // Write the header of the lts.
     412         116 :   stream << detail::labelled_transition_system_mark();
     413         116 :   stream << data_spec;
     414         116 :   stream << parameters;
     415         116 :   stream << action_labels;
     416         116 : }
     417             : 
     418        1536 : void write_transition(atermpp::aterm_ostream& stream, std::size_t from, const process::timed_multi_action& label, std::size_t to)
     419             : {
     420        1536 :   stream << detail::transition_mark();
     421        1536 :   stream << atermpp::aterm_int(from);
     422        1536 :   stream << label;
     423        1536 :   stream << atermpp::aterm_int(to);
     424        1536 : }
     425             : 
     426         874 : void write_transition(atermpp::aterm_ostream& stream, std::size_t from, const process::timed_multi_action& label, const probabilistic_lts_lts_t::probabilistic_state_t& to)
     427             : {
     428         874 :   if (to.size() == 1)
     429             :   {
     430             :     // Actually a non probabilistic transition.
     431         770 :     write_transition(stream, from, label, to.begin()->state());
     432             :   }
     433             :   else
     434             :   {
     435         104 :     stream << detail::probabilistic_transition_mark();
     436         104 :     stream << atermpp::aterm_int(from);
     437         104 :     stream << label;
     438         104 :     stream << to;
     439             :   }
     440         874 : }
     441             : 
     442           0 : void write_state_label(atermpp::aterm_ostream& stream, const state_label_lts& label)
     443             : {
     444             :   // During reading we assume that state labels are the only aterm_list.
     445           0 :   stream << label;
     446           0 : }
     447             : 
     448           0 : void write_initial_state(atermpp::aterm_ostream& stream, std::size_t index)
     449             : {
     450           0 :   stream << detail::initial_state_mark();
     451           0 :   stream << probabilistic_lts_lts_t::probabilistic_state_t(index);
     452           0 : }
     453             : 
     454          62 : void probabilistic_lts_lts_t::save(const std::string& filename) const
     455             : {
     456          62 :   mCRL2log(log::verbose) << "Starting to save a probabilistic lts to the file " << filename << ".\n";
     457          62 :   detail::write_to_lts(*this, filename);
     458          62 : }
     459             : 
     460          54 : void lts_lts_t::save(std::string const& filename) const
     461             : {
     462          54 :   mCRL2log(log::verbose) << "Starting to save an lts to the file " << filename << ".\n";
     463          54 :   detail::write_to_lts(*this, filename);
     464          54 : }
     465             : 
     466           8 : void probabilistic_lts_lts_t::load(const std::string& filename)
     467             : {
     468           8 :   mCRL2log(log::verbose) << "Starting to load a probabilistic lts from the file " << filename << ".\n";
     469           8 :   detail::read_from_lts(*this, filename);
     470           8 : }
     471             : 
     472         108 : void lts_lts_t::load(const std::string& filename)
     473             : {
     474         108 :   mCRL2log(log::verbose) << "Starting to load an lts from the file " << filename << ".\n";
     475         108 :   detail::read_from_lts(*this, filename);
     476         108 : }
     477             : 
     478          21 : } // namespace mcrl2::lts

Generated by: LCOV version 1.13