mcrl2::process::process_specification

Include file:

#include "mcrl2/process/process_specification.h
class mcrl2::process::process_specification

Process specification consisting of a data specification, action labels, a sequence of process equations and a process initialization.

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::vector<process_equation> m_equations

The equations of the specification.

std::set<data::variable> m_global_variables

The set of global variables.

process_expression m_initial_process

The initial state of the specification.

Protected member functions

void construct_from_aterm(const atermpp::aterm_appl &t)

Initializes the specification with an aterm.

Parameters:

  • t A term

Public member functions

const process::action_label_list &action_labels() const

Returns the action label specification.

Returns: The action label specification

process::action_label_list &action_labels()

Returns the action label specification.

Returns: The action label specification

const data::data_specification &data() const

Returns the data specification.

Returns: The data specification

data::data_specification &data()

Returns the data specification.

Returns: The data specification

const std::vector<process_equation> &equations() const

Returns the equations of the process specification.

Returns: The equations of the process specification

std::vector<process_equation> &equations()

Returns the equations of the process specification.

Returns: The equations of the process specification

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

Returns the declared free variables of the process specification.

Returns: The declared free variables of the process specification.

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

Returns the declared free variables of the process specification.

Returns: The declared free variables of the process specification.

const process_expression &init() const

Returns the initialization of the process specification.

Returns: The initialization of the process specification

process_expression &init()

Returns the initialization of the process specification.

Returns: The initialization of the process specification

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

Reads a process 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.
process_specification()

Constructor.

process_specification(atermpp::aterm_appl t, const bool data_specification_is_type_checked = true)

Constructor.

Parameters:

  • t A term containing an aterm representation of a process specification.
  • data_specification_is_type_checked A boolean that indicates whether the data specification has been type checked. If so, the internal data specification data structures will be set up. Otherwise, the function declare_data_specification_to_be_type_checked must be invoked after type checking, before the data specification can be used.
process_specification(data::data_specification data, process::action_label_list action_labels, process_equation_list equations, process_expression init)

Constructor that sets the global variables to empty;.

process_specification(data::data_specification data, process::action_label_list action_labels, data::variable_list global_variables, process_equation_list equations, process_expression init)

Constructor of a process specification.

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

Writes the process specification to a stream.

Parameters:

  • stream The output stream.
  • binary If binary is true the process specification 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.