17#ifndef MCRL2_LTS_TRACE_H
18#define MCRL2_LTS_TRACE_H
338 " where there are no states at earlier positions.");
361 ifstream is(filename.c_str(),ifstream::binary|ifstream::in);
365 throw runtime_error(
"Error loading trace (could not open file " + filename +
").");
417 throw runtime_error(
"Error saving trace to " + (filename.empty()?std::string(
" stdout"):filename) +
".");
422 throw runtime_error(
"Error saving trace to " + (filename.empty()?std::string(
" stdout"):filename) +
".\n" + err.what());
426 const std::vector<lps::state>&
states()
const
431 const std::vector<lps::multi_action>&
actions()
const
472 throw runtime_error(std::string(
"stream does not contain an mCRL2 trace.\n") + e.what());
482 std::vector<bool> has_state_outgoing_transition(
lts.
num_states(),
false);
488 if (has_state_outgoing_transition.at(t.from()))
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.");
493 has_state_outgoing_transition[t.from()]=
true;
494 outgoing_transition[t.from()]=t;
508 throw mcrl2::runtime_error(
"The trace has multiple state labels for some states, and hence is not a trace.");
522 throw mcrl2::runtime_error(
"The trace has multiple state labels for some states, and hence is not a trace.");
540 std::getline(is,action);
546 action = action.substr(0,action.find_last_not_of(
" \r")+1);
581 std::map<mcrl2::lps::multi_action,std::size_t>
583 for(std::size_t i=0; i<
m_actions.size(); ++i)
585 auto [element, inserted] =
586 obtain_unique_numbers_for_action_labels.insert(
588 obtain_unique_numbers_for_action_labels.size()));
607 for (std::size_t i=0; i<
m_actions.size(); i++)
619 void save_text(
const std::string& filename, std::string separator)
const
629 os.open(filename.c_str(),ofstream::binary|ofstream::out|ofstream::trunc);
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.
static const action_label_lts & tau_action()
This class contains labelled transition systems in .lts format.
A class that contains a labelled transition system.
states_size_type num_state_labels() const
Gets the number of state labels of this LTS.
void add_transition(const transition &t)
Add a transition to the lts.
states_size_type num_states() const
Gets the number of states of this LTS.
ACTION_LABEL_T action_label(const labels_size_type action) const
Gets the label of an action.
bool has_state_info() const
Checks whether this LTS has state values associated with its states.
void set_initial_state(const states_size_type state)
Sets the initial state number of this LTS.
std::vector< state_label_lts >::size_type states_size_type
The sort that contains the indices of states.
STATE_LABEL_T state_label(const states_size_type state) const
Gets the label of a state.
states_size_type add_state(const STATE_LABEL_T &label=STATE_LABEL_T())
Adds a state to this LTS.
state_label_lts state_label_t
The type of state labels.
const std::vector< transition > & get_transitions() const
Gets a const reference to the vector of transitions of the current lts.
states_size_type initial_state() const
Gets the initial state number of this LTS.
labels_size_type add_action(const ACTION_LABEL_T &label)
Adds an action with a label to this LTS.
This class contains state labels for an labelled transition system in .lts format.
This class contains a trace consisting of a sequence of (timed) actions possibly with intermediate st...
void load(const std::string &filename, trace_format tf=tfUnknown)
Replace the trace with the trace in the file.
void set_position(std::size_t pos)
Set the current position after the m_pos'th action of the trace.
mcrl2::data::data_specification m_spec
std::size_t number_of_states() const
Get the number of states in the current trace.
void increase_position()
Increase the current position by one, except if this brings one beyond the end of the trace.
trace(const mcrl2::data::data_specification &spec, const mcrl2::process::action_label_list &act_decls)
Constructor for an empty trace.
void save_text_to_stream(std::ostream &os, std::string separator) const
bool current_action_exists() const
Indicate whether the current action exists.
bool m_data_specification_and_act_decls_are_defined
const std::vector< lps::state > & states() const
bool operator<(const trace &t) const
void set_state(const lps::state &s)
Set the state at the current position.
const lps::state & next_state() const
Get the state at the current position in the trace.
bool current_state_exists() const
Indicate whether a current state exists.
const lps::state & current_state() const
Get the state at the current position in the trace.
void save_line(const std::string &filename) const
mcrl2::data::data_expression current_time()
Get the time of the current state in the trace.
trace_format
Formats in which traces can be saved on disk.
process::action_label_list m_act_decls
void clear_current_state()
Remove the current state and all states following it.
void save_mcrl2(const std::string &filename) const
std::size_t get_position() const
Get the current position in the trace.
void save_text(const std::string &filename, std::string separator) const
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.
void reset_position()
Set the current position back to the beginning of the trace.
std::size_t number_of_actions() const
Get the number of actions in the current trace.
std::vector< mcrl2::lps::multi_action > m_actions
void save(const std::string &filename, trace_format tf=tfMcrl2) const
Output the trace into a file with the indicated name.
trace()
Default constructor for an empty trace.
void load_plain(std::istream &is)
mcrl2::lps::multi_action current_action()
Get the outgoing action from the current position in the trace.
void load_mcrl2(const std::string &filename)
void save_plain(const std::string &filename) const
void decrease_position()
Decrease the current position in the trace by one provided the largest position is larger than 0.
trace(const std::string &filename, trace_format tf=tfUnknown)
Construct the trace on the basis of an input file.
std::vector< lps::state > m_states
trace_format detectFormat(std::istream &is)
void truncate()
Truncates the trace at the current position.
const std::vector< lps::multi_action > & actions() const
void add_action(const mcrl2::lps::multi_action &action)
Add an action to the current trace.
A class containing triples, source label and target representing transitions.
Standard exception class for reporting runtime errors.
add your file description here.
This file contains a class that contains labelled transition systems in lts (mcrl2) format.
std::string pp(const abstraction &x)
multi_action parse_multi_action(std::stringstream &in, const process::action_label_list &action_decls, const data::data_specification &data_spec=data::detail::default_specification())
Parses a multi_action from an input stream.
atermpp::term_list< action_label > action_label_list
\brief list of action_labels
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...