mcrl2::lps::stochastic_specification

Include file:

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

Linear process specification.

Public member functions

stochastic_specification()

Constructor.

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.