LCOV - code coverage report
Current view: top level - lts/source - liblts_lts.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 197 221 89.1 %
Date: 2021-05-13 00:46:59 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             :   // Ensure unique indices for the probabilistic states.
     142         232 :   mcrl2::utilities::indexed_set<probabilistic_lts_lts_t::probabilistic_state_t> probabilistic_states;
     143             : 
     144             :   // Keep track of the number of states (derived from the transitions).
     145         116 :   std::size_t number_of_states = 1;
     146             : 
     147        2620 :   while (true)
     148             :   {
     149        5356 :     aterm term = stream.get();
     150        2736 :     if (!term.defined())
     151             :     {
     152             :       // The default constructed term indicates the end of the stream.
     153         116 :       break;
     154             :     }
     155             : 
     156        2620 :     if (term == transition_mark())
     157             :     {
     158        3072 :       aterm_int from;
     159        3072 :       process::timed_multi_action action;
     160        3072 :       aterm_int to;
     161             : 
     162        1536 :       stream >> from;
     163        1536 :       stream >> action;
     164        1536 :       stream >> to;
     165             : 
     166        3072 :       const action_label_lts lts_action(lps::multi_action(action.actions(),action.time()));
     167        1536 :       const auto [index, inserted] = multi_actions.insert(lts_action);
     168             : 
     169        1536 :       std::size_t target_index = to.value();
     170             :       if constexpr (std::is_same<LTS, probabilistic_lts_lts_t>::value)
     171             :       {
     172           8 :         probabilistic_lts_lts_t::probabilistic_state_t lts_state(to.value());
     173             : 
     174             :         // For probabilistic lts it is necessary to add the state first (and use the returned index).
     175             :         bool state_inserted;
     176           4 :         std::tie(target_index, state_inserted) = probabilistic_states.insert(lts_state);
     177             : 
     178           4 :         if (state_inserted)
     179             :         {
     180           4 :           std::size_t actual_index = lts.add_probabilistic_state(lts_state);
     181           4 :           utilities::mcrl2_unused(actual_index);
     182           4 :           assert(actual_index == target_index);
     183             :         }
     184             :       }
     185             : 
     186             :       // Add the transition and update the number of states.
     187        1536 :       lts.add_transition(transition(from.value(), index, target_index));
     188        1536 :       number_of_states = std::max(number_of_states, std::max(from.value() + 1, to.value() + 1));
     189             : 
     190        1536 :       if (inserted)
     191             :       {
     192         868 :         std::size_t actual_index = lts.add_action(lts_action);
     193         868 :         utilities::mcrl2_unused(actual_index);
     194         868 :         assert(actual_index == index);
     195             :       }
     196             : 
     197             :     }
     198        1084 :     else if(term == probabilistic_transition_mark())
     199             :     {
     200             :       if constexpr (std::is_same<LTS, probabilistic_lts_lts_t>::value)
     201             :       {
     202         208 :         aterm_int from;
     203         208 :         process::timed_multi_action action;
     204         208 :         probabilistic_lts_lts_t::probabilistic_state_t to;
     205             : 
     206         104 :         stream >> from;
     207         104 :         stream >> action;
     208         104 :         stream >> to;
     209             : 
     210         208 :         const action_label_lts lts_action(lps::multi_action(action.actions(),action.time()));
     211         104 :         const auto [index, inserted] = multi_actions.insert(lts_action);
     212             : 
     213             :         // Compute the index of the probabilistic state.
     214         104 :         const auto [to_index, state_inserted] = probabilistic_states.insert(to);
     215             : 
     216         104 :         if (state_inserted)
     217             :         {
     218          48 :           std::size_t actual_index = lts.add_probabilistic_state(to);
     219          48 :           utilities::mcrl2_unused(actual_index);
     220          48 :           assert(actual_index == to_index);
     221             :         }
     222             : 
     223         104 :         lts.add_transition(transition(from.value(), index, to_index));
     224             : 
     225             :         // Update the number of states
     226         104 :         number_of_states = std::max(number_of_states, std::max(from.value() + 1, to_index + 1));
     227             : 
     228         104 :         if (inserted)
     229             :         {
     230          32 :           std::size_t actual_index = lts.add_action(action_label_lts(lps::multi_action(action.actions())));
     231          32 :           utilities::mcrl2_unused(actual_index);
     232          32 :           assert(actual_index == index);
     233             :         }
     234             :       }
     235             :       else
     236             :       {
     237           0 :         throw mcrl2::runtime_error("Attempting to read a probabilistic LTS as a regular LTS.");
     238             :       }
     239             :     }
     240         980 :     else if (term.function() == atermpp::detail::g_term_pool().as_list())
     241             :     {
     242             :       // Lists always represent state labels, only need to add the indices.
     243         864 :       lts.add_state(reinterpret_cast<const state_label_lts&>(term));
     244             :     }
     245         116 :     else if (term == initial_state_mark())
     246             :     {
     247             :       // Read the initial state.
     248         232 :       probabilistic_lts_lts_t::probabilistic_state_t state;
     249         116 :       stream >> state;
     250         116 :       initial_state = state;
     251             :     }
     252             :     else
     253             :     {
     254           0 :       throw mcrl2::runtime_error("Unknown mark in labelled transition system (LTS) stream.");
     255             :     }
     256             :   }
     257             : 
     258             :   // The initial state can only be set after the states are known.
     259         116 :   if (initial_state)
     260             :   {
     261             :     // If the lts has no state labels, we need to add empty states labels.
     262         116 :     lts.set_num_states(number_of_states, lts.has_state_info());
     263             : 
     264         116 :     set_initial_state(lts, initial_state.value());
     265             :   }
     266             :   else
     267             :   {
     268           0 :     throw mcrl2::runtime_error("Missing initial state in labelled transition system (LTS) stream.");
     269             :   }
     270         116 : }
     271             : 
     272             : template <class LTS_TRANSITION_SYSTEM>     
     273         116 : static void read_from_lts(LTS_TRANSITION_SYSTEM& lts, const std::string& filename)
     274             : {
     275             :   static_assert(std::is_same<LTS_TRANSITION_SYSTEM,probabilistic_lts_lts_t>::value || 
     276             :                 std::is_same<LTS_TRANSITION_SYSTEM,lts_lts_t>::value,
     277             :                 "Function read_from_lts can only be applied to a (probabilistic) lts. ");
     278             : 
     279         232 :   std::ifstream fstream;
     280         116 :   if (!filename.empty())
     281             :   {
     282         116 :     fstream.open(filename, std::ifstream::in | std::ifstream::binary);
     283         116 :     if (fstream.fail())
     284             :     {
     285           0 :       if (filename.empty())
     286             :       {
     287           0 :         throw mcrl2::runtime_error("Fail to open standard input to read an lts.");
     288             :       }
     289             :       else 
     290             :       {
     291           0 :         throw mcrl2::runtime_error("Fail to open file " + filename + " to read an lts.");
     292             :       }
     293             :     }
     294             :   }
     295             : 
     296             :   try
     297             :   {
     298         232 :     atermpp::binary_aterm_istream stream(filename.empty() ? std::cin : fstream);
     299         116 :     stream >> lts;
     300             :   }
     301           0 :   catch (const std::exception& ex)
     302             :   {
     303           0 :     mCRL2log(log::error) << ex.what() << "\n";
     304           0 :     if (filename.empty())
     305             :     {
     306           0 :       throw mcrl2::runtime_error("Fail to correctly read an lts from standard input.");
     307             :     }
     308             :     else
     309             :     {
     310           0 :       throw mcrl2::runtime_error("Fail to correctly read an lts from the file " + filename + ".");
     311             :     }
     312             :   }
     313         116 : }
     314             : 
     315          62 : void write_initial_state(atermpp::aterm_ostream& stream, const probabilistic_lts_lts_t& lts)
     316             : {
     317          62 :   stream << detail::initial_state_mark();
     318          62 :   stream << lts.initial_probabilistic_state();
     319          62 : }
     320             : 
     321          54 : void write_initial_state(atermpp::aterm_ostream& stream, const lts_lts_t& lts)
     322             : {
     323          54 :   stream << detail::initial_state_mark();
     324          54 :   stream << probabilistic_lts_lts_t::probabilistic_state_t(lts.initial_state());
     325          54 : }
     326             : 
     327             : template <class LTS>
     328         116 : static void write_lts(atermpp::aterm_ostream& stream, const LTS& lts)
     329             : {
     330             :   static_assert(std::is_same<LTS,probabilistic_lts_lts_t>::value ||
     331             :                 std::is_same<LTS,lts_lts_t>::value,
     332             :                 "Function write_lts can only be applied to a (probabilistic) lts. ");
     333             : 
     334             :   // Write the process related information.
     335         116 :   write_lts_header(stream,
     336             :    lts.data(),
     337             :    lts.process_parameters(),
     338             :    lts.action_label_declarations());
     339             : 
     340        1756 :   for (auto& trans : lts.get_transitions())
     341             :   {
     342        3280 :     lts_lts_t::action_label_t label = lts.action_label(lts.apply_hidden_label_map(trans.label()));
     343             : 
     344             :     if constexpr (std::is_same<LTS, probabilistic_lts_lts_t>::value)
     345             :     {
     346         874 :       write_transition(stream, trans.from(), process::timed_multi_action(label.actions(), label.time()), lts.probabilistic_state(trans.to()));
     347             :     }
     348             :     else
     349             :     {
     350         766 :       write_transition(stream, trans.from(), process::timed_multi_action(label.actions(), label.time()), trans.to());
     351             :     }
     352             :   }
     353             : 
     354         116 :   if (lts.has_state_info())
     355             :   {
     356         980 :     for (std::size_t i = 0; i < lts.num_state_labels(); ++i)
     357             :     {
     358             :       // Write state labels as such, we assume that all list terms without headers are state labels.
     359         864 :       stream << lts.state_label(i);
     360             :     }
     361             :   }
     362             : 
     363             :   // Write the initial state.
     364         116 :   write_initial_state(stream, lts);
     365         116 : }
     366             : 
     367             : template <class LTS_TRANSITION_SYSTEM>
     368         116 : static void write_to_lts(const LTS_TRANSITION_SYSTEM& lts, const std::string& filename)
     369             : {
     370             :   static_assert(std::is_same<LTS_TRANSITION_SYSTEM,probabilistic_lts_lts_t>::value ||
     371             :                 std::is_same<LTS_TRANSITION_SYSTEM,lts_lts_t>::value,
     372             :                 "Function write_to_lts can only be applied to a (probabilistic) lts. ");
     373             : 
     374         232 :   std::ofstream fstream;
     375         116 :   if (!filename.empty())
     376             :   {
     377         116 :     fstream.open(filename, std::ofstream::out | std::ofstream::binary);
     378         116 :     if (fstream.fail())
     379             :     {
     380           0 :       throw mcrl2::runtime_error("Fail to open file " + filename + " for writing.");
     381             :     }
     382             :   }
     383             : 
     384             :   try
     385             :   {
     386         232 :     atermpp::binary_aterm_ostream stream(filename.empty() ? std::cout : fstream);
     387         116 :     stream << lts;
     388             :   }
     389           0 :   catch (const std::exception& ex)
     390             :   {
     391           0 :     mCRL2log(log::error) << ex.what() << "\n";
     392           0 :     throw mcrl2::runtime_error("Fail to write lts correctly to the file " + filename + ".");
     393             :   }
     394         116 : }
     395             : 
     396             : } // namespace detail
     397             : 
     398             : // Implementation of public functions.
     399             : 
     400         108 : atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, lts_lts_t& lts)
     401             : {
     402         108 :   read_lts(stream, lts);
     403         108 :   return stream;
     404             : }
     405             : 
     406           8 : atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, probabilistic_lts_lts_t& lts)
     407             : {
     408           8 :   read_lts(stream, lts);
     409           8 :   return stream;
     410             : }
     411             : 
     412          54 : atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const lts_lts_t& lts)
     413             : {
     414          54 :   detail::write_lts(stream, lts);
     415          54 :   return stream;
     416             : }
     417             : 
     418          62 : atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const probabilistic_lts_lts_t& lts)
     419             : {
     420          62 :   detail::write_lts(stream, lts);
     421          62 :   return stream;
     422             : }
     423             : 
     424         116 : void write_lts_header(atermpp::aterm_ostream& stream,
     425             :   const data::data_specification& data_spec,
     426             :   const data::variable_list& parameters,
     427             :   const process::action_label_list& action_labels)
     428             : {
     429             :   // We set the transformer for all other elements (transitions, state labels and the initial state).
     430         116 :   stream << data::detail::remove_index_impl;
     431             : 
     432             :   // Write the header of the lts.
     433         116 :   stream << detail::labelled_transition_system_mark();
     434         116 :   stream << data_spec;
     435         116 :   stream << parameters;
     436         116 :   stream << action_labels;
     437         116 : }
     438             : 
     439        1536 : void write_transition(atermpp::aterm_ostream& stream, std::size_t from, const process::timed_multi_action& label, std::size_t to)
     440             : {
     441        1536 :   stream << detail::transition_mark();
     442        1536 :   stream << atermpp::aterm_int(from);
     443        1536 :   stream << label;
     444        1536 :   stream << atermpp::aterm_int(to);
     445        1536 : }
     446             : 
     447         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)
     448             : {
     449         874 :   if (to.size() == 1)
     450             :   {
     451             :     // Actually a non probabilistic transition.
     452         770 :     write_transition(stream, from, label, to.begin()->state());
     453             :   }
     454             :   else
     455             :   {
     456         104 :     stream << detail::probabilistic_transition_mark();
     457         104 :     stream << atermpp::aterm_int(from);
     458         104 :     stream << label;
     459         104 :     stream << to;
     460             :   }
     461         874 : }
     462             : 
     463           0 : void write_state_label(atermpp::aterm_ostream& stream, const state_label_lts& label)
     464             : {
     465             :   // During reading we assume that state labels are the only aterm_list.
     466           0 :   stream << label;
     467           0 : }
     468             : 
     469           0 : void write_initial_state(atermpp::aterm_ostream& stream, std::size_t index)
     470             : {
     471           0 :   stream << detail::initial_state_mark();
     472           0 :   stream << probabilistic_lts_lts_t::probabilistic_state_t(index);
     473           0 : }
     474             : 
     475          62 : void probabilistic_lts_lts_t::save(const std::string& filename) const
     476             : {
     477          62 :   mCRL2log(log::verbose) << "Starting to save a probabilistic lts to the file " << filename << ".\n";
     478          62 :   detail::write_to_lts(*this, filename);
     479          62 : }
     480             : 
     481          54 : void lts_lts_t::save(std::string const& filename) const
     482             : {
     483          54 :   mCRL2log(log::verbose) << "Starting to save an lts to the file " << filename << ".\n";
     484          54 :   detail::write_to_lts(*this, filename);
     485          54 : }
     486             : 
     487           8 : void probabilistic_lts_lts_t::load(const std::string& filename)
     488             : {
     489           8 :   mCRL2log(log::verbose) << "Starting to load a probabilistic lts from the file " << filename << ".\n";
     490           8 :   detail::read_from_lts(*this, filename);
     491           8 : }
     492             : 
     493         108 : void lts_lts_t::load(const std::string& filename)
     494             : {
     495         108 :   mCRL2log(log::verbose) << "Starting to load an lts from the file " << filename << ".\n";
     496         108 :   detail::read_from_lts(*this, filename);
     497         108 : }
     498             : 
     499          21 : } // namespace mcrl2::lts

Generated by: LCOV version 1.13