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

#include <trace.h>

Public Types
enum	trace_format { tfMcrl2 , tfPlain , tfLine , tfUnknown }
	Formats in which traces can be saved on disk. More...

Public Member Functions
	trace ()
	Default constructor for an empty trace.

	trace (const mcrl2::data::data_specification &spec, const mcrl2::process::action_label_list &act_decls)
	Constructor for an empty trace.

	trace (const std::string &filename, trace_format tf=tfUnknown)
	Construct the trace on the basis of an input file.

	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.

bool	operator< (const trace &t) const

void	reset_position ()
	Set the current position back to the beginning of the trace.

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

void	decrease_position ()
	Decrease the current position in the trace by one provided the largest position is larger than 0.

void	set_position (std::size_t pos)
	Set the current position after the m_pos'th action of the trace.

std::size_t	get_position () const
	Get the current position in the trace.

std::size_t	number_of_actions () const
	Get the number of actions in the current trace.

std::size_t	number_of_states () const
	Get the number of states in the current 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.

const lps::state &	next_state () const
	Get the state at the current position in the trace.

const lps::state &	current_state () const
	Get the state at the current position in the trace.

bool	current_action_exists () const
	Indicate whether the current action exists.

mcrl2::lps::multi_action	current_action ()
	Get the outgoing action from the current position in the trace.

mcrl2::data::data_expression	current_time ()
	Get the time of the current state in the trace.

void	truncate ()
	Truncates the trace at the current position.

void	add_action (const mcrl2::lps::multi_action &action)
	Add an action to the current trace.

void	set_state (const lps::state &s)
	Set the state at the current position.

void	load (const std::string &filename, trace_format tf=tfUnknown)
	Replace the trace with the trace in the file.

void	save (const std::string &filename, trace_format tf=tfMcrl2) const
	Output the trace into a file with the indicated name.

const std::vector< lps::state > &	states () const

const std::vector< lps::multi_action > &	actions () const

Protected Member Functions
void	init ()

trace_format	detectFormat (std::istream &is)

void	load_mcrl2 (const std::string &filename)

void	load_plain (std::istream &is)

void	save_mcrl2 (const std::string &filename) const

void	save_text_to_stream (std::ostream &os, std::string separator) const

void	save_text (const std::string &filename, std::string separator) const

void	save_line (const std::string &filename) const

void	save_plain (const std::string &filename) const

Protected Attributes
std::vector< lps::state >	m_states

std::vector< mcrl2::lps::multi_action >	m_actions

std::size_t	m_pos

mcrl2::data::data_specification	m_spec

process::action_label_list	m_act_decls

bool	m_data_specification_and_act_decls_are_defined

Detailed Description

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.

Definition at line 51 of file trace.h.

Member Enumeration Documentation

◆ trace_format

enum mcrl2::lts::trace::trace_format

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.

Enumerator
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

Definition at line 66 of file trace.h.

Constructor & Destructor Documentation

◆ trace() [1/4]

mcrl2::lts::trace::trace ( )

inline

Default constructor for an empty trace.

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

Definition at line 94 of file trace.h.

◆ trace() [2/4]

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

inline

Constructor for an empty trace.

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

Parameters

[in]	spec	The data specification that is used when parsing multi actions.
[in]	act_decls	An action label list with action declarations that is used to parse multi actions.

Definition at line 105 of file trace.h.

◆ trace() [3/4]

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

inline

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

[in]	filename	The name of the file from which the trace is read.
[in]	tf	The format in which the trace was stored. Default: '''tfUnknown'''.

Exceptions

mcrl2::runtime_error message in case of failure

Definition at line 119 of file trace.h.

◆ trace() [4/4]

mcrl2::lts::trace::trace	(	const std::string &	filename,
		const mcrl2::data::data_specification &	spec,
		const mcrl2::process::action_label_list &	act_decls,
		trace_format	tf = `tfUnknown`
	)

inline

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

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

Exceptions

mcrl2::runtime_error message in case of failure

Definition at line 134 of file trace.h.

Member Function Documentation

◆ actions()

const std::vector< lps::multi_action > & mcrl2::lts::trace::actions ( ) const

inline

Definition at line 431 of file trace.h.

◆ add_action()

void mcrl2::lts::trace::add_action ( const mcrl2::lps::multi_action & action )

inline

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

[in] action The multi_action to be stored in the trace.

Definition at line 319 of file trace.h.

◆ clear_current_state()

void mcrl2::lts::trace::clear_current_state ( )

inline

Remove the current state and all states following it.

Definition at line 226 of file trace.h.

◆ current_action()

mcrl2::lps::multi_action mcrl2::lts::trace::current_action ( )

inline

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.

Definition at line 283 of file trace.h.

◆ current_action_exists()

bool mcrl2::lts::trace::current_action_exists ( ) const

inline

Indicate whether the current action exists.

Returns: A boolean indicating that the current action exists;

Definition at line 272 of file trace.h.

◆ current_state()

const lps::state & mcrl2::lts::trace::current_state ( ) const

inline

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.

Definition at line 260 of file trace.h.

◆ current_state_exists()

bool mcrl2::lts::trace::current_state_exists ( ) const

inline

Indicate whether a current state exists.

Returns: A boolean indicating whether the current state exists.

Definition at line 234 of file trace.h.

◆ current_time()

mcrl2::data::data_expression mcrl2::lts::trace::current_time ( )

inline

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.

Definition at line 294 of file trace.h.

◆ decrease_position()

void mcrl2::lts::trace::decrease_position ( )

inline

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.

Definition at line 179 of file trace.h.

◆ detectFormat()

trace_format mcrl2::lts::trace::detectFormat ( std::istream & is )

inlineprotected

