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

Generated by: LCOV version 1.12