mcrl2::lts::trace

Include file:

#include "mcrl2/lts/trace.h
class mcrl2::lts::trace

This class contains a trace consisting of a sequence of (timed) actions possibly with intermediate states.

A trace is a sequence of actions. Actions can have a time tag as a positive real number. Between two actions, before the first action and after the last action there can be a state. In the current version of the trace library an action, a state and a time tag are arbitrary expressions of sort AtermAppl. It is expected that this will change in the near future to match the data types used in the LPS library.An important property of a state is its current position. All operations on a state operate with respect to its current position. A trace can be traversed by increasing and decreasing the current position between 0 up to the length. If a new action is added to a trace, the trace above the current position is lost. For each action a state can only be added once.States can be saved in two formats. A human readable ascii format containging only a sequence of untimed actions and a more compact aterm format also containing time and state information.

Public types

type mcrl2::lts::trace::trace_format

Values:

  • tfMcrl2 Format is stored as an aterm
  • tfPlain Format is stored in plain text. In this format there are only actions
  • tfLine Format is stored in a line of text. In this format there are only actions
  • tfUnknown This value indicates that the format is unknown

Formats in which traces can be saved on disk.

There are several formats for traces. The tfMcrl2 format saves a trace as an mCRL2 term in aterm internal format. This is a compact but unreadable format. The tfPlain format is an ascii representation of the trace, which is human readable but only contains the actions and no time or state information. tfUnknown is only used to read traces, when it is not known what the format is. In this case it is determined based on the format of the input file.

Protected attributes

process::action_label_list mcrl2::lts::trace::m_act_decls
std::vector<mcrl2::lps::multi_action> mcrl2::lts::trace::m_actions
bool mcrl2::lts::trace::m_data_specification_and_act_decls_are_defined
std::size_t mcrl2::lts::trace::m_pos
mcrl2::data::data_specification mcrl2::lts::trace::m_spec
std::vector<lps::state> mcrl2::lts::trace::m_states

Public member functions

const std::vector<lps::multi_action> &actions() const
void add_action(const mcrl2::lps::multi_action &action)

Add an action to the current trace.

Add an action to the current trace at the current position. The current position is increased and the length of the trace is set to this new current position. The old actions in the trace at the current at higher positions are removed.

Parameters:

  • action The multi_action to be stored in the trace.
void clear_current_state()

Remove the current state and all states following it.

mcrl2::lps::multi_action current_action()

Get the outgoing action from the current position in the trace.

This routine returns the action at the current position of the trace. It is not allowed to request an action if no action is available.

Returns: An action_list representing the action at the current position of the trace.

const lps::state &current_state() const

Get the state at the current position in the trace.

The state at position 0 is the initial state. If no state is defined at the current position an exception is thrown.

Returns: The state at the current position of the trace.

bool current_state_exists() const

Indicate whether a current state exists.

Returns: A boolean indicating whether the current state exists.

mcrl2::data::data_expression current_time()

Get the time of the current state in the trace.

This is the time at which the last action occurred (if any).

Returns: A data_expression representing the current time, or a default data_expression if the time is not defined.

void decrease_position()

Decrease the current position in the trace by one provided the largest position is larger than 0.

The initial position corresponds to m_pos=0.

std::size_t get_position() const

Get the current position in the trace.

The current position of the trace is a non negative number smaller than the length of the trace.

Returns: The current position of the trace.

void increase_position()

Increase the current position by one, except if this brings one beyond the end of the trace.

The initial position corresponds to m_pos=0.

void load(const std::string &filename, trace_format tf = tfUnknown)

Replace the trace with the trace in the file.

The trace is replaced with the trace in the file. If the format is tfPlain the trace can only consist of actions.

Parameters:

  • filename The name of the file from which the trace is read.
  • tf The expected format of the trace in the stream (default: tfUnknown).

exception * mcrl2::runtime_error message in case of failure

const lps::state &next_state() const

Get the state at the current position in the trace.

The state at position 0 is the initial state. If no state is defined at the next position an exception is thrown.

Returns: The state at the current position of the trace.

std::size_t number_of_actions() const

Get the number of actions in the current trace.

Returns: A positive number indicating the number of actions in the trace.

std::size_t number_of_states() const

Get the number of states in the current trace.

Returns: A positive number indicating the number of states in the trace.

bool operator<(const trace &t) const
void reset_position()

Set the current position back to the beginning of the trace.

The trace itself remains unaltered.

void save(const std::string &filename, trace_format tf = tfMcrl2) const

Output the trace into a file with the indicated name.

Write the trace to a file with the indicated name.

Parameters:

  • filename The name of the file that is written.
  • tf The format used to represent the trace in the stream. If the format is tfPlain only actions are written. Default: tfMcrl2.

exception * mcrl2::runtime_error message in case of failure

void set_position(std::size_t pos)

Set the current position after the m_pos’th action of the trace.

The initial position corresponds to m_pos=0. If m_pos is larger than the length of the trace, no new position is set.

Parameters:

  • m_pos The new position in the trace.
void set_state(const lps::state &s)

Set the state at the current position.

It is necessary that all states at earlier positions are also set. If not an mcrl2::runtime_error exception is thrown.

Parameters:

  • s The new state.
const std::vector<lps::state> &states() const
trace()

Default constructor for an empty trace.

The current position and length of trace are set to 0.

trace(const mcrl2::data::data_specification &spec, const mcrl2::process::action_label_list &act_decls)

Constructor for an empty trace.

The current position and length of trace are set to 0.

Parameters:

  • spec The data specification that is used when parsing multi actions.
  • act_decls An action label list with action declarations that is used to parse multi actions.
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.

A trace is read from the input file. If the format is tfUnknown it is automatically determined what the format of the trace is.

Parameters:

  • filename The name of the file from which the trace is read.
  • spec A data specification.
  • act_decls A list of action declarations.
  • tf The format in which the trace was stored. Default: ‘’’tfUnknown’’’.

exception * mcrl2::runtime_error message in case of failure

trace(const std::string &filename, trace_format tf = tfUnknown)

Construct the trace on the basis of an input file.

A trace is read from the input file. If the format is tfUnknown it is automatically determined what the format of the trace is.

Parameters:

  • filename The name of the file from which the trace is read.
  • tf The format in which the trace was stored. Default: ‘’’tfUnknown’’’.

exception * mcrl2::runtime_error message in case of failure

void truncate()

Truncates the trace at the current position.

This function removes the next action at the current position and all subsequent actions and states. The state and the time at the current position remain untouched.

Protected member functions

trace_format detectFormat(std::istream &is)
void init()
void load_mcrl2(const std::string &filename)
void load_plain(std::istream &is)
void save_line(const std::string &filename) const
void save_mcrl2(const std::string &filename) const
void save_plain(const std::string &filename) const
void save_text(const std::string &filename, std::string separator) const
void save_text_to_stream(std::ostream &os, std::string separator) const