mcrl2::lps::pins

Include file:

#include "mcrl2/lps/ltsmin.h
class mcrl2::lps::pins

Public types

type datatype_index

typedef for std::size_t

the index type for datatype maps

type guard_evaluation_t

Values:

  • GUARD_FALSE
  • GUARD_TRUE
  • GUARD_MAYBE

guard evaluations have ternary logic. A guard may not always rewrite to true or false

type ltsmin_state_type

typedef for int *

the state type used by LTSMin

type substitution_t

typedef for data::rewriter::substitution_type

Protected attributes

std::vector<std::vector<std::size_t>> guard_parameters_list
std::vector<pins_data_type *> m_data_types
lps::next_state_generator m_generator
lps::next_state_generator m_generator_reduced
std::size_t m_group_count
std::vector<std::vector<std::size_t>> m_guard_info
std::vector<std::string> m_guard_names
atermpp::indexed_set<atermpp::aterm> m_guards
std::vector<data::variable> m_parameters_list
std::vector<std::string> m_process_parameter_names
std::vector<std::vector<std::size_t>> m_read_group
lps::specification m_specification
lps::specification m_specification_reduced
std::size_t m_state_length

the number of process parameters

std::vector<std::size_t> m_unique_data_type_index
std::vector<pins_data_type *> m_unique_data_types

The unique type mappings (is contained in m_data_types).

std::vector<std::vector<std::size_t>> m_update_group
std::vector<std::vector<std::size_t>> m_write_group

Protected member functions

pins_data_type &action_label_type_map()

Returns the action data type.

const pins_data_type &action_label_type_map() const

Returns the action data type.

const data::data_specification &data() const

Returns the data specification of the LPS specification.

void initialize_read_write_groups()
std::string print_vector(Iter first, Iter last) const
std::string print_vector(const Container &c) const
const linear_process &process() const

Returns the process of the LPS specification.

const linear_process &process_reduced() const

Returns the reduced process of the LPS specification, i.e. with conditions with guards removed.

pins_data_type &state_type_map(std::size_t i)

Returns the data type of the i-th state parameter.

const pins_data_type &state_type_map(std::size_t i) const

Returns the data type of the i-th state parameter.

Public member functions

void _long(ltsmin_state_type const &src, std::size_t group, StateFunction &f, const ltsmin_state_type &dest, int *&labels, lps::next_state_generator *generator)

Iterates over the ‘next states’ of a particular summand of state src that are generated by a group of summands, and invokes a callback function for each discovered state.

StateFunction is a callback function that must provide the function operator() with the following interface: void operator()(ltsmin_state_type const& next_state, int* const& edge_labels, int group); where

  • next_state is the target state of the transition
  • edge_labels is an array of edge labels
  • group is the number of the summand from which the next state was generated, or -1 if it is unknown which summand

Parameters:

  • src An LTSMin state.
  • group the number of the summand.
  • f A state function.
  • dest A destination state, which is modified and passed to the callback. Must provide space for at least process_parameter_count() items.
  • labels An array of labels, which is modified and passed to the callback. Must provide space for at least edge_label_count() items.
  • generator The next state generator to use.
pins_data_type &data_type(std::size_t i)

Returns a reference to the datatype map with index i.

Pre: 0 <= i < datatype_count()

std::size_t datatype_count() const

Returns the number of unique datatype maps. Note that the datatype map for action labels is included, so this number equals the number of different process parameter types + 1.

std::size_t edge_label_count() const

Returns the number of labels per edge.

std::string edge_label_name(std::size_t) const

Returns the name of the i-th action label (always “action”).

Pre: 0 <= i < edge_label_count()

datatype_index edge_label_type(std::size_t) const

Returns the datatype map index corresponding to edge label i.

Pre: 0 <= i < edge_label_count()

guard_evaluation_t eval_guard_long(ltsmin_state_type const &src, std::size_t guard)
void get_initial_state(ltsmin_state_type &s)

Assigns the initial state to s.

std::size_t group_count() const

Returns the number of available groups. This equals the number of action summands of the LPS.

std::size_t guard_count() const
const std::vector<std::size_t> &guard_info(std::size_t index) const
const std::string &guard_name(std::size_t index)
const std::vector<std::size_t> &guard_parameters(std::size_t index) const
std::string info()

Prints an overview of several relevant attributes.

void next_state_all(ltsmin_state_type const &src, StateFunction &f, ltsmin_state_type const &dest, int *&labels)

Iterates over the ‘next states’ of state src, and invokes a callback function for each discovered state.

StateFunction is a callback function that must provide the function operator() with the following interface: void operator()(ltsmin_state_type const& next_state, int* const& edge_labels, int group=-1); where

  • next_state is the target state of the transition
  • edge_labels is an array of edge labels
  • group is the number of the summand from which the next state was generated, or -1 if it is unknown which summand

Parameters:

  • src An LTSMin state
  • f A ‘callback’ function object
  • dest A destination state, which is modified and passed to the callback. Must provide space for at least process_parameter_count() items.
  • labels An array of labels, which is modified and passed to the callback. Must provide space for at least edge_label_count() items.
void next_state_long(ltsmin_state_type const &src, std::size_t group, StateFunction &f, ltsmin_state_type const &dest, int *&labels)
pins(const std::string &filename, const std::string &rewriter_strategy)

Constructor.

Parameters:

  • filename The name of a file containing an mCRL2 specification
  • rewriter_strategy The rewriter strategy used for generating next states
std::size_t process_parameter_count() const

Returns the number of process parameters of the LPS.

std::string process_parameter_name(std::size_t i) const

Returns a human-readable, unique name for process parameter i.

datatype_index process_parameter_type(std::size_t i) const

Returns the datatype map index corresponding to process parameter i.

Pre: 0 <= i < process_parameter_count()

const std::vector<std::size_t> &read_group(std::size_t index) const

Indices of process parameters that influence event or next state of a summand by being read.

Parameters:

  • index the selected summand

Returns: reference to a vector of indices of parameters

Pre: 0 <= i < group_count()

lps::specification reduce_specification(const lps::specification &spec)

extracts all guards from the original specification and returns a new one with the guards removed.

std::set<std::string> summand_action_names(std::size_t i) const

Returns the names of the actions that appear in the summand with index i, with 0 <= i < group_count().

const std::vector<std::size_t> &update_group(std::size_t index) const

Indices of process parameters that influence event or next state of a summand by being read except from the guards.

Parameters:

  • index the selected summand

Returns: reference to a vector of indices of parameters

Pre: 0 <= i < group_count()

void update_long(ltsmin_state_type const &src, std::size_t group, StateFunction &f, ltsmin_state_type const &dest, int *&labels)
const std::vector<std::size_t> &write_group(std::size_t index) const

Indices of process parameters that influence event or next state of a summand by being written.

Parameters:

  • index the selected summand

Returns: reference to a vector of indices of parameters

Pre: 0 <= i < group_count()

~pins()

Public static member functions

static lps::specification load_specification(const std::string &filename)