mcrl2::lps::specification_base

Include file:

#include "mcrl2/lps/specification.h

class mcrl2::lps::specification_base

Public types

type mcrl2::lps::specification_base::initial_process_type

typedef for InitialProcessExpression

The initial process type.

type mcrl2::lps::specification_base::process_type

typedef for LinearProcess

The process type.

Protected attributes

process::action_label_list mcrl2::lps::specification_base::m_action_labels

The action specification of the specification.

data::data_specification mcrl2::lps::specification_base::m_data

The data specification of the specification.

std::set<data::variable> mcrl2::lps::specification_base::m_global_variables

The set of global variables.

InitialProcessExpression mcrl2::lps::specification_base::m_initial_process

The initial state of the specification.

LinearProcess mcrl2::lps::specification_base::m_process

The linear process of the specification.

Public member functions

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 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.

data::data_specification &data()

Returns a reference to the data specification.

Returns: The data specification.

const data::data_specification &data() const

Returns the data specification.

Returns: The data specification.

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

Returns the declared free variables of the LPS.

Returns: The declared free variables of the LPS.

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

Returns the declared free variables of the LPS.

Returns: The declared free variables of the LPS.

InitialProcessExpression &initial_process()

Returns a reference to the initial process.

Returns: The initial process.

const InitialProcessExpression &initial_process() const

Returns the initial process.

Returns: The initial process.

LinearProcess &process()

Returns a reference to the linear process of the specification.

Returns: The linear process of the specification.

const LinearProcess &process() const

Returns the linear process of the specification.

Returns: The linear process of the specification.

specification_base()

Constructor.

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