mCRL2
Loading...
Searching...
No Matches
liblts_aut.cpp
Go to the documentation of this file.
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//
10
11#include <fstream>
13#include "mcrl2/lts/lts_aut.h"
15
16
17using namespace mcrl2::lts;
18
19static void read_newline(std::istream& is, const std::size_t line_no)
20{
21 char ch;
22 is.get(ch);
23
24 // Skip over spaces
25 while (ch == ' ')
26 {
27 is.get(ch);
28 }
29
30 // Windows systems typically have a carriage return before a newline.
31 if (ch == '\r')
32 {
33 is.get(ch);
34 }
35
36 if (ch != '\n' && !is.eof()) // Last line does not need to be terminated with an eoln.
37 {
38 if (line_no==1)
39 {
40 throw mcrl2::runtime_error("Expect a newline after the header des(...,...,...).");
41 }
42 else
43 {
44 throw mcrl2::runtime_error("Expect a newline after the transition at line " + std::to_string(line_no) + ".");
45 }
46 }
47}
48
49// reads a number, puts it in s, and reads one extra character, which must be either a space or a closing bracket.
50static void read_natural_number_to_string(std::istream& is, std::string& s, const std::size_t line_no)
51{
52 assert(s.empty());
53 char ch;
54 is >> std::skipws >> ch;
55 for( ; isdigit(ch) ; is.get(ch))
56 {
57 s.push_back(ch);
58 }
59 is.putback(ch);
60 if (s.empty())
61 {
62 throw mcrl2::runtime_error("Expect a number at line " + std::to_string(line_no) + ".");
63 }
64}
65
66template <class AUT_LTS_TYPE>
67static 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 assert(labs.at(action_label_string::tau_action())==0);
74 if (i==labs.end())
75 {
76 label=l.add_action(as);
77 labs[as]=label;
78 }
79 else
80 {
81 label=i->second;
82 }
83 return label;
84}
85
86static void check_state(std::size_t state, std::size_t number_of_states, std::size_t line_no)
87{
88 if (state>=number_of_states)
89 {
90 throw mcrl2::runtime_error("The state number " + std::to_string(state) + " is higher than the number of states (" +
91 std::to_string(number_of_states) + "). Found at line " + std::to_string(line_no) + ".");
92 }
93}
94
96 std::size_t number_of_states, std::size_t line_no)
97{
99 {
100 check_state(p.state(), number_of_states, line_no);
101 }
102}
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.
109 std::istream& is,
111 const std::size_t line_no)
112{
113 assert(result.size()==0);
114
115 std::size_t state;
116
117 is >> std::skipws >> state;
118
119 if (!is.good())
120 {
121 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 is >> std::skipws >> ch;
127 is.putback(ch);
128
129 if (!isdigit(ch))
130 {
131 // There is only a single state.
132 result.set(state);
133 return;
134 }
135 bool ready=false;
136
138 while (is.good() && !ready)
139 {
140 // Now read a probabilities followed by the next state.
141 std::string enumerator;
142 read_natural_number_to_string(is,enumerator,line_no);
143 char ch;
144 is >> std::skipws >> ch;
145 if (ch != '/')
146 {
147 throw mcrl2::runtime_error("Expect a / in a probability at line " + std::to_string(line_no) + ".");
148 }
149
150 std::string denominator;
151 read_natural_number_to_string(is,denominator,line_no);
153 remainder=remainder-frac;
154 result.add(state, frac);
155
156 is >> std::skipws >> state;
157
158 if (!is.good())
159 {
160 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 is >> std::skipws >> ch;
166 is.putback(ch);
167
168 if (!isdigit(ch))
169 {
170 ready=true;
171 }
172 }
173
174 result.add(state, remainder);
175}
176
177
178static void read_aut_header(
179 std::istream& is,
181 std::size_t& num_transitions,
182 std::size_t& num_states)
183{
184 std::string s;
185 is.width(3);
186 is >> std::skipws >> s;
187
188 if (s!="des")
189 {
190 throw mcrl2::runtime_error("Expect an .aut file to start with 'des'.");
191 }
192
193 char ch;
194 is >> std::skipws >> ch;
195
196 if (ch != '(')
197 {
198 throw mcrl2::runtime_error("Expect an opening bracket '(' after 'des' in the first line of a .aut file.");
199 }
200
201 read_probabilistic_state(is,initial_state,1);
202
203 is >> std::skipws >> ch;
204 if (ch != ',')
205 {
206 throw mcrl2::runtime_error("Expect a comma after the first number in the first line of a .aut file.");
207 }
208
209 is >> std::skipws >> num_transitions;
210
211 is >> std::skipws >> ch;
212 if (ch != ',')
213 {
214 throw mcrl2::runtime_error("Expect a comma after the second number in the first line of a .aut file.");
215 }
216
217 is >> std::skipws >> num_states;
218
219 is >> ch;
220
221 if (ch != ')')
222 {
223 throw mcrl2::runtime_error("Expect a closing bracket ')' after the third number in the first line of a .aut file.");
224 }
225
226 read_newline(is,1);
227}
228
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 is >> std::skipws >> ch;
237 if (is.eof())
238 {
239 return false;
240 }
241 if (ch == 0x04) // found EOT character that separates two files
242 {
243 return false;
244 }
245
246 is >> std::skipws >> from;
247
248 is >> std::skipws >> ch;
249 if (ch != ',')
250 {
251 throw mcrl2::runtime_error("Expect that the first number is followed by a comma at line " + std::to_string(line_no) + ".");
252 }
253
254 is >> std::skipws >> ch;
255 if (ch == '"')
256 {
257 label="";
258 // In case the label is using quotes whitespaces
259 // in the label are preserved.
260 is >> std::noskipws >> ch;
261 while ((ch != '"') && !is.eof())
262 {
263 label.push_back(ch);
264 is >> ch;
265 }
266 if (ch != '"')
267 {
268 throw mcrl2::runtime_error("Expect that the second item is a quoted label (using \") at line " + std::to_string(line_no) + ".");
269 }
270 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 label = ch;
277 is >> ch;
278 while ((ch != ',') && !is.eof())
279 {
280 label.push_back(ch);
281 is >> ch;
282 }
283 }
284
285 if (ch != ',')
286 {
287 throw mcrl2::runtime_error("Expect a comma after the quoted label at line " + std::to_string(line_no) + ".");
288 }
289
290 return true;
291}
292
294 std::istream& is,
295 std::size_t& from,
296 std::string& label,
298 const std::size_t line_no)
299{
301 {
302 return false;
303 }
304
305 read_probabilistic_state(is,target_probabilistic_state,line_no);
306
307 char ch;
308 is >> ch;
309 if (ch != ')')
310 {
311 throw mcrl2::runtime_error("Expect a closing bracket at the end of the transition at line " + std::to_string(line_no) + ".");
312 }
313
314 read_newline(is,line_no);
315 return true;
316}
317
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{
326 {
327 return false;
328 }
329
330 is >> std::skipws >> to;
331
332 char ch;
333 is >> ch;
334 if (ch != ')')
335 {
336 throw mcrl2::runtime_error("Expect a closing bracket at the end of the transition at line " + std::to_string(line_no) + ".");
337 }
338
339 read_newline(is,line_no);
340 return true;
341}
342
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 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 if (probabilistic_state.size()<=1)
354 {
355 index = indices_of_single_probabilistic_states.insert(
356 std::pair< std::size_t, std::size_t>
357 (probabilistic_state.get(),fresh_index)).first->second;
358 }
359 else
360 {
361 assert(probabilistic_state.size()>1);
362 index = indices_of_multiple_probabilistic_states.insert(
363 std::pair< mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t, std::size_t>
364 (probabilistic_state,fresh_index)).first->second;
365 }
366
367 if (index==fresh_index)
368 {
369 std::size_t probabilistic_state_index=l.add_and_reset_probabilistic_state(probabilistic_state);
370 assert(probabilistic_state_index==index);
371 (void)probabilistic_state_index; // Avoid unused variable warning.
372 }
373 return index;
374}
375
376
377static void read_from_aut(probabilistic_lts_aut_t& l, std::istream& is)
378{
379 std::size_t line_no = 1;
380 std::size_t ntrans=0, nstate=0;
381
383 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 mcrl2::utilities::unordered_map < std::size_t, std::size_t> indices_of_single_probabilistic_states;
390 mcrl2::utilities::unordered_map < mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t, std::size_t> indices_of_multiple_probabilistic_states;
391
392 check_states(initial_probabilistic_state, nstate, line_no);
393
394 if (nstate==0)
395 {
396 throw mcrl2::runtime_error("cannot parse AUT input that has no states; at least an initial state is required.");
397 }
398
399 l.set_num_states(nstate,false);
400 l.clear_transitions(ntrans); // Reserve enough space for the transitions.
401
402 mcrl2::utilities::unordered_map < action_label_string, std::size_t > action_labels;
403 action_labels[action_label_string::tau_action()]=0; // A tau action is always stored at position 0.
404 l.set_initial_probabilistic_state(initial_probabilistic_state);
405
407 std::size_t from;
408 std::string s;
409
410 while (!is.eof())
411 {
412 probabilistic_target_state.clear();
413
414 line_no++;
415
416 if (!read_aut_transition(is,from,s,probabilistic_target_state,line_no))
417 {
418 break; // encountered EOF or something that is not a transition
419 }
420
421 check_state(from, nstate, line_no);
422 check_states(probabilistic_target_state, nstate, line_no);
423 std::size_t index = add_probablistic_state(probabilistic_target_state, l, indices_of_single_probabilistic_states, indices_of_multiple_probabilistic_states);
424
425 l.add_transition(transition(from,find_label_index(s,action_labels,l),index));
426 }
427
428 if (ntrans != l.num_transitions())
429 {
430 throw mcrl2::runtime_error("number of transitions read (" + std::to_string(l.num_transitions()) +
431 ") does not correspond to the number of transition given in the header (" + std::to_string(ntrans) + ").");
432 }
433}
434
435static void read_from_aut(lts_aut_t& l, std::istream& is)
436{
437 std::size_t line_no = 1;
438 std::size_t ntrans=0, nstate=0;
439
441 read_aut_header(is,initial_probabilistic_state,ntrans,nstate);
442
443 if (initial_probabilistic_state.size()>1)
444 {
445 throw mcrl2::runtime_error("Encountered an initial probability distribution while reading an non probabilistic .aut file.");
446 }
447
448 check_states(initial_probabilistic_state, nstate, line_no);
449
450 if (nstate==0)
451 {
452 throw mcrl2::runtime_error("cannot parse AUT input that has no states; at least an initial state is required.");
453 }
454
455 l.set_num_states(nstate,false);
456 l.clear_transitions(ntrans); // Reserve enough space for the transitions.
457
458 mcrl2::utilities::unordered_map < action_label_string, std::size_t > action_labels;
459 action_labels[action_label_string::tau_action()]=0; // A tau action is always stored at position 0.
460 l.set_initial_state(initial_probabilistic_state.get());
461
462 std::size_t from, to;
463 std::string s;
464 while (!is.eof())
465 {
466 line_no++;
467
468 if (!read_aut_transition(is,from,s,to,line_no))
469 {
470 break; // eof encountered
471 }
472
473 check_state(from, nstate, line_no);
474 check_state(to, nstate, line_no);
475 l.add_transition(transition(from,find_label_index(s,action_labels,l),to));
476 }
477
478 if (ntrans != l.num_transitions())
479 {
480 throw mcrl2::runtime_error("number of transitions read (" + std::to_string(l.num_transitions()) +
481 ") does not correspond to the number of transition given in the header (" + std::to_string(ntrans) + ").");
482 }
483}
484
485
487{
489 bool first_element=true;
490 if (prob_state.size()<=1) // This is a simple probabilistic state.
491 {
492 os << prob_state.get();
493 }
494 else // The state consists of a vector of states and probability pairs.
495 {
497 {
498 if (first_element)
499 {
500 os << p.state();
501 previous_probability=p.probability();
502 first_element=false;
503 }
504 else
505 {
506 os << " " << pp(previous_probability) << " " << p.state();
507 previous_probability=p.probability();
508 }
509 }
510 }
511}
512
513static 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 os << "des (";
518
519 os << "," << l.num_transitions() << "," << l.num_states() << ")" << "\n";
520
521 for (const transition& t: l.get_transitions())
522 {
523 os << "(" << t.from() << ",\"" << pp(l.action_label(l.apply_hidden_label_map(t.label()))) << "\",";
525 os << ")" << "\n";
526 }
527}
528
529static 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 os << "des (" << l.initial_state() << "," << l.num_transitions() << "," << l.num_states() << ")" << "\n";
533
534 for (const transition& t: l.get_transitions())
535 {
536 os << "(" << t.from() << ",\""
537 << pp(l.action_label(l.apply_hidden_label_map(t.label()))) << "\","
538 << t.to() << ")" << "\n";
539 }
540}
541
542namespace mcrl2
543{
544namespace lts
545{
546
547void probabilistic_lts_aut_t::load(const std::string& filename)
548{
549 if (filename=="" || filename=="-")
550 {
551 read_from_aut(*this, std::cin);
552 }
553 else
554 {
555 std::ifstream is(filename.c_str());
556
557 if (!is.is_open())
558 {
559 throw mcrl2::runtime_error("cannot open .aut file '" + filename + ".");
560 }
561
562 read_from_aut(*this,is);
563 is.close();
564 }
565}
566
567void probabilistic_lts_aut_t::load(std::istream& is)
568{
569 read_from_aut(*this,is);
570}
571
572void probabilistic_lts_aut_t::save(std::string const& filename) const
573{
574 if (filename=="" || filename=="-")
575 {
576 write_to_aut(*this, std::cout);
577 }
578 else
579 {
580 std::ofstream os(filename.c_str());
581
582 if (!os.is_open())
583 {
584 throw mcrl2::runtime_error("cannot create .aut file '" + filename + ".");
585 return;
586 }
587 write_to_aut(*this,os);
588 os.close();
589 }
590}
591
592void lts_aut_t::load(const std::string& filename)
593{
594 if (filename.empty() || filename=="-")
595 {
596 read_from_aut(*this, std::cin);
597 }
598 else
599 {
600 std::ifstream is(filename.c_str());
601
602 if (!is.is_open())
603 {
604 throw mcrl2::runtime_error("cannot open .aut file '" + filename + ".");
605 }
606
607 read_from_aut(*this,is);
608 is.close();
609 }
610}
611
612void lts_aut_t::load(std::istream& is)
613{
614 read_from_aut(*this,is);
615}
616
617void lts_aut_t::save(std::string const& filename) const
618{
619 if (filename.empty() || filename=="-")
620 {
621 write_to_aut(*this, std::cout);
622 }
623 else
624 {
625 std::ofstream os(filename.c_str());
626
627 if (!os.is_open())
628 {
629 throw mcrl2::runtime_error("cannot create .aut file '" + filename + ".");
630 return;
631 }
632 write_to_aut(*this,os);
633 os.close();
634 }
635}
636
637
638}
639}
Read-only balanced binary tree of terms.
This class contains strings to be used as values for action labels in lts's.
static const action_label_string & tau_action()
A simple labelled transition format with only strings as action labels.
Definition lts_aut.h:70
void load(const std::string &filename)
Load the labelled transition system from a file.
void save(const std::string &filename) const
Save the labelled transition system to file.
A class that contains a labelled transition system.
Definition lts.h:83
void add_transition(const transition &t)
Add a transition to the lts.
Definition lts.h:544
states_size_type num_states() const
Gets the number of states of this LTS.
Definition lts.h:245
void clear_transitions(const std::size_t n=0)
Clear the transitions of an lts.
Definition lts.h:484
void set_num_states(const states_size_type n, const bool has_state_labels=true)
Sets the number of states of this LTS.
Definition lts.h:280
ACTION_LABEL_T action_label(const labels_size_type action) const
Gets the label of an action.
Definition lts.h:470
void set_initial_state(const states_size_type state)
Sets the initial state number of this LTS.
Definition lts.h:334
labels_size_type apply_hidden_label_map(const labels_size_type action) const
If the action label is registered hidden, it returns tau, otherwise the original label.
Definition lts.h:438
const std::vector< transition > & get_transitions() const
Gets a const reference to the vector of transitions of the current lts.
Definition lts.h:526
states_size_type initial_state() const
Gets the initial state number of this LTS.
Definition lts.h:326
transitions_size_type num_transitions() const
Gets the number of transitions of this LTS.
Definition lts.h:302
This class contains labels for probabilistic transistions, consisting of a numerator and a denominato...
static probabilistic_arbitrary_precision_fraction & one()
Constant one.
A simple labelled transition format with only strings as action labels.
Definition lts_aut.h:103
void load(const std::string &filename)
Load the labelled transition system from a file.
void save(const std::string &filename) const
Save the labelled transition system to file.
void set_initial_probabilistic_state(const PROBABILISTIC_STATE_T &state)
Sets the probabilistic initial state number of this LTS.
const PROBABILISTIC_STATE_T & initial_probabilistic_state() const
Gets the initial state number of this LTS.
states_size_type add_and_reset_probabilistic_state(PROBABILISTIC_STATE_T &s)
Adds a probabilistic state to this LTS and resets the state to empty.
const PROBABILISTIC_STATE_T & probabilistic_state(const states_size_type index) const
Gets the probabilistic label of an index.
void set(const STATE &s)
Set this probabilistic state to a single state with probability one.
std::size_t size() const
Gets the number of probabilistic states in the vector representation of this state....
STATE get() const
Get a probabilistic state if is is simple, i.e., consists of a single state.
void clear()
Makes the probabilistic state empty.
void add(const STATE &s, const PROBABILITY &p)
Add a state with a probability to the probabilistic state.
A class containing triples, source label and target representing transitions.
Definition transition.h:43
Standard exception class for reporting runtime errors.
Definition exception.h:27
iterator find(const Args &... args)
std::pair< iterator, bool > insert(const value_type &pair)
Inserts elements.
const T & at(const key_type &key) const
Provides access to the value associated with the given key.
typename Set::const_iterator const_iterator
static void read_probabilistic_state(std::istream &is, mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t &result, const std::size_t line_no)
static void write_probabilistic_state(const mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t &prob_state, std::ostream &os)
static void read_from_aut(probabilistic_lts_aut_t &l, std::istream &is)
static size_t add_probablistic_state(mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t &probabilistic_state, probabilistic_lts_aut_t &l, mcrl2::utilities::unordered_map< std::size_t, std::size_t > &indices_of_single_probabilistic_states, mcrl2::utilities::unordered_map< mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t, std::size_t > &indices_of_multiple_probabilistic_states)
static void read_newline(std::istream &is, const std::size_t line_no)
static void read_aut_header(std::istream &is, mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t &initial_state, std::size_t &num_transitions, std::size_t &num_states)
static void write_to_aut(const probabilistic_lts_aut_t &l, std::ostream &os)
static bool read_initial_part_of_an_aut_transition(std::istream &is, std::size_t &from, std::string &label, const std::size_t line_no)
static void read_natural_number_to_string(std::istream &is, std::string &s, const std::size_t line_no)
static void check_states(mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t &probability_state, std::size_t number_of_states, std::size_t line_no)
static void check_state(std::size_t state, std::size_t number_of_states, std::size_t line_no)
static bool read_aut_transition(std::istream &is, std::size_t &from, std::string &label, mcrl2::lts::probabilistic_lts_aut_t::probabilistic_state_t &target_probabilistic_state, const std::size_t line_no)
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)
This file contains a class that contains labelled transition systems in aut format.
std::string pp(const abstraction &x)
Definition data.cpp:39
atermpp::term_balanced_tree< data::data_expression > state
Definition state.h:24
The main LTS namespace.
std::size_t to(const outgoing_pair_t &p)
Target state of a label state pair.
std::size_t label(const outgoing_pair_t &p)
Label of a pair of a label and target state.
std::size_t from(const outgoing_transitions_per_state_action_t::const_iterator &i)
From state of an iterator exploring transitions per outgoing state and action.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72