mcrl2::lps::stochastic_specification

Include file:

#include "mcrl2/lps/stochastic_specification.h
class mcrl2::lps::stochastic_specification

Linear process specification.

Public member functions

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

Constructor.

stochastic_specification(const stochastic_specification &other)

Constructor.

stochastic_specification(const atermpp::aterm_appl &t)

Constructor.

Parameters:

  • t A term

stochastic_specification(const data::data_specification &data, const process::action_label_list &action_labels, const std::set<data::variable> &global_variables, const stochastic_linear_process &lps, const stochastic_process_initializer &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

stochastic_specification(const specification &other)

Constructor. This constructor is explicit as implicit conversions of this kind is a source of bugs.