mcrl2::trace::Trace

Include file:

#include "mcrl2/trace/trace.h
class mcrl2::trace::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.

Private attributes

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

Private member functions

TraceFormat detectFormat(std::istream &is)
void init()
bool isTimedMAct(const atermpp::aterm_appl &t)
void loadMcrl2(std::istream &is)
void loadPlain(std::istream &is)
atermpp::aterm_appl makeTimedMAct(const mcrl2::lps::multi_action &ma)
atermpp::aterm readATerm(std::istream &is)
void saveMcrl2(std::ostream &os)
void savePlain(std::ostream &os)
const atermpp::function_symbol &trace_pair() const

Public member functions

const std::vector<lps::multi_action> &actions() const
void addAction(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.

bool current_state_exists() const

Indicate whether a current state exists.

Returns: A boolean indicating whether the current state exists.

mcrl2::lps::multi_action currentAction()

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 mcrl2::lps::state &currentState() 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.

mcrl2::data::data_expression currentTime()

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 decreasePosition()

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

The initial position corresponds to pos=0.

std::size_t getPosition() 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 increasePosition()

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

The initial position corresponds to pos=0.

void load(std::istream &is, TraceFormat tf = tfUnknown)

Replace the trace with the content of the stream.

The trace is replaced with the trace in the stream. If a problem occurs while reading the stream, a core dump occurs. If the format is tfPlain the trace can only consist of actions.

Parameters:

  • is The stream 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

void load(const std::string &filename, TraceFormat 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 mcrl2::lps::state &nextState() 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 resetPosition()

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

The trace itself remains unaltered.

void save(std::ostream &os, TraceFormat tf = tfMcrl2)

Output the trace into the indicated stream.

Output the trace into the indicated stream. If a problem occurs, this routine dumps core.

Parameters:

  • os The stream to which the trace 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 save(std::string const &filename, TraceFormat tf = tfMcrl2)

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 setPosition(std::size_t pos)

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

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

Parameters:

  • pos The new position in the trace.
void setState(const mcrl2::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(std::istream &is, TraceFormat tf = tfUnknown)

Construct the trace in the basis of an input stream.

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

Parameters:

  • is The input stream 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

Trace(std::istream &is, const mcrl2::data::data_specification &spec, const mcrl2::process::action_label_list &act_decls, TraceFormat tf = tfUnknown)

Construct the trace in the basis of an input stream.

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

Parameters:

  • is The input stream from which the trace is read.
  • tf The format in which the trace was stored. Default: ‘’‘tfUnknown’‘’.
  • 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.

exception * mcrl2::runtime_error message in case of failure

Trace(std::string const &filename, TraceFormat 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

Trace(std::string const &filename, const mcrl2::data::data_specification &spec, const mcrl2::process::action_label_list &act_decls, TraceFormat 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

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.