mcrl2::lps::pins_data_type
===============================================================================


Include file:

.. code-block:: c++

   #include "mcrl2/lps/ltsmin.h

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

.. cpp:member:: const process::action_label_list & mcrl2::lps::pins_data_type::m_action_labels
  
  

  

.. cpp:member:: const data::data_specification & mcrl2::lps::pins_data_type::m_data
  
  

  

.. cpp:member:: utilities::indexed_set< atermpp::aterm > mcrl2::lps::pins_data_type::m_indexed_set
  
  

  

.. cpp:member:: bool mcrl2::lps::pins_data_type::m_is_bounded
  
  

  

Public member functions
-------------------------------------------------------------------------------

.. cpp:function:: 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 } 



.. cpp:function:: 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). 

  

.. cpp:function:: atermpp::aterm get(std::size_t i)
  
  Returns the value at index i. 

  

.. cpp:function:: index_iterator index_begin() const
  
  Returns an iterator to the beginning of the indices. 

  

.. cpp:function:: index_iterator index_end() const
  
  Returns an iterator to the end of the indices. 

  

.. cpp:function:: utilities::indexed_set<atermpp::aterm>& indexed_set()
  
  Returns the indexed_set holding the values. 

  

.. cpp:function:: const utilities::indexed_set<atermpp::aterm>& indexed_set() const
  
  Returns the indexed_set holding the values. 

  

.. cpp:function:: 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. 

  

.. cpp:function:: virtual const std::string& name() const =0
  
  Returns the name of the data type. 

  

.. cpp:function:: std::size_t operator[](const atermpp::aterm &x)
  
  Returns the index of the value x. 

  

.. cpp:function:: 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 } 



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

  

.. cpp:function:: 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 

.. cpp:function:: 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 

.. cpp:function:: std::size_t size() const
  
  Returns the number of values that are stored in the map. 

  

.. cpp:function:: virtual ~pins_data_type()=default
  
  Destructor.