mcrl2::lps::specification_base

Include file:

#include "mcrl2/lps/specification.h
class mcrl2::lps::specification_base

Public types

type process_type

typedef for LinearProcess

The process type.

Protected attributes

process::action_label_list m_action_labels

The action specification of the specification.

data::data_specification m_data

The data specification of the specification.

std::set<data::variable> m_global_variables

The set of global variables.

InitialProcessExpression m_initial_process

The initial state of the specification.

LinearProcess m_process

The linear process of the specification.

Protected member functions

void construct_from_aterm(const atermpp::aterm_appl &t, bool stochastic_distributions_allowed = true)

Initializes the specification with an aterm.

Parameters:

  • t An aterm.
  • stochastic_distributions_allowed A boolean indicating that the specification can contain stochastic operators.
const atermpp::aterm_appl &get(const atermpp::aterm_appl &t, std::size_t i)

Returns the i-th element of t, converted to aterm_appl.

Public member functions

const process::action_label_list &action_labels() const

Returns a sequence of action labels. This sequence contains all action labels occurring in the specification (but it can have more).

Returns: A sequence of action labels.

process::action_label_list &action_labels()

Returns a sequence of action labels. This sequence contains all action labels occurring in the specification (but it can have more).

Returns: A sequence of action labels.

const data::data_specification &data() const

Returns the data specification.

Returns: The data specification.

data::data_specification &data()

Returns a reference to the data specification.

Returns: The data specification.

const std::set<data::variable> &global_variables() const

Returns the declared free variables of the LPS.

Returns: The declared free variables of the LPS.

std::set<data::variable> &global_variables()

Returns the declared free variables of the LPS.

Returns: The declared free variables of the LPS.

const InitialProcessExpression &initial_process() const

Returns the initial process.

Returns: The initial process.

InitialProcessExpression &initial_process()

Returns a reference to the initial process.

Returns: The initial process.

void load(std::istream &stream, bool binary = true, const std::string &source = "")

Reads the specification from a stream.

Parameters:

  • stream An input stream.
  • binary An boolean that if true means the stream contains a term in binary encoding.
  • source The source from which the stream originates. Used for error messages.
const LinearProcess &process() const

Returns the linear process of the specification.

Returns: The linear process of the specification.

LinearProcess &process()

Returns a reference to the linear process of the specification.

Returns: The linear process of the specification.

void save(std::ostream &stream, bool binary = true) const

Writes the specification to a stream.

Parameters:

  • stream The output stream.
  • binary If binary is true the linear process is saved in compressed binary format. Otherwise an ascii representation is saved. In general the binary format is much more compact than the ascii representation.
specification_base()

Constructor.

specification_base(const specification_base<LinearProcess, InitialProcessExpression> &other)
specification_base(const atermpp::aterm_appl &t, bool stochastic_distributions_allowed = true)

Constructor.

Parameters:

  • t A term
  • stochastic_distributions_allowed A boolean indicating that the specification can contain stochastic operators.
specification_base(const data::data_specification &data, const process::action_label_list &action_labels, const std::set<data::variable> &global_variables, const LinearProcess &lps, const InitialProcessExpression &initial_process)

Constructor.

Parameters:

  • data A data specification
  • action_labels A sequence of action labels
  • global_variables A set of global variables
  • lps A linear process
  • initial_process A process initializer