ltsmin.h

Go to the documentation of this file.

// Author(s): Wieger Wesselink
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
/// \file mcrl2/lps/ltsmin.h
/// \brief PINS interface for exploring an LPS from the LTSmin toolset.
 
#ifndef MCRL2_LPS_LTSMIN_H
#define MCRL2_LPS_LTSMIN_H
 
constexpr int MCRL2_GUARDS = 1;
 
#include <memory>
 
#include "mcrl2/data/join.h"
#include "mcrl2/lps/find.h"
#include "mcrl2/lps/io.h"
#include "mcrl2/lps/explorer.h"
#include "mcrl2/lps/parse.h"
 
// For backwards compatibility
using mcrl2_log_level_t = mcrl2::log::log_level_t;
using mcrl2::log::logger;
 
namespace mcrl2::log {
  using mcrl2_logger = mcrl2::log::logger;
}
 
#ifdef MCRL2_ENABLE_JITTYC
#define MCRL2_JITTYC_AVAILABLE
#endif
 
namespace mcrl2::lps
{
 
/// \brief Generates possible values of the data type (at most max_size).
inline
std::vector<std::string> generate_values(const data::data_specification& dataspec, const data::sort_expression& s, std::size_t max_size = 1000)
{
  using enumerator_element = data::enumerator_list_element_with_substitution<>;
 
  std::vector<std::string> result;
  std::size_t max_iterations = 10000;
  data::rewriter rewr(dataspec);
  data::enumerator_identifier_generator id_generator;
  bool accept_solutions_with_variables = false;
  data::enumerator_algorithm<data::rewriter, data::rewriter> E(rewr, dataspec, rewr, id_generator, accept_solutions_with_variables, max_iterations);
  data::mutable_indexed_substitution<> sigma;
  data::variable x("x", s);
  data::variable_list v_list{x};
 
  E.enumerate(enumerator_element(v_list, data::sort_bool::true_()),
              sigma,
              [&](const enumerator_element& p)
              {
                p.add_assignments(v_list, sigma, rewr);
                result.push_back(data::pp(sigma(x)));
                return result.size() >= max_size;
              }
  );
  return result;
}
 
/// \brief Models a pins data type. A pins data type maintains a mapping between known values
/// of a data type and integers.
class pins_data_type
{
  protected:
    utilities::indexed_set<atermpp::aterm> m_indexed_set;
    const data::data_specification& m_data;
    const process::action_label_list& m_action_labels;
    bool m_is_bounded;
 
  public:
 
    /// \brief Forward iterator used for iterating over indices.
    class index_iterator: public boost::iterator_facade<index_iterator, const std::size_t, boost::forward_traversal_tag>
    {
      public:
        explicit index_iterator(std::size_t index = 0)
          : m_index(index)
        {}
 
     private:
        friend class boost::iterator_core_access;
 
        void increment()
        {
          m_index++;
        }
 
        bool equal(const index_iterator& other) const
        {
          return this->m_index == other.m_index;
        }
 
        const std::size_t& dereference() const
        {
          return m_index;
        }
 
        std::ptrdiff_t distance_to(const index_iterator& other) const
        {
          return static_cast<std::ptrdiff_t>(other.m_index) - static_cast<std::ptrdiff_t>(this->m_index);
        }
 
        std::size_t m_index;
    };
 
    /// \brief Constructor
    pins_data_type(const data::data_specification& data,
                   const process::action_label_list& action_labels,
                   bool is_bounded = false)
      : // m_generator(generator),
        m_data(data),
        m_action_labels(action_labels),
        m_is_bounded(is_bounded)
    {}
 
    /// \brief Destructor.
    virtual ~pins_data_type() = default;
 
    /// \brief 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
    virtual std::string serialize(int i) const = 0;
 
    /// \brief Deserializes a string to a data value, and returns the corresponding index.
    /// If the value is not in the mapping, it will be added.
    /// \return The index of the data value.
    /// \throw <std::runtime_error> { if deserialization failed }
    virtual std::size_t deserialize(const std::string& s) = 0;
 
    /// \brief 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 print(int i) const = 0;
 
    /// \brief Parses a string to a data value, and returns the corresponding index.
    /// If the value is not in the mapping, it will be added.
    /// \return The index of the data value.
    /// \throw <std::runtime_error> { if parsing failed }
    virtual std::size_t parse(const std::string& s) = 0;
 
