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)
//
 
#ifndef MCRL2_LPS_LTSMIN_H
#define MCRL2_LPS_LTSMIN_H
 
#define MCRL2_GUARDS 1
 
#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
typedef mcrl2::log::log_level_t mcrl2_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 {
 
namespace lps {
 
inline
std::vector<std::string> generate_values(const data::data_specification& dataspec, const data::sort_expression& s, std::size_t max_size = 1000)
{
  typedef data::enumerator_list_element_with_substitution<> enumerator_element;
 
  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;
}
 
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:
 
    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 other.m_index - this->m_index;
        }
 
        std::size_t m_index;
    };
 
    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)
    {}
 
    virtual ~pins_data_type() = default;
 
    virtual std::string serialize(int i) const = 0;
 
    virtual std::size_t deserialize(const std::string& s) = 0;
 
    virtual std::string print(int i) const = 0;
 
    virtual std::size_t parse(const std::string& s) = 0;
 
    virtual const std::string& name() const = 0;
 
    virtual std::vector<std::string> generate_values(std::size_t max_size) const = 0;
 
    bool is_bounded() const
    {
      return m_is_bounded;
    }
 
    std::size_t size() const
    {
      return m_indexed_set.size();
    }
 
    index_iterator index_begin() const
    {
      return index_iterator(0);
    }
 
    index_iterator index_end() const
    {
      return index_iterator(size());
    }
 
    std::size_t operator[](const atermpp::aterm& x)
    {
      return m_indexed_set.insert(x).first;
    }
 
    atermpp::aterm get(std::size_t i)
    {
      return m_indexed_set.at(i);
    }
 
    utilities::indexed_set<atermpp::aterm>& indexed_set()
    {
      return m_indexed_set;
    }
 
    const utilities::indexed_set<atermpp::aterm>& indexed_set() const
    {
      return m_indexed_set;
    }
};
 
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);
    }
};
 
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:
    typedef int* ltsmin_state_type; 
    enum guard_evaluation_t { GUARD_FALSE = 0, GUARD_TRUE = 1, GUARD_MAYBE = 2 };
 
    typedef data::rewriter::substitution_type substitution_t;
 
  protected:
    std::size_t m_group_count;
    std::size_t m_state_length; 
    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;
    typedef lps::explorer<false, false, lps::specification>  generator_type;
    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;
    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;
 
    std::vector<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;
 
    pins_data_type& action_label_type_map()
    {
      return *m_data_types.back();
    }
 
    const pins_data_type& action_label_type_map() const
    {
      return *m_data_types.back();
    }
 
    pins_data_type& state_type_map(std::size_t i)
    {
      return *m_data_types[i];
    }
 
    const pins_data_type& state_type_map(std::size_t i) const
    {
      return *m_data_types[i];
    }
 
    const linear_process& process() const
    {
      return m_specification.process();
    }
 
    const linear_process& process_reduced() const
    {
      return m_specification_reduced.process();
    }
 
    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:
    typedef std::size_t datatype_index; 
    std::size_t process_parameter_count() const
    {
      return m_specification.process().process_parameters().size();
    }
 
    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;
    }
 
    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::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.push_back(lps::action_summand(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;
    }
 
    pins(const std::string& filename, const std::string& rewriter_strategy)
      : m_specification(load_specification(filename)),
        m_generator(m_specification, data::parse_rewrite_strategy(rewriter_strategy)),
        m_parameters_list(process().process_parameters().begin(), process().process_parameters().end()),
        m_specification_reduced(reduce_specification(m_specification)),
        m_generator_reduced(m_specification_reduced, data::parse_rewrite_strategy(rewriter_strategy))
    {
      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())
        {
          pins_data_type* dt = new state_data_type(m_specification.data(), m_specification.action_labels(), s, m_specification.data().is_certainly_finite(s));
          m_data_types.push_back(dt);
          m_unique_data_types.push_back(dt);
          existing_type_maps[s] = dt;
        }
        else
        {
          m_data_types.push_back(j->second);
        }
      }
      pins_data_type* dt = new action_label_data_type(m_specification.data(), m_specification.action_labels());
      m_data_types.push_back(dt);
      m_unique_data_types.push_back(dt);
 
      for (auto m_data_type : m_data_types)
      {
        std::vector<pins_data_type*>::const_iterator j = std::find(m_unique_data_types.begin(), m_unique_data_types.end(), m_data_type);
        assert(j != m_unique_data_types.end());
        m_unique_data_type_index.push_back(j - m_unique_data_types.begin());
      }
    }
 
    ~pins()
    {
      // make sure the pins data types are not deleted twice
      std::set<pins_data_type*> deleted;
      for (auto& data_type_ptr: m_data_types)
      {
        if (deleted.find(data_type_ptr) == deleted.end())
        {
          delete data_type_ptr;
          deleted.insert(data_type_ptr);
        }
      }
    }
 
    std::size_t datatype_count() const
    {
      return m_unique_data_types.size();
    }
 
    pins_data_type& data_type(std::size_t i)
    {
      assert (i < m_data_types.size());
      return *m_unique_data_types[i];
    }
 
    const std::vector<std::size_t>& read_group(std::size_t index) const
    {
      return m_read_group[index];
    }
 
    const std::vector<std::size_t>& write_group(std::size_t index) const
    {
      return m_write_group[index];
    }
 
    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];
    }
 
    std::string process_parameter_name(std::size_t i) const
    {
      return m_process_parameter_names[i];
    }
 
    datatype_index process_parameter_type(std::size_t i) const
    {
      return m_unique_data_type_index[i];
    }
 
    std::size_t edge_label_count() const
    {
      return 1;
    }
 
    datatype_index edge_label_type(std::size_t) const
    {
      return m_unique_data_types.size() - 1;
    }
 
    std::string edge_label_name(std::size_t) const
    {
      return action_label_type_map().name();
    }
 
    void get_initial_state(ltsmin_state_type& s)
    {
      state initial_state(m_generator.initial_state().begin(), m_generator.initial_state().size());
      for (std::size_t i = 0; i < m_state_length; i++)
      {
        s[i] = state_type_map(i)[initial_state[i]];
      }
    }
 
    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;
    }
 
    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]));
      }
      // data::data_expression_vector source = state_arguments;
      state source(state_arguments.begin(),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] = state_type_map(j)[destination[j]];
        }
        labels[0] = 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);
    }
 
    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(),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] = state_type_map(j)[destination[j]];
        }
        labels[0] = 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_FALSE;
      } else if(result == data::sort_bool::true_()) { // the guard rewrites to true.
        return GUARD_TRUE;
      } else { // the guard does not rewrite to true or false, so maybe...
        return GUARD_MAYBE;
      }
    }
 
    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";
      ltsmin_state_type init = new int[process_parameter_count()];
      get_initial_state(init);
      out << "initial state = " << print_vector(init, init + process_parameter_count()) << std::endl;
      delete[] init;
 
      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 lps
 
} // namespace mcrl2
 
#endif // MCRL2_LPS_LTSMIN_H