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 4285 : static void read_newline(std::istream& is, const std::size_t line_no)
20 : {
21 : char ch;
22 4285 : is.get(ch);
23 :
24 : // Skip over spaces
25 4293 : while (ch == ' ')
26 : {
27 8 : is.get(ch);
28 : }
29 :
30 : // Windows systems typically have a carriage return before a newline.
31 4285 : if (ch == '\r')
32 : {
33 0 : is.get(ch);
34 : }
35 :
36 4285 : 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 4285 : }
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 1694 : static void read_natural_number_to_string(std::istream& is, std::string& s, const std::size_t line_no)
51 : {
52 1694 : assert(s.empty());
53 : char ch;
54 1694 : is >> std::skipws >> ch;
55 3388 : for( ; isdigit(ch) ; is.get(ch))
56 : {
57 1694 : s.push_back(ch);
58 : }
59 1694 : is.putback(ch);
60 1694 : if (s.empty())
61 : {
62 0 : throw mcrl2::runtime_error("Expect a number at line " + std::to_string(line_no) + ".");
63 : }
64 1694 : }
65 :
66 : template <class AUT_LTS_TYPE>
67 3739 : 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 3739 : assert(labs.at(action_label_string::tau_action())==0);
72 3739 : action_label_string as(s);
73 3739 : const mcrl2::utilities::unordered_map < action_label_string, std::size_t >::const_iterator i=labs.find(as);
74 3739 : if (i==labs.end())
75 : {
76 1678 : label=l.add_action(as);
77 1678 : labs[as]=label;
78 : }
79 : else
80 : {
81 2061 : label=i->second;
82 : }
83 3739 : return label;
84 3739 : }
85 :
86 8291 : static void check_state(std::size_t state, std::size_t number_of_states, std::size_t line_no)
87 : {
88 8291 : 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 8291 : }
94 :
95 925 : 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 2117 : for(mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t::state_probability_pair& p: probability_state)
99 : {
100 1192 : check_state(p.state(), number_of_states, line_no);
101 : }
102 925 : }
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 925 : 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 925 : assert(result.size()==0);
114 :
115 : std::size_t state;
116 :
117 925 : is >> std::skipws >> state;
118 :
119 925 : 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 925 : is >> std::skipws >> ch;
127 925 : is.putback(ch);
128 :
129 925 : if (!isdigit(ch))
130 : {
131 : // There is only a single state.
132 580 : result.set(state);
133 580 : return;
134 : }
135 345 : bool ready=false;
136 :
137 345 : mcrl2::lts::probabilistic_arbitrary_precision_fraction remainder=mcrl2::lts::probabilistic_arbitrary_precision_fraction::one();
138 1192 : while (is.good() && !ready)
139 : {
140 : // Now read a probabilities followed by the next state.
141 847 : std::string enumerator;
142 847 : read_natural_number_to_string(is,enumerator,line_no);
143 : char ch;
144 847 : is >> std::skipws >> ch;
145 847 : if (ch != '/')
146 : {
147 0 : throw mcrl2::runtime_error("Expect a / in a probability at line " + std::to_string(line_no) + ".");
148 : }
149 :
150 847 : std::string denominator;
151 847 : read_natural_number_to_string(is,denominator,line_no);
152 847 : mcrl2::lts::probabilistic_arbitrary_precision_fraction frac(enumerator,denominator);
153 847 : remainder=remainder-frac;
154 847 : result.add(state, frac);
155 :
156 847 : is >> std::skipws >> state;
157 :
158 847 : 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 847 : is >> std::skipws >> ch;
166 847 : is.putback(ch);
167 :
168 847 : if (!isdigit(ch))
169 : {
170 345 : ready=true;
171 : }
172 847 : }
173 :
174 345 : result.add(state, remainder);
175 345 : }
176 :
177 :
178 546 : 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 546 : std::string s;
185 546 : is.width(3);
186 546 : is >> std::skipws >> s;
187 :
188 546 : if (s!="des")
189 : {
190 0 : throw mcrl2::runtime_error("Expect an .aut file to start with 'des'.");
191 : }
192 :
193 : char ch;
194 546 : is >> std::skipws >> ch;
195 :
196 546 : 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 546 : read_probabilistic_state(is,initial_state,1);
202 :
203 546 : is >> std::skipws >> ch;
204 546 : 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 546 : is >> std::skipws >> num_transitions;
210 :
211 546 : is >> std::skipws >> ch;
212 546 : 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 546 : is >> std::skipws >> num_states;
218 :
219 546 : is >> ch;
220 :
221 546 : 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 546 : read_newline(is,1);
227 546 : }
228 :
229 4285 : 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 4285 : is >> std::skipws >> ch;
237 4285 : if (is.eof())
238 : {
239 546 : return false;
240 : }
241 3739 : if (ch == 0x04) // found EOT character that separates two files
242 : {
243 0 : return false;
244 : }
245 :
246 3739 : is >> std::skipws >> from;
247 :
248 3739 : is >> std::skipws >> ch;
249 3739 : 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 3739 : is >> std::skipws >> ch;
255 3739 : if (ch == '"')
256 : {
257 3553 : label="";
258 : // In case the label is using quotes whitespaces
259 : // in the label are preserved.
260 3553 : is >> std::noskipws >> ch;
261 51172 : while ((ch != '"') && !is.eof())
262 : {
263 47619 : label.push_back(ch);
264 47619 : is >> ch;
265 : }
266 3553 : 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 3553 : 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 186 : label = ch;
277 186 : is >> ch;
278 298 : while ((ch != ',') && !is.eof())
279 : {
280 112 : label.push_back(ch);
281 112 : is >> ch;
282 : }
283 : }
284 :
285 3739 : 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 3739 : return true;
291 : }
292 :
293 397 : 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 397 : if (!read_initial_part_of_an_aut_transition(is,from,label,line_no))
301 : {
302 18 : return false;
303 : }
304 :
305 379 : read_probabilistic_state(is,target_probabilistic_state,line_no);
306 :
307 : char ch;
308 379 : is >> ch;
309 379 : 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 379 : read_newline(is,line_no);
315 379 : return true;
316 : }
317 :
318 3888 : 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 3888 : if (!read_initial_part_of_an_aut_transition(is,from,label,line_no))
326 : {
327 528 : return false;
328 : }
329 :
330 3360 : is >> std::skipws >> to;
331 :
332 : char ch;
333 3360 : is >> ch;
334 3360 : 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 3360 : read_newline(is,line_no);
340 3360 : return true;
341 : }
342 :
343 379 : static size_t add_probablistic_state(
344 : mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t& probabilistic_state,
345 : probabilistic_lts_aut_t& l,
346 : mcrl2::utilities::unordered_map < std::size_t, std::size_t>& indices_of_single_probabilistic_states,
347 : mcrl2::utilities::unordered_map < mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t, std::size_t>&
348 : indices_of_multiple_probabilistic_states)
349 : {
350 379 : std::size_t fresh_index = indices_of_single_probabilistic_states.size()+indices_of_multiple_probabilistic_states.size();
351 : std::size_t index;
352 : // Check whether probabilistic states exists.
353 379 : if (probabilistic_state.size()<=1)
354 : {
355 43 : index = indices_of_single_probabilistic_states.insert(
356 0 : std::pair< std::size_t, std::size_t>
357 86 : (probabilistic_state.get(),fresh_index)).first->second;
358 : }
359 : else
360 : {
361 336 : assert(probabilistic_state.size()>1);
362 336 : index = indices_of_multiple_probabilistic_states.insert(
363 672 : std::pair< mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t, std::size_t>
364 336 : (probabilistic_state,fresh_index)).first->second;
365 : }
366 :
367 379 : if (index==fresh_index)
368 : {
369 129 : std::size_t probabilistic_state_index=l.add_and_reset_probabilistic_state(probabilistic_state);
370 129 : assert(probabilistic_state_index==index);
371 : (void)probabilistic_state_index; // Avoid unused variable warning.
372 : }
373 379 : return index;
374 : }
375 :
376 :
377 18 : static void read_from_aut(probabilistic_lts_aut_t& l, std::istream& is)
378 : {
379 18 : std::size_t line_no = 1;
380 18 : std::size_t ntrans=0, nstate=0;
381 :
382 18 : mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t initial_probabilistic_state;
383 18 : read_aut_header(is,initial_probabilistic_state,ntrans,nstate);
384 :
385 : // The two unordered maps below are used to determine a unique index for each probabilistic state.
386 : // Because most states consist of one probabilistic state, the unordered maps are duplicated into
387 : // indices_of_single_probabilistic_states and indices_of_multiple_probabilistic_states.
388 : // The map indices_of_single_probabilistic_states requires far less memory.
389 18 : mcrl2::utilities::unordered_map < std::size_t, std::size_t> indices_of_single_probabilistic_states;
390 18 : mcrl2::utilities::unordered_map < mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t, std::size_t> indices_of_multiple_probabilistic_states;
391 :
392 18 : check_states(initial_probabilistic_state, nstate, line_no);
393 :
394 18 : if (nstate==0)
395 : {
396 0 : throw mcrl2::runtime_error("cannot parse AUT input that has no states; at least an initial state is required.");
397 : }
398 :
399 18 : l.set_num_states(nstate,false);
400 18 : l.clear_transitions(ntrans); // Reserve enough space for the transitions.
401 :
402 18 : mcrl2::utilities::unordered_map < action_label_string, std::size_t > action_labels;
403 18 : action_labels[action_label_string::tau_action()]=0; // A tau action is always stored at position 0.
404 18 : l.set_initial_probabilistic_state(initial_probabilistic_state);
405 :
406 18 : mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t probabilistic_target_state;
407 : std::size_t from;
408 18 : std::string s;
409 :
410 397 : while (!is.eof())
411 : {
412 397 : probabilistic_target_state.clear();
413 :
414 397 : line_no++;
415 :
416 397 : if (!read_aut_transition(is,from,s,probabilistic_target_state,line_no))
417 : {
418 18 : break; // encountered EOF or something that is not a transition
419 : }
420 :
421 379 : check_state(from, nstate, line_no);
422 379 : check_states(probabilistic_target_state, nstate, line_no);
423 379 : std::size_t index = add_probablistic_state(probabilistic_target_state, l, indices_of_single_probabilistic_states, indices_of_multiple_probabilistic_states);
424 :
425 379 : l.add_transition(transition(from,find_label_index(s,action_labels,l),index));
426 : }
427 :
428 18 : if (ntrans != l.num_transitions())
429 : {
430 0 : throw mcrl2::runtime_error("number of transitions read (" + std::to_string(l.num_transitions()) +
431 0 : ") does not correspond to the number of transition given in the header (" + std::to_string(ntrans) + ").");
432 : }
433 18 : }
434 :
435 528 : static void read_from_aut(lts_aut_t& l, std::istream& is)
436 : {
437 528 : std::size_t line_no = 1;
438 528 : std::size_t ntrans=0, nstate=0;
439 :
440 528 : mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t initial_probabilistic_state;
441 528 : read_aut_header(is,initial_probabilistic_state,ntrans,nstate);
442 :
443 528 : if (initial_probabilistic_state.size()>1)
444 : {
445 0 : throw mcrl2::runtime_error("Encountered an initial probability distribution while reading an non probabilistic .aut file.");
446 : }
447 :
448 528 : check_states(initial_probabilistic_state, nstate, line_no);
449 :
450 528 : if (nstate==0)
451 : {
452 0 : throw mcrl2::runtime_error("cannot parse AUT input that has no states; at least an initial state is required.");
453 : }
454 :
455 528 : l.set_num_states(nstate,false);
456 528 : l.clear_transitions(ntrans); // Reserve enough space for the transitions.
457 :
458 528 : mcrl2::utilities::unordered_map < action_label_string, std::size_t > action_labels;
459 528 : action_labels[action_label_string::tau_action()]=0; // A tau action is always stored at position 0.
460 528 : l.set_initial_state(initial_probabilistic_state.get());
461 :
462 : std::size_t from, to;
463 528 : std::string s;
464 3888 : while (!is.eof())
465 : {
466 3888 : line_no++;
467 :
468 3888 : if (!read_aut_transition(is,from,s,to,line_no))
469 : {
470 528 : break; // eof encountered
471 : }
472 :
473 3360 : check_state(from, nstate, line_no);
474 3360 : check_state(to, nstate, line_no);
475 3360 : l.add_transition(transition(from,find_label_index(s,action_labels,l),to));
476 : }
477 :
478 528 : if (ntrans != l.num_transitions())
479 : {
480 0 : throw mcrl2::runtime_error("number of transitions read (" + std::to_string(l.num_transitions()) +
481 0 : ") does not correspond to the number of transition given in the header (" + std::to_string(ntrans) + ").");
482 : }
483 528 : }
484 :
485 :
486 0 : static void write_probabilistic_state(const mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t& prob_state, std::ostream& os)
487 : {
488 0 : mcrl2::lts::probabilistic_arbitrary_precision_fraction previous_probability;
489 0 : bool first_element=true;
490 0 : if (prob_state.size()<=1) // This is a simple probabilistic state.
491 : {
492 0 : os << prob_state.get();
493 : }
494 : else // The state consists of a vector of states and probability pairs.
495 : {
496 0 : for (const mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t::state_probability_pair& p: prob_state)
497 : {
498 0 : if (first_element)
499 : {
500 0 : os << p.state();
501 0 : previous_probability=p.probability();
502 0 : first_element=false;
503 : }
504 : else
505 : {
506 0 : os << " " << pp(previous_probability) << " " << p.state();
507 0 : previous_probability=p.probability();
508 : }
509 : }
510 : }
511 0 : }
512 :
513 0 : static void write_to_aut(const probabilistic_lts_aut_t& l, std::ostream& os)
514 : {
515 : // Do not use "endl" below to avoid flushing. Use "\n" instead.
516 0 : os << "des (";
517 0 : write_probabilistic_state(l.initial_probabilistic_state(),os);
518 :
519 0 : os << "," << l.num_transitions() << "," << l.num_states() << ")" << "\n";
520 :
521 0 : for (const transition& t: l.get_transitions())
522 : {
523 0 : os << "(" << t.from() << ",\"" << pp(l.action_label(l.apply_hidden_label_map(t.label()))) << "\",";
524 0 : write_probabilistic_state(l.probabilistic_state(t.to()),os);
525 0 : os << ")" << "\n";
526 : }
527 0 : }
528 :
529 66 : static void write_to_aut(const lts_aut_t& l, std::ostream& os)
530 : {
531 : // Do not use "endl" below to avoid flushing. Use "\n" instead.
532 66 : os << "des (" << l.initial_state() << "," << l.num_transitions() << "," << l.num_states() << ")" << "\n";
533 :
534 880 : for (const transition& t: l.get_transitions())
535 : {
536 814 : os << "(" << t.from() << ",\""
537 1628 : << pp(l.action_label(l.apply_hidden_label_map(t.label()))) << "\","
538 814 : << t.to() << ")" << "\n";
539 : }
540 66 : }
541 :
542 : namespace mcrl2
543 : {
544 : namespace lts
545 : {
546 :
547 10 : void probabilistic_lts_aut_t::load(const std::string& filename)
548 : {
549 10 : if (filename=="" || filename=="-")
550 : {
551 0 : read_from_aut(*this, std::cin);
552 : }
553 : else
554 : {
555 10 : std::ifstream is(filename.c_str());
556 :
557 10 : if (!is.is_open())
558 : {
559 0 : throw mcrl2::runtime_error("cannot open .aut file '" + filename + ".");
560 : }
561 :
562 10 : read_from_aut(*this,is);
563 10 : is.close();
564 10 : }
565 10 : }
566 :
567 8 : void probabilistic_lts_aut_t::load(std::istream& is)
568 : {
569 8 : read_from_aut(*this,is);
570 8 : }
571 :
572 0 : void probabilistic_lts_aut_t::save(std::string const& filename) const
573 : {
574 0 : if (filename=="" || filename=="-")
575 : {
576 0 : write_to_aut(*this, std::cout);
577 : }
578 : else
579 : {
580 0 : std::ofstream os(filename.c_str());
581 :
582 0 : if (!os.is_open())
583 : {
584 0 : throw mcrl2::runtime_error("cannot create .aut file '" + filename + ".");
585 : return;
586 : }
587 0 : write_to_aut(*this,os);
588 0 : os.close();
589 0 : }
590 : }
591 :
592 66 : void lts_aut_t::load(const std::string& filename)
593 : {
594 66 : if (filename.empty() || filename=="-")
595 : {
596 0 : read_from_aut(*this, std::cin);
597 : }
598 : else
599 : {
600 66 : std::ifstream is(filename.c_str());
601 :
602 66 : if (!is.is_open())
603 : {
604 0 : throw mcrl2::runtime_error("cannot open .aut file '" + filename + ".");
605 : }
606 :
607 66 : read_from_aut(*this,is);
608 66 : is.close();
609 66 : }
610 66 : }
611 :
612 462 : void lts_aut_t::load(std::istream& is)
613 : {
614 462 : read_from_aut(*this,is);
615 462 : }
616 :
617 66 : void lts_aut_t::save(std::string const& filename) const
618 : {
619 66 : if (filename.empty() || filename=="-")
620 : {
621 0 : write_to_aut(*this, std::cout);
622 : }
623 : else
624 : {
625 66 : std::ofstream os(filename.c_str());
626 :
627 66 : if (!os.is_open())
628 : {
629 0 : throw mcrl2::runtime_error("cannot create .aut file '" + filename + ".");
630 : return;
631 : }
632 66 : write_to_aut(*this,os);
633 66 : os.close();
634 66 : }
635 : }
636 :
637 :
638 : }
639 : }
|