    /// \brief Returns the name of the data type.
    virtual const std::string& name() const = 0;
 
    /// \brief Generates possible values of the data type (at most max_size).
    virtual std::vector<std::string> generate_values(std::size_t max_size) const = 0;
 
    /// \brief Returns true if the number of elements is bounded. If this property can
    /// not be computed for a data type, false is returned.
    bool is_bounded() const
    {
      return m_is_bounded;
    }
 
    /// \brief Returns the number of values that are stored in the map.
    std::size_t size() const
    {
      return m_indexed_set.size();
    }
 
    /// \brief Returns an iterator to the beginning of the indices
    index_iterator index_begin() const
    {
      return index_iterator(0);
    }
 
    /// \brief Returns an iterator to the end of the indices
    index_iterator index_end() const
    {
      return index_iterator(size());
    }
 
    /// \brief Returns the index of the value x
    std::size_t operator[](const atermpp::aterm& x)
    {
      return m_indexed_set.insert(x).first;
    }
 
    /// \brief Returns the value at index i
    atermpp::aterm get(std::size_t i)
    {
      return m_indexed_set.at(i);
    }
 
    /// \brief Returns the indexed_set holding the values
    utilities::indexed_set<atermpp::aterm>& indexed_set()
    {
      return m_indexed_set;
    }
 
    /// \brief Returns the indexed_set holding the values
    const utilities::indexed_set<atermpp::aterm>& indexed_set() const
    {
      return m_indexed_set;
    }
};
 
/// \brief Models the mapping of mCRL2 state values to integers.
class state_data_type: public pins_data_type
{
  protected:
    std::string m_name;
    data::sort_expression m_sort;
 
    std::size_t expression2index(const data::data_expression& x)
    {
      return m_indexed_set.insert(x).first;
    }
 
    data::data_expression index2expression(std::size_t i) const
    {
      return static_cast<data::data_expression>(m_indexed_set.at(i));
    }
 
  public:
    state_data_type(const data::data_specification& data,
                    const process::action_label_list& action_labels,
                    const data::sort_expression& sort,
                    bool sort_is_finite
                   )
      : pins_data_type(data, action_labels, sort_is_finite),
        m_sort(sort)
    {
      m_name = data::pp(m_sort);
    }
 
    // prints the expression as an ATerm string
    std::string serialize(int i) const override
    {
      data::data_expression e = index2expression(i);
      atermpp::aterm t = data::detail::remove_index(static_cast<atermpp::aterm&>(e));
      return pp(t);
    }
 
    std::size_t deserialize(const std::string& s) override
    {
      atermpp::aterm t = data::detail::add_index(atermpp::read_term_from_string(s));
      return expression2index(atermpp::down_cast<data::data_expression>(t));
    }
 
    std::string print(int i) const override
    {
      return data::pp(index2expression(i));
    }
 
    std::size_t parse(const std::string& s) override
    {
      return expression2index(data::parse_data_expression(s, m_data));
    }
 
    const std::string& name() const override
    {
      return m_name;
    }
 
    std::vector<std::string> generate_values(std::size_t max_size) const override
    {
      return lps::generate_values(m_data, m_sort, max_size);
    }
};
 
/// \brief Models the mapping of mCRL2 action labels to integers.
class action_label_data_type: public pins_data_type
{
  protected:
    std::string m_name;
 
  public:
    action_label_data_type(const data::data_specification& data, const process::action_label_list& action_labels)
      : pins_data_type(data, action_labels, false)
    {
      m_name = "action_labels";
    }
 
    std::string serialize(int i) const override
    {
      return pp(m_indexed_set.at(i));
    }
 
    std::size_t deserialize(const std::string& s) override
    {
      return m_indexed_set.insert(atermpp::read_term_from_string(s)).first;
    }
 
    std::string print(int i) const override
    {
      return lps::pp(lps::multi_action(m_indexed_set.at(i)));
    }
 
    std::size_t parse(const std::string& s) override
    {
      lps::multi_action m = lps::parse_multi_action(s, m_action_labels, m_data);
      return m_indexed_set.insert(m).first;
    }
 
    const std::string& name() const override
    {
      return m_name;
    }
 
