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 mcrl2/lts/trace.h
10 : /// \brief This class allows to flexibly manipulate traces.
11 : /// \details This class allows to build, traverse and store traces.
12 : /// Traces are sequences of (possibly timed) multi actions, that may be endowed with state
13 : /// information for the intermediate states. In the trace the current position is being
14 : /// maintained. Adding actions or setting states is always relative to the current position.
15 : /// \author Muck van Weerdenburg
16 :
17 : #ifndef MCRL2_LTS_TRACE_H
18 : #define MCRL2_LTS_TRACE_H
19 :
20 : #include <fstream>
21 : #include "mcrl2/lps/parse.h"
22 : #include "mcrl2/lps/state.h"
23 : #include "mcrl2/lts/lts_lts.h"
24 :
25 : namespace mcrl2
26 : {
27 : /** \brief The namespace for traces.
28 : * \details The namespace trace contains all data structures and members of the
29 : * trace library.
30 : */
31 : namespace lts
32 : {
33 :
34 :
35 : /// \brief This class contains a trace consisting of a sequence of (timed) actions possibly with intermediate states
36 : /// \details A trace is a sequence of actions. Actions can have a time
37 : /// tag as a positive real number. Between two actions, before the first action and after the last
38 : /// action there can be a state. In the current version of the trace library an action, a state and
39 : /// a time tag are arbitrary expressions of sort AtermAppl. It is expected that this will change
40 : /// in the near future to match the data types used in the LPS library.
41 : ///
42 : /// An important property of a state is its current position. All operations on a state
43 : /// operate with respect to its current position. A trace can be traversed by increasing
44 : /// and decreasing the current position between 0 up to the length. If a new action is
45 : /// added to a trace, the trace above the current position is lost. For each action
46 : /// a state can only be added once.
47 : ///
48 : /// States can be saved in two formats. A human readable ascii format containging only a
49 : /// sequence of untimed actions and a more compact aterm format also containing time and
50 : /// state information.
51 : class trace
52 : {
53 : public:
54 : ////////////////////////////////////////////////////////////
55 : //
56 : /// \brief Formats in which traces can be saved on disk
57 : /// \details There are several formats for traces.
58 : /// The tfMcrl2 format saves a trace as an mCRL2 term in aterm internal format.
59 : /// This is a compact but unreadable format.
60 : /// The tfPlain format is an ascii representation of the trace, which is
61 : /// human readable but only contains the actions and no time or state information.
62 : /// tfUnknown is only used to read traces, when it is
63 : /// not known what the format is. In this case it is determined based
64 : /// on the format of the input file.
65 :
66 : enum trace_format
67 : {
68 : tfMcrl2, /**< Format is stored as an aterm */
69 : tfPlain, /**< Format is stored in plain text. In this format there are only actions */
70 : tfLine, /**< Format is stored in a line of text. In this format there are only actions */
71 : tfUnknown /**< This value indicates that the format is unknown */
72 : };
73 :
74 : protected:
75 : // The number of states is always less than one plus the number of actions.
76 : // In case all states are there, then it is one more than the number of actions.
77 : // Otherwise there are less. So, an invariant is actions.size()+1 >= states.size();
78 : // The states and actions are supposed to be contiguous,
79 : // in the sense that if a state, or action, at position n exists, then also the
80 : // states and actions at positions n'<n exist.
81 :
82 : std::vector < lps::state > m_states;
83 : std::vector < mcrl2::lps::multi_action > m_actions;
84 : std::size_t m_pos; // Invariant: m_pos <= actions.size().
85 :
86 : mcrl2::data::data_specification m_spec;
87 : process::action_label_list m_act_decls;
88 : bool m_data_specification_and_act_decls_are_defined;
89 :
90 : public:
91 : /// \brief Default constructor for an empty trace.
92 : /// \details The current position
93 : /// and length of trace are set to 0.
94 2 : trace()
95 2 : : m_data_specification_and_act_decls_are_defined(false)
96 : {
97 2 : init();
98 2 : }
99 :
100 : /// \brief Constructor for an empty trace.
101 : /// \details The current position
102 : /// and length of trace are set to 0.
103 : /// \param[in] spec The data specification that is used when parsing multi actions.
104 : /// \param[in] act_decls An action label list with action declarations that is used to parse multi actions.
105 2 : trace(const mcrl2::data::data_specification& spec, const mcrl2::process::action_label_list& act_decls)
106 2 : : m_spec(spec),
107 2 : m_act_decls(act_decls),
108 2 : m_data_specification_and_act_decls_are_defined(true)
109 : {
110 2 : init();
111 2 : }
112 :
113 : /// \brief Construct the trace on the basis of an input file.
114 : /// \details A trace is read from the input file. If the format is tfUnknown it
115 : /// is automatically determined what the format of the trace is.
116 : /// \param[in] filename The name of the file from which the trace is read.
117 : /// \param[in] tf The format in which the trace was stored. Default: '''tfUnknown'''.
118 : /// \exception mcrl2::runtime_error message in case of failure
119 : trace(const std::string& filename, trace_format tf = tfUnknown)
120 : : m_data_specification_and_act_decls_are_defined(false)
121 : {
122 : init();
123 : load(filename,tf);
124 : }
125 :
126 : /// \brief Construct the trace on the basis of an input file.
127 : /// \details A trace is read from the input file. If the format is tfUnknown it
128 : /// is automatically determined what the format of the trace is.
129 : /// \param[in] filename The name of the file from which the trace is read.
130 : /// \param[in] spec A data specification.
131 : /// \param[in] act_decls A list of action declarations.
132 : /// \param[in] tf The format in which the trace was stored. Default: '''tfUnknown'''.
133 : /// \exception mcrl2::runtime_error message in case of failure
134 0 : trace(const std::string& filename,
135 : const mcrl2::data::data_specification& spec,
136 : const mcrl2::process::action_label_list& act_decls,
137 : trace_format tf = tfUnknown)
138 0 : : m_spec(spec),
139 0 : m_act_decls(act_decls),
140 0 : m_data_specification_and_act_decls_are_defined(true)
141 : {
142 0 : init();
143 : try
144 : {
145 0 : load(filename,tf);
146 : }
147 0 : catch (...)
148 : {
149 0 : throw;
150 0 : }
151 0 : }
152 :
153 : bool operator <(const trace& t) const
154 : {
155 : return ((m_states<t.m_states) ||
156 : (m_states==t.m_states && m_actions<t.m_actions));
157 : }
158 :
159 : /// \brief Set the current position back to the beginning of the trace
160 : /// \details The trace itself remains unaltered.
161 18 : void reset_position()
162 : {
163 18 : assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
164 18 : m_pos = 0;
165 18 : }
166 :
167 : /// \brief Increase the current position by one, except if this brings one beyond the end of the trace.
168 : /// \details The initial position corresponds to m_pos=0.
169 18 : void increase_position()
170 : {
171 18 : if (m_pos < m_actions.size())
172 : {
173 18 : ++m_pos;
174 : }
175 18 : }
176 :
177 : /// \brief Decrease the current position in the trace by one provided the largest position is larger than 0.
178 : /// \details The initial position corresponds to m_pos=0.
179 : void decrease_position()
180 : {
181 : if (m_pos >0)
182 : {
183 : --m_pos;
184 : }
185 : }
186 :
187 : /// \brief Set the current position after the m_pos'th action of the trace.
188 : /// \details The initial position corresponds to m_pos=0. If m_pos is larger than
189 : /// the length of the trace, no new position is set.
190 : /// \param[in] m_pos The new position in the trace.
191 : void set_position(std::size_t pos)
192 : {
193 : if (pos <= m_actions.size())
194 : {
195 : this->m_pos = pos;
196 : }
197 : }
198 :
199 : /// \brief Get the current position in the trace.
200 : /// \details The current position of the trace is a non negative number
201 : /// smaller than the length of the trace.
202 : /// \return The current position of the trace.
203 : std::size_t get_position() const
204 : {
205 : assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
206 : return m_pos;
207 : }
208 :
209 : /// \brief Get the number of actions in the current trace.
210 : /// \return A positive number indicating the number of actions in the trace.
211 8 : std::size_t number_of_actions() const
212 : {
213 8 : assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
214 8 : return m_actions.size();
215 : }
216 :
217 : /// \brief Get the number of states in the current trace.
218 : /// \return A positive number indicating the number of states in the trace.
219 11 : std::size_t number_of_states() const
220 : {
221 11 : assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
222 11 : return m_states.size();
223 : }
224 :
225 : /// \brief Remove the current state and all states following it.
226 : void clear_current_state()
227 : {
228 : assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
229 : m_states.resize(m_pos);
230 : }
231 :
232 : /// \brief Indicate whether a current state exists.
233 : /// \return A boolean indicating whether the current state exists.
234 0 : bool current_state_exists() const
235 : {
236 0 : assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
237 0 : return m_states.size()>m_pos;
238 : }
239 :
240 : /// \brief Get the state at the current position in the trace.
241 : /// \details The state at
242 : /// position 0 is the initial state. If no state is defined at
243 : /// the next position an exception is thrown.
244 : /// \return The state at the current position of the trace.
245 4 : const lps::state& next_state() const
246 : {
247 4 : assert(m_actions.size()+1 >= m_states.size() && m_pos+1 <=m_actions.size());
248 4 : if (m_pos>=m_states.size())
249 : {
250 0 : throw mcrl2::runtime_error("Requesting a state in a trace at a non existing position " + std::to_string(m_pos+1) + ".");
251 : }
252 4 : return m_states[m_pos+1];
253 : }
254 :
255 : /// \brief Get the state at the current position in the trace.
256 : /// \details The state at
257 : /// position 0 is the initial state. If no state is defined at
258 : /// the current position an exception is thrown.
259 : /// \return The state at the current position of the trace.
260 6 : const lps::state& current_state() const
261 : {
262 6 : assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
263 6 : if (m_pos>=m_states.size())
264 : {
265 0 : throw mcrl2::runtime_error("Requesting a state in a trace at a non existing position " + std::to_string(m_pos) + ".");
266 : }
267 6 : return m_states[m_pos];
268 : }
269 :
270 : /// \brief Indicate whether the current action exists.
271 : /// \return A boolean indicating that the current action exists;
272 0 : bool current_action_exists() const
273 : {
274 0 : assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
275 0 : return m_pos < m_actions.size();
276 : }
277 :
278 : /// \brief Get the outgoing action from the current position in the trace.
279 : /// \details This routine returns the action at the current position of the
280 : /// trace. It is not allowed to request an action if no action is available.
281 : /// \return An action_list representing the action at the current position of the
282 : /// trace.
283 12 : mcrl2::lps::multi_action current_action()
284 : {
285 12 : assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
286 12 : assert(m_pos < m_actions.size());
287 12 : return m_actions[m_pos];
288 : }
289 :
290 : /// \brief Get the time of the current state in the trace.
291 : /// \details This is the time at which
292 : /// the last action occurred (if any).
293 : /// \return A data_expression representing the current time, or a default data_expression if the time is not defined.
294 : mcrl2::data::data_expression current_time()
295 : {
296 : assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
297 : return m_actions[m_pos].time();
298 : }
299 :
300 : /// \brief Truncates the trace at the current position.
301 : /// \details This function removes the next action at the current position and all
302 : /// subsequent actions and states. The state and the time at the current
303 : /// position remain untouched.
304 30 : void truncate()
305 : {
306 30 : m_actions.resize(m_pos);
307 30 : if (m_pos+1<m_states.size()) // Only throw states away that exist.
308 : {
309 2 : m_states.resize(m_pos+1);
310 : }
311 30 : }
312 :
313 : /// \brief Add an action to the current trace.
314 : /// \details Add an action to the current trace at the current position. The current
315 : /// position is increased and the length of the trace is set to this new current position.
316 : /// The old actions in the trace at the current at higher positions are removed.
317 : /// \param [in] action The multi_action to be stored in the trace.
318 :
319 18 : void add_action(const mcrl2::lps::multi_action& action)
320 : {
321 18 : assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
322 18 : truncate(); // Take care that actions and states have the appropriate size.
323 18 : m_pos++;
324 18 : m_actions.push_back(action);
325 18 : }
326 :
327 : /// \brief Set the state at the current position.
328 : /// \details It is necessary that all states at earlier positions are also set.
329 : /// If not an mcrl2::runtime_error exception is thrown.
330 : /// \param [in] s The new state.
331 : // void set_state(const mcrl2::lps::state& s)
332 16 : void set_state(const lps::state& s)
333 : {
334 16 : assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
335 16 : if (m_pos>m_states.size())
336 : {
337 0 : throw mcrl2::runtime_error("Setting a state in a trace at a position " + std::to_string(m_pos) +
338 0 : " where there are no states at earlier positions.");
339 : }
340 :
341 16 : if (m_states.size()==m_pos)
342 : {
343 13 : m_states.push_back(s);
344 : }
345 : else
346 : {
347 3 : m_states[m_pos] = s;
348 : }
349 16 : }
350 :
351 : /// \brief Replace the trace with the trace in the file.
352 : /// \details The trace is replaced with the trace in the file.
353 : /// If the format is tfPlain the trace can only consist of actions.
354 : /// \param [in] filename The name of the file from which the trace is read.
355 : /// \param [in] tf The expected format of the trace in the stream (default: tfUnknown).
356 : /// \exception mcrl2::runtime_error message in case of failure
357 :
358 8 : void load(const std::string& filename, trace_format tf = tfUnknown)
359 : {
360 : using std::ifstream;
361 8 : ifstream is(filename.c_str(),ifstream::binary|ifstream::in);
362 :
363 8 : if (!is.is_open())
364 : {
365 0 : throw runtime_error("Error loading trace (could not open file " + filename +").");
366 : }
367 :
368 : try
369 : {
370 8 : if (tf == tfUnknown)
371 : {
372 8 : tf = detectFormat(is);
373 : }
374 :
375 8 : switch (tf)
376 : {
377 5 : case tfMcrl2:
378 5 : load_mcrl2(filename);
379 5 : break;
380 3 : case tfPlain:
381 3 : load_plain(is);
382 3 : break;
383 0 : default:
384 0 : break;
385 : }
386 :
387 : }
388 0 : catch (mcrl2::runtime_error& err)
389 : {
390 0 : throw mcrl2::runtime_error("Error loading trace: " + std::string(err.what()));
391 0 : }
392 8 : }
393 :
394 : /// \brief Output the trace into a file with the indicated name.
395 : /// \details Write the trace to a file with the indicated name.
396 : /// \param [in] filename The name of the file that is written.
397 : /// \param [in] tf The format used to represent the trace in the stream. If
398 : /// the format is tfPlain only actions are written. Default: tfMcrl2.
399 : /// \exception mcrl2::runtime_error message in case of failure
400 :
401 8 : void save(const std::string& filename, trace_format tf = tfMcrl2) const
402 : {
403 : try
404 : {
405 8 : switch (tf)
406 : {
407 5 : case tfMcrl2:
408 5 : save_mcrl2(filename);
409 5 : break;
410 3 : case tfPlain:
411 3 : save_plain(filename);
412 3 : break;
413 0 : case tfLine:
414 0 : save_line(filename);
415 0 : break;
416 0 : default:
417 0 : throw runtime_error("Error saving trace to " + (filename.empty()?std::string(" stdout"):filename) + ".");
418 : }
419 : }
420 0 : catch (runtime_error& err)
421 : {
422 0 : throw runtime_error("Error saving trace to " + (filename.empty()?std::string(" stdout"):filename) + ".\n" + err.what());
423 0 : }
424 8 : }
425 :
426 0 : const std::vector<lps::state>& states() const
427 : {
428 0 : return m_states;
429 : }
430 :
431 : const std::vector<lps::multi_action>& actions() const
432 : {
433 : return m_actions;
434 : }
435 :
436 : protected:
437 :
438 4 : void init()
439 : {
440 4 : m_pos = 0;
441 4 : truncate(); // Take care that m_pos 0 exists.
442 4 : }
443 :
444 8 : trace_format detectFormat(std::istream& is)
445 : {
446 8 : trace_format fmt = tfPlain;
447 :
448 8 : char c=is.peek();
449 8 : if (is.bad())
450 : {
451 0 : throw runtime_error("Could not read from stream.");
452 : }
453 :
454 8 : if (c==0) // Weak check. A lts in aterm format starts with a 0. This is not possible
455 : // for a trace in textual format.
456 : {
457 5 : fmt = tfMcrl2;
458 : }
459 :
460 8 : return fmt;
461 : }
462 :
463 5 : void load_mcrl2(const std::string& filename)
464 : {
465 5 : mcrl2::lts::lts_lts_t lts;
466 : try
467 : {
468 5 : lts.load(filename);
469 : }
470 0 : catch (mcrl2::runtime_error& e)
471 : {
472 0 : throw runtime_error(std::string("stream does not contain an mCRL2 trace.\n") + e.what());
473 0 : }
474 :
475 5 : m_spec = lts.data();
476 5 : m_act_decls = lts.action_label_declarations();
477 5 : m_data_specification_and_act_decls_are_defined = m_spec==data::data_specification() && m_act_decls == process::action_label_list();
478 :
479 5 : reset_position();
480 5 : truncate();
481 :
482 5 : std::vector<bool> has_state_outgoing_transition(lts.num_states(),false);
483 5 : std::vector<transition> outgoing_transition(lts.num_states(),transition(0,0,0));
484 :
485 : // The transition system that is read may not be a trace, but a more complex transition system.
486 11 : for(const transition& t: lts.get_transitions())
487 : {
488 6 : if (has_state_outgoing_transition.at(t.from()))
489 : {
490 0 : throw runtime_error("The tracefile contains an labelled transition system that is not a trace. State " +
491 0 : std::to_string(t.from()) + " has multiple outgoing transitions.");
492 : }
493 6 : has_state_outgoing_transition[t.from()]=true;
494 6 : outgoing_transition[t.from()]=t;
495 : }
496 :
497 : // The transition file that is read is a trace. We read the trace sequentially,
498 : // but it might be that the transitions are non consecutive in the trace, if the
499 : // trace file results from an arbitrary .lts. So, we first put all transitions in
500 : // a vector with transition (i,label,j) put at position i.
501 :
502 5 : lts_lts_t::states_size_type current_state=lts.initial_state();
503 5 : if (lts.has_state_info())
504 : {
505 3 : assert(current_state<lts.num_state_labels());
506 3 : if (lts.state_label(current_state).size()!=1)
507 : {
508 0 : throw mcrl2::runtime_error("The trace has multiple state labels for some states, and hence is not a trace.");
509 : }
510 3 : set_state(lts.state_label(current_state).front());
511 : }
512 :
513 11 : while (has_state_outgoing_transition.at(current_state))
514 : {
515 6 : add_action(lts.action_label(outgoing_transition[current_state].label()));
516 6 : current_state=outgoing_transition[current_state].to();
517 6 : if (lts.has_state_info())
518 : {
519 3 : assert(current_state<lts.num_state_labels());
520 3 : if (lts.state_label(current_state).size()!=1)
521 : {
522 0 : throw mcrl2::runtime_error("The trace has multiple state labels for some states, and hence is not a trace.");
523 : }
524 3 : set_state(lts.state_label(current_state).front());
525 : }
526 : }
527 :
528 5 : reset_position();
529 5 : }
530 :
531 3 : void load_plain(std::istream& is)
532 : {
533 3 : reset_position();
534 3 : truncate();
535 3 : m_states.clear(); // Throw all states away, also the initial state.
536 :
537 3 : std::string action;
538 13 : while (!is.eof())
539 : {
540 10 : std::getline(is,action);
541 10 : if (is.bad())
542 : {
543 0 : throw mcrl2::runtime_error("Error while reading from stream.");
544 : }
545 :
546 10 : action = action.substr(0,action.find_last_not_of(" \r")+1);
547 10 : if (!action.empty())
548 : {
549 6 : if (m_data_specification_and_act_decls_are_defined)
550 : {
551 0 : add_action(mcrl2::lps::parse_multi_action(action,m_act_decls,m_spec));
552 : }
553 : else
554 : {
555 6 : add_action(mcrl2::lps::multi_action(mcrl2::process::action(
556 12 : mcrl2::process::action_label(mcrl2::core::identifier_string(action),mcrl2::data::sort_expression_list()),
557 12 : mcrl2::data::data_expression_list())));
558 : }
559 : }
560 : }
561 3 : is.clear();
562 :
563 3 : reset_position();
564 3 : }
565 :
566 5 : void save_mcrl2(const std::string& filename) const
567 : {
568 : // The trace is saved as an .lts in lts format.
569 5 : lts_lts_t lts;
570 5 : if (m_data_specification_and_act_decls_are_defined)
571 : {
572 3 : lts.set_data(m_spec);
573 3 : lts.set_action_label_declarations(m_act_decls);
574 : }
575 5 : assert(m_actions.size()+1 >= m_states.size());
576 :
577 8 : lts.add_state(m_states.size()>0?
578 3 : lts_lts_t::state_label_t(m_states[0]):
579 : lts_lts_t::state_label_t());
580 :
581 : std::map<mcrl2::lps::multi_action,std::size_t>
582 15 : obtain_unique_numbers_for_action_labels({std::pair(action_label_lts::tau_action(),0)});
583 11 : for(std::size_t i=0; i<m_actions.size(); ++i)
584 : {
585 6 : auto [element, inserted] =
586 6 : obtain_unique_numbers_for_action_labels.insert(
587 12 : std::pair(m_actions[i],
588 12 : obtain_unique_numbers_for_action_labels.size()));
589 6 : if (inserted)
590 : {
591 6 : lts.add_action(action_label_lts(m_actions[i]));
592 : }
593 6 : lts.add_transition(transition(i,element->second,i+1));
594 :
595 9 : lts.add_state(m_states.size()>i+1?
596 3 : lts_lts_t::state_label_t(m_states[i+1]):
597 : lts_lts_t::state_label_t());
598 : }
599 5 : lts.set_initial_state(0);
600 :
601 5 : lts.save(filename);
602 5 : }
603 :
604 3 : void save_text_to_stream(std::ostream& os, std::string separator) const
605 : {
606 3 : std::string sep;
607 9 : for (std::size_t i=0; i<m_actions.size(); i++)
608 : {
609 6 : os << sep << pp(m_actions[i]);
610 6 : sep = separator;
611 6 : if (os.bad())
612 : {
613 0 : throw runtime_error("Could not write to stream.");
614 : }
615 : }
616 3 : os << std::endl;
617 3 : }
618 :
619 3 : void save_text(const std::string& filename, std::string separator) const
620 : {
621 3 : if (filename=="")
622 : {
623 0 : save_text_to_stream(std::cout, separator);
624 : }
625 : else
626 : {
627 : using std::ofstream;
628 3 : ofstream os;
629 3 : os.open(filename.c_str(),ofstream::binary|ofstream::out|ofstream::trunc);
630 3 : if (!os.is_open())
631 : {
632 0 : os.close();
633 0 : throw runtime_error("Could not open file.");
634 : }
635 3 : save_text_to_stream(os, separator);
636 3 : os.close();
637 3 : }
638 3 : }
639 :
640 0 : void save_line(const std::string& filename) const
641 : {
642 0 : save_text(filename, ";");
643 0 : }
644 :
645 3 : void save_plain(const std::string& filename) const
646 : {
647 3 : save_text(filename, "\n");
648 3 : }
649 :
650 : };
651 :
652 : }
653 : }
654 : #endif // MCRL2_LTS_TRACE_H
|
