LCOV - code coverage report
Current view: top level - lts/source - liblts_aut.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 213 276 77.2 %
Date: 2021-05-13 00:46:59 Functions: 21 24 87.5 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Muck van Weerdenburg, 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_aut.cpp
      10             : 
      11             : #include <fstream>
      12             : #include "mcrl2/utilities/unordered_map.h"
      13             : #include "mcrl2/lts/lts_aut.h"
      14             : #include "mcrl2/lts/detail/liblts_swap_to_from_probabilistic_lts.h"
      15             : 
      16             : 
      17             : using namespace mcrl2::lts;
      18             : 
      19        5035 : static void read_newline(std::istream& is, const std::size_t line_no)
      20             : {
      21             :   char ch;
      22        5035 :   is.get(ch);
      23             : 
      24             :   // Skip over spaces
      25       10837 :   while (ch == ' ')
      26             :   {
      27        2901 :     is.get(ch);
      28             :   }
      29             : 
      30             :   // Windows systems typically have a carriage return before a newline.
      31        5035 :   if (ch == '\r')
      32             :   {
      33           0 :     is.get(ch);
      34             :   }
      35             : 
      36        5035 :   if (ch != '\n' && !is.eof()) // Last line does not need to be terminated with an eoln.
      37             :   {
      38           0 :     if (line_no==1)
      39             :     {
      40           0 :       throw mcrl2::runtime_error("Expect a newline after the header des(...,...,...).");
      41             :     }
      42             :     else
      43             :     {
      44           0 :       throw mcrl2::runtime_error("Expect a newline after the transition at line " + std::to_string(line_no) + ".");
      45             :     }
      46             :   }
      47        5035 : }
      48             : 
      49             : // reads a number, puts it in s, and reads one extra character, which must be either a space or a closing bracket.
      50        1740 : static void read_natural_number_to_string(std::istream& is, std::string& s, const std::size_t line_no)
      51             : {
      52        1740 :   assert(s.empty());
      53             :   char ch;
      54        1740 :   is >> std::skipws >> ch;
      55        5220 :   for( ; isdigit(ch) ; is.get(ch))
      56             :   {
      57        1740 :     s.push_back(ch);
      58             :   }
      59        1740 :   is.putback(ch);
      60        1740 :   if (s.empty())
      61             :   {
      62           0 :     throw mcrl2::runtime_error("Expect a number at line " + std::to_string(line_no) + ".");
      63             :   }
      64        1740 : }
      65             : 
      66             : template <class AUT_LTS_TYPE>
      67        4462 : static std::size_t find_label_index(const std::string& s, mcrl2::utilities::unordered_map < action_label_string, std::size_t >& labs, AUT_LTS_TYPE& l)
      68             : {
      69             :   std::size_t label;
      70             : 
      71        4462 :   assert(labs.at(action_label_string::tau_action())==0);
      72        8924 :   action_label_string as(s);
      73        4462 :   const mcrl2::utilities::unordered_map < action_label_string, std::size_t >::const_iterator i=labs.find(as);
      74        4462 :   if (i==labs.end())
      75             :   {
      76        2068 :     label=l.add_action(as);
      77        2068 :     labs[as]=label;
      78             :   }
      79             :   else
      80             :   {
      81        2394 :     label=i->second;
      82             :   }
      83        8924 :   return label;
      84             : }
      85             : 
      86       10367 : static void check_state(std::size_t state, std::size_t number_of_states, std::size_t line_no)
      87             : {
      88       10367 :   if (state>=number_of_states)
      89             :   {
      90           0 :     throw mcrl2::runtime_error("The state number " + std::to_string(state) + " is higher than the number of states (" +
      91           0 :                                std::to_string(number_of_states) + ").  Found at line " + std::to_string(line_no) + ".");
      92             :   }
      93       10367 : } 
      94             : 
      95         973 : static void check_states(mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t& probability_state,
      96             :                          std::size_t number_of_states, std::size_t line_no)
      97             : {
      98        2816 :   for(mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t::state_probability_pair& p: probability_state)
      99             :   {
     100        1843 :     check_state(p.state(), number_of_states, line_no);
     101             :   }
     102         973 : } 
     103             : 
     104             : // This procedure tries to read states, indicated by numbers
     105             : // with in between fractions of the shape number/number. The
     106             : // last state number is put in state. The remainder as pairs
     107             : // in the vector. Typical expected input is 3 2/3 4 1/6 78 1/6 3.
     108         973 : static void read_probabilistic_state(
     109             :   std::istream& is,
     110             :   mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t& result,
     111             :   const std::size_t line_no)
     112             : {
     113         973 :   assert(result.size()==0);
     114             : 
     115             :   std::size_t state;
     116             : 
     117         973 :   is >> std::skipws >> state;
     118             : 
     119         973 :   if (!is.good())
     120             :   {
     121           0 :     throw mcrl2::runtime_error("Expect a state number at line " + std::to_string(line_no) + ".");
     122             :   }
     123             : 
     124             :   // Check whether the next character is a digit. If so a probability follows.
     125             :   char ch;
     126         973 :   is >> std::skipws >> ch;
     127         973 :   is.putback(ch);
     128             : 
     129         973 :   if (!isdigit(ch))
     130             :   {
     131             :     // There is only a single state.
     132         605 :     result.set(state);
     133         605 :     return;
     134             :   }
     135         368 :   bool ready=false;
     136             : 
     137         736 :   mcrl2::lts::probabilistic_arbitrary_precision_fraction remainder=mcrl2::lts::probabilistic_arbitrary_precision_fraction::one();
     138        2108 :   while (is.good() && !ready)
     139             :   {
     140             :     // Now read a probabilities followed by the next state.
     141        1740 :     std::string enumerator;
     142         870 :     read_natural_number_to_string(is,enumerator,line_no);
     143             :     char ch;
     144         870 :     is >> std::skipws >> ch;
     145         870 :     if (ch != '/')
     146             :     {
     147           0 :       throw mcrl2::runtime_error("Expect a / in a probability at line " + std::to_string(line_no) + ".");
     148             :     }
     149             : 
     150        1740 :     std::string denominator;
     151         870 :     read_natural_number_to_string(is,denominator,line_no);
     152        1740 :     mcrl2::lts::probabilistic_arbitrary_precision_fraction frac(enumerator,denominator);
     153         870 :     remainder=remainder-frac;
     154         870 :     result.add(state, frac);
     155             :     
     156         870 :     is >> std::skipws >> state;
     157             : 
     158         870 :     if (!is.good())
     159             :     {
     160           0 :       throw mcrl2::runtime_error("Expect a state number at line " + std::to_string(line_no) + ".");
     161             :     }
     162             : 
     163             :     // Check whether the next character is a digit.
     164             :     
     165         870 :     is >> std::skipws >> ch;
     166         870 :     is.putback(ch);
     167             : 
     168         870 :     if (!isdigit(ch))
     169             :     {
     170         368 :       ready=true;
     171             :     }
     172             :   }
     173             :   
     174         368 :   result.add(state, remainder);
     175             : }
     176             : 
     177             : 
     178         573 : static void read_aut_header(
     179             :   std::istream& is,
     180             :   mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t& initial_state,
     181             :   std::size_t& num_transitions,
     182             :   std::size_t& num_states)
     183             : {
     184        1146 :   std::string s;
     185         573 :   is.width(3);
     186         573 :   is >> std::skipws >> s;
     187             : 
     188         573 :   if (s!="des")
     189             :   {
     190           0 :     throw mcrl2::runtime_error("Expect an .aut file to start with 'des'.");
     191             :   }
     192             : 
     193             :   char ch;
     194         573 :   is >> std::skipws >> ch;
     195             : 
     196         573 :   if (ch != '(')
     197             :   {
     198           0 :     throw mcrl2::runtime_error("Expect an opening bracket '(' after 'des' in the first line of a .aut file.");
     199             :   }
     200             : 
     201         573 :   read_probabilistic_state(is,initial_state,1);
     202             : 
     203         573 :   is >> std::skipws >> ch;
     204         573 :   if (ch != ',')
     205             :   {
     206           0 :     throw mcrl2::runtime_error("Expect a comma after the first number in the first line of a .aut file.");
     207             :   }
     208             : 
     209         573 :   is >> std::skipws >> num_transitions;
     210             : 
     211         573 :   is >> std::skipws >> ch;
     212         573 :   if (ch != ',')
     213             :   {
     214           0 :     throw mcrl2::runtime_error("Expect a comma after the second number in the first line of a .aut file.");
     215             :   }
     216             : 
     217         573 :   is >> std::skipws >> num_states;
     218             : 
     219         573 :   is >> ch;
     220             : 
     221         573 :   if (ch != ')')
     222             :   {
     223           0 :     throw mcrl2::runtime_error("Expect a closing bracket ')' after the third number in the first line of a .aut file.");
     224             :   }
     225             : 
     226         573 :   read_newline(is,1);
     227         573 : }
     228             : 
     229        5035 : static bool read_initial_part_of_an_aut_transition(
     230             :   std::istream& is,
     231             :   std::size_t& from,
     232             :   std::string& label,
     233             :   const std::size_t line_no)
     234             : {
     235             :   char ch;
     236        5035 :   is >> std::skipws >> ch;
     237        5035 :   if (is.eof())
     238             :   {
     239         573 :     return false;
     240             :   }
     241        4462 :   if (ch == 0x04) // found EOT character that separates two files
     242             :   {
     243           0 :     return false;
     244             :   }
     245             : 
     246        4462 :   is >> std::skipws >> from;
     247             : 
     248        4462 :   is >> std::skipws >> ch;
     249        4462 :   if (ch != ',')
     250             :   {
     251           0 :     throw mcrl2::runtime_error("Expect that the first number is followed by a comma at line " + std::to_string(line_no) + ".");
     252             :   }
     253             : 
     254        4462 :   is >> std::skipws >> ch;
     255        4462 :   if (ch == '"')
     256             :   {
     257        4263 :     label="";
     258             :     // In case the label is using quotes whitespaces
     259             :     // in the label are preserved. 
     260        4263 :     is >> std::noskipws >> ch;
     261      156953 :     while ((ch != '"') && !is.eof())
     262             :     {
     263       76345 :       label.push_back(ch);
     264       76345 :       is >> ch;
     265             :     }
     266        4263 :     if (ch != '"')
     267             :     {
     268           0 :       throw mcrl2::runtime_error("Expect that the second item is a quoted label (using \") at line " + std::to_string(line_no) + ".");
     269             :     }
     270        4263 :     is >> std::skipws >> ch;
     271             :   }
     272             :   else
     273             :   {
     274             :     // In case the label is not within quotes,
     275             :     // whitespaces are removed from the label. 
     276         199 :     label = ch;
     277         199 :     is >> ch;
     278         475 :     while ((ch != ',') && !is.eof())
     279             :     {
     280         138 :       label.push_back(ch);
     281         138 :       is >> ch;
     282             :     }
     283             :   }
     284             : 
     285        4462 :   if (ch != ',')
     286             :   {
     287           0 :     throw mcrl2::runtime_error("Expect a comma after the quoted label at line " + std::to_string(line_no) + ".");
     288             :   }
     289             :   
     290        4462 :   return true;
     291             : }
     292             : 
     293         415 : static bool read_aut_transition(
     294             :   std::istream& is,
     295             :   std::size_t& from,
     296             :   std::string& label,
     297             :   mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t& target_probabilistic_state,
     298             :   const std::size_t line_no)
     299             : {
     300         415 :   if (!read_initial_part_of_an_aut_transition(is,from,label,line_no))
     301             :   {
     302          15 :     return false;
     303             :   }
     304             : 
     305         400 :   read_probabilistic_state(is,target_probabilistic_state,line_no);
     306             : 
     307             :   char ch;
     308         400 :   is >> ch;
     309         400 :   if (ch != ')')
     310             :   {
     311           0 :     throw mcrl2::runtime_error("Expect a closing bracket at the end of the transition at line " + std::to_string(line_no) + ".");
     312             :   }
     313             : 
     314         400 :   read_newline(is,line_no);
     315         400 :   return true;
     316             : }
     317             : 
     318        4620 : static bool read_aut_transition(
     319             :   std::istream& is,
     320             :   std::size_t& from,
     321             :   std::string& label,
     322             :   std::size_t& to,
     323             :   const std::size_t line_no)
     324             : {
     325        4620 :   if (!read_initial_part_of_an_aut_transition(is,from,label,line_no))
     326             :   {
     327         558 :     return false;
     328             :   }
     329             : 
     330        4062 :   is >> std::skipws >> to;
     331             : 
     332             :   char ch;
     333        4062 :   is >> ch;
     334        4062 :   if (ch != ')')
     335             :   {
     336           0 :     throw mcrl2::runtime_error("Expect a closing bracket at the end of the transition at line " + std::to_string(line_no) + ".");
     337             :   }
     338             : 
     339        4062 :   read_newline(is,line_no);
     340        4062 :   return true;
     341             : }
     342             : 
     343             : 
     344          15 : static void read_from_aut(probabilistic_lts_aut_t& l, std::istream& is)
     345             : {
     346          15 :   std::size_t line_no = 1;
     347          15 :   std::size_t ntrans=0, nstate=0;
     348             : 
     349          30 :   mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t initial_probabilistic_state;
     350          15 :   read_aut_header(is,initial_probabilistic_state,ntrans,nstate);
     351             : 
     352             :   // The two unordered maps below are used to determine a unique index for each probabilistic state.
     353             :   // Because most states consist of one probabilistic state, the unordered maps are duplicated into
     354             :   // indices_of_single_probabilistic_states and indices_of_multiple_probabilistic_states.
     355             :   // The map indices_of_single_probabilistic_states requires far less memory.
     356          30 :   mcrl2::utilities::unordered_map < std::size_t, std::size_t> indices_of_single_probabilistic_states;
     357          30 :   mcrl2::utilities::unordered_map < mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t, std::size_t> indices_of_multiple_probabilistic_states;
     358             :   
     359          15 :   check_states(initial_probabilistic_state, nstate, line_no);
     360             : 
     361          15 :   if (nstate==0)
     362             :   {
     363           0 :     throw mcrl2::runtime_error("cannot parse AUT input that has no states; at least an initial state is required.");
     364             :   }
     365             : 
     366          15 :   l.set_num_states(nstate,false);
     367          15 :   l.clear_transitions(ntrans); // Reserve enough space for the transitions.
     368             :   
     369          30 :   mcrl2::utilities::unordered_map < action_label_string, std::size_t > action_labels;
     370          15 :   action_labels[action_label_string::tau_action()]=0; // A tau action is always stored at position 0.
     371          15 :   l.set_initial_probabilistic_state(initial_probabilistic_state); 
     372             : 
     373          30 :   mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t probabilistic_target_state;
     374             :   std::size_t from;
     375          30 :   std::string s;
     376             : 
     377         815 :   while (!is.eof())
     378             :   {
     379         415 :     probabilistic_target_state.clear();
     380             : 
     381         415 :     line_no++;
     382             : 
     383         415 :     if (!read_aut_transition(is,from,s,probabilistic_target_state,line_no))
     384             :     {
     385          15 :       break; // encountered EOF or something that is not a transition
     386             :     }
     387             : 
     388         400 :     check_state(from, nstate, line_no);
     389         400 :     check_states(probabilistic_target_state, nstate, line_no);
     390             :     // Check whether probabilistic state exists. 
     391         400 :     std::size_t fresh_index = indices_of_single_probabilistic_states.size()+indices_of_multiple_probabilistic_states.size();
     392             :     std::size_t index;
     393         400 :     if (probabilistic_target_state.size()==1)
     394             :     {
     395          90 :       index = indices_of_single_probabilistic_states.insert(
     396          90 :                        std::pair< std::size_t, std::size_t>
     397         225 :                        (probabilistic_target_state.begin()->state(),fresh_index)).first->second;
     398             :     }
     399             :     else
     400             :     {
     401         355 :       assert(probabilistic_target_state.size()>1);
     402         710 :       index = indices_of_multiple_probabilistic_states.insert(
     403         710 :                        std::pair< mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t, std::size_t>
     404        1065 :                        (probabilistic_target_state,fresh_index)).first->second;
     405             :     }
     406             :     
     407         400 :     if (index==fresh_index) 
     408             :     {
     409         143 :       std::size_t probabilistic_state_index=l.add_and_reset_probabilistic_state(probabilistic_target_state);
     410         143 :       assert(probabilistic_state_index==index);
     411             :       (void)probabilistic_state_index; // Avoid unused variable warning.
     412             :     }
     413             : 
     414         400 :     l.add_transition(transition(from,find_label_index(s,action_labels,l),index));
     415             :   }
     416             : 
     417          15 :   if (ntrans != l.num_transitions())
     418             :   {
     419           0 :     throw mcrl2::runtime_error("number of transitions read (" + std::to_string(l.num_transitions()) +
     420           0 :                                ") does not correspond to the number of transition given in the header (" + std::to_string(ntrans) + ").");
     421             :   }
     422          15 : }
     423             : 
     424         558 : static void read_from_aut(lts_aut_t& l, std::istream& is)
     425             : {
     426         558 :   std::size_t line_no = 1;
     427         558 :   std::size_t ntrans=0, nstate=0;
     428             : 
     429        1116 :   mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t initial_probabilistic_state;
     430         558 :   read_aut_header(is,initial_probabilistic_state,ntrans,nstate);
     431             :   
     432         558 :   if (initial_probabilistic_state.size()>1)
     433             :   {
     434           0 :     throw mcrl2::runtime_error("Encountered an initial probability distribution while reading an non probabilistic .aut file.");
     435             :   }
     436             : 
     437         558 :   check_states(initial_probabilistic_state, nstate, line_no);
     438             : 
     439         558 :   if (nstate==0)
     440             :   {
     441           0 :     throw mcrl2::runtime_error("cannot parse AUT input that has no states; at least an initial state is required.");
     442             :   }
     443             : 
     444         558 :   l.set_num_states(nstate,false);
     445         558 :   l.clear_transitions(ntrans); // Reserve enough space for the transitions.
     446             :   
     447        1116 :   mcrl2::utilities::unordered_map < action_label_string, std::size_t > action_labels;
     448         558 :   action_labels[action_label_string::tau_action()]=0; // A tau action is always stored at position 0.
     449         558 :   l.set_initial_state(initial_probabilistic_state.begin()->state()); 
     450             : 
     451             :   std::size_t from, to;
     452        1116 :   std::string s;
     453        8682 :   while (!is.eof())
     454             :   {
     455        4620 :     line_no++;
     456             : 
     457        4620 :     if (!read_aut_transition(is,from,s,to,line_no))
     458             :     {
     459         558 :       break; // eof encountered
     460             :     }
     461             : 
     462        4062 :     check_state(from, nstate, line_no);
     463        4062 :     check_state(to, nstate, line_no);
     464        4062 :     l.add_transition(transition(from,find_label_index(s,action_labels,l),to));
     465             :   }
     466             : 
     467         558 :   if (ntrans != l.num_transitions())
     468             :   {
     469           0 :     throw mcrl2::runtime_error("number of transitions read (" + std::to_string(l.num_transitions()) +
     470           0 :                                ") does not correspond to the number of transition given in the header (" + std::to_string(ntrans) + ").");
     471             :   }
     472         558 : }
     473             : 
     474             : 
     475           0 : static void write_probabilistic_state(const mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t& prob_state, std::ostream& os)
     476             : {
     477           0 :   mcrl2::lts::probabilistic_arbitrary_precision_fraction previous_probability;
     478           0 :   bool first_element=true;
     479           0 :   for (const mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t::state_probability_pair& p: prob_state)
     480             :   {
     481           0 :     if (first_element)
     482             :     {
     483           0 :       os << p.state();
     484           0 :       previous_probability=p.probability();
     485           0 :       first_element=false;
     486             :     }
     487             :     else
     488             :     {
     489           0 :       os << " " << pp(previous_probability) << " " << p.state();
     490           0 :       previous_probability=p.probability();
     491             :     }
     492             :   }
     493           0 : }
     494             : 
     495           0 : static void write_to_aut(const probabilistic_lts_aut_t& l, std::ostream& os)
     496             : {
     497             :   // Do not use "endl" below to avoid flushing. Use "\n" instead.
     498           0 :   os << "des (";
     499           0 :   write_probabilistic_state(l.initial_probabilistic_state(),os);
     500             : 
     501           0 :   os << "," << l.num_transitions() << "," << l.num_states() << ")" << "\n";
     502             : 
     503           0 :   for (const transition& t: l.get_transitions())
     504             :   {
     505           0 :     os << "(" << t.from() << ",\"" << pp(l.action_label(l.apply_hidden_label_map(t.label()))) << "\",";
     506           0 :     write_probabilistic_state(l.probabilistic_state(t.to()),os);
     507           0 :     os << ")" << "\n";
     508             :   }
     509           0 : }
     510             : 
     511          54 : static void write_to_aut(const lts_aut_t& l, std::ostream& os)
     512             : {
     513             :   // Do not use "endl" below to avoid flushing. Use "\n" instead.
     514          54 :   os << "des (" << l.initial_state() << "," << l.num_transitions() << "," << l.num_states() << ")" << "\n"; 
     515             : 
     516         820 :   for (const transition& t: l.get_transitions())
     517             :   {
     518         766 :     os << "(" << t.from() << ",\"" 
     519        1532 :        << pp(l.action_label(l.apply_hidden_label_map(t.label()))) << "\"," 
     520         766 :        << t.to() << ")" << "\n";
     521             :   }
     522          54 : }
     523             : 
     524             : namespace mcrl2
     525             : {
     526             : namespace lts
     527             : {
     528             : 
     529           8 : void probabilistic_lts_aut_t::load(const std::string& filename)
     530             : {
     531           8 :   if (filename=="" || filename=="-")
     532             :   {
     533           0 :     read_from_aut(*this, std::cin);
     534             :   }
     535             :   else
     536             :   {
     537          16 :     std::ifstream is(filename.c_str());
     538             : 
     539           8 :     if (!is.is_open())
     540             :     {
     541           0 :       throw mcrl2::runtime_error("cannot open .aut file '" + filename + ".");
     542             :     }
     543             : 
     544           8 :     read_from_aut(*this,is);
     545           8 :     is.close();
     546             :   }
     547           8 : }
     548             : 
     549           7 : void probabilistic_lts_aut_t::load(std::istream& is)
     550             : {
     551           7 :   read_from_aut(*this,is);
     552           7 : }
     553             : 
     554           0 : void probabilistic_lts_aut_t::save(std::string const& filename) const
     555             : {
     556           0 :   if (filename=="" || filename=="-")
     557             :   {
     558           0 :     write_to_aut(*this, std::cout);
     559             :   }
     560             :   else
     561             :   {
     562           0 :     std::ofstream os(filename.c_str());
     563             : 
     564           0 :     if (!os.is_open())
     565             :     {
     566           0 :       throw mcrl2::runtime_error("cannot create .aut file '" + filename + ".");
     567             :       return;
     568             :     }
     569           0 :     write_to_aut(*this,os);
     570           0 :     os.close();
     571             :   }
     572           0 : }
     573             : 
     574         121 : void lts_aut_t::load(const std::string& filename)
     575             : {
     576         121 :   if (filename=="" || filename=="-")
     577             :   {
     578           0 :     read_from_aut(*this, std::cin);
     579             :   }
     580             :   else
     581             :   {
     582         242 :     std::ifstream is(filename.c_str());
     583             : 
     584         121 :     if (!is.is_open())
     585             :     {
     586           0 :       throw mcrl2::runtime_error("cannot open .aut file '" + filename + ".");
     587             :     }
     588             : 
     589         121 :     read_from_aut(*this,is);
     590         121 :     is.close();
     591             :   }
     592         121 : }
     593             : 
     594         437 : void lts_aut_t::load(std::istream& is)
     595             : {
     596         437 :   read_from_aut(*this,is);
     597         437 : }
     598             : 
     599          54 : void lts_aut_t::save(std::string const& filename) const
     600             : {
     601          54 :   if (filename=="" || filename=="-")
     602             :   {
     603           0 :     write_to_aut(*this, std::cout);
     604             :   }
     605             :   else
     606             :   {
     607         108 :     std::ofstream os(filename.c_str());
     608             : 
     609          54 :     if (!os.is_open())
     610             :     {
     611           0 :       throw mcrl2::runtime_error("cannot create .aut file '" + filename + ".");
     612             :       return;
     613             :     }
     614          54 :     write_to_aut(*this,os);
     615          54 :     os.close();
     616             :   }
     617          54 : }
     618             : 
     619             : 
     620             : }
     621          21 : }

Generated by: LCOV version 1.13