    // TODO: get rid of this useless function
    std::vector<std::string> generate_values(std::size_t) const override
    {
      return std::vector<std::string>();
    }
};
 
class pins
{
  public:
    using ltsmin_state_type = int*; /**< the state type used by LTSMin */
 
    /// \brief guard evaluations have ternary logic. A guard may not always rewrite
    /// to true or false
    enum class guard_evaluation_t { GUARD_FALSE = 0, GUARD_TRUE = 1, GUARD_MAYBE = 2 };
 
    using substitution_t = data::rewriter::substitution_type;
 
  protected:
    std::size_t m_group_count = 0UL;
    std::size_t m_state_length = 0UL; /**< the number of process parameters */
    std::vector<std::vector<std::size_t> > m_read_group;
    std::vector<std::vector<std::size_t> > m_write_group;
    std::vector<std::vector<std::size_t> > m_update_group;
    lps::specification m_specification;
    using generator_type = lps::explorer<false, false, lps::specification>;
    data::rewriter m_rewriter;
    generator_type m_generator;
 
    std::vector<data::variable> m_parameters_list;
    std::vector<std::string> m_process_parameter_names;
 
    utilities::indexed_set<atermpp::aterm> m_guards;
    std::vector<std::vector<std::size_t> > guard_parameters_list;
    std::vector<std::vector<std::size_t> > m_guard_info;
    std::vector<std::string> m_guard_names;
 
    // For guard-splitting we use a different generator with a different spec.
    // This second spec has guards removed from the conditions.
    lps::specification m_specification_reduced;
    data::rewriter m_rewriter_reduced;
    generator_type m_generator_reduced;
 
    // The type mappings
    // m_data_types[0] ... m_data_types[N-1] contain the state parameter mappings
    // m_data_types[N] contains the action label values
    // where N is the number of process parameters
    std::vector<pins_data_type*> m_data_types;
 
    /// The unique type mappings; owns the data types that m_data_types refers to.
    std::vector<std::unique_ptr<pins_data_type>> m_unique_data_types;
 
    // maps process parameter index to the corresponding index in m_unique_data_types
    std::vector<std::size_t> m_unique_data_type_index;
 
    /// \brief Returns the action data type
    pins_data_type& action_label_type_map()
    {
      return *m_data_types.back();
    }
 
    /// \brief Returns the action data type
    const pins_data_type& action_label_type_map() const
    {
      return *m_data_types.back();
    }
 
    /// \brief Returns the data type of the i-th state parameter
    pins_data_type& state_type_map(std::size_t i)
    {
      return *m_data_types[i];
    }
 
    /// \brief Returns the data type of the i-th state parameter
    const pins_data_type& state_type_map(std::size_t i) const
    {
      return *m_data_types[i];
    }
 
    /// \brief Returns the process of the LPS specification
    const linear_process& process() const
    {
      return m_specification.process();
    }
 
    /// \brief Returns the reduced process of the LPS specification,
    /// i.e. with conditions with guards removed.
    const linear_process& process_reduced() const
    {
      return m_specification_reduced.process();
    }
 
    /// \brief Returns the data specification of the LPS specification
    const data::data_specification& data() const
    {
      return m_specification.data();
    }
 
    template <typename Iter>
    std::string print_vector(Iter first, Iter last) const
    {
      std::ostringstream out;
      out << "[";
      for (Iter i = first; i != last; ++i)
      {
        if (i != first)
        {
          out << ", ";
        }
        out << *i;
      }
      out << "]";
      return out.str();
    }
 
    template <typename Container>
    std::string print_vector(const Container& c) const
    {
      return print_vector(c.begin(), c.end());
    }
 
