LCOV - code coverage report
Current view: top level - lts/source - liblts_lts.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 224 304 73.7 %
Date: 2019-06-19 00:50:04 Functions: 45 55 81.8 %
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 <string>
      12             : #include <cstring>
      13             : #include <sstream>
      14             : #include "mcrl2/atermpp/aterm_int.h"
      15             : #include "mcrl2/data/data_expression.h"
      16             : #include "mcrl2/data/detail/io.h"
      17             : #include "mcrl2/lps/multi_action.h"
      18             : #include "mcrl2/lts/lts_lts.h"
      19             : // #include "mcrl2/lts/detail/liblts_swap_to_from_probabilistic_lts.h"
      20             : 
      21             : namespace mcrl2
      22             : {
      23             : namespace lts
      24             : {
      25             : namespace detail
      26             : {
      27             : 
      28             : using namespace atermpp;
      29             : 
      30        2598 : static atermpp::function_symbol transition_empty_header()
      31             : {
      32        2598 :   static atermpp::function_symbol tr("transition_empty_list",0);
      33        2598 :   return tr;
      34             : }
      35             : 
      36        3810 : static atermpp::function_symbol probabilistic_transition_list_header()  // This contains a transition with a probabilistic target.
      37             : {
      38        3810 :   static atermpp::function_symbol tr("transition_list",4);
      39        3810 :   return tr;
      40             : }
      41             : 
      42        3810 : static atermpp::function_symbol plain_transition_list_header()  // This contains a transition with a single state as target. 
      43             : {
      44        3810 :   static atermpp::function_symbol tr("plain_transition_list",4);
      45        3810 :   return tr;
      46             : }
      47             : 
      48         260 : static atermpp::function_symbol num_of_states_labels_and_initial_state()
      49             : {
      50         260 :   static atermpp::function_symbol nslais("num_of_states_labels_and_initial_state",3);
      51         260 :   return nslais;
      52             : }
      53             : 
      54         208 : static atermpp::function_symbol lts_header()
      55             : {
      56         208 :   static atermpp::function_symbol lts("labelled_transition_system",4);
      57         208 :   return lts;
      58             : }
      59             : 
      60         572 : static atermpp::function_symbol meta_data_header()
      61             : {
      62         572 :   static atermpp::function_symbol mdh("meta_data_header",4);
      63         572 :   return mdh;
      64             : }
      65             : 
      66         944 : static atermpp::function_symbol temporary_multi_action_header()
      67             : {
      68         944 :   static atermpp::function_symbol mdh("multi_action",2);
      69         944 :   return mdh;
      70             : }
      71             : 
      72          52 : static aterm_list state_probability_list(const probabilistic_lts_lts_t::probabilistic_state_t& target)
      73             : {
      74          52 :   aterm_list result;
      75         104 :   for(const lps::state_probability_pair<std::size_t, mcrl2::lps::probabilistic_data_expression>& p: target)
      76             :   {
      77          52 :     result.push_front(p.probability());
      78          52 :     result.push_front(aterm_int(p.state()));
      79             :   }
      80          52 :   return result;
      81             : }
      82             : 
      83         104 : static probabilistic_lts_lts_t::probabilistic_state_t aterm_list_to_probabilistic_state(const atermpp::aterm_list& l)
      84             : {
      85         208 :   std::vector<lps::state_probability_pair<std::size_t, mcrl2::lps::probabilistic_data_expression>> result;
      86         208 :   for(aterm_list::const_iterator i=l.begin(); i!=l.end(); ++i)
      87             :   {
      88         104 :     const std::size_t state_number=down_cast<aterm_int>(*i).value();
      89         104 :     assert(i!=l.end());
      90         104 :     ++i;
      91         104 :     const lps::probabilistic_data_expression& t=down_cast<lps::probabilistic_data_expression>(*i);
      92         104 :     result.push_back(lps::state_probability_pair<std::size_t, mcrl2::lps::probabilistic_data_expression>(state_number,t));
      93             :   }
      94         208 :   return probabilistic_lts_lts_t::probabilistic_state_t(result.begin(),result.end());
      95             : }
      96             : 
      97             : /// Below we introduce aterm representations for a list with all transition,
      98             : /// which can subsequently be stored as an aterm.
      99        4174 : class aterm_probabilistic_transition_list: public aterm_appl
     100             : {
     101             :   public:
     102          52 :     aterm_probabilistic_transition_list()
     103          52 :       : aterm_appl(transition_empty_header())
     104          52 :     {}
     105             : 
     106             :     // Construct a probabilistic transition list element. If the target probabilistic state only contains
     107             :     // a single state, store it as a plain_transition_element. 
     108           0 :     aterm_probabilistic_transition_list(const std::size_t source, 
     109             :                                         const std::size_t label, 
     110             :                                         const probabilistic_lts_lts_t::probabilistic_state_t& target,
     111             :                                         const aterm_probabilistic_transition_list& next_transition)
     112           0 :       : aterm_appl((target.size()==1)?plain_transition_list_header():probabilistic_transition_list_header(), 
     113             :                    aterm_int(source),
     114             :                    aterm_int(label), 
     115           0 :                    ((target.size()==1)?
     116           0 :                            static_cast<aterm>(aterm_int(target.begin()->state())):
     117           0 :                            static_cast<aterm>(state_probability_list(target))),
     118           0 :                    next_transition)
     119           0 :     {} 
     120             : 
     121         762 :     aterm_probabilistic_transition_list(const std::size_t source, 
     122             :                                         const std::size_t label, 
     123             :                                         const std::size_t target,
     124             :                                         const aterm_probabilistic_transition_list& next_transition)
     125        1524 :       : aterm_appl(plain_transition_list_header(), 
     126             :                    aterm_int(source),
     127             :                    aterm_int(label), 
     128             :                    aterm_int(target),
     129        2286 :                    next_transition)
     130         762 :     {} 
     131             : 
     132         762 :     bool is_probabilistic_transition()
     133             :     {
     134         762 :       assert(function()==probabilistic_transition_list_header() || function()==plain_transition_list_header());
     135         762 :       return function()==probabilistic_transition_list_header();
     136             :     }
     137             : 
     138         762 :     std::size_t source() const
     139             :     {
     140         762 :       return (atermpp::down_cast<aterm_int>((*this)[0]).value());
     141             :     }
     142             : 
     143         762 :     std::size_t label() const
     144             :     {
     145         762 :       return (atermpp::down_cast<aterm_int>((*this)[1]).value());
     146             :     }
     147             : 
     148           0 :     probabilistic_lts_lts_t::probabilistic_state_t probabilistic_target() const
     149             :     {
     150           0 :       if (function()==plain_transition_list_header())
     151             :       {
     152           0 :         return probabilistic_lts_lts_t::probabilistic_state_t(atermpp::down_cast<aterm_int>((*this)[2]).value());
     153             :       } 
     154           0 :       assert(function()==probabilistic_transition_list_header());
     155           0 :       return aterm_list_to_probabilistic_state(atermpp::down_cast<aterm_list>((*this)[2]));
     156             :     }
     157             : 
     158         762 :     std::size_t plain_target() const
     159             :     {
     160         762 :       return atermpp::down_cast<aterm_int>((*this)[2]).value();
     161             :     }
     162             : 
     163        2286 :     const aterm_probabilistic_transition_list& next() const 
     164             :     {
     165        2286 :       return atermpp::down_cast<aterm_probabilistic_transition_list>((*this)[3]);
     166             :     }
     167             : };
     168             : 
     169             : // typedef term_list<aterm_probabilistic_transition> aterm_transition_list;
     170             : typedef term_list<state_label_lts> state_labels_t;               // The state labels listed consecutively.
     171             : typedef term_list<atermpp::aterm_appl> action_labels_t;          // A multiaction has the shape "multi_action(action_list,data_expression)
     172             : typedef term_list<data::data_expression> probabilistic_labels_t; // This contains a list of probabilities.
     173             : typedef term_list<data::function_symbol> boolean_list_t;         // A list with constants true or false, indicating
     174             :                                                                  // whether a state is probabilistic.
     175             : 
     176         520 : class aterm_labelled_transition_system: public atermpp::aterm_appl
     177             : {
     178             :   public:
     179         260 :     aterm_labelled_transition_system(const aterm& a)
     180         260 :       : aterm_appl(a)
     181         260 :     {}
     182             : 
     183          52 :     aterm_labelled_transition_system(
     184             :                const probabilistic_lts_lts_t& ts,
     185             :                const aterm_probabilistic_transition_list& transitions,
     186             :                const state_labels_t& state_label_list,
     187             :                const action_labels_t& action_label_list)
     188         104 :       : aterm_appl(lts_header(),
     189         104 :                    aterm_appl(meta_data_header(),
     190         104 :                               data::detail::data_specification_to_aterm(ts.data()),
     191          52 :                               ts.process_parameters(),
     192          52 :                               ts.action_label_declarations(),
     193         104 :                               aterm_appl(num_of_states_labels_and_initial_state(),
     194             :                                          aterm_int(ts.num_states()),
     195             :                                          aterm_int(ts.num_action_labels()),
     196         104 :                                          state_probability_list(ts.initial_probabilistic_state()))),
     197             :                    transitions,
     198             :                    state_label_list,
     199             :                    action_label_list
     200         364 :                   )
     201          52 :     {}
     202             : 
     203           0 :     aterm_labelled_transition_system(
     204             :                const lts_lts_t& ts,
     205             :                const aterm_probabilistic_transition_list& transitions,
     206             :                const state_labels_t& state_label_list,
     207             :                const action_labels_t& action_label_list)
     208           0 :       : aterm_appl(lts_header(),
     209           0 :                    aterm_appl(meta_data_header(),
     210           0 :                               data::detail::data_specification_to_aterm(ts.data()),
     211           0 :                               ts.process_parameters(),
     212           0 :                               ts.action_label_declarations(),
     213           0 :                               aterm_appl(num_of_states_labels_and_initial_state(),
     214             :                                          aterm_int(ts.num_states()),
     215             :                                          aterm_int(ts.num_action_labels()),
     216           0 :                                          state_probability_list(probabilistic_lts_lts_t::probabilistic_state_t(ts.initial_state())))),
     217             :                    transitions,
     218             :                    state_label_list,
     219             :                    action_label_list
     220           0 :                   )
     221           0 :     {}
     222             : 
     223             :     // \brief add_index() adds a unique index to some term types, such as variables, to access data about them 
     224             :     //        quickly. When loading a term, these indices must first be added before a term can be used in the toolset.
     225          52 :     void add_indices()
     226             :     {
     227         104 :       aterm_appl md=meta_data();
     228         104 :       aterm_probabilistic_transition_list trans=transitions(); 
     229         104 :       state_labels_t state_labels=get_state_labels();
     230         104 :       action_labels_t action_label_declarations=get_action_label_declarations();
     231             :       
     232          52 :       (*this)=aterm(); // Clear this aterm. It is often huge, and in this way the list of transitions can be garbage collected,
     233             :                        // while being transformed. 
     234             :       
     235             :       // Add indices to the transitions. This list is often too long to fit on the stack.
     236             :       // Therefore, it is done using this ad_hoc routine. Note that the list is reverted. 
     237             : 
     238         104 :       std::unordered_map<atermpp::aterm_appl, atermpp::aterm> cache;
     239         104 :       aterm_appl new_trans=aterm_appl(transition_empty_header());
     240        1576 :       while (trans.function()!= transition_empty_header())
     241             :       {
     242         762 :         assert(trans.size()>3);
     243         762 :         if (trans.function()==probabilistic_transition_list_header())
     244             :         {
     245           0 :           new_trans=aterm_appl(probabilistic_transition_list_header(),
     246           0 :                              trans[0],
     247           0 :                              trans[1],
     248           0 :                              data::detail::add_index(trans[2],cache),
     249           0 :                              new_trans);
     250             :         }
     251             :         else
     252             :         {
     253        1524 :           new_trans=aterm_appl(plain_transition_list_header(),
     254         762 :                              trans[0],
     255         762 :                              trans[1],
     256         762 :                              trans[2],
     257         762 :                              new_trans);
     258             :         }
     259         762 :         trans=trans.next();
     260             :       }
     261             :       
     262         104 :       *this = aterm_appl(lts_header(),
     263         104 :                              data::detail::add_index(md,cache),
     264             :                              new_trans,
     265         104 :                              data::detail::add_index(state_labels,cache),
     266         156 :                              data::detail::add_index(action_label_declarations,cache));
     267          52 :     }
     268             : 
     269             :     /// \brief Remove indices from dedicated terms such as variables and process names. 
     270             :     //  Note that this code can be optimised, as in non probabilistic transition systems
     271             :     //  the code for add indices can be skipped on transition lists. 
     272          52 :     void remove_indices()
     273             :     {
     274         104 :       aterm_appl md=meta_data();
     275         104 :       aterm_probabilistic_transition_list trans=transitions(); 
     276         104 :       state_labels_t state_labels=get_state_labels();
     277         104 :       action_labels_t action_label_declarations=get_action_label_declarations();
     278             :       
     279          52 :       (*this)=aterm(); // Clear this aterm. It is often huge, and in this way the list of transitions can be garbage collected,
     280             :                        // while being transformed. 
     281             :       
     282         104 :       std::unordered_map<atermpp::aterm_appl, atermpp::aterm> cache;
     283             :       // Remove indices from the transitions. This list is often too long to fit on the stack.
     284             :       // Therefore, it is done using this ad_hoc routine. Note that the list is reverted. 
     285             :       
     286         104 :       aterm_appl new_trans=aterm_appl(transition_empty_header());
     287        1576 :       while (trans.function()!= transition_empty_header())
     288             :       {
     289         762 :         if (trans.function()==probabilistic_transition_list_header())
     290             :         {
     291           0 :           new_trans=aterm_appl(probabilistic_transition_list_header(),
     292           0 :                                  trans[0],
     293           0 :                                  trans[1],
     294           0 :                                  data::detail::remove_index(trans[2],cache),
     295           0 :                                  new_trans);
     296             :         }
     297             :         else 
     298             :         {
     299        1524 :           new_trans=aterm_appl(plain_transition_list_header(),
     300         762 :                                  trans[0],
     301         762 :                                  trans[1],
     302         762 :                                  trans[2],
     303         762 :                                  new_trans);
     304             :         }
     305         762 :         trans=trans.next();
     306             :       } 
     307             : 
     308         104 :       *this = aterm_appl(lts_header(),
     309         104 :                              data::detail::remove_index(md,cache),
     310             :                              new_trans,
     311         104 :                              data::detail::remove_index(state_labels,cache),
     312         156 :                              data::detail::remove_index(action_label_declarations,cache));
     313          52 :     }
     314             : 
     315          52 :     const data::data_specification data() const
     316             :     {
     317          52 :       return data::data_specification(down_cast<aterm_appl>(meta_data()[0]));
     318             :     }
     319             :     
     320          52 :     const data::variable_list process_parameters() const
     321             :     {
     322          52 :       return down_cast<data::variable_list>(meta_data()[1]);
     323             :     }
     324             :     
     325          52 :     const process::action_label_list action_label_declarations() const
     326             :     {
     327          52 :       return down_cast<process::action_label_list>(meta_data()[2]);
     328             :     }
     329             : 
     330          52 :     std::size_t num_states() const
     331             :     {
     332          52 :       const aterm_appl& t=down_cast<aterm_appl>(meta_data()[3]);
     333          52 :       assert(t.function()==num_of_states_labels_and_initial_state());
     334          52 :       return down_cast<aterm_int>(t[0]).value();
     335             :     }
     336             : 
     337          52 :     std::size_t num_action_labels() const
     338             :     {
     339          52 :       const aterm_appl& t=down_cast<aterm_appl>(meta_data()[3]);
     340          52 :       assert(t.function()==num_of_states_labels_and_initial_state());
     341          52 :       return down_cast<aterm_int>(t[1]).value();
     342             :     }
     343             : 
     344         104 :     probabilistic_lts_lts_t::probabilistic_state_t initial_probabilistic_state() const
     345             :     {
     346         104 :       const aterm_appl& t=down_cast<aterm_appl>(meta_data()[3]);
     347         104 :       assert(t.function()==num_of_states_labels_and_initial_state());
     348             :       
     349         104 :       return aterm_list_to_probabilistic_state(down_cast<aterm_list>(t[2]));
     350             :     }
     351             :     
     352         156 :     aterm_probabilistic_transition_list transitions() const
     353             :     {
     354         156 :       return down_cast<aterm_probabilistic_transition_list>((*this)[1]);
     355             :     }
     356             :   
     357         260 :     state_labels_t get_state_labels() const
     358             :     {
     359         260 :       return down_cast<state_labels_t>((*this)[2]);
     360             :     }
     361             :   
     362         240 :     action_labels_t get_action_label_declarations() const
     363             :     {
     364         240 :       return down_cast<action_labels_t>((*this)[3]);
     365             :     }
     366             :   
     367             :   protected:
     368             :     
     369         468 :     const aterm_appl& meta_data() const
     370             :     {
     371         468 :       assert(atermpp::down_cast<aterm_appl>((*this)[0]).function()==meta_data_header());
     372         468 :       return atermpp::down_cast<aterm_appl>((*this)[0]);
     373             :     }
     374             : };
     375             : 
     376          52 : static void read_transitions(lts_lts_t& l, const aterm_labelled_transition_system& input_lts)
     377             : {
     378         104 :   aterm_probabilistic_transition_list input_transitions=input_lts.transitions();
     379             : 
     380        1576 :   while (input_transitions.function()!= transition_empty_header()) 
     381             :   {
     382        3048 :     assert(input_transitions.function()==probabilistic_transition_list_header() ||
     383        2286 :            input_transitions.function()==plain_transition_list_header()); // In this last case, there is one probabilistic target state. 
     384         762 :     if (input_transitions.is_probabilistic_transition())
     385             :     {
     386           0 :       throw mcrl2::runtime_error("Trying to read a non probabilistic LTS that appears to contain a probabilistic transition.");
     387             :     }
     388         762 :     l.add_transition(transition(input_transitions.source(), input_transitions.label(), input_transitions.plain_target()));
     389         762 :     input_transitions=input_transitions.next();
     390             :   }
     391          52 : }
     392             : 
     393           0 : static void read_transitions(probabilistic_lts_lts_t& l, const aterm_labelled_transition_system& input_lts)
     394             : {
     395           0 :   aterm_probabilistic_transition_list input_transitions=input_lts.transitions();
     396             : 
     397           0 :   while (input_transitions.function()!= transition_empty_header()) 
     398             :   {
     399           0 :     assert(input_transitions.function()==probabilistic_transition_list_header() ||
     400           0 :            input_transitions.function()==plain_transition_list_header()); // In this last case, there is one probabilistic target state. 
     401           0 :     const std::size_t prob_state_index=l.add_probabilistic_state(input_transitions.probabilistic_target());
     402           0 :     l.add_transition(transition(input_transitions.source(), input_transitions.label(), prob_state_index));
     403           0 :     input_transitions=input_transitions.next();
     404             :   }
     405           0 : }
     406             : 
     407          52 : static void set_initial_state(lts_lts_t& l, const aterm_labelled_transition_system& input_lts)
     408             : {
     409         104 :   const probabilistic_lts_lts_t::probabilistic_state_t& initial_state=input_lts.initial_probabilistic_state();
     410          52 :   if (initial_state.size()>1)
     411             :   {
     412           0 :     throw mcrl2::runtime_error("The initial state of the non probabilistic input lts is probabilistic.");
     413             :   }
     414          52 :   l.set_initial_state(input_lts.initial_probabilistic_state().begin()->state());
     415          52 : }
     416             : 
     417           0 : static void set_initial_state(probabilistic_lts_lts_t& l, const aterm_labelled_transition_system& input_lts)
     418             : {
     419           0 :   l.set_initial_probabilistic_state(input_lts.initial_probabilistic_state());
     420           0 : }
     421             : 
     422             : template <class LTS_TRANSITION_SYSTEM>     
     423          52 : static void read_from_lts(LTS_TRANSITION_SYSTEM& l, const std::string& filename)
     424             : {
     425             :   static_assert(std::is_same<LTS_TRANSITION_SYSTEM,probabilistic_lts_lts_t>::value || 
     426             :                 std::is_same<LTS_TRANSITION_SYSTEM,lts_lts_t>::value,
     427             :                 "Function read_from_lts can only be applied to a (probabilistic) lts. ");
     428         104 :   aterm input;
     429          52 :   if (filename=="")
     430             :   {
     431           0 :     input=read_term_from_binary_stream(std::cin);
     432             :   }
     433             :   else 
     434             :   {
     435         104 :     std::ifstream stream;
     436          52 :     stream.exceptions ( std::ifstream::failbit | std::ifstream::badbit );
     437             :     try
     438             :     {  
     439          52 :       stream.open(filename, std::ifstream::in | std::ifstream::binary);
     440             :     }
     441           0 :     catch (std::ifstream::failure&)
     442             :     {
     443           0 :       if (filename=="")
     444             :       {
     445           0 :         throw mcrl2::runtime_error("Fail to open standard input to read an lts.");
     446             :       }
     447             :       else 
     448             :       {
     449           0 :         throw mcrl2::runtime_error("Fail to open file " + filename + " to read an lts.");
     450             :       }
     451             :     }
     452             : 
     453             :     try
     454             :     {
     455          52 :       input=atermpp::read_term_from_binary_stream(stream);
     456          52 :       stream.close();
     457             :     }
     458           0 :     catch (std::ifstream::failure&)
     459             :     {
     460           0 :       if (filename=="")
     461             :       {
     462           0 :         throw mcrl2::runtime_error("Fail to correctly read an lts from standard input.");
     463             :       }
     464             :       else
     465             :       {
     466           0 :         throw mcrl2::runtime_error("Fail to correctly read an lts from the file " + filename + ".");
     467             :       }
     468             :     }
     469             :     
     470             :   }
     471             : 
     472          52 :   if (!input.type_is_appl() || down_cast<aterm_appl>(input).function()!=lts_header())
     473             :   {
     474           0 :     throw runtime_error("The input file " + filename + " is not in proper .lts format.");
     475             :   }
     476             :   
     477             :   // First check whether the input is a valid lts.
     478         104 :   const aterm meta_data=atermpp::down_cast<aterm_appl>(input)[0];
     479          52 :   if (!meta_data.type_is_appl() || down_cast<aterm_appl>(meta_data).function()!=meta_data_header())
     480             :   {
     481           0 :     throw runtime_error("The input file " + filename + " is not in proper .lts format. There is a problem with the datatypes, process parameters and action declarations.");
     482             :   }
     483             :   
     484         104 :   aterm_labelled_transition_system input_lts(input); // We are copying an aterm. This is cheap. 
     485          52 :   input_lts.add_indices();  // Add indices to certain term types, such as variables, and process/pbes names. 
     486             :   
     487          52 :   l.set_data(input_lts.data());
     488             : 
     489          52 :   l.set_process_parameters(input_lts.process_parameters());
     490             : 
     491          52 :   l.set_action_label_declarations(input_lts.action_label_declarations());
     492             :   
     493             :   // reading transition differs for an lts_lts and a probabilistic_lts.
     494          52 :   read_transitions(l,input_lts);
     495             : 
     496          52 :   if (input_lts.get_state_labels().size()==0)
     497             :   {
     498           0 :     l.set_num_states(input_lts.num_states());
     499             :   }
     500             :   else
     501             :   {
     502          52 :     assert(input_lts.num_states()==input_lts.get_state_labels().size());
     503         426 :     for (const state_label_lts& state_label: input_lts.get_state_labels())
     504             :     {
     505         374 :       l.add_state(state_label_lts(state_label));
     506             :     }
     507             :   }
     508             : 
     509          52 :   if (input_lts.get_action_label_declarations().size()==0)
     510             :   {
     511          10 :     l.set_num_action_labels(input_lts.num_action_labels());
     512             :   }
     513             :   else
     514             :   {
     515          42 :     assert(input_lts.num_action_labels()==input_lts.get_action_label_declarations().size());
     516         514 :     for (const atermpp::aterm_appl& t: input_lts.get_action_label_declarations())
     517             :     {
     518         472 :       assert(t.function()==temporary_multi_action_header());
     519         944 :       const lps::multi_action action=lps::multi_action(down_cast<process::action_list>(t[0]), down_cast<data::data_expression>(t[1]));
     520         472 :       if (!action.actions().empty() || action.has_time()) // The empty label is tau, which is present by default.
     521             :       {
     522         430 :         l.add_action(action_label_lts(action)); 
     523             :       }
     524             :     }
     525             :   }
     526          52 :   set_initial_state(l, input_lts);
     527          52 : }
     528             : 
     529           0 : aterm_probabilistic_transition_list make_transition_list(const lts_lts_t& l)
     530             : {
     531           0 :   aterm_probabilistic_transition_list resulting_transitions;
     532             :   
     533           0 :   for(std::vector<transition>::const_reverse_iterator i=l.get_transitions().rbegin();
     534           0 :                 i!=l.get_transitions().rend(); ++i)
     535             :   {
     536             :     // The transitions are stored in reverse order.
     537           0 :     resulting_transitions=aterm_probabilistic_transition_list(
     538             :                                 i->from(), 
     539             :                                 l.apply_hidden_label_map(i->label()), 
     540             :                                 i->to(),
     541           0 :                                 resulting_transitions);
     542             :   }
     543           0 :   return resulting_transitions;
     544             : }
     545             : 
     546          52 : aterm_probabilistic_transition_list make_transition_list(const probabilistic_lts_lts_t& l)
     547             : {
     548          52 :   aterm_probabilistic_transition_list resulting_transitions;
     549             :   
     550        2442 :   for(std::vector<transition>::const_reverse_iterator i=l.get_transitions().rbegin();
     551        1628 :                 i!=l.get_transitions().rend(); ++i)
     552             :   {
     553         762 :     const probabilistic_lts_lts_t::probabilistic_state_t& probabilistic_state = l.probabilistic_state(i->to());
     554             :     // The transitions are stored in reverse order.
     555         762 :     if (probabilistic_state.size()==1)
     556             :     {
     557             :       // The target is a single state with probability 1. 
     558        1524 :       resulting_transitions=aterm_probabilistic_transition_list(
     559             :                                 i->from(), 
     560             :                                 l.apply_hidden_label_map(i->label()), 
     561        1524 :                                 probabilistic_state.begin()->state(),
     562         762 :                                 resulting_transitions);
     563             :     }
     564             :     else
     565             :     {
     566             :       // The target is a probabilistic state with at least two plain states. 
     567           0 :       resulting_transitions=aterm_probabilistic_transition_list(
     568             :                                 i->from(), 
     569             :                                 l.apply_hidden_label_map(i->label()), 
     570             :                                 probabilistic_state,
     571           0 :                                 resulting_transitions);
     572             :     }
     573             :   }
     574          52 :   return resulting_transitions;
     575             : }
     576             : 
     577             : template <class LTS_TRANSITION_SYSTEM>     
     578          52 : static void write_to_lts(const LTS_TRANSITION_SYSTEM& l, const std::string& filename)
     579             : {
     580             :   static_assert(std::is_same<LTS_TRANSITION_SYSTEM,probabilistic_lts_lts_t>::value || 
     581             :                 std::is_same<LTS_TRANSITION_SYSTEM,lts_lts_t>::value,
     582             :                 "Function read_from_lts can only be applied to a (probabilistic) lts. ");
     583             :   
     584             :   // This is different for an probabilistic lts and a non probabilistic lts. 
     585         104 :   const aterm_probabilistic_transition_list transitions=make_transition_list(l);  
     586         104 :   state_labels_t state_label_list;
     587          52 :   if (l.has_state_info())
     588         426 :   { for(std::size_t i=l.num_state_labels(); i>0;)
     589             :     {
     590         374 :       --i;
     591         374 :       state_label_list.push_front(l.state_label(i));
     592             :     }
     593             :   }
     594             : 
     595         104 :   action_labels_t action_label_list;
     596          52 :   if (l.has_action_info())
     597             :   { 
     598         514 :     for(std::size_t i=l.num_action_labels(); i>0;)
     599             :     {
     600         472 :       --i;
     601         472 :       action_label_list.push_front(atermpp::aterm_appl(temporary_multi_action_header(),l.action_label(i).actions(),l.action_label(i).time()));
     602             :     }
     603             :   }
     604             : 
     605             :   aterm_labelled_transition_system t0(l,
     606             :                                       transitions,
     607             :                                       state_label_list,
     608         104 :                                       action_label_list);
     609          52 :   t0.remove_indices();
     610             : 
     611          52 :   if (filename=="")
     612             :   {
     613           0 :     atermpp::write_term_to_binary_stream(t0, std::cout);
     614             :   }
     615             :   else 
     616             :   {
     617         104 :     std::ofstream stream;
     618          52 :     stream.exceptions ( std::ofstream::failbit | std::ofstream::badbit );
     619             :     try
     620             :     {
     621          52 :       stream.open(filename, std::ofstream::out | std::ofstream::binary);
     622             :     }
     623           0 :     catch (std::ofstream::failure&)
     624             :     {
     625           0 :       throw mcrl2::runtime_error("Fail to open file " + filename + " for writing.");
     626             :     }
     627             :     try
     628             :     { 
     629          52 :       atermpp::write_term_to_binary_stream(t0, stream);
     630          52 :       stream.close();
     631             :     }
     632           0 :     catch (std::ofstream::failure&)
     633             :     {
     634           0 :       throw mcrl2::runtime_error("Fail to write lts correctly to the file " + filename + ".");
     635             :     }
     636             :   }
     637          52 : }
     638             : 
     639             : } // namespace detail
     640             : 
     641          52 : void probabilistic_lts_lts_t::save(const std::string& filename) const
     642             : {
     643          52 :   mCRL2log(log::verbose) << "Starting to save a probabilistic lts to the file " << filename << ".\n";
     644          52 :   detail::write_to_lts(*this,filename);
     645          52 : }
     646             : 
     647           0 : void lts_lts_t::save(std::string const& filename) const
     648             : {
     649           0 :   mCRL2log(log::verbose) << "Starting to save an lts to the file " << filename << ".\n";
     650           0 :   detail::write_to_lts(*this,filename);
     651           0 : }
     652             : 
     653           0 : void probabilistic_lts_lts_t::load(const std::string& filename)
     654             : {
     655           0 :   mCRL2log(log::verbose) << "Starting to load a probabilistic lts from the file " << filename << ".\n";
     656           0 :   detail::read_from_lts(*this,filename);
     657           0 : }
     658             : 
     659          52 : void lts_lts_t::load(const std::string& filename)
     660             : {
     661          52 :   mCRL2log(log::verbose) << "Starting to load an lts from the file " << filename << ".\n";
     662          52 :   detail::read_from_lts(*this,filename);
     663          52 : }
     664             : 
     665             : 
     666             : }
     667          21 : }

Generated by: LCOV version 1.12