mcrl2::lps::pins_data_type

Include file:

#include "mcrl2/lps/ltsmin.h

class mcrl2::lps::pins_data_type

Models a pins data type. A pins data type maintains a mapping between known values of a data type and integers.

Protected attributes

const process::action_label_list &mcrl2::lps::pins_data_type::m_action_labels

const data::data_specification &mcrl2::lps::pins_data_type::m_data

utilities::indexed_set<atermpp::aterm> mcrl2::lps::pins_data_type::m_indexed_set

bool mcrl2::lps::pins_data_type::m_is_bounded

Public member functions

virtual std::size_t deserialize(const std::string &s) = 0

Deserializes a string to a data value, and returns the corresponding index. If the value is not in the mapping, it will be added.

Returns: The index of the data value. exception * <std::runtime_error> { if deserialization failed }

virtual std::vector<std::string> generate_values(std::size_t max_size) const = 0

Generates possible values of the data type (at most max_size).

atermpp::aterm get(std::size_t i)

Returns the value at index i.

index_iterator index_begin() const

Returns an iterator to the beginning of the indices.

index_iterator index_end() const

Returns an iterator to the end of the indices.

utilities::indexed_set<atermpp::aterm> &indexed_set()

Returns the indexed_set holding the values.

const utilities::indexed_set<atermpp::aterm> &indexed_set() const

Returns the indexed_set holding the values.

bool is_bounded() const

Returns true if the number of elements is bounded. If this property can not be computed for a data type, false is returned.

virtual const std::string &name() const = 0

Returns the name of the data type.

std::size_t operator[](const atermpp::aterm &x)

Returns the index of the value x.

virtual std::size_t parse(const std::string &s) = 0

Parses a string to a data value, and returns the corresponding index. If the value is not in the mapping, it will be added.

Returns: The index of the data value. exception * <std::runtime_error> { if parsing failed }

pins_data_type(const data::data_specification &data, const process::action_label_list &action_labels, bool is_bounded = false)

Constructor.

virtual std::string print(int i) const = 0

Returns a human readable representation of the value with index i. N.B. It is not guaranteed that parse(print(i)) == i.

Pre: i is a valid index

virtual std::string serialize(int i) const = 0

Serializes the i-th value of the data type to a binary string. It is guaranteed that serialize(deserialize(i)) == i.

Pre: i is a valid index

std::size_t size() const

Returns the number of values that are stored in the map.

virtual ~pins_data_type() = default

Destructor.