    void initialize_read_write_groups()
    {
      std::set<data::variable> parameters(process().process_parameters().begin(), process().process_parameters().end());
 
      const lps::linear_process& proc = process();
 
      m_group_count  = proc.action_summands().size();
      m_state_length = proc.process_parameters().size();
 
      m_read_group.resize(m_group_count);
      m_write_group.resize(m_group_count);
 
      // iterate over the list of summands
      {
        std::size_t i = 0;
        for (const auto & summand : proc.action_summands())
        {
          std::set<data::variable> used_read_variables;
          std::set<data::variable> used_write_variables;
 
          data::find_free_variables(summand.condition(), std::inserter(used_read_variables, used_read_variables.end()));
          lps::find_free_variables(summand.multi_action(), std::inserter(used_read_variables, used_read_variables.end()));
 
          for (const auto & assignment : summand.assignments())
          {
            if (assignment.lhs() != assignment.rhs())
            {
              data::find_all_variables(assignment.lhs(), std::inserter(used_write_variables, used_write_variables.end()));
              data::find_all_variables(assignment.rhs(), std::inserter(used_read_variables, used_read_variables.end()));
            }
          }
 
          // process parameters used in condition, action or assignment of summand
          std::set<data::variable> used_read_parameters;
          std::set<data::variable> used_write_parameters;
 
          std::set_intersection(used_read_variables.begin(),
                                used_read_variables.end(),
                                parameters.begin(),
                                parameters.end(),
                                std::inserter(used_read_parameters,
                                              used_read_parameters.begin()));
          std::set_intersection(used_write_variables.begin(),
                                used_write_variables.end(),
                                parameters.begin(),
                                parameters.end(),
                                std::inserter(used_write_parameters,
                                              used_write_parameters.begin()));
 
          std::size_t j = 0;
          for (auto & param : m_parameters_list)
          {
            if (used_read_parameters.find(param) != used_read_parameters.end())
            {
              m_read_group[i].push_back(j);
            }
            if (used_write_parameters.find(param) != used_write_parameters.end())
            {
              m_write_group[i].push_back(j);
            }
            j++;
          }
          i++;
        }
      }
 
      m_update_group.resize(m_group_count);
 
      // iterate over the list of reduced summands
      {
        std::size_t i = 0;
        for (const auto & reduced_summand : process_reduced().action_summands())
        {
          std::set<data::variable> used_update_variables;
 
          data::find_free_variables(reduced_summand.condition(), std::inserter(used_update_variables, used_update_variables.end()));
          lps::find_free_variables(reduced_summand.multi_action(), std::inserter(used_update_variables, used_update_variables.end()));
 
          for (const auto & assignment : reduced_summand.assignments())
          {
            if (assignment.lhs() != assignment.rhs())
            {
              data::find_all_variables(assignment.rhs(), std::inserter(used_update_variables, used_update_variables.end()));
            }
          }
 
          // process parameters used in the action and assignment of summand
          std::set<data::variable> used_update_parameters;
 
          std::set_intersection(used_update_variables.begin(),
                                used_update_variables.end(),
                                parameters.begin(),
                                parameters.end(),
                                std::inserter(used_update_parameters,
                                              used_update_parameters.begin()));
 
          std::size_t j = 0;
          for (auto & param : m_parameters_list)
          {
            if (used_update_parameters.find(param) != used_update_parameters.end())
            {
              m_update_group[i].push_back(j);
            }
            j++;
          }
          i++;
        }
      }
    }
 
  public:
    using datatype_index = std::size_t; /**< the index type for datatype maps */
 
    /// \brief Returns the number of process parameters of the LPS
    std::size_t process_parameter_count() const
    {
      return m_specification.process().process_parameters().size();
    }
 
    /// \brief Returns the number of available groups. This equals the number of action summands of the LPS.
    std::size_t group_count() const
    {
      return m_specification.process().action_summands().size();
    }
 
    static lps::specification load_specification(const std::string& filename)
    {
      lps::specification specification;
      load_lps(specification, filename);
      return specification;
    }
 
    /// \brief extracts all guards from the original specification and
    /// returns a new one with the guards removed.
    lps::specification reduce_specification(const lps::specification& spec) {
      // the list of summands
      std::vector<lps::action_summand> reduced_summands;
      for (const auto & summand : spec.process().action_summands())
      {
        // contains info about which guards this transition group has.
        std::vector<std::size_t> guard_info;
 
        // the initial new condition of a summand is always true.
        // this maybe joined with conjuncts which have local variables.
        data::data_expression reduced_condition = data::sort_bool::true_();
 
        // process variables and guards in condition
        std::set<data::data_expression> conjuncts = data::split_and(summand.condition());
        std::set<data::variable> summation_variables(summand.summation_variables().begin(), summand.summation_variables().end());
 
        for (const auto & conjunct : conjuncts)
        {
          // check if the conjunct is new
          std::size_t at = m_guards.index(conjunct);
          bool is_new = (at == utilities::indexed_set<atermpp::aterm>::npos);
          bool use_conjunct_as_guard = true;
 
          if (is_new) { // we have not encountered the guard yet
            std::set<data::variable> conjunct_variables;
            data::find_free_variables(conjunct, std::inserter(conjunct_variables, conjunct_variables.end()));
 
            if (!summand.summation_variables().empty())
            {
              // the conjunct may contain summation variables, in which case it can not be
              // used as guard.
              std::set<data::variable> summation_variables_in_conjunct;
              std::set_intersection(conjunct_variables.begin(),
                  conjunct_variables.end(),
                  summation_variables.begin(),
                  summation_variables.end(),
                  std::inserter(summation_variables_in_conjunct, summation_variables_in_conjunct.begin()));
 
              if (!summation_variables_in_conjunct.empty()) {
                // this conjunct contains summation variables and will not be used as guard.
                use_conjunct_as_guard = false;
 
                std::string printed_guard(data::pp(conjunct).substr(0, 80));
                mCRL2log(log::log_level_t::verbose)
                    << "Guard '" << printed_guard + (printed_guard.size() > 80?"...":"") << "' in summand "
                    << reduced_summands.size()
                    << " introduces local variables. To remove the guard from the condition, try instantiating the summand with 'lpssuminst'."
                    << std::endl;
 
                // add conjunct to new summand condition
                if (reduced_condition == data::sort_bool::true_()) {
                  reduced_condition = conjunct;
                } else {
                  reduced_condition = data::sort_bool::and_(reduced_condition, conjunct);
                }
              }
            }
            if (use_conjunct_as_guard) {
              // add conjunct to guards
              std::vector<std::size_t> guard_parameters;
              if (!conjunct_variables.empty())
              {
                // compute indexes of parameters used by the guard
                std::size_t p = 0;
                for (auto & param : m_parameters_list)
                {
                  if (conjunct_variables.find(param) != conjunct_variables.end())
                  {
                    guard_parameters.push_back(p);
                  }
                  p++;
                }
              }
              // add conjunct to the set of guards
              at = m_guards.insert(conjunct).first;
              m_guard_names.push_back(data::pp(conjunct));
              guard_parameters_list.push_back(guard_parameters);
            }
          }
          if (use_conjunct_as_guard) {
            // add the guard index to the list of guards of this summand.
            guard_info.push_back(at);
          }
        }
 
        // set which guards belong to which transition group
        m_guard_info.push_back(guard_info);
 
        // add the new summand to the list of summands.
        reduced_summands.emplace_back(summand.summation_variables(),
            reduced_condition,
            summand.multi_action(),
            summand.assignments());
      }
 
      // create a new LPS
      lps::linear_process lps_reduced(process().process_parameters(), process().deadlock_summands(), reduced_summands);
 
      // create a new spec
      lps::specification specification_reduced(m_specification.data(), m_specification.action_labels(), m_specification.global_variables(), lps_reduced, m_specification.initial_process());
      return specification_reduced;
    }
 
    /// \brief Constructor
    /// \param filename The name of a file containing an mCRL2 specification
    /// \param rewriter_strategy The rewriter strategy used for generating next states
    pins(const std::string& filename, const std::string& rewriter_strategy)
      : m_specification(load_specification(filename)),
        m_rewriter(lps::construct_rewriter(m_specification, data::parse_rewrite_strategy(rewriter_strategy), false)),
        m_generator(m_specification, lps::explorer_options(data::parse_rewrite_strategy(rewriter_strategy)), m_rewriter),
        m_parameters_list(process().process_parameters().begin(), process().process_parameters().end()),
        m_specification_reduced(reduce_specification(m_specification)),
        m_rewriter_reduced(lps::construct_rewriter(m_specification_reduced, data::parse_rewrite_strategy(rewriter_strategy), false)),
        m_generator_reduced(m_specification_reduced, lps::explorer_options(data::parse_rewrite_strategy(rewriter_strategy)), m_rewriter_reduced)
    {
      initialize_read_write_groups();
 
      // store the process parameter names in a vector, to have random access to them
      data::variable_list params = m_specification.process().process_parameters();
      for (const auto & param : params)
      {
        m_process_parameter_names.push_back(param.name());
      }
 
      // Each state parameter type gets it's own pins_data_type. State parameters of the same
      // type share the pins_data_type.
      std::map<data::sort_expression, pins_data_type*> existing_type_maps;
      std::vector<data::variable> parameters(process().process_parameters().begin(),process().process_parameters().end());
      for (std::size_t i = 0; i < params.size(); i++)
      {
        data::sort_expression s = parameters[i].sort();
        std::map<data::sort_expression, pins_data_type*>::const_iterator j = existing_type_maps.find(s);
        if (j == existing_type_maps.end())
        {
          m_unique_data_types.push_back(std::make_unique<state_data_type>(m_specification.data(), m_specification.action_labels(), s, m_specification.data().is_certainly_finite(s)));
          pins_data_type* dt = m_unique_data_types.back().get();
          m_data_types.push_back(dt);
          existing_type_maps[s] = dt;
        }
        else
        {
          m_data_types.push_back(j->second);
        }
      }
      m_unique_data_types.push_back(std::make_unique<action_label_data_type>(m_specification.data(), m_specification.action_labels()));
      m_data_types.push_back(m_unique_data_types.back().get());
 
      for (pins_data_type* data_type : m_data_types)
      {
        auto j = std::find_if(m_unique_data_types.begin(), m_unique_data_types.end(),
            [&](const std::unique_ptr<pins_data_type>& unique_data_type) { return unique_data_type.get() == data_type; });
        assert(j != m_unique_data_types.end());
        m_unique_data_type_index.push_back(j - m_unique_data_types.begin());
      }
    }
 
    /// \brief 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 datatype_count() const
    {
      return m_unique_data_types.size();
    }
 
    /// \brief Returns a reference to the datatype map with index i.
    /// \pre 0 <= i < datatype_count()
    pins_data_type& data_type(std::size_t i)
    {
      assert (i < m_data_types.size());
      return *m_unique_data_types[i];
    }
 
    /// \brief Indices of process parameters that influence event or next state of a summand by being read
    /// \param[in] index the selected summand
    /// \returns reference to a vector of indices of parameters
    /// \pre 0 <= i < group_count()
    const std::vector<std::size_t>& read_group(std::size_t index) const
    {
      return m_read_group[index];
    }
 
    /// \brief Indices of process parameters that influence event or next state of a summand by being written
    /// \param[in] index the selected summand
    /// \returns reference to a vector of indices of parameters
    /// \pre 0 <= i < group_count()
    const std::vector<std::size_t>& write_group(std::size_t index) const
    {
      return m_write_group[index];
    }
 
    /// \brief Indices of process parameters that influence event or next state of a summand by being read except from the guards.
    /// \param[in] index the selected summand
    /// \returns reference to a vector of indices of parameters
    /// \pre 0 <= i < group_count()
    const std::vector<std::size_t>& update_group(std::size_t index) const
    {
      return m_update_group[index];
    }
 
    const std::vector<std::size_t>& guard_parameters(std::size_t index) const
    {
      return guard_parameters_list[index];
    }
 
    const std::vector<std::size_t>& guard_info(std::size_t index) const
    {
      return m_guard_info[index];
    }
 
    std::size_t guard_count() const
    {
      return m_guards.size();
    }
 
    const std::string& guard_name(std::size_t index) {
      return m_guard_names[index];
    }
 
    /// \brief Returns a human-readable, unique name for process parameter i
    std::string process_parameter_name(std::size_t i) const
    {
      return m_process_parameter_names[i];
    }
 
    /// \brief Returns the datatype map index corresponding to process parameter i
    /// \pre 0 <= i < process_parameter_count()
    datatype_index process_parameter_type(std::size_t i) const
    {
      return m_unique_data_type_index[i];
    }
 
    /// \brief Returns the number of labels per edge.
    std::size_t edge_label_count() const
    {
      return 1;
    }
 
    /// \brief Returns the datatype map index corresponding to edge label i
    /// \pre 0 <= i < edge_label_count()
    datatype_index edge_label_type(std::size_t) const
    {
      return m_unique_data_types.size() - 1;
    }
 
    /// \brief Returns the name of the i-th action label (always "action").
    /// \pre 0 <= i < edge_label_count()
    std::string edge_label_name(std::size_t) const
    {
      return action_label_type_map().name();
    }
 
    /// \brief Assigns the initial state to s.
    void get_initial_state(ltsmin_state_type& s)
    {
      state initial_state(m_generator.initial_state().begin(), static_cast<int>(m_generator.initial_state().size()));
      for (std::size_t i = 0; i < m_state_length; i++)
      {
        s[i] = static_cast<int>(state_type_map(i)[initial_state[i]]);
      }
    }
 
    /// \brief Returns the names of the actions that appear in the summand with index i,
    /// with 0 <= i < group_count().
    std::set<std::string> summand_action_names(std::size_t i) const
    {
      std::set<std::string> result;
      auto const l = process().action_summands()[i].multi_action().actions(); // Using a reference in whatever this type
                                                                              // is, leads to a failing lps_ltsmin_test.
      for (const auto & i : l)
      {
        result.insert(std::string(i.label().name()));
      }
      return result;
    }
 
    /// \brief 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:
    /// <code>void operator()(ltsmin_state_type const& next_state, int* const& edge_labels, int group=-1);</code>
    /// where
    /// - \a next_state is the target state of the transition
    /// - \a edge_labels is an array of edge labels
    /// - \a group is the number of the summand from which the next state was generated, or -1 if it is unknown which summand
    ///
    /// \param src An LTSMin state
    /// \param f A 'callback' function object
    /// \param dest A destination state, which is modified and passed to the callback.  Must provide space for at least process_parameter_count() items.
    /// \param labels An array of labels, which is modified and passed to the callback.  Must provide space for at least edge_label_count() items.
    template <typename StateFunction>
    void next_state_all(ltsmin_state_type const& src, StateFunction& f, ltsmin_state_type const& dest, int* const& labels)
    {
      std::size_t nparams = process_parameter_count();
      data::data_expression_vector state_arguments(nparams);
      for (std::size_t i = 0; i < nparams; i++)
      {
        state_arguments[i] = static_cast<data::data_expression>(state_type_map(i).get(src[i]));
      }
      state source(state_arguments.begin(), static_cast<int>(nparams));
 
      std::list<generator_type::transition> transitions = m_generator.out_edges(source);
      for (const generator_type::transition& t: transitions)
      {
        state destination = t.state;
        for (std::size_t j = 0; j < nparams; j++)
        {
          dest[j] = static_cast<int>(state_type_map(j)[destination[j]]);
        }
        labels[0] = static_cast<int>(action_label_type_map()[t.action]);
        f(dest, labels);
      }
    }
 
    template <typename StateFunction>
    void next_state_long(ltsmin_state_type const& src, std::size_t group, StateFunction& f, ltsmin_state_type const& dest, int* const& labels)
    {
      _long(src, group, f, dest, labels, &m_generator);
    }
 
    template <typename StateFunction>
    void update_long(ltsmin_state_type const& src, std::size_t group, StateFunction& f, ltsmin_state_type const& dest, int* const& labels)
    {
      _long(src, group, f, dest, labels, &m_generator_reduced);
    }
 
    /// \brief 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:
    /// <code>void operator()(ltsmin_state_type const& next_state, int* const& edge_labels, int group);</code>
    /// 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
    ///
    /// \param src An LTSMin state.
    /// \param group the number of the summand.
    /// \param f A state function.
    /// \param dest A destination state, which is modified and passed to the callback.
    ///        Must provide space for at least process_parameter_count() items.
    /// \param labels An array of labels, which is modified and passed to the callback.
    ///        Must provide space for at least edge_label_count() items.
    /// \param generator The next state generator to use.
    template <typename StateFunction>
    void _long(ltsmin_state_type const& src,
               std::size_t group,
               StateFunction& f,
               const ltsmin_state_type& dest,
               int* const& labels,
               generator_type* generator)
    {
      std::size_t nparams = process_parameter_count();
      data::data_expression_vector state_arguments(nparams);
      for (std::size_t i = 0; i < nparams; i++)
      {
        state_arguments[i] = static_cast<data::data_expression>(state_type_map(i).get(src[i]));
      }
      state source(state_arguments.begin(), static_cast<int>(nparams));
 
      std::list<generator_type::transition> transitions = generator->out_edges(source, group);
 
      for (const generator_type::transition& t: transitions)
      {
        state destination = t.state;
        for (std::size_t j = 0; j < nparams; j++)
        {
          dest[j] = static_cast<int>(state_type_map(j)[destination[j]]);
        }
        labels[0] = static_cast<int>(action_label_type_map()[t.action]);
        f(dest, labels);
      }
    }
 
    guard_evaluation_t eval_guard_long(ltsmin_state_type const& src, std::size_t guard) {
      std::size_t nparams = process_parameter_count();
      substitution_t substitution;
      for (std::size_t i = 0; i < nparams; i++)
      {
        data::data_expression value(static_cast<data::data_expression>(state_type_map(i).get(src[i])));
        substitution[m_parameters_list[i]] = value;
      }
 
      // get the result by rewriting the guard with the substitution.
      data::data_expression result = m_generator_reduced.get_rewriter()(
          static_cast<data::data_expression>(m_guards.at(guard)),
          substitution);
 
      if(result == data::sort_bool::false_()) { // the guard rewrites to false.
        return guard_evaluation_t::GUARD_FALSE;
      } else if(result == data::sort_bool::true_()) { // the guard rewrites to true.
        return guard_evaluation_t::GUARD_TRUE;
      } else { // the guard does not rewrite to true or false, so maybe...
        return guard_evaluation_t::GUARD_MAYBE;
      }
    }
 
    /// \brief Prints an overview of several relevant attributes.
    std::string info()
    {
      std::ostringstream out;
 
      out << "\n--- EDGE LABELS ---\n";
      out << "edge_label_count() = " << edge_label_count() << std::endl;
      for (std::size_t i = 0; i < edge_label_count(); i++)
      {
        out << "\n";
        out << "edge_label_name(" << i << ") = " << edge_label_name(i) << std::endl;
        out << "edge_label_type(" << i << ") = " << edge_label_type(i) << std::endl;
      }
 
      out << "\n--- PROCESS PARAMETERS ---\n";
      out << "process_parameter_count() = " << process_parameter_count() << std::endl;
      for (std::size_t i = 0; i < process_parameter_count(); i++)
      {
        out << "\n";
        out << "process_parameter_name(" << i << ") = " << process_parameter_name(i) << std::endl;
        out << "process_parameter_type(" << i << ") = " << process_parameter_type(i) << std::endl;
      }
 
      out << "\n--- SUMMANDS ---\n";
      out << "group_count() = " << group_count() << std::endl;
      for (std::size_t i = 0; i < group_count(); i++)
      {
        out << std::endl;
        out << "  read_group(" << i << ") = " << print_vector(read_group(i)) << std::endl;
        out << " write_group(" << i << ") = " << print_vector(write_group(i)) << std::endl;
        out << "update_group(" << i << ") = " << print_vector(update_group(i)) << std::endl;
      }
 
      out << "\n--- GUARDS ---\n";
      out << "guard_count() = " << guard_count() << std::endl;
      for (std::size_t i = 0; i < guard_count(); i++)
      {
        out << "guard(" << i << ") = " << print_vector(guard_parameters(i)) << std::endl;
      }
 
      out << "\n--- INITIAL STATE ---\n";
      std::vector<int> init(process_parameter_count());
      ltsmin_state_type init_state = init.data();
      get_initial_state(init_state);
      out << "initial state = " << print_vector(init.data(), init.data() + process_parameter_count()) << std::endl;
 
      out << "\n--- DATA TYPE MAPS ---\n";
      out << "datatype_count() = " << datatype_count() << std::endl;
      for (std::size_t i = 0; i < datatype_count(); i++)
      {
        const pins_data_type& type = data_type(i);
        out << "\n";
        out << "datatype " << i << "\n"
            << " name    = " << type.name() << "\n"
            << " size    = " << type.size() << "\n"
            << " bounded = " << std::boolalpha << type.is_bounded() << "\n";
        if (type.is_bounded())
        {
          out << " possible values: " << core::detail::print_set(type.generate_values(10)) << std::endl;
        }
        out << std::endl;
      }
 
      return out.str();
    }
};
 
} // namespace mcrl2::lps
 
#endif // MCRL2_LPS_LTSMIN_H