Definition at line 444 of file trace.h.

◆ get_position()

std::size_t mcrl2::lts::trace::get_position ( ) const

inline

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.

Definition at line 203 of file trace.h.

◆ increase_position()

void mcrl2::lts::trace::increase_position ( )

inline

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.

Definition at line 169 of file trace.h.

◆ init()

void mcrl2::lts::trace::init ( )

inlineprotected

Definition at line 438 of file trace.h.

◆ load()

void mcrl2::lts::trace::load	(	const std::string &	filename,
		trace_format	tf = `tfUnknown`
	)

inline

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

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

Exceptions

mcrl2::runtime_error message in case of failure

Definition at line 358 of file trace.h.

◆ load_mcrl2()

void mcrl2::lts::trace::load_mcrl2 ( const std::string & filename )

inlineprotected

Definition at line 463 of file trace.h.

◆ load_plain()

void mcrl2::lts::trace::load_plain ( std::istream & is )

inlineprotected

Definition at line 531 of file trace.h.

◆ next_state()

const lps::state & mcrl2::lts::trace::next_state ( ) const

inline

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.

Definition at line 245 of file trace.h.

◆ number_of_actions()

std::size_t mcrl2::lts::trace::number_of_actions ( ) const

inline

Get the number of actions in the current trace.

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

Definition at line 211 of file trace.h.

◆ number_of_states()

std::size_t mcrl2::lts::trace::number_of_states ( ) const

inline

Get the number of states in the current trace.

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

Definition at line 219 of file trace.h.

◆ operator<()

bool mcrl2::lts::trace::operator< ( const trace & t ) const

inline

Definition at line 153 of file trace.h.

◆ reset_position()

void mcrl2::lts::trace::reset_position ( )

inline

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

The trace itself remains unaltered.

Definition at line 161 of file trace.h.

◆ save()

void mcrl2::lts::trace::save	(	const std::string &	filename,
		trace_format	tf = `tfMcrl2`
	)		const

inline

Output the trace into a file with the indicated name.

Write the trace to a file with the indicated name.

Parameters

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

Exceptions

mcrl2::runtime_error message in case of failure

Definition at line 401 of file trace.h.

◆ save_line()

void mcrl2::lts::trace::save_line ( const std::string & filename ) const

inlineprotected

Definition at line 640 of file trace.h.

◆ save_mcrl2()

void mcrl2::lts::trace::save_mcrl2 ( const std::string & filename ) const

inlineprotected

Definition at line 566 of file trace.h.

◆ save_plain()

void mcrl2::lts::trace::save_plain ( const std::string & filename ) const

inlineprotected

Definition at line 645 of file trace.h.

◆ save_text()

void mcrl2::lts::trace::save_text	(	const std::string &	filename,
		std::string	separator
	)		const

inlineprotected

Definition at line 619 of file trace.h.

◆ save_text_to_stream()

void mcrl2::lts::trace::save_text_to_stream	(	std::ostream &	os,
		std::string	separator
	)		const

inlineprotected

Definition at line 604 of file trace.h.

◆ set_position()

void mcrl2::lts::trace::set_position ( std::size_t pos )

inline

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

[in] m_pos The new position in the trace.

Definition at line 191 of file trace.h.

◆ set_state()

void mcrl2::lts::trace::set_state ( const lps::state & s )

inline

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

[in] s The new state.

Definition at line 332 of file trace.h.

◆ states()

const std::vector< lps::state > & mcrl2::lts::trace::states ( ) const

inline

Definition at line 426 of file trace.h.

◆ truncate()

void mcrl2::lts::trace::truncate ( )

inline

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.

Definition at line 304 of file trace.h.

Member Data Documentation

◆ m_act_decls

process::action_label_list mcrl2::lts::trace::m_act_decls

protected

Definition at line 87 of file trace.h.

◆ m_actions

std::vector< mcrl2::lps::multi_action > mcrl2::lts::trace::m_actions

protected

Definition at line 83 of file trace.h.

◆ m_data_specification_and_act_decls_are_defined

bool mcrl2::lts::trace::m_data_specification_and_act_decls_are_defined

protected

Definition at line 88 of file trace.h.

◆ m_pos

std::size_t mcrl2::lts::trace::m_pos

protected

Definition at line 84 of file trace.h.

◆ m_spec

mcrl2::data::data_specification mcrl2::lts::trace::m_spec

protected

Definition at line 86 of file trace.h.

◆ m_states

std::vector< lps::state > mcrl2::lts::trace::m_states

protected

Definition at line 82 of file trace.h.

The documentation for this class was generated from the following file:

lts/include/mcrl2/lts/trace.h

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Member Enumeration Documentation

◆ trace_format

Constructor & Destructor Documentation

◆ trace() [1/4]

◆ trace() [2/4]

◆ trace() [3/4]

◆ trace() [4/4]

Member Function Documentation

◆ actions()

◆ add_action()

◆ clear_current_state()

◆ current_action()

◆ current_action_exists()

◆ current_state()

◆ current_state_exists()

◆ current_time()

◆ decrease_position()

◆ detectFormat()

◆ get_position()

◆ increase_position()

◆ init()

◆ load()

◆ load_mcrl2()

◆ load_plain()

◆ next_state()

◆ number_of_actions()

◆ number_of_states()

◆ operator<()

◆ reset_position()

◆ save()

◆ save_line()

◆ save_mcrl2()

◆ save_plain()

◆ save_text()

◆ save_text_to_stream()

◆ set_position()

◆ set_state()

◆ states()

◆ truncate()

Member Data Documentation

◆ m_act_decls

◆ m_actions

◆ m_data_specification_and_act_decls_are_defined

◆ m_pos

◆ m_spec

◆ m_states