mCRL2
Searching...
No Matches
trace.h
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//
6// (See accompanying file LICENSE_1_0.txt or copy at
8//
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
25namespace mcrl2
26{
31namespace lts
32{
33
34
51class trace
52{
53 public:
55 //
65
67 {
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
89
90 public:
96 {
97 init();
98 }
99
106 : m_spec(spec),
107 m_act_decls(act_decls),
109 {
110 init();
111 }
112
119 trace(const std::string& filename, trace_format tf = tfUnknown)
121 {
122 init();
124 }
125
134 trace(const std::string& filename,
136 const mcrl2::process::action_label_list& act_decls,
138 : m_spec(spec),
139 m_act_decls(act_decls),
141 {
142 init();
143 try
144 {
146 }
147 catch (...)
148 {
149 throw;
150 }
151 }
152
153 bool operator <(const trace& t) const
154 {
155 return ((m_states<t.m_states) ||
157 }
158
162 {
163 assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
164 m_pos = 0;
165 }
166
170 {
171 if (m_pos < m_actions.size())
172 {
173 ++m_pos;
174 }
175 }
176
180 {
181 if (m_pos >0)
182 {
183 --m_pos;
184 }
185 }
186
191 void set_position(std::size_t pos)
192 {
193 if (pos <= m_actions.size())
194 {
195 this->m_pos = pos;
196 }
197 }
198
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
211 std::size_t number_of_actions() const
212 {
213 assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
214 return m_actions.size();
215 }
216
219 std::size_t number_of_states() const
220 {
221 assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
222 return m_states.size();
223 }
224
227 {
228 assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
229 m_states.resize(m_pos);
230 }
231
235 {
236 assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
237 return m_states.size()>m_pos;
238 }
239
245 const lps::state& next_state() const
246 {
247 assert(m_actions.size()+1 >= m_states.size() && m_pos+1 <=m_actions.size());
248 if (m_pos>=m_states.size())
249 {
250 throw mcrl2::runtime_error("Requesting a state in a trace at a non existing position " + std::to_string(m_pos+1) + ".");
251 }
252 return m_states[m_pos+1];
253 }
254
261 {
262 assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
263 if (m_pos>=m_states.size())
264 {
265 throw mcrl2::runtime_error("Requesting a state in a trace at a non existing position " + std::to_string(m_pos) + ".");
266 }
267 return m_states[m_pos];
268 }
269
273 {
274 assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
275 return m_pos < m_actions.size();
276 }
277
284 {
285 assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
286 assert(m_pos < m_actions.size());
287 return m_actions[m_pos];
288 }
289
295 {
296 assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
297 return m_actions[m_pos].time();
298 }
299
304 void truncate()
305 {
306 m_actions.resize(m_pos);
307 if (m_pos+1<m_states.size()) // Only throw states away that exist.
308 {
309 m_states.resize(m_pos+1);
310 }
311 }
312
318
320 {
321 assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
322 truncate(); // Take care that actions and states have the appropriate size.
323 m_pos++;
324 m_actions.push_back(action);
325 }
326
331 // void set_state(const mcrl2::lps::state& s)
332 void set_state(const lps::state& s)
333 {
334 assert(m_actions.size()+1 >= m_states.size() && m_pos <=m_actions.size());
335 if (m_pos>m_states.size())
336 {
337 throw mcrl2::runtime_error("Setting a state in a trace at a position " + std::to_string(m_pos) +
338 " where there are no states at earlier positions.");
339 }
340
341 if (m_states.size()==m_pos)
342 {
343 m_states.push_back(s);
344 }
345 else
346 {
347 m_states[m_pos] = s;
348 }
349 }
350
357
358 void load(const std::string& filename, trace_format tf = tfUnknown)
359 {
360 using std::ifstream;
361 ifstream is(filename.c_str(),ifstream::binary|ifstream::in);
362
363 if (!is.is_open())
364 {
365 throw runtime_error("Error loading trace (could not open file " + filename +").");
366 }
367
368 try
369 {
370 if (tf == tfUnknown)
371 {
372 tf = detectFormat(is);
373 }
374
375 switch (tf)
376 {
377 case tfMcrl2:
379 break;
380 case tfPlain:
382 break;
383 default:
384 break;
385 }
386
387 }
388 catch (mcrl2::runtime_error& err)
389 {
391 }
392 }
393
400
401 void save(const std::string& filename, trace_format tf = tfMcrl2) const
402 {
403 try
404 {
405 switch (tf)
406 {
407 case tfMcrl2:
408 save_mcrl2(filename);
409 break;
410 case tfPlain:
411 save_plain(filename);
412 break;
413 case tfLine:
414 save_line(filename);
415 break;
416 default:
417 throw runtime_error("Error saving trace to " + (filename.empty()?std::string(" stdout"):filename) + ".");
418 }
419 }
420 catch (runtime_error& err)
421 {
422 throw runtime_error("Error saving trace to " + (filename.empty()?std::string(" stdout"):filename) + ".\n" + err.what());
423 }
424 }
425
426 const std::vector<lps::state>& states() const
427 {
428 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 void init()
439 {
440 m_pos = 0;
441 truncate(); // Take care that m_pos 0 exists.
442 }
443
444 trace_format detectFormat(std::istream& is)
445 {
446 trace_format fmt = tfPlain;
447
448 char c=is.peek();
450 {
451 throw runtime_error("Could not read from stream.");
452 }
453
454 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 fmt = tfMcrl2;
458 }
459
460 return fmt;
461 }
462
464 {
466 try
467 {
469 }
470 catch (mcrl2::runtime_error& e)
471 {
472 throw runtime_error(std::string("stream does not contain an mCRL2 trace.\n") + e.what());
473 }
474
475 m_spec = lts.data();
476 m_act_decls = lts.action_label_declarations();
478
480 truncate();
481
482 std::vector<bool> has_state_outgoing_transition(lts.num_states(),false);
483 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 for(const transition& t: lts.get_transitions())
487 {
488 if (has_state_outgoing_transition.at(t.from()))
489 {
490 throw runtime_error("The tracefile contains an labelled transition system that is not a trace. State " +
491 std::to_string(t.from()) + " has multiple outgoing transitions.");
492 }
493 has_state_outgoing_transition[t.from()]=true;
494 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
503 if (lts.has_state_info())
504 {
506 if (lts.state_label(current_state).size()!=1)
507 {
508 throw mcrl2::runtime_error("The trace has multiple state labels for some states, and hence is not a trace.");
509 }
511 }
512
513 while (has_state_outgoing_transition.at(current_state))
514 {
516 current_state=outgoing_transition[current_state].to();
517 if (lts.has_state_info())
518 {
520 if (lts.state_label(current_state).size()!=1)
521 {
522 throw mcrl2::runtime_error("The trace has multiple state labels for some states, and hence is not a trace.");
523 }
525 }
526 }
527
529 }
530
532 {
534 truncate();
535 m_states.clear(); // Throw all states away, also the initial state.
536
537 std::string action;
538 while (!is.eof())
539 {
540 std::getline(is,action);
542 {
543 throw mcrl2::runtime_error("Error while reading from stream.");
544 }
545
546 action = action.substr(0,action.find_last_not_of(" \r")+1);
547 if (!action.empty())
548 {
550 {
552 }
553 else
554 {
558 }
559 }
560 }
561 is.clear();
562
564 }
565
566 void save_mcrl2(const std::string& filename) const
567 {
568 // The trace is saved as an .lts in lts format.
571 {
572 lts.set_data(m_spec);
573 lts.set_action_label_declarations(m_act_decls);
574 }
575 assert(m_actions.size()+1 >= m_states.size());
576
580
581 std::map<mcrl2::lps::multi_action,std::size_t>
582 obtain_unique_numbers_for_action_labels({std::pair(action_label_lts::tau_action(),0)});
583 for(std::size_t i=0; i<m_actions.size(); ++i)
584 {
585 auto [element, inserted] =
586 obtain_unique_numbers_for_action_labels.insert(
587 std::pair(m_actions[i],
588 obtain_unique_numbers_for_action_labels.size()));
589 if (inserted)
590 {
592 }
594
598 }
600
601 lts.save(filename);
602 }
603
604 void save_text_to_stream(std::ostream& os, std::string separator) const
605 {
606 std::string sep;
607 for (std::size_t i=0; i<m_actions.size(); i++)
608 {
609 os << sep << pp(m_actions[i]);
610 sep = separator;
612 {
613 throw runtime_error("Could not write to stream.");
614 }
615 }
616 os << std::endl;
617 }
618
619 void save_text(const std::string& filename, std::string separator) const
620 {
621 if (filename=="")
622 {
623 save_text_to_stream(std::cout, separator);
624 }
625 else
626 {
627 using std::ofstream;
628 ofstream os;
629 os.open(filename.c_str(),ofstream::binary|ofstream::out|ofstream::trunc);
630 if (!os.is_open())
631 {
632 os.close();
633 throw runtime_error("Could not open file.");
634 }
635 save_text_to_stream(os, separator);
636 os.close();
637 }
638 }
639
640 void save_line(const std::string& filename) const
641 {
642 save_text(filename, ";");
643 }
644
645 void save_plain(const std::string& filename) const
646 {
647 save_text(filename, "\n");
648 }
649
650};
651
652}
653}
654#endif // MCRL2_LTS_TRACE_H
Term containing a string.
Read-only balanced binary tree of terms.
\brief A timed multi-action
A class containing the values for action labels for the .lts format.
Definition lts_lts.h:137
static const action_label_lts & tau_action()
Definition lts_lts.h:175
This class contains labelled transition systems in .lts format.
Definition lts_lts.h:374
A class that contains a labelled transition system.
Definition lts.h:83
states_size_type num_state_labels() const
Gets the number of state labels of this LTS.
Definition lts.h:271
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
ACTION_LABEL_T action_label(const labels_size_type action) const
Gets the label of an action.
Definition lts.h:470
bool has_state_info() const
Checks whether this LTS has state values associated with its states.
Definition lts.h:636
void set_initial_state(const states_size_type state)
Sets the initial state number of this LTS.
Definition lts.h:334
std::vector< state_label_lts >::size_type states_size_type
The sort that contains the indices of states.
Definition lts.h:100
STATE_LABEL_T state_label(const states_size_type state) const
Gets the label of a state.
Definition lts.h:450
Adds a state to this LTS.
Definition lts.h:347
state_label_lts state_label_t
The type of state labels.
Definition lts.h:88
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
Adds an action with a label to this LTS.
Definition lts.h:361
This class contains state labels for an labelled transition system in .lts format.
Definition lts_lts.h:40
This class contains a trace consisting of a sequence of (timed) actions possibly with intermediate st...
Definition trace.h:52
void load(const std::string &filename, trace_format tf=tfUnknown)
Replace the trace with the trace in the file.
Definition trace.h:358
void set_position(std::size_t pos)
Set the current position after the m_pos'th action of the trace.
Definition trace.h:191
mcrl2::data::data_specification m_spec
Definition trace.h:86
std::size_t number_of_states() const
Get the number of states in the current trace.
Definition trace.h:219
void increase_position()
Increase the current position by one, except if this brings one beyond the end of the trace.
Definition trace.h:169
trace(const mcrl2::data::data_specification &spec, const mcrl2::process::action_label_list &act_decls)
Constructor for an empty trace.
Definition trace.h:105
void save_text_to_stream(std::ostream &os, std::string separator) const
Definition trace.h:604
bool current_action_exists() const
Indicate whether the current action exists.
Definition trace.h:272
bool m_data_specification_and_act_decls_are_defined
Definition trace.h:88
const std::vector< lps::state > & states() const
Definition trace.h:426
bool operator<(const trace &t) const
Definition trace.h:153
void set_state(const lps::state &s)
Set the state at the current position.
Definition trace.h:332
const lps::state & next_state() const
Get the state at the current position in the trace.
Definition trace.h:245
bool current_state_exists() const
Indicate whether a current state exists.
Definition trace.h:234
const lps::state & current_state() const
Get the state at the current position in the trace.
Definition trace.h:260
void save_line(const std::string &filename) const
Definition trace.h:640
mcrl2::data::data_expression current_time()
Get the time of the current state in the trace.
Definition trace.h:294
trace_format
Formats in which traces can be saved on disk.
Definition trace.h:67
process::action_label_list m_act_decls
Definition trace.h:87
void clear_current_state()
Remove the current state and all states following it.
Definition trace.h:226
void save_mcrl2(const std::string &filename) const
Definition trace.h:566
std::size_t get_position() const
Get the current position in the trace.
Definition trace.h:203
void save_text(const std::string &filename, std::string separator) const
Definition trace.h:619
trace(const std::string &filename, const mcrl2::data::data_specification &spec, const mcrl2::process::action_label_list &act_decls, trace_format tf=tfUnknown)
Construct the trace on the basis of an input file.
Definition trace.h:134
void reset_position()
Set the current position back to the beginning of the trace.
Definition trace.h:161
std::size_t number_of_actions() const
Get the number of actions in the current trace.
Definition trace.h:211
std::vector< mcrl2::lps::multi_action > m_actions
Definition trace.h:83
void save(const std::string &filename, trace_format tf=tfMcrl2) const
Output the trace into a file with the indicated name.
Definition trace.h:401
trace()
Default constructor for an empty trace.
Definition trace.h:94
Definition trace.h:531
mcrl2::lps::multi_action current_action()
Get the outgoing action from the current position in the trace.
Definition trace.h:283
Definition trace.h:463
std::size_t m_pos
Definition trace.h:84
void save_plain(const std::string &filename) const
Definition trace.h:645
void decrease_position()
Decrease the current position in the trace by one provided the largest position is larger than 0.
Definition trace.h:179
trace(const std::string &filename, trace_format tf=tfUnknown)
Construct the trace on the basis of an input file.
Definition trace.h:119
std::vector< lps::state > m_states
Definition trace.h:82
trace_format detectFormat(std::istream &is)
Definition trace.h:444
void truncate()
Truncates the trace at the current position.
Definition trace.h:304
const std::vector< lps::multi_action > & actions() const
Definition trace.h:431
Add an action to the current trace.
Definition trace.h:319
A class containing triples, source label and target representing transitions.
Definition transition.h:43
\brief An action label
Standard exception class for reporting runtime errors.
Definition exception.